---

Step * of Lemma p-reduce-eqmod-exp

∀p:ℕ+. ∀n:ℕ. ∀m:{n...}. ∀z:ℤ.  (z mod(p^m) ≡ z mod p^n)
BY
{ (Auto
   THEN (Subst' m ~ n + (m - n) 0 THENA Auto)
   THEN (GenConcl ⌜(m - n) = k ∈ ℕ⌝⋅ THENA Auto)
   THEN ThinVar  `m'
   THEN Unfold `p-reduce` 0
   THEN (RWO "exp_add" 0 THENA Auto)) }

1
1. p : ℕ+
2. n : ℕ
3. z : ℤ
4. k : ℕ
⊢ (z mod (p^n * p^k)) ≡ z mod p^n

---

Latex:

---

Latex:
\mforall{}p:\mBbbN{}\msupplus{}.  \mforall{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  \mforall{}z:\mBbbZ{}.    (z  mod(p\^{}m)  \mequiv{}  z  mod  p\^{}n)


By

---

Latex:
(Auto
  THEN  (Subst'  m  \msim{}  n  +  (m  -  n)  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(m  -  n)  =  k\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar    `m'
  THEN  Unfold  `p-reduce`  0
  THEN  (RWO  "exp\_add"  0  THENA  Auto))

---

Home Index