Step
*
1
2
of Lemma
choose_wf
1. n : ℤ
2. 0 < n
3. ∀[i:{0...n - 1}]. (choose(n - 1;i) ∈ ℕ)
4. i : {0...n}
⊢ choose(n;i) ∈ ℕ
BY
{ ((RecCaseSplit `choose`) THENA Auto) }
1
.....truecase.....
1. n : ℤ
2. 0 < n
3. ∀[i:{0...n - 1}]. (choose(n - 1;i) ∈ ℕ)
4. i : {0...n}
5. (i = 0 ∈ ℤ) ∨ (i = n ∈ ℤ)
⊢ 1 ∈ ℕ
2
.....falsecase.....
1. n : ℤ
2. 0 < n
3. ∀[i:{0...n - 1}]. (choose(n - 1;i) ∈ ℕ)
4. i : {0...n}
5. (¬(i = 0 ∈ ℤ)) ∧ (¬(i = n ∈ ℤ))
⊢ choose(n - 1;i - 1) + choose(n - 1;i) ∈ ℕ
Latex:
Latex:
1. n : \mBbbZ{}
2. 0 < n
3. \mforall{}[i:\{0...n - 1\}]. (choose(n - 1;i) \mmember{} \mBbbN{})
4. i : \{0...n\}
\mvdash{} choose(n;i) \mmember{} \mBbbN{}
By
Latex:
((RecCaseSplit `choose`) THENA Auto)
Home
Index