Step | Hyp | Ref
| Expression |
1 | | 2nn 8193 |
. . 3
⊢ 2 ∈
ℕ |
2 | | ibcval5 9690 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 2 ∈ ℕ) → (𝑁C2) = ((seq((𝑁 − 2) + 1)( · , I ,
ℂ)‘𝑁) /
(!‘2))) |
3 | 1, 2 | mpan2 415 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑁C2) = ((seq((𝑁 − 2) + 1)( · , I ,
ℂ)‘𝑁) /
(!‘2))) |
4 | | 2m1e1 8156 |
. . . . . . . 8
⊢ (2
− 1) = 1 |
5 | 4 | oveq2i 5543 |
. . . . . . 7
⊢ ((𝑁 − 2) + (2 − 1)) =
((𝑁 − 2) +
1) |
6 | | nn0cn 8298 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
7 | | 2cn 8110 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
8 | | ax-1cn 7069 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
9 | | npncan 7329 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 2) + (2 − 1)) = (𝑁 − 1)) |
10 | 7, 8, 9 | mp3an23 1260 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → ((𝑁 − 2) + (2 − 1)) =
(𝑁 −
1)) |
11 | 6, 10 | syl 14 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 2) + (2
− 1)) = (𝑁 −
1)) |
12 | 5, 11 | syl5eqr 2127 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 2) + 1)
= (𝑁 −
1)) |
13 | | iseqeq1 9434 |
. . . . . 6
⊢ (((𝑁 − 2) + 1) = (𝑁 − 1) → seq((𝑁 − 2) + 1)( · , I ,
ℂ) = seq(𝑁 −
1)( · , I , ℂ)) |
14 | 12, 13 | syl 14 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ seq((𝑁 − 2) +
1)( · , I , ℂ) = seq(𝑁 − 1)( · , I ,
ℂ)) |
15 | 14 | fveq1d 5200 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (seq((𝑁 − 2) +
1)( · , I , ℂ)‘𝑁) = (seq(𝑁 − 1)( · , I ,
ℂ)‘𝑁)) |
16 | | nn0z 8371 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
17 | | peano2zm 8389 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
18 | 16, 17 | syl 14 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 − 1) ∈
ℤ) |
19 | | uzid 8633 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
20 | 16, 19 | syl 14 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘𝑁)) |
21 | | npcan 7317 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
22 | 6, 8, 21 | sylancl 404 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1) + 1)
= 𝑁) |
23 | 22 | fveq2d 5202 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (ℤ≥‘((𝑁 − 1) + 1)) =
(ℤ≥‘𝑁)) |
24 | 20, 23 | eleqtrrd 2158 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘((𝑁 − 1) + 1))) |
25 | | cnex 7097 |
. . . . . . . 8
⊢ ℂ
∈ V |
26 | 25 | a1i 9 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ℂ ∈ V) |
27 | | eluzelcn 8630 |
. . . . . . . . 9
⊢ (𝑥 ∈
(ℤ≥‘(𝑁 − 1)) → 𝑥 ∈ ℂ) |
28 | 27 | adantl 271 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
(ℤ≥‘(𝑁 − 1))) → 𝑥 ∈ ℂ) |
29 | | fvi 5251 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → ( I
‘𝑥) = 𝑥) |
30 | 29 | eleq1d 2147 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (( I
‘𝑥) ∈ ℂ
↔ 𝑥 ∈
ℂ)) |
31 | 30 | ibir 175 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → ( I
‘𝑥) ∈
ℂ) |
32 | 28, 31 | syl 14 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
(ℤ≥‘(𝑁 − 1))) → ( I ‘𝑥) ∈
ℂ) |
33 | | mulcl 7100 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
34 | 33 | adantl 271 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ ℂ
∧ 𝑦 ∈ ℂ))
→ (𝑥 · 𝑦) ∈
ℂ) |
35 | 18, 24, 26, 32, 34 | iseqm1 9447 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I , ℂ)‘𝑁) = ((seq(𝑁 − 1)( · , I ,
ℂ)‘(𝑁 −
1)) · ( I ‘𝑁))) |
36 | 18, 26, 32, 34 | iseq1 9442 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I , ℂ)‘(𝑁 − 1)) = ( I ‘(𝑁 − 1))) |
37 | | fvi 5251 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈ ℤ
→ ( I ‘(𝑁
− 1)) = (𝑁 −
1)) |
38 | 18, 37 | syl 14 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ( I ‘(𝑁
− 1)) = (𝑁 −
1)) |
39 | 36, 38 | eqtrd 2113 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I , ℂ)‘(𝑁 − 1)) = (𝑁 − 1)) |
40 | | fvi 5251 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ( I ‘𝑁) =
𝑁) |
41 | 39, 40 | oveq12d 5550 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((seq(𝑁 − 1)(
· , I , ℂ)‘(𝑁 − 1)) · ( I ‘𝑁)) = ((𝑁 − 1) · 𝑁)) |
42 | 35, 41 | eqtrd 2113 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I , ℂ)‘𝑁) = ((𝑁 − 1) · 𝑁)) |
43 | | subcl 7307 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
1) ∈ ℂ) |
44 | 6, 8, 43 | sylancl 404 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 − 1) ∈
ℂ) |
45 | 44, 6 | mulcomd 7140 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1)
· 𝑁) = (𝑁 · (𝑁 − 1))) |
46 | 42, 45 | eqtrd 2113 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I , ℂ)‘𝑁) = (𝑁 · (𝑁 − 1))) |
47 | 15, 46 | eqtrd 2113 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (seq((𝑁 − 2) +
1)( · , I , ℂ)‘𝑁) = (𝑁 · (𝑁 − 1))) |
48 | | fac2 9658 |
. . . 4
⊢
(!‘2) = 2 |
49 | 48 | a1i 9 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (!‘2) = 2) |
50 | 47, 49 | oveq12d 5550 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((seq((𝑁 − 2)
+ 1)( · , I , ℂ)‘𝑁) / (!‘2)) = ((𝑁 · (𝑁 − 1)) / 2)) |
51 | 3, 50 | eqtrd 2113 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝑁C2) = ((𝑁 · (𝑁 − 1)) / 2)) |