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