---

Step * 1 1 1 1 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. ¬(greatest-p-zero(n;a) = n ∈ ℤ)
9. k : ℕ+
10. greatest-p-zero(n;a) = k ∈ ℕ+
11. v : ℕp^(1 + k)
12. (a (1 + k)) = v ∈ ℕp^(1 + k)
13. 0 < p^k
14. (a k) = 0 ∈ ℤ
15. (v ÷ p^k) = 0 ∈ ℤ
16. v = (v rem p^k) ∈ ℤ
17. (0 ≤ (v rem p^k)) ∧ v rem p^k < p^k
⊢ v = 0 ∈ ℤ
BY
{ (Assert v ≡ 0 mod p^k BY
         ((InstLemma `p-adic-property` [⌜p⌝;⌜a⌝;⌜k⌝;⌜1 + k⌝]⋅ THENA Auto)
          THEN HypSubst' (-7) (-1)
          THEN HypSubst' (-5) (-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. ¬(greatest-p-zero(n;a) = n ∈ ℤ)
9. k : ℕ+
10. greatest-p-zero(n;a) = k ∈ ℕ+
11. v : ℕp^(1 + k)
12. (a (1 + k)) = v ∈ ℕp^(1 + k)
13. 0 < p^k
14. (a k) = 0 ∈ ℤ
15. (v ÷ p^k) = 0 ∈ ℤ
16. v = (v rem p^k) ∈ ℤ
17. (0 ≤ (v rem p^k)) ∧ v rem p^k < p^k
18. v ≡ 0 mod p^k
⊢ v = 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.  \mneg{}(greatest-p-zero(n;a)  =  n)
9.  k  :  \mBbbN{}\msupplus{}
10.  greatest-p-zero(n;a)  =  k
11.  v  :  \mBbbN{}p\^{}(1  +  k)
12.  (a  (1  +  k))  =  v
13.  0  <  p\^{}k
14.  (a  k)  =  0
15.  (v  \mdiv{}  p\^{}k)  =  0
16.  v  =  (v  rem  p\^{}k)
17.  (0  \mleq{}  (v  rem  p\^{}k))  \mwedge{}  v  rem  p\^{}k  <  p\^{}k
\mvdash{}  v  =  0


By

---

Latex:
(Assert  v  \mequiv{}  0  mod  p\^{}k  BY
              ((InstLemma  `p-adic-property`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}1  +  k\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  HypSubst'  (-7)  (-1)
                THEN  HypSubst'  (-5)  (-1)
                THEN  Auto))

---

Home Index