Step | Hyp | Ref
| Expression |
1 | | elnn0 9177 |
. 2
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
2 | | nnm1nn0 9216 |
. . . . . 6
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
3 | | nn0uz 9561 |
. . . . . 6
โข
โ0 = (โคโฅโ0) |
4 | 2, 3 | eleqtrdi 2270 |
. . . . 5
โข (๐ โ โ โ (๐ โ 1) โ
(โคโฅโ0)) |
5 | | elfznn0 10113 |
. . . . . . 7
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โ0) |
6 | 5 | adantl 277 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (0...(๐ โ 1))) โ ๐ โ โ0) |
7 | 6 | nn0cnd 9230 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (0...(๐ โ 1))) โ ๐ โ โ) |
8 | | id 19 |
. . . . 5
โข (๐ = 0 โ ๐ = 0) |
9 | 4, 7, 8 | fsum1p 11425 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (0...(๐ โ 1))๐ = (0 + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))๐)) |
10 | | 1e0p1 9424 |
. . . . . . . . 9
โข 1 = (0 +
1) |
11 | 10 | oveq1i 5884 |
. . . . . . . 8
โข
(1...(๐ โ 1))
= ((0 + 1)...(๐ โ
1)) |
12 | 11 | sumeq1i 11370 |
. . . . . . 7
โข
ฮฃ๐ โ
(1...(๐ โ 1))๐ = ฮฃ๐ โ ((0 + 1)...(๐ โ 1))๐ |
13 | 12 | oveq2i 5885 |
. . . . . 6
โข (0 +
ฮฃ๐ โ (1...(๐ โ 1))๐) = (0 + ฮฃ๐ โ ((0 + 1)...(๐ โ 1))๐) |
14 | | 1zzd 9279 |
. . . . . . . . 9
โข (๐ โ โ โ 1 โ
โค) |
15 | 2 | nn0zd 9372 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) โ
โค) |
16 | 14, 15 | fzfigd 10430 |
. . . . . . . 8
โข (๐ โ โ โ
(1...(๐ โ 1)) โ
Fin) |
17 | | elfznn 10053 |
. . . . . . . . . 10
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โ) |
18 | 17 | adantl 277 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
19 | 18 | nncnd 8932 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
20 | 16, 19 | fsumcl 11407 |
. . . . . . 7
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))๐ โ โ) |
21 | 20 | addid2d 8106 |
. . . . . 6
โข (๐ โ โ โ (0 +
ฮฃ๐ โ (1...(๐ โ 1))๐) = ฮฃ๐ โ (1...(๐ โ 1))๐) |
22 | 13, 21 | eqtr3id 2224 |
. . . . 5
โข (๐ โ โ โ (0 +
ฮฃ๐ โ ((0 +
1)...(๐ โ 1))๐) = ฮฃ๐ โ (1...(๐ โ 1))๐) |
23 | | arisum 11505 |
. . . . . . 7
โข ((๐ โ 1) โ
โ0 โ ฮฃ๐ โ (1...(๐ โ 1))๐ = ((((๐ โ 1)โ2) + (๐ โ 1)) / 2)) |
24 | 2, 23 | syl 14 |
. . . . . 6
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))๐ = ((((๐ โ 1)โ2) + (๐ โ 1)) / 2)) |
25 | | nncn 8926 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
26 | 25 | 2timesd 9160 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (2
ยท ๐) = (๐ + ๐)) |
27 | 26 | oveq2d 5890 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((๐โ2) โ (2 ยท
๐)) = ((๐โ2) โ (๐ + ๐))) |
28 | 25 | sqcld 10651 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐โ2) โ
โ) |
29 | 28, 25, 25 | subsub4d 8298 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((๐โ2) โ ๐) โ ๐) = ((๐โ2) โ (๐ + ๐))) |
30 | 27, 29 | eqtr4d 2213 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((๐โ2) โ (2 ยท
๐)) = (((๐โ2) โ ๐) โ ๐)) |
31 | 30 | oveq1d 5889 |
. . . . . . . . . 10
โข (๐ โ โ โ (((๐โ2) โ (2 ยท
๐)) + 1) = ((((๐โ2) โ ๐) โ ๐) + 1)) |
32 | | binom2sub1 10634 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((๐ โ 1)โ2) = (((๐โ2) โ (2 ยท
๐)) + 1)) |
33 | 25, 32 | syl 14 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ โ 1)โ2) = (((๐โ2) โ (2 ยท
๐)) + 1)) |
34 | 28, 25 | subcld 8267 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((๐โ2) โ ๐) โ
โ) |
35 | | 1cnd 7972 |
. . . . . . . . . . 11
โข (๐ โ โ โ 1 โ
โ) |
36 | 34, 25, 35 | subsubd 8295 |
. . . . . . . . . 10
โข (๐ โ โ โ (((๐โ2) โ ๐) โ (๐ โ 1)) = ((((๐โ2) โ ๐) โ ๐) + 1)) |
37 | 31, 33, 36 | 3eqtr4d 2220 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ โ 1)โ2) = (((๐โ2) โ ๐) โ (๐ โ 1))) |
38 | 37 | oveq1d 5889 |
. . . . . . . 8
โข (๐ โ โ โ (((๐ โ 1)โ2) + (๐ โ 1)) = ((((๐โ2) โ ๐) โ (๐ โ 1)) + (๐ โ 1))) |
39 | | ax-1cn 7903 |
. . . . . . . . . 10
โข 1 โ
โ |
40 | | subcl 8155 |
. . . . . . . . . 10
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
1) โ โ) |
41 | 25, 39, 40 | sylancl 413 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
42 | 34, 41 | npcand 8271 |
. . . . . . . 8
โข (๐ โ โ โ ((((๐โ2) โ ๐) โ (๐ โ 1)) + (๐ โ 1)) = ((๐โ2) โ ๐)) |
43 | 38, 42 | eqtrd 2210 |
. . . . . . 7
โข (๐ โ โ โ (((๐ โ 1)โ2) + (๐ โ 1)) = ((๐โ2) โ ๐)) |
44 | 43 | oveq1d 5889 |
. . . . . 6
โข (๐ โ โ โ ((((๐ โ 1)โ2) + (๐ โ 1)) / 2) = (((๐โ2) โ ๐) / 2)) |
45 | 24, 44 | eqtrd 2210 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ โ (1...(๐ โ 1))๐ = (((๐โ2) โ ๐) / 2)) |
46 | 22, 45 | eqtrd 2210 |
. . . 4
โข (๐ โ โ โ (0 +
ฮฃ๐ โ ((0 +
1)...(๐ โ 1))๐) = (((๐โ2) โ ๐) / 2)) |
47 | 9, 46 | eqtrd 2210 |
. . 3
โข (๐ โ โ โ
ฮฃ๐ โ (0...(๐ โ 1))๐ = (((๐โ2) โ ๐) / 2)) |
48 | | oveq1 5881 |
. . . . . . . 8
โข (๐ = 0 โ (๐ โ 1) = (0 โ
1)) |
49 | 48 | oveq2d 5890 |
. . . . . . 7
โข (๐ = 0 โ (0...(๐ โ 1)) = (0...(0 โ
1))) |
50 | | 0re 7956 |
. . . . . . . . 9
โข 0 โ
โ |
51 | | ltm1 8802 |
. . . . . . . . 9
โข (0 โ
โ โ (0 โ 1) < 0) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . 8
โข (0
โ 1) < 0 |
53 | | 0z 9263 |
. . . . . . . . 9
โข 0 โ
โค |
54 | | peano2zm 9290 |
. . . . . . . . . 10
โข (0 โ
โค โ (0 โ 1) โ โค) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . 9
โข (0
โ 1) โ โค |
56 | | fzn 10041 |
. . . . . . . . 9
โข ((0
โ โค โง (0 โ 1) โ โค) โ ((0 โ 1) < 0
โ (0...(0 โ 1)) = โ
)) |
57 | 53, 55, 56 | mp2an 426 |
. . . . . . . 8
โข ((0
โ 1) < 0 โ (0...(0 โ 1)) = โ
) |
58 | 52, 57 | mpbi 145 |
. . . . . . 7
โข (0...(0
โ 1)) = โ
|
59 | 49, 58 | eqtrdi 2226 |
. . . . . 6
โข (๐ = 0 โ (0...(๐ โ 1)) =
โ
) |
60 | 59 | sumeq1d 11373 |
. . . . 5
โข (๐ = 0 โ ฮฃ๐ โ (0...(๐ โ 1))๐ = ฮฃ๐ โ โ
๐) |
61 | | sum0 11395 |
. . . . 5
โข
ฮฃ๐ โ
โ
๐ =
0 |
62 | 60, 61 | eqtrdi 2226 |
. . . 4
โข (๐ = 0 โ ฮฃ๐ โ (0...(๐ โ 1))๐ = 0) |
63 | | sq0i 10611 |
. . . . . . . 8
โข (๐ = 0 โ (๐โ2) = 0) |
64 | | id 19 |
. . . . . . . 8
โข (๐ = 0 โ ๐ = 0) |
65 | 63, 64 | oveq12d 5892 |
. . . . . . 7
โข (๐ = 0 โ ((๐โ2) โ ๐) = (0 โ 0)) |
66 | | 0m0e0 9030 |
. . . . . . 7
โข (0
โ 0) = 0 |
67 | 65, 66 | eqtrdi 2226 |
. . . . . 6
โข (๐ = 0 โ ((๐โ2) โ ๐) = 0) |
68 | 67 | oveq1d 5889 |
. . . . 5
โข (๐ = 0 โ (((๐โ2) โ ๐) / 2) = (0 / 2)) |
69 | | 2cn 8989 |
. . . . . 6
โข 2 โ
โ |
70 | | 2ap0 9011 |
. . . . . 6
โข 2 #
0 |
71 | 69, 70 | div0api 8702 |
. . . . 5
โข (0 / 2) =
0 |
72 | 68, 71 | eqtrdi 2226 |
. . . 4
โข (๐ = 0 โ (((๐โ2) โ ๐) / 2) = 0) |
73 | 62, 72 | eqtr4d 2213 |
. . 3
โข (๐ = 0 โ ฮฃ๐ โ (0...(๐ โ 1))๐ = (((๐โ2) โ ๐) / 2)) |
74 | 47, 73 | jaoi 716 |
. 2
โข ((๐ โ โ โจ ๐ = 0) โ ฮฃ๐ โ (0...(๐ โ 1))๐ = (((๐โ2) โ ๐) / 2)) |
75 | 1, 74 | sylbi 121 |
1
โข (๐ โ โ0
โ ฮฃ๐ โ
(0...(๐ โ 1))๐ = (((๐โ2) โ ๐) / 2)) |