---

Step * 2 2 2 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. ∀i:ℕ+(n - 1) + 1
     (((i ≤ greatest-p-zero(n - 1;a)) ⇒ ((a i) = 0 ∈ ℤ)) ∧ (greatest-p-zero(n - 1;a) < i ⇒ (¬((a i) = 0 ∈ ℤ))))
9. 0 < n
10. greatest-p-zero(n - 1;a) ≤ n
11. i : ℕ+n + 1
12. (i ≤ greatest-p-zero(n - 1;a)) ⇒ ((a i) = 0 ∈ ℤ)
13. greatest-p-zero(n - 1;a) < i
14. ¬(i = n ∈ ℤ)
⊢ ¬((a i) = 0 ∈ ℤ)
BY
{ (D 8 With ⌜i⌝  THENA Auto) }

1
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 ∈ ℤ)

---

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.  \mforall{}i:\mBbbN{}\msupplus{}(n  -  1)  +  1
          (((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))))
9.  0  <  n
10.  greatest-p-zero(n  -  1;a)  \mleq{}  n
11.  i  :  \mBbbN{}\msupplus{}n  +  1
12.  (i  \mleq{}  greatest-p-zero(n  -  1;a))  {}\mRightarrow{}  ((a  i)  =  0)
13.  greatest-p-zero(n  -  1;a)  <  i
14.  \mneg{}(i  =  n)
\mvdash{}  \mneg{}((a  i)  =  0)


By

---

Latex:
(D  8  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)

---

Home Index