---

Step * 1 of Lemma div_nat_induction


1. b : {b:ℤ| 1 < b} 
2. [P] : ℕ ⟶ ℙ
3. P[0]
4. ∀i:ℕ+. (P[i ÷ b] ⇒ P[i])
5. i : ℕ
6. ∀i1:ℕi. P[i1]
7. ¬(i = 0 ∈ ℤ)
8. j : ℤ
9. j = (i ÷ b) ∈ ℤ
⊢ P[i]
BY
{ (InstHyp [⌜j⌝] (-4)⋅ THEN ElimVar `j' THEN Auto) }

1
1. b : {b:ℤ| 1 < b} 
2. P : ℕ ⟶ ℙ
3. P[0]
4. ∀i:ℕ+. (P[i ÷ b] ⇒ P[i])
5. i : ℕ
6. ∀i1:ℕi. P[i1]
7. ¬(i = 0 ∈ ℤ)
8. j : ℤ
9. i ÷ b ∈ ℤ
⊢ i ÷ b ∈ ℕi

---

Latex:

---

Latex:

1.  b  :  \{b:\mBbbZ{}|  1  <  b\} 
2.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
3.  P[0]
4.  \mforall{}i:\mBbbN{}\msupplus{}.  (P[i  \mdiv{}  b]  {}\mRightarrow{}  P[i])
5.  i  :  \mBbbN{}
6.  \mforall{}i1:\mBbbN{}i.  P[i1]
7.  \mneg{}(i  =  0)
8.  j  :  \mBbbZ{}
9.  j  =  (i  \mdiv{}  b)
\mvdash{}  P[i]


By

---

Latex:
(InstHyp  [\mkleeneopen{}j\mkleeneclose{}]  (-4)\mcdot{}  THEN  ElimVar  `j'  THEN  Auto)

---

Home Index