---

Step * of Lemma div_nat_induction

∀b:{b:ℤ| 1 < b} . ∀[P:ℕ ⟶ ℙ]. (P[0] ⇒ (∀i:ℕ+. (P[i ÷ b] ⇒ P[i])) ⇒ (∀i:ℕ. P[i]))
BY
{ TACTIC:((GeneralInductionOnNat THENA Auto)
          THEN CaseNat 0 `i'
          THEN Auto
          THEN (Evaluate ⌜j = (i ÷ b) ∈ ℤ⌝⋅ THENA 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. j = (i ÷ b) ∈ ℤ
⊢ P[i]

---

Latex:

---

Latex:
\mforall{}b:\{b:\mBbbZ{}|  1  <  b\}  .  \mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (P[0]  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}\msupplus{}.  (P[i  \mdiv{}  b]  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}.  P[i]))


By

---

Latex:
TACTIC:((GeneralInductionOnNat  THENA  Auto)
                THEN  CaseNat  0  `i'
                THEN  Auto
                THEN  (Evaluate  \mkleeneopen{}j  =  (i  \mdiv{}  b)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index