Step | Hyp | Ref
| Expression |
1 | | elnn0 9177 |
. 2
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
2 | | 1zzd 9279 |
. . . . . 6
โข (๐ โ โ โ 1 โ
โค) |
3 | | nnz 9271 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
4 | | elfzelz 10024 |
. . . . . . . 8
โข (๐ โ (1...๐) โ ๐ โ โค) |
5 | 4 | zcnd 9375 |
. . . . . . 7
โข (๐ โ (1...๐) โ ๐ โ โ) |
6 | 5 | adantl 277 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ๐ โ โ) |
7 | | id 19 |
. . . . . 6
โข (๐ = (๐ + 1) โ ๐ = (๐ + 1)) |
8 | 2, 2, 3, 6, 7 | fsumshftm 11452 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ โ (1...๐)๐ = ฮฃ๐ โ ((1 โ 1)...(๐ โ 1))(๐ + 1)) |
9 | | 1m1e0 8987 |
. . . . . . 7
โข (1
โ 1) = 0 |
10 | 9 | oveq1i 5884 |
. . . . . 6
โข ((1
โ 1)...(๐ โ 1))
= (0...(๐ โ
1)) |
11 | 10 | sumeq1i 11370 |
. . . . 5
โข
ฮฃ๐ โ ((1
โ 1)...(๐ โ
1))(๐ + 1) = ฮฃ๐ โ (0...(๐ โ 1))(๐ + 1) |
12 | 8, 11 | eqtrdi 2226 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (1...๐)๐ = ฮฃ๐ โ (0...(๐ โ 1))(๐ + 1)) |
13 | | elfznn0 10113 |
. . . . . . . . 9
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โ0) |
14 | 13 | adantl 277 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (0...(๐ โ 1))) โ ๐ โ โ0) |
15 | | bcnp1n 10738 |
. . . . . . . 8
โข (๐ โ โ0
โ ((๐ + 1)C๐) = (๐ + 1)) |
16 | 14, 15 | syl 14 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (0...(๐ โ 1))) โ ((๐ + 1)C๐) = (๐ + 1)) |
17 | 14 | nn0cnd 9230 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (0...(๐ โ 1))) โ ๐ โ โ) |
18 | | ax-1cn 7903 |
. . . . . . . . 9
โข 1 โ
โ |
19 | | addcom 8093 |
. . . . . . . . 9
โข ((๐ โ โ โง 1 โ
โ) โ (๐ + 1) =
(1 + ๐)) |
20 | 17, 18, 19 | sylancl 413 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (0...(๐ โ 1))) โ (๐ + 1) = (1 + ๐)) |
21 | 20 | oveq1d 5889 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (0...(๐ โ 1))) โ ((๐ + 1)C๐) = ((1 + ๐)C๐)) |
22 | 16, 21 | eqtr3d 2212 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (0...(๐ โ 1))) โ (๐ + 1) = ((1 + ๐)C๐)) |
23 | 22 | sumeq2dv 11375 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ โ (0...(๐ โ 1))(๐ + 1) = ฮฃ๐ โ (0...(๐ โ 1))((1 + ๐)C๐)) |
24 | | 1nn0 9191 |
. . . . . 6
โข 1 โ
โ0 |
25 | | nnm1nn0 9216 |
. . . . . 6
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
26 | | bcxmas 11496 |
. . . . . 6
โข ((1
โ โ0 โง (๐ โ 1) โ โ0)
โ (((1 + 1) + (๐
โ 1))C(๐ โ 1))
= ฮฃ๐ โ
(0...(๐ โ 1))((1 +
๐)C๐)) |
27 | 24, 25, 26 | sylancr 414 |
. . . . 5
โข (๐ โ โ โ (((1 + 1)
+ (๐ โ 1))C(๐ โ 1)) = ฮฃ๐ โ (0...(๐ โ 1))((1 + ๐)C๐)) |
28 | 23, 27 | eqtr4d 2213 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (0...(๐ โ 1))(๐ + 1) = (((1 + 1) + (๐ โ 1))C(๐ โ 1))) |
29 | | 1cnd 7972 |
. . . . . . 7
โข (๐ โ โ โ 1 โ
โ) |
30 | | nncn 8926 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
31 | 29, 29, 30 | ppncand 8307 |
. . . . . . 7
โข (๐ โ โ โ ((1 + 1)
+ (๐ โ 1)) = (1 +
๐)) |
32 | 29, 30, 31 | comraddd 8113 |
. . . . . 6
โข (๐ โ โ โ ((1 + 1)
+ (๐ โ 1)) = (๐ + 1)) |
33 | 32 | oveq1d 5889 |
. . . . 5
โข (๐ โ โ โ (((1 + 1)
+ (๐ โ 1))C(๐ โ 1)) = ((๐ + 1)C(๐ โ 1))) |
34 | | nnnn0 9182 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ0) |
35 | | bcp1m1 10744 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ + 1)C(๐ โ 1)) = (((๐ + 1) ยท ๐) / 2)) |
36 | 34, 35 | syl 14 |
. . . . 5
โข (๐ โ โ โ ((๐ + 1)C(๐ โ 1)) = (((๐ + 1) ยท ๐) / 2)) |
37 | | sqval 10577 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐โ2) = (๐ ยท ๐)) |
38 | 37 | eqcomd 2183 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ ยท ๐) = (๐โ2)) |
39 | | mullid 7954 |
. . . . . . . . 9
โข (๐ โ โ โ (1
ยท ๐) = ๐) |
40 | 38, 39 | oveq12d 5892 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ ยท ๐) + (1 ยท ๐)) = ((๐โ2) + ๐)) |
41 | 30, 40 | syl 14 |
. . . . . . 7
โข (๐ โ โ โ ((๐ ยท ๐) + (1 ยท ๐)) = ((๐โ2) + ๐)) |
42 | 30, 30, 29, 41 | joinlmuladdmuld 7984 |
. . . . . 6
โข (๐ โ โ โ ((๐ + 1) ยท ๐) = ((๐โ2) + ๐)) |
43 | 42 | oveq1d 5889 |
. . . . 5
โข (๐ โ โ โ (((๐ + 1) ยท ๐) / 2) = (((๐โ2) + ๐) / 2)) |
44 | 33, 36, 43 | 3eqtrd 2214 |
. . . 4
โข (๐ โ โ โ (((1 + 1)
+ (๐ โ 1))C(๐ โ 1)) = (((๐โ2) + ๐) / 2)) |
45 | 12, 28, 44 | 3eqtrd 2214 |
. . 3
โข (๐ โ โ โ
ฮฃ๐ โ (1...๐)๐ = (((๐โ2) + ๐) / 2)) |
46 | | oveq2 5882 |
. . . . . . 7
โข (๐ = 0 โ (1...๐) = (1...0)) |
47 | | fz10 10045 |
. . . . . . 7
โข (1...0) =
โ
|
48 | 46, 47 | eqtrdi 2226 |
. . . . . 6
โข (๐ = 0 โ (1...๐) = โ
) |
49 | 48 | sumeq1d 11373 |
. . . . 5
โข (๐ = 0 โ ฮฃ๐ โ (1...๐)๐ = ฮฃ๐ โ โ
๐) |
50 | | sum0 11395 |
. . . . 5
โข
ฮฃ๐ โ
โ
๐ =
0 |
51 | 49, 50 | eqtrdi 2226 |
. . . 4
โข (๐ = 0 โ ฮฃ๐ โ (1...๐)๐ = 0) |
52 | | sq0i 10611 |
. . . . . . . 8
โข (๐ = 0 โ (๐โ2) = 0) |
53 | | id 19 |
. . . . . . . 8
โข (๐ = 0 โ ๐ = 0) |
54 | 52, 53 | oveq12d 5892 |
. . . . . . 7
โข (๐ = 0 โ ((๐โ2) + ๐) = (0 + 0)) |
55 | | 00id 8097 |
. . . . . . 7
โข (0 + 0) =
0 |
56 | 54, 55 | eqtrdi 2226 |
. . . . . 6
โข (๐ = 0 โ ((๐โ2) + ๐) = 0) |
57 | 56 | oveq1d 5889 |
. . . . 5
โข (๐ = 0 โ (((๐โ2) + ๐) / 2) = (0 / 2)) |
58 | | 2cn 8989 |
. . . . . 6
โข 2 โ
โ |
59 | | 2ap0 9011 |
. . . . . 6
โข 2 #
0 |
60 | 58, 59 | div0api 8702 |
. . . . 5
โข (0 / 2) =
0 |
61 | 57, 60 | eqtrdi 2226 |
. . . 4
โข (๐ = 0 โ (((๐โ2) + ๐) / 2) = 0) |
62 | 51, 61 | eqtr4d 2213 |
. . 3
โข (๐ = 0 โ ฮฃ๐ โ (1...๐)๐ = (((๐โ2) + ๐) / 2)) |
63 | 45, 62 | jaoi 716 |
. 2
โข ((๐ โ โ โจ ๐ = 0) โ ฮฃ๐ โ (1...๐)๐ = (((๐โ2) + ๐) / 2)) |
64 | 1, 63 | sylbi 121 |
1
โข (๐ โ โ0
โ ฮฃ๐ โ
(1...๐)๐ = (((๐โ2) + ๐) / 2)) |