---

Step * 1 1 1 of Lemma div_induction


1. b : {b:ℤ| 1 < b} 
2. [P] : ℤ ⟶ ℙ
3. P[0]
4. ∀i:ℤ-o. (P[i ÷ b] ⇒ P[i])
5. [n] : ℕ
6. ∀[m:ℕn]. ∀i:{i:ℤ| |i| < m} . P[i]
7. i : {i:ℤ| |i| < n} 
8. ¬(i = 0 ∈ ℤ)
9. i' : ℤ
10. i' = (i ÷ b) ∈ ℤ
11. ¬(n = 0 ∈ ℤ)
⊢ P[i]
BY
{ xxx((BHyp 4  THENA Auto) THEN InstHyp [⌜n - 1⌝;⌜i'⌝] 6⋅ THEN Auto THEN HypSubst' (-2) 0)⋅xxx }

1
1. b : {b:ℤ| 1 < b} 
2. P : ℤ ⟶ ℙ
3. P[0]
4. ∀i:ℤ-o. (P[i ÷ b] ⇒ P[i])
5. n : ℕ
6. ∀[m:ℕn]. ∀i:{i:ℤ| |i| < m} . P[i]
7. i : {i:ℤ| |i| < n} 
8. ¬(i = 0 ∈ ℤ)
9. i' : ℤ
10. i' = (i ÷ b) ∈ ℤ
11. ¬(n = 0 ∈ ℤ)
⊢ i ÷ b ∈ {i:ℤ| |i| < n - 1} 

---

Latex:

---

Latex:

1.  b  :  \{b:\mBbbZ{}|  1  <  b\} 
2.  [P]  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbP{}
3.  P[0]
4.  \mforall{}i:\mBbbZ{}\msupminus{}\msupzero{}.  (P[i  \mdiv{}  b]  {}\mRightarrow{}  P[i])
5.  [n]  :  \mBbbN{}
6.  \mforall{}[m:\mBbbN{}n].  \mforall{}i:\{i:\mBbbZ{}|  |i|  <  m\}  .  P[i]
7.  i  :  \{i:\mBbbZ{}|  |i|  <  n\} 
8.  \mneg{}(i  =  0)
9.  i'  :  \mBbbZ{}
10.  i'  =  (i  \mdiv{}  b)
11.  \mneg{}(n  =  0)
\mvdash{}  P[i]


By

---

Latex:
xxx((BHyp  4    THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}i'\mkleeneclose{}]  6\mcdot{}  THEN  Auto  THEN  HypSubst'  (-2)  0)\mcdot{}xxx

---

Home Index