metamath/valid/mathd-numbertheory-136.mm

$(
  @{
    mathd-numbertheory-136.0 @e |- ( ph -> N e. NN0 ) $@
    mathd-numbertheory-136.1 @e |- ( ph -> ( ( ; ; 1 2 3 x. N ) + ; 1 7 ) = ; ; ; ; 3 9 5 0 0 ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-136 @p |- ( ph -> N = ; ; 3 2 1 ) @=
      ? @.
  @}
$)