metamath/valid/mathd-numbertheory-64.mm

$(
  @{
    mathd-numbertheory-64.0 @e |- ( ph -> X e. NN ) $@
    mathd-numbertheory-64.1 @e |- ( ph -> ; 4 7 || ( ( ; 3 0 x. X ) - ; 4 2 ) ) $@
    mathd-numbertheory-64.2 @e |- ( ph -> A. x e. NN ( ; 4 7 || ( ( ; 3 0 x. x ) - ; 4 2 ) -> X <_ x ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-64 @p |- ( ph -> X = ; 3 9 ) @=
      ? @.
  @}
$)