---

Step * 2 2 2 1 of Lemma greatest-p-zero-property


1. p : ℕ+
2. a : p-adics(p)
3. n : ℤ
4. ¬n < 1
5. a n ≠ 0
6. 0 < n
7. greatest-p-zero(n - 1;a) ≤ (n - 1)
8. 0 < n
9. greatest-p-zero(n - 1;a) ≤ n
10. i : ℕ+n + 1
11. (i ≤ greatest-p-zero(n - 1;a)) ⇒ ((a i) = 0 ∈ ℤ)
12. greatest-p-zero(n - 1;a) < i
13. ¬(i = n ∈ ℤ)
14. ((i ≤ greatest-p-zero(n - 1;a)) ⇒ ((a i) = 0 ∈ ℤ)) ∧ (greatest-p-zero(n - 1;a) < i ⇒ (¬((a i) = 0 ∈ ℤ)))
⊢ ¬((a i) = 0 ∈ ℤ)
BY
{ (RepeatFor 2 (D -1) THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}\msupplus{}
2.  a  :  p-adics(p)
3.  n  :  \mBbbZ{}
4.  \mneg{}n  <  1
5.  a  n  \mneq{}  0
6.  0  <  n
7.  greatest-p-zero(n  -  1;a)  \mleq{}  (n  -  1)
8.  0  <  n
9.  greatest-p-zero(n  -  1;a)  \mleq{}  n
10.  i  :  \mBbbN{}\msupplus{}n  +  1
11.  (i  \mleq{}  greatest-p-zero(n  -  1;a))  {}\mRightarrow{}  ((a  i)  =  0)
12.  greatest-p-zero(n  -  1;a)  <  i
13.  \mneg{}(i  =  n)
14.  ((i  \mleq{}  greatest-p-zero(n  -  1;a))  {}\mRightarrow{}  ((a  i)  =  0))
\mwedge{}  (greatest-p-zero(n  -  1;a)  <  i  {}\mRightarrow{}  (\mneg{}((a  i)  =  0)))
\mvdash{}  \mneg{}((a  i)  =  0)


By

---

Latex:
(RepeatFor  2  (D  -1)  THEN  Auto)

---

Home Index