metamath/valid/mathd-numbertheory-780.mm

$(
  @{
    mathd-numbertheory-780.0 @e |- ( ph -> M e. NN ) $@
    mathd-numbertheory-780.1 @e |- ( ph -> X e. NN0 ) $@
    mathd-numbertheory-780.2 @e |- ( ph -> ; 1 0 <_ M ) $@
    mathd-numbertheory-780.3 @e |- ( ph -> M <_ ; 9 9 ) $@
    mathd-numbertheory-780.4 @e |- ( ph -> ( ( 6 x. X ) mod M ) = 1 ) $@
    mathd-numbertheory-780.5 @e |- ( ph -> ( ( X - ( 6 ^ 2 ) ) mod M ) = 0 ) $@
    @( (Contributed by Kunhao Zheng, 9-Aug-2021.) @)
    mathd-numbertheory-780 @p |- ( ph -> M = ; 4 3 ) @=
      ? @.
  @}
$)