Step | Hyp | Ref
| Expression |
1 | | 1zzd 12541 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ 1 โ
โค) |
2 | | nnz 12527 |
. . . 4
โข (๐ โ โ โ ๐ โ
โค) |
3 | 2 | adantr 482 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ ๐ โ
โค) |
4 | | simplr 768 |
. . . 4
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ ๐ด โ โ) |
5 | | 2nn 12233 |
. . . . . 6
โข 2 โ
โ |
6 | | elfznn 13477 |
. . . . . . . 8
โข (๐ โ (1...๐) โ ๐ โ โ) |
7 | 6 | adantl 483 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ ๐ โ โ) |
8 | 7 | nnnn0d 12480 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ ๐ โ โ0) |
9 | | nnexpcl 13987 |
. . . . . 6
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
10 | 5, 8, 9 | sylancr 588 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ (2โ๐) โ โ) |
11 | 10 | nncnd 12176 |
. . . 4
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ (2โ๐) โ โ) |
12 | 10 | nnne0d 12210 |
. . . 4
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ (2โ๐) โ 0) |
13 | 4, 11, 12 | divcld 11938 |
. . 3
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ (๐ด / (2โ๐)) โ โ) |
14 | | oveq2 7370 |
. . . 4
โข (๐ = (๐ + 1) โ (2โ๐) = (2โ(๐ + 1))) |
15 | 14 | oveq2d 7378 |
. . 3
โข (๐ = (๐ + 1) โ (๐ด / (2โ๐)) = (๐ด / (2โ(๐ + 1)))) |
16 | 1, 1, 3, 13, 15 | fsumshftm 15673 |
. 2
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ (1...๐)(๐ด / (2โ๐)) = ฮฃ๐ โ ((1 โ 1)...(๐ โ 1))(๐ด / (2โ(๐ + 1)))) |
17 | | 1m1e0 12232 |
. . . . 5
โข (1
โ 1) = 0 |
18 | 17 | oveq1i 7372 |
. . . 4
โข ((1
โ 1)...(๐ โ 1))
= (0...(๐ โ
1)) |
19 | 18 | sumeq1i 15590 |
. . 3
โข
ฮฃ๐ โ ((1
โ 1)...(๐ โ
1))(๐ด / (2โ(๐ + 1))) = ฮฃ๐ โ (0...(๐ โ 1))(๐ด / (2โ(๐ + 1))) |
20 | | halfcn 12375 |
. . . . . . . . . 10
โข (1 / 2)
โ โ |
21 | | elfznn0 13541 |
. . . . . . . . . . 11
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โ0) |
22 | 21 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ ๐ โ โ0) |
23 | | expcl 13992 |
. . . . . . . . . 10
โข (((1 / 2)
โ โ โง ๐
โ โ0) โ ((1 / 2)โ๐) โ โ) |
24 | 20, 22, 23 | sylancr 588 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((1 / 2)โ๐) โ
โ) |
25 | | 2cnd 12238 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ 2 โ
โ) |
26 | | 2ne0 12264 |
. . . . . . . . . 10
โข 2 โ
0 |
27 | 26 | a1i 11 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ 2 โ
0) |
28 | 24, 25, 27 | divrecd 11941 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (((1 / 2)โ๐) / 2) = (((1 / 2)โ๐) ยท (1 /
2))) |
29 | | expp1 13981 |
. . . . . . . . 9
โข (((1 / 2)
โ โ โง ๐
โ โ0) โ ((1 / 2)โ(๐ + 1)) = (((1 / 2)โ๐) ยท (1 / 2))) |
30 | 20, 22, 29 | sylancr 588 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((1 / 2)โ(๐ + 1)) = (((1 / 2)โ๐) ยท (1 /
2))) |
31 | | elfzelz 13448 |
. . . . . . . . . . 11
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โค) |
32 | 31 | peano2zd 12617 |
. . . . . . . . . 10
โข (๐ โ (0...(๐ โ 1)) โ (๐ + 1) โ โค) |
33 | 32 | adantl 483 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐ + 1) โ โค) |
34 | 25, 27, 33 | exprecd 14066 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((1 / 2)โ(๐ + 1)) = (1 / (2โ(๐ + 1)))) |
35 | 28, 30, 34 | 3eqtr2rd 2784 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (1 / (2โ(๐ + 1))) = (((1 / 2)โ๐) / 2)) |
36 | 35 | oveq2d 7378 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐ด ยท (1 / (2โ(๐ + 1)))) = (๐ด ยท (((1 / 2)โ๐) / 2))) |
37 | | simplr 768 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ ๐ด โ โ) |
38 | | peano2nn0 12460 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
39 | 22, 38 | syl 17 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐ + 1) โ
โ0) |
40 | | nnexpcl 13987 |
. . . . . . . . 9
โข ((2
โ โ โง (๐ +
1) โ โ0) โ (2โ(๐ + 1)) โ โ) |
41 | 5, 39, 40 | sylancr 588 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (2โ(๐ + 1)) โ
โ) |
42 | 41 | nncnd 12176 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (2โ(๐ + 1)) โ
โ) |
43 | 41 | nnne0d 12210 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (2โ(๐ + 1)) โ 0) |
44 | 37, 42, 43 | divrecd 11941 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐ด / (2โ(๐ + 1))) = (๐ด ยท (1 / (2โ(๐ + 1))))) |
45 | 24, 37, 25, 27 | div12d 11974 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (((1 / 2)โ๐) ยท (๐ด / 2)) = (๐ด ยท (((1 / 2)โ๐) / 2))) |
46 | 36, 44, 45 | 3eqtr4d 2787 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐ด / (2โ(๐ + 1))) = (((1 / 2)โ๐) ยท (๐ด / 2))) |
47 | 46 | sumeq2dv 15595 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ (0...(๐ โ 1))(๐ด / (2โ(๐ + 1))) = ฮฃ๐ โ (0...(๐ โ 1))(((1 / 2)โ๐) ยท (๐ด / 2))) |
48 | | fzfid 13885 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ
(0...(๐ โ 1)) โ
Fin) |
49 | | halfcl 12385 |
. . . . . 6
โข (๐ด โ โ โ (๐ด / 2) โ
โ) |
50 | 49 | adantl 483 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ด / 2) โ
โ) |
51 | 48, 50, 24 | fsummulc1 15677 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ
(ฮฃ๐ โ
(0...(๐ โ 1))((1 /
2)โ๐) ยท (๐ด / 2)) = ฮฃ๐ โ (0...(๐ โ 1))(((1 / 2)โ๐) ยท (๐ด / 2))) |
52 | 47, 51 | eqtr4d 2780 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ (0...(๐ โ 1))(๐ด / (2โ(๐ + 1))) = (ฮฃ๐ โ (0...(๐ โ 1))((1 / 2)โ๐) ยท (๐ด / 2))) |
53 | 19, 52 | eqtrid 2789 |
. 2
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ ((1 โ
1)...(๐ โ 1))(๐ด / (2โ(๐ + 1))) = (ฮฃ๐ โ (0...(๐ โ 1))((1 / 2)โ๐) ยท (๐ด / 2))) |
54 | | 2cnd 12238 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ) โ 2 โ
โ) |
55 | 26 | a1i 11 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ) โ 2 โ
0) |
56 | 54, 55, 3 | exprecd 14066 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โ) โ ((1 /
2)โ๐) = (1 /
(2โ๐))) |
57 | 56 | oveq2d 7378 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1
โ ((1 / 2)โ๐)) =
(1 โ (1 / (2โ๐)))) |
58 | | 1mhlfehlf 12379 |
. . . . . . 7
โข (1
โ (1 / 2)) = (1 / 2) |
59 | 58 | a1i 11 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1
โ (1 / 2)) = (1 / 2)) |
60 | 57, 59 | oveq12d 7380 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ ((1
โ ((1 / 2)โ๐)) /
(1 โ (1 / 2))) = ((1 โ (1 / (2โ๐))) / (1 / 2))) |
61 | | simpr 486 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ ๐ด โ
โ) |
62 | 61, 54, 55 | divrec2d 11942 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ด / 2) = ((1 / 2) ยท ๐ด)) |
63 | 60, 62 | oveq12d 7380 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ (((1
โ ((1 / 2)โ๐)) /
(1 โ (1 / 2))) ยท (๐ด / 2)) = (((1 โ (1 / (2โ๐))) / (1 / 2)) ยท ((1 / 2)
ยท ๐ด))) |
64 | | ax-1cn 11116 |
. . . . . . 7
โข 1 โ
โ |
65 | | nnnn0 12427 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ0) |
66 | 65 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ด โ โ) โ ๐ โ
โ0) |
67 | | nnexpcl 13987 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
68 | 5, 66, 67 | sylancr 588 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โ) โ
(2โ๐) โ
โ) |
69 | 68 | nnrecred 12211 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ) โ (1 /
(2โ๐)) โ
โ) |
70 | 69 | recnd 11190 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โ) โ (1 /
(2โ๐)) โ
โ) |
71 | | subcl 11407 |
. . . . . . 7
โข ((1
โ โ โง (1 / (2โ๐)) โ โ) โ (1 โ (1 /
(2โ๐))) โ
โ) |
72 | 64, 70, 71 | sylancr 588 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1
โ (1 / (2โ๐)))
โ โ) |
73 | 20 | a1i 11 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1 / 2)
โ โ) |
74 | | 0re 11164 |
. . . . . . . 8
โข 0 โ
โ |
75 | | halfgt0 12376 |
. . . . . . . 8
โข 0 < (1
/ 2) |
76 | 74, 75 | gtneii 11274 |
. . . . . . 7
โข (1 / 2)
โ 0 |
77 | 76 | a1i 11 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1 / 2)
โ 0) |
78 | 72, 73, 77 | divcld 11938 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ ((1
โ (1 / (2โ๐))) /
(1 / 2)) โ โ) |
79 | 78, 73, 61 | mulassd 11185 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ ((((1
โ (1 / (2โ๐))) /
(1 / 2)) ยท (1 / 2)) ยท ๐ด) = (((1 โ (1 / (2โ๐))) / (1 / 2)) ยท ((1 / 2)
ยท ๐ด))) |
80 | 72, 73, 77 | divcan1d 11939 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ (((1
โ (1 / (2โ๐))) /
(1 / 2)) ยท (1 / 2)) = (1 โ (1 / (2โ๐)))) |
81 | 80 | oveq1d 7377 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ ((((1
โ (1 / (2โ๐))) /
(1 / 2)) ยท (1 / 2)) ยท ๐ด) = ((1 โ (1 / (2โ๐))) ยท ๐ด)) |
82 | 63, 79, 81 | 3eqtr2d 2783 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ (((1
โ ((1 / 2)โ๐)) /
(1 โ (1 / 2))) ยท (๐ด / 2)) = ((1 โ (1 / (2โ๐))) ยท ๐ด)) |
83 | | halfre 12374 |
. . . . . . 7
โข (1 / 2)
โ โ |
84 | | halflt1 12378 |
. . . . . . 7
โข (1 / 2)
< 1 |
85 | 83, 84 | ltneii 11275 |
. . . . . 6
โข (1 / 2)
โ 1 |
86 | 85 | a1i 11 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ (1 / 2)
โ 1) |
87 | 73, 86, 66 | geoser 15759 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ (0...(๐ โ 1))((1 / 2)โ๐) = ((1 โ ((1 /
2)โ๐)) / (1 โ (1
/ 2)))) |
88 | 87 | oveq1d 7377 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ
(ฮฃ๐ โ
(0...(๐ โ 1))((1 /
2)โ๐) ยท (๐ด / 2)) = (((1 โ ((1 /
2)โ๐)) / (1 โ (1
/ 2))) ยท (๐ด /
2))) |
89 | | mulid2 11161 |
. . . . . . 7
โข (๐ด โ โ โ (1
ยท ๐ด) = ๐ด) |
90 | 89 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1
ยท ๐ด) = ๐ด) |
91 | 90 | eqcomd 2743 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ ๐ด = (1 ยท ๐ด)) |
92 | 68 | nncnd 12176 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ
(2โ๐) โ
โ) |
93 | 68 | nnne0d 12210 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ
(2โ๐) โ
0) |
94 | 61, 92, 93 | divrec2d 11942 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ด / (2โ๐)) = ((1 / (2โ๐)) ยท ๐ด)) |
95 | 91, 94 | oveq12d 7380 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ด โ (๐ด / (2โ๐))) = ((1 ยท ๐ด) โ ((1 / (2โ๐)) ยท ๐ด))) |
96 | 64 | a1i 11 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ 1 โ
โ) |
97 | 96, 70, 61 | subdird 11619 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ ((1
โ (1 / (2โ๐)))
ยท ๐ด) = ((1 ยท
๐ด) โ ((1 /
(2โ๐)) ยท ๐ด))) |
98 | 95, 97 | eqtr4d 2780 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ด โ (๐ด / (2โ๐))) = ((1 โ (1 / (2โ๐))) ยท ๐ด)) |
99 | 82, 88, 98 | 3eqtr4d 2787 |
. 2
โข ((๐ โ โ โง ๐ด โ โ) โ
(ฮฃ๐ โ
(0...(๐ โ 1))((1 /
2)โ๐) ยท (๐ด / 2)) = (๐ด โ (๐ด / (2โ๐)))) |
100 | 16, 53, 99 | 3eqtrd 2781 |
1
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ (1...๐)(๐ด / (2โ๐)) = (๐ด โ (๐ด / (2โ๐)))) |