---

Step * 2 of Lemma div_induction


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]
BY
{ ((Auto THEN InstHyp [⌜|i| + 1⌝;⌜i⌝] (-2)⋅) THEN Auto) }

---

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.  \mforall{}[n:\mBbbN{}].  \mforall{}i:\{i:\mBbbZ{}|  |i|  <  n\}  .  P[i]
\mvdash{}  \mforall{}i:\mBbbZ{}.  P[i]


By

---

Latex:
((Auto  THEN  InstHyp  [\mkleeneopen{}|i|  +  1\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  (-2)\mcdot{})  THEN  Auto)

---

Home Index