Step | Hyp | Ref
| Expression |
1 | | 2nn 8631 |
. . 3
⊢ 2 ∈
ℕ |
2 | | ibcval5 10225 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 2 ∈ ℕ) → (𝑁C2) = ((seq((𝑁 − 2) + 1)( · , I ,
ℂ)‘𝑁) /
(!‘2))) |
3 | 1, 2 | mpan2 417 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑁C2) = ((seq((𝑁 − 2) + 1)( · , I ,
ℂ)‘𝑁) /
(!‘2))) |
4 | | 2m1e1 8594 |
. . . . . . . 8
⊢ (2
− 1) = 1 |
5 | 4 | oveq2i 5677 |
. . . . . . 7
⊢ ((𝑁 − 2) + (2 − 1)) =
((𝑁 − 2) +
1) |
6 | | nn0cn 8737 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
7 | | 2cn 8547 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
8 | | ax-1cn 7492 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
9 | | npncan 7757 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 2) + (2 − 1)) = (𝑁 − 1)) |
10 | 7, 8, 9 | mp3an23 1266 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → ((𝑁 − 2) + (2 − 1)) =
(𝑁 −
1)) |
11 | 6, 10 | syl 14 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 2) + (2
− 1)) = (𝑁 −
1)) |
12 | 5, 11 | syl5eqr 2135 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 2) + 1)
= (𝑁 −
1)) |
13 | | iseqeq1 9912 |
. . . . . 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 5320 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (seq((𝑁 − 2) +
1)( · , I , ℂ)‘𝑁) = (seq(𝑁 − 1)( · , I ,
ℂ)‘𝑁)) |
16 | | nn0z 8824 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
17 | | peano2zm 8842 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
18 | 16, 17 | syl 14 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 − 1) ∈
ℤ) |
19 | | uzid 9087 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
20 | 16, 19 | syl 14 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘𝑁)) |
21 | | npcan 7745 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
22 | 6, 8, 21 | sylancl 405 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1) + 1)
= 𝑁) |
23 | 22 | fveq2d 5322 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (ℤ≥‘((𝑁 − 1) + 1)) =
(ℤ≥‘𝑁)) |
24 | 20, 23 | eleqtrrd 2168 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘((𝑁 − 1) + 1))) |
25 | | eluzelcn 9084 |
. . . . . . . . 9
⊢ (𝑥 ∈
(ℤ≥‘(𝑁 − 1)) → 𝑥 ∈ ℂ) |
26 | 25 | adantl 272 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
(ℤ≥‘(𝑁 − 1))) → 𝑥 ∈ ℂ) |
27 | | fvi 5374 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → ( I
‘𝑥) = 𝑥) |
28 | 27 | eleq1d 2157 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (( I
‘𝑥) ∈ ℂ
↔ 𝑥 ∈
ℂ)) |
29 | 28 | ibir 176 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → ( I
‘𝑥) ∈
ℂ) |
30 | 26, 29 | syl 14 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
(ℤ≥‘(𝑁 − 1))) → ( I ‘𝑥) ∈
ℂ) |
31 | | mulcl 7523 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
32 | 31 | adantl 272 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ ℂ
∧ 𝑦 ∈ ℂ))
→ (𝑥 · 𝑦) ∈
ℂ) |
33 | 18, 24, 30, 32 | iseqm1 9942 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I , ℂ)‘𝑁) = ((seq(𝑁 − 1)( · , I ,
ℂ)‘(𝑁 −
1)) · ( I ‘𝑁))) |
34 | 18, 30, 32 | iseq1 9929 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I , ℂ)‘(𝑁 − 1)) = ( I ‘(𝑁 − 1))) |
35 | | fvi 5374 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈ ℤ
→ ( I ‘(𝑁
− 1)) = (𝑁 −
1)) |
36 | 18, 35 | syl 14 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ( I ‘(𝑁
− 1)) = (𝑁 −
1)) |
37 | 34, 36 | eqtrd 2121 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I , ℂ)‘(𝑁 − 1)) = (𝑁 − 1)) |
38 | | fvi 5374 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ( I ‘𝑁) =
𝑁) |
39 | 37, 38 | oveq12d 5684 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((seq(𝑁 − 1)(
· , I , ℂ)‘(𝑁 − 1)) · ( I ‘𝑁)) = ((𝑁 − 1) · 𝑁)) |
40 | 33, 39 | eqtrd 2121 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I , ℂ)‘𝑁) = ((𝑁 − 1) · 𝑁)) |
41 | | subcl 7735 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
1) ∈ ℂ) |
42 | 6, 8, 41 | sylancl 405 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 − 1) ∈
ℂ) |
43 | 42, 6 | mulcomd 7563 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1)
· 𝑁) = (𝑁 · (𝑁 − 1))) |
44 | 40, 43 | eqtrd 2121 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (seq(𝑁 − 1)(
· , I , ℂ)‘𝑁) = (𝑁 · (𝑁 − 1))) |
45 | 15, 44 | eqtrd 2121 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (seq((𝑁 − 2) +
1)( · , I , ℂ)‘𝑁) = (𝑁 · (𝑁 − 1))) |
46 | | fac2 10193 |
. . . 4
⊢
(!‘2) = 2 |
47 | 46 | a1i 9 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (!‘2) = 2) |
48 | 45, 47 | oveq12d 5684 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((seq((𝑁 − 2)
+ 1)( · , I , ℂ)‘𝑁) / (!‘2)) = ((𝑁 · (𝑁 − 1)) / 2)) |
49 | 3, 48 | eqtrd 2121 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝑁C2) = ((𝑁 · (𝑁 − 1)) / 2)) |