Proof of Theorem bcn2
Step | Hyp | Ref
| Expression |
1 | | 2nn 12046 |
. . 3
⊢ 2 ∈
ℕ |
2 | | bcval5 14030 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 2 ∈ ℕ) → (𝑁C2) = ((seq((𝑁 − 2) + 1)( · , I )‘𝑁) /
(!‘2))) |
3 | 1, 2 | mpan2 688 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑁C2) = ((seq((𝑁 − 2) + 1)( · , I
)‘𝑁) /
(!‘2))) |
4 | | 2m1e1 12099 |
. . . . . . . 8
⊢ (2
− 1) = 1 |
5 | 4 | oveq2i 7282 |
. . . . . . 7
⊢ ((𝑁 − 2) + (2 − 1)) =
((𝑁 − 2) +
1) |
6 | | nn0cn 12243 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
7 | | 2cn 12048 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
8 | | ax-1cn 10930 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
9 | | npncan 11242 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 2) + (2 − 1)) = (𝑁 − 1)) |
10 | 7, 8, 9 | mp3an23 1452 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → ((𝑁 − 2) + (2 − 1)) =
(𝑁 −
1)) |
11 | 6, 10 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 2) + (2
− 1)) = (𝑁 −
1)) |
12 | 5, 11 | eqtr3id 2794 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 2) + 1)
= (𝑁 −
1)) |
13 | 12 | seqeq1d 13725 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ seq((𝑁 − 2) +
1)( · , I ) = seq(𝑁
− 1)( · , I )) |
14 | 13 | fveq1d 6773 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (seq((𝑁 − 2) +
1)( · , I )‘𝑁)
= (seq(𝑁 − 1)(
· , I )‘𝑁)) |
15 | | nn0z 12343 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
16 | | peano2zm 12363 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 − 1) ∈
ℤ) |
18 | | uzid 12596 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
19 | 15, 18 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘𝑁)) |
20 | | npcan 11230 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
21 | 6, 8, 20 | sylancl 586 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1) + 1)
= 𝑁) |
22 | 21 | fveq2d 6775 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (ℤ≥‘((𝑁 − 1) + 1)) =
(ℤ≥‘𝑁)) |
23 | 19, 22 | eleqtrrd 2844 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘((𝑁 − 1) + 1))) |
24 | | seqm1 13738 |
. . . . . . 7
⊢ (((𝑁 − 1) ∈ ℤ ∧
𝑁 ∈
(ℤ≥‘((𝑁 − 1) + 1))) → (seq(𝑁 − 1)( · , I
)‘𝑁) = ((seq(𝑁 − 1)( · , I
)‘(𝑁 − 1))
· ( I ‘𝑁))) |
25 | 17, 23, 24 | syl2anc 584 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I )‘𝑁) =
((seq(𝑁 − 1)(
· , I )‘(𝑁
− 1)) · ( I ‘𝑁))) |
26 | | seq1 13732 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈ ℤ
→ (seq(𝑁 − 1)(
· , I )‘(𝑁
− 1)) = ( I ‘(𝑁
− 1))) |
27 | 17, 26 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I )‘(𝑁
− 1)) = ( I ‘(𝑁
− 1))) |
28 | | fvi 6841 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈ ℤ
→ ( I ‘(𝑁
− 1)) = (𝑁 −
1)) |
29 | 17, 28 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ( I ‘(𝑁
− 1)) = (𝑁 −
1)) |
30 | 27, 29 | eqtrd 2780 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I )‘(𝑁
− 1)) = (𝑁 −
1)) |
31 | | fvi 6841 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ( I ‘𝑁) =
𝑁) |
32 | 30, 31 | oveq12d 7289 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((seq(𝑁 − 1)(
· , I )‘(𝑁
− 1)) · ( I ‘𝑁)) = ((𝑁 − 1) · 𝑁)) |
33 | 25, 32 | eqtrd 2780 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I )‘𝑁) =
((𝑁 − 1) ·
𝑁)) |
34 | | subcl 11220 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
1) ∈ ℂ) |
35 | 6, 8, 34 | sylancl 586 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 − 1) ∈
ℂ) |
36 | 35, 6 | mulcomd 10997 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1)
· 𝑁) = (𝑁 · (𝑁 − 1))) |
37 | 33, 36 | eqtrd 2780 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I )‘𝑁) =
(𝑁 · (𝑁 − 1))) |
38 | 14, 37 | eqtrd 2780 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (seq((𝑁 − 2) +
1)( · , I )‘𝑁)
= (𝑁 · (𝑁 − 1))) |
39 | | fac2 13991 |
. . . 4
⊢
(!‘2) = 2 |
40 | 39 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (!‘2) = 2) |
41 | 38, 40 | oveq12d 7289 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((seq((𝑁 − 2)
+ 1)( · , I )‘𝑁) / (!‘2)) = ((𝑁 · (𝑁 − 1)) / 2)) |
42 | 3, 41 | eqtrd 2780 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝑁C2) = ((𝑁 · (𝑁 − 1)) / 2)) |