---

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


1. p : ℕ+
2. a : p-adics(p)
3. n : ℤ
4. ¬n < 1
5. 0 < n
6. greatest-p-zero(n - 1;a) ≤ (n - 1)
7. ∀i:ℕ+(n - 1) + 1
     (((i ≤ greatest-p-zero(n - 1;a)) ⇒ ((a i) = 0 ∈ ℤ)) ∧ (greatest-p-zero(n - 1;a) < i ⇒ (¬((a i) = 0 ∈ ℤ))))
8. 0 < n
9. (a n) = 0 ∈ ℤ
10. n ≤ n
11. i : ℕ+n + 1
12. i ≤ n
⊢ (a i) = 0 ∈ ℤ
BY
{ (Assert ⌜((a i) ≤ (a n)) ∧ (0 ≤ (a i))⌝⋅ THENM Auto) }

1
.....assertion..... 
1. p : ℕ+
2. a : p-adics(p)
3. n : ℤ
4. ¬n < 1
5. 0 < n
6. greatest-p-zero(n - 1;a) ≤ (n - 1)
7. ∀i:ℕ+(n - 1) + 1
     (((i ≤ greatest-p-zero(n - 1;a)) ⇒ ((a i) = 0 ∈ ℤ)) ∧ (greatest-p-zero(n - 1;a) < i ⇒ (¬((a i) = 0 ∈ ℤ))))
8. 0 < n
9. (a n) = 0 ∈ ℤ
10. n ≤ n
11. i : ℕ+n + 1
12. i ≤ n
⊢ ((a i) ≤ (a n)) ∧ (0 ≤ (a i))

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}\msupplus{}
2.  a  :  p-adics(p)
3.  n  :  \mBbbZ{}
4.  \mneg{}n  <  1
5.  0  <  n
6.  greatest-p-zero(n  -  1;a)  \mleq{}  (n  -  1)
7.  \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))))
8.  0  <  n
9.  (a  n)  =  0
10.  n  \mleq{}  n
11.  i  :  \mBbbN{}\msupplus{}n  +  1
12.  i  \mleq{}  n
\mvdash{}  (a  i)  =  0


By

---

Latex:
(Assert  \mkleeneopen{}((a  i)  \mleq{}  (a  n))  \mwedge{}  (0  \mleq{}  (a  i))\mkleeneclose{}\mcdot{}  THENM  Auto)

---

Home Index