---

Step * 1 of Lemma div_induction

.....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]
BY
{ xxx(InstLemma `uniform-comp-nat-induction` [⌜λ2n.∀i:{i:ℤ| |i| < n} . P[i]⌝]⋅
      THEN Auto
      THEN CaseNat 0 `i'
      THEN Auto
      THEN (Evaluate ⌜i' = (i ÷ b) ∈ ℤ⌝⋅ THENA Auto))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) ∈ ℤ
⊢ P[i]

---

Latex:

---

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


By

---

Latex:
xxx(InstLemma  `uniform-comp-nat-induction`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.\mforall{}i:\{i:\mBbbZ{}|  |i|  <  n\}  .  P[i]\mkleeneclose{}]\mcdot{}
        THEN  Auto
        THEN  CaseNat  0  `i'
        THEN  Auto
        THEN  (Evaluate  \mkleeneopen{}i'  =  (i  \mdiv{}  b)\mkleeneclose{}\mcdot{}  THENA  Auto))xxx

---

Home Index