---

Step * 1 1 1 1 of Lemma p-shift_wf


1. p : ℕ+
2. a : p-adics(p)
3. k : ℕ+
4. (a k) = 0 ∈ ℤ
5. n : ℕ+
⊢ (a (n + k)) ÷ p^k ∈ ℕp^n
BY
{ ((InstLemma `p-adic-property` [⌜p⌝;⌜a⌝;⌜k⌝;⌜n + k⌝]⋅ THENA Auto)
   THEN HypSubst' (-3) (-1)
   THEN D -1
   THEN (Subst' a (n + k) ~ p^k * c 0 THENA Auto)
   THEN (RWO "div-cancel2" 0 THENA Auto)) }

1
1. p : ℕ+
2. a : p-adics(p)
3. k : ℕ+
4. (a k) = 0 ∈ ℤ
5. n : ℕ+
6. c : ℤ
7. ((a (n + k)) - 0) = (p^k * c) ∈ ℤ
⊢ c ∈ ℕp^n

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}\msupplus{}
2.  a  :  p-adics(p)
3.  k  :  \mBbbN{}\msupplus{}
4.  (a  k)  =  0
5.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  (a  (n  +  k))  \mdiv{}  p\^{}k  \mmember{}  \mBbbN{}p\^{}n


By

---

Latex:
((InstLemma  `p-adic-property`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}n  +  k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-3)  (-1)
  THEN  D  -1
  THEN  (Subst'  a  (n  +  k)  \msim{}  p\^{}k  *  c  0  THENA  Auto)
  THEN  (RWO  "div-cancel2"  0  THENA  Auto))

---

Home Index