Step * 1 1 1 1 1 1 1 1 of Lemma p-unit-part-unique


1. {2...}
2. : ℕ+@i
⊢ (p^n mod p) 0 ∈ ℕ
BY
(RWO "modulus-is-rem" THEN Auto) }


Latex:


Latex:

1.  p  :  \{2...\}
2.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  (p\^{}n  mod  p)  =  0


By


Latex:
(RWO  "modulus-is-rem"  0  THEN  Auto)




Home Index