metamath/valid/mathd-numbertheory-22.mm

$(
  @{
    mathd-numbertheory-22.0 @e |- ( ph -> B e. NN0 ) $@
    mathd-numbertheory-22.1 @e |- ( ph -> B < ; 1 0 ) $@
    mathd-numbertheory-22.2 @e |- ( ph -> ( sqrt ` ; B 6 ) e. NN ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-22 @p |- ( ph -> ( B = 3 \/ B = 1 ) ) @=
      ? @.
  @}
$)