---

Step * of Lemma p-adic-bounds

∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ+.  ((0 ≤ ((a (n + 1)) - a n)) ∧ (((a (n + 1)) - a n) ≤ (p^(n + 1) - p^n)))
BY
{ (Auto THEN (D 2 THEN (Unhide THENA Auto)) THEN (InstHyp [⌜n⌝] 3⋅ THENA Auto) THEN D -1 THEN HypSubst' (-1) 0) }

1
1. p : ℕ+
2. a : n:ℕ+ ⟶ ℕp^n
3. ∀n:ℕ+. ((a (n + 1)) ≡ (a n) mod p^n)
4. n : ℕ+
5. c : ℤ
6. ((a (n + 1)) - a n) = (p^n * c) ∈ ℤ
⊢ 0 ≤ (p^n * c)

2
1. p : ℕ+
2. a : n:ℕ+ ⟶ ℕp^n
3. ∀n:ℕ+. ((a (n + 1)) ≡ (a n) mod p^n)
4. n : ℕ+
5. 0 ≤ ((a (n + 1)) - a n)
6. c : ℤ
7. ((a (n + 1)) - a n) = (p^n * c) ∈ ℤ
⊢ (p^n * c) ≤ (p^(n + 1) - p^n)

---

Latex:

---

Latex:
\mforall{}p:\mBbbN{}\msupplus{}.  \mforall{}a:p-adics(p).  \mforall{}n:\mBbbN{}\msupplus{}.
    ((0  \mleq{}  ((a  (n  +  1))  -  a  n))  \mwedge{}  (((a  (n  +  1))  -  a  n)  \mleq{}  (p\^{}(n  +  1)  -  p\^{}n)))


By

---

Latex:
(Auto
  THEN  (D  2  THEN  (Unhide  THENA  Auto))
  THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  HypSubst'  (-1)  0)

---

Home Index