metamath/valid/mathd-algebra-185.mm

$(
  @{
    mathd-algebra-185.0 @e |- F = ( x e. RR |-> ( abs ` ( x + 4 ) ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-185 @p |- ( ph -> ( # ` { x e. ZZ | ( F ` x ) < 9 } ) = ; 1 7 ) @=
      ? @.
  @}
$)