---

Step * of Lemma div_induction

∀b:{b:ℤ| 1 < b} . ∀[P:ℤ ⟶ ℙ]. (P[0] ⇒ (∀i:ℤ-o. (P[i ÷ b] ⇒ P[i])) ⇒ (∀i:ℤ. P[i]))
BY
{ xxx(RepeatFor 4 ((D 0 THENA Auto)) THEN Assert ⌜∀[n:ℕ]. ∀i:{i:ℤ| |i| < n} . P[i]⌝⋅)xxx }

1
.....assertion..... 
1. b : {b:ℤ| 1 < b} 
2. [P] : ℤ ⟶ ℙ
3. P[0]
4. ∀i:ℤ-o. (P[i ÷ b] ⇒ P[i])
⊢ ∀[n:ℕ]. ∀i:{i:ℤ| |i| < n} . P[i]

2
1. b : {b:ℤ| 1 < b} 
2. [P] : ℤ ⟶ ℙ
3. P[0]
4. ∀i:ℤ-o. (P[i ÷ b] ⇒ P[i])
5. ∀[n:ℕ]. ∀i:{i:ℤ| |i| < n} . P[i]
⊢ ∀i:ℤ. P[i]

---

Latex:

---

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


By

---

Latex:
xxx(RepeatFor  4  ((D  0  THENA  Auto))  THEN  Assert  \mkleeneopen{}\mforall{}[n:\mBbbN{}].  \mforall{}i:\{i:\mBbbZ{}|  |i|  <  n\}  .  P[i]\mkleeneclose{}\mcdot{})xxx

---

Home Index