metamath/valid/mathd-numbertheory-43.mm

$(
  @{
    mathd-numbertheory-43.0 @e |- ( ph -> N e. NN ) $@
    mathd-numbertheory-43.1 @e |- ( ph -> ( ; 1 5 ^ N ) || ( ! ` ; ; 9 4 2 ) ) $@
    mathd-numbertheory-43.2 @e |- ( ph -> A. n e. NN ( ( ; 1 5 ^ n ) || ( ! ` ; ; 9 4 2 ) -> n <_ N ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-43 @p |- ( ph -> N = ; ; 2 3 3 ) @=
      ? @.
  @}
$)