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


1. p : {2...}
2. n : ℕ+@i
⊢ (p^n mod p) = 0 ∈ ℕ
BY
{ (RWO "modulus-is-rem" 0 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