---

Step * 1 1 1 of Lemma shift-greatest-p-zero-unit


1. p : ℕ+
2. a : p-adics(p)
3. n : ℕ+
4. ¬((a n) = 0 ∈ ℤ)
5. 0 < greatest-p-zero(n;a)
6. greatest-p-zero(n;a) ≤ n
7. ∀i:ℕ+n + 1. (((i ≤ greatest-p-zero(n;a)) ⇒ ((a i) = 0 ∈ ℤ)) ∧ (greatest-p-zero(n;a) < i ⇒ (¬((a i) = 0 ∈ ℤ))))
8. (a greatest-p-zero(n;a)) = 0 ∈ ℤ
9. ¬(greatest-p-zero(n;a) = n ∈ ℤ)
⊢ ¬((p-shift(p;a;greatest-p-zero(n;a)) 1) = 0 ∈ ℤ)
BY
{ (Assert ¬((a (1 + greatest-p-zero(n;a))) = 0 ∈ ℤ) BY
         ((D -3 With ⌜1 + greatest-p-zero(n;a)⌝  THENA Auto) THEN RepeatFor 2 (D -1) THEN Auto)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mneg{}((a  (1  +  greatest-p-zero(n;a)))  =  0)  BY
              ((D  -3  With  \mkleeneopen{}1  +  greatest-p-zero(n;a)\mkleeneclose{}    THENA  Auto)  THEN  RepeatFor  2  (D  -1)  THEN  Auto))

---

Home Index