Step | Hyp | Ref
| Expression |
1 | | 1zzd 9282 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ 1 โ
โค) |
2 | | nnz 9274 |
. . . 4
โข (๐ โ โ โ ๐ โ
โค) |
3 | 2 | adantr 276 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ ๐ โ
โค) |
4 | | simplr 528 |
. . . 4
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ ๐ด โ โ) |
5 | | 2nn 9082 |
. . . . . 6
โข 2 โ
โ |
6 | | elfznn 10056 |
. . . . . . . 8
โข (๐ โ (1...๐) โ ๐ โ โ) |
7 | 6 | adantl 277 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ ๐ โ โ) |
8 | 7 | nnnn0d 9231 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ ๐ โ โ0) |
9 | | nnexpcl 10535 |
. . . . . 6
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
10 | 5, 8, 9 | sylancr 414 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ (2โ๐) โ โ) |
11 | 10 | nncnd 8935 |
. . . 4
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ (2โ๐) โ โ) |
12 | 10 | nnap0d 8967 |
. . . 4
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ (2โ๐) # 0) |
13 | 4, 11, 12 | divclapd 8749 |
. . 3
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (1...๐)) โ (๐ด / (2โ๐)) โ โ) |
14 | | oveq2 5885 |
. . . 4
โข (๐ = (๐ + 1) โ (2โ๐) = (2โ(๐ + 1))) |
15 | 14 | oveq2d 5893 |
. . 3
โข (๐ = (๐ + 1) โ (๐ด / (2โ๐)) = (๐ด / (2โ(๐ + 1)))) |
16 | 1, 1, 3, 13, 15 | fsumshftm 11455 |
. 2
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ (1...๐)(๐ด / (2โ๐)) = ฮฃ๐ โ ((1 โ 1)...(๐ โ 1))(๐ด / (2โ(๐ + 1)))) |
17 | | 1m1e0 8990 |
. . . . 5
โข (1
โ 1) = 0 |
18 | 17 | oveq1i 5887 |
. . . 4
โข ((1
โ 1)...(๐ โ 1))
= (0...(๐ โ
1)) |
19 | 18 | sumeq1i 11373 |
. . 3
โข
ฮฃ๐ โ ((1
โ 1)...(๐ โ
1))(๐ด / (2โ(๐ + 1))) = ฮฃ๐ โ (0...(๐ โ 1))(๐ด / (2โ(๐ + 1))) |
20 | | halfcn 9135 |
. . . . . . . . . 10
โข (1 / 2)
โ โ |
21 | | elfznn0 10116 |
. . . . . . . . . . 11
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โ0) |
22 | 21 | adantl 277 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ ๐ โ โ0) |
23 | | expcl 10540 |
. . . . . . . . . 10
โข (((1 / 2)
โ โ โง ๐
โ โ0) โ ((1 / 2)โ๐) โ โ) |
24 | 20, 22, 23 | sylancr 414 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((1 / 2)โ๐) โ
โ) |
25 | | 2cnd 8994 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ 2 โ
โ) |
26 | | 2ap0 9014 |
. . . . . . . . . 10
โข 2 #
0 |
27 | 26 | a1i 9 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ 2 # 0) |
28 | 24, 25, 27 | divrecapd 8752 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (((1 / 2)โ๐) / 2) = (((1 / 2)โ๐) ยท (1 /
2))) |
29 | | expp1 10529 |
. . . . . . . . 9
โข (((1 / 2)
โ โ โง ๐
โ โ0) โ ((1 / 2)โ(๐ + 1)) = (((1 / 2)โ๐) ยท (1 / 2))) |
30 | 20, 22, 29 | sylancr 414 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((1 / 2)โ(๐ + 1)) = (((1 / 2)โ๐) ยท (1 /
2))) |
31 | | elfzelz 10027 |
. . . . . . . . . . 11
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โค) |
32 | 31 | peano2zd 9380 |
. . . . . . . . . 10
โข (๐ โ (0...(๐ โ 1)) โ (๐ + 1) โ โค) |
33 | 32 | adantl 277 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐ + 1) โ โค) |
34 | 25, 27, 33 | exprecapd 10664 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((1 / 2)โ(๐ + 1)) = (1 / (2โ(๐ + 1)))) |
35 | 28, 30, 34 | 3eqtr2rd 2217 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (1 / (2โ(๐ + 1))) = (((1 / 2)โ๐) / 2)) |
36 | 35 | oveq2d 5893 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐ด ยท (1 / (2โ(๐ + 1)))) = (๐ด ยท (((1 / 2)โ๐) / 2))) |
37 | | simplr 528 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ ๐ด โ โ) |
38 | | peano2nn0 9218 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
39 | 22, 38 | syl 14 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐ + 1) โ
โ0) |
40 | | nnexpcl 10535 |
. . . . . . . . 9
โข ((2
โ โ โง (๐ +
1) โ โ0) โ (2โ(๐ + 1)) โ โ) |
41 | 5, 39, 40 | sylancr 414 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (2โ(๐ + 1)) โ
โ) |
42 | 41 | nncnd 8935 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (2โ(๐ + 1)) โ
โ) |
43 | 41 | nnap0d 8967 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (2โ(๐ + 1)) # 0) |
44 | 37, 42, 43 | divrecapd 8752 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐ด / (2โ(๐ + 1))) = (๐ด ยท (1 / (2โ(๐ + 1))))) |
45 | 24, 37, 25, 27 | div12apd 8786 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (((1 / 2)โ๐) ยท (๐ด / 2)) = (๐ด ยท (((1 / 2)โ๐) / 2))) |
46 | 36, 44, 45 | 3eqtr4d 2220 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐ด / (2โ(๐ + 1))) = (((1 / 2)โ๐) ยท (๐ด / 2))) |
47 | 46 | sumeq2dv 11378 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ (0...(๐ โ 1))(๐ด / (2โ(๐ + 1))) = ฮฃ๐ โ (0...(๐ โ 1))(((1 / 2)โ๐) ยท (๐ด / 2))) |
48 | | 0zd 9267 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ 0 โ
โค) |
49 | 3, 1 | zsubcld 9382 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ โ 1) โ
โค) |
50 | 48, 49 | fzfigd 10433 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ
(0...(๐ โ 1)) โ
Fin) |
51 | | halfcl 9147 |
. . . . . 6
โข (๐ด โ โ โ (๐ด / 2) โ
โ) |
52 | 51 | adantl 277 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ด / 2) โ
โ) |
53 | 50, 52, 24 | fsummulc1 11459 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ
(ฮฃ๐ โ
(0...(๐ โ 1))((1 /
2)โ๐) ยท (๐ด / 2)) = ฮฃ๐ โ (0...(๐ โ 1))(((1 / 2)โ๐) ยท (๐ด / 2))) |
54 | 47, 53 | eqtr4d 2213 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ (0...(๐ โ 1))(๐ด / (2โ(๐ + 1))) = (ฮฃ๐ โ (0...(๐ โ 1))((1 / 2)โ๐) ยท (๐ด / 2))) |
55 | 19, 54 | eqtrid 2222 |
. 2
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ ((1 โ
1)...(๐ โ 1))(๐ด / (2โ(๐ + 1))) = (ฮฃ๐ โ (0...(๐ โ 1))((1 / 2)โ๐) ยท (๐ด / 2))) |
56 | | 2cnd 8994 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ) โ 2 โ
โ) |
57 | 26 | a1i 9 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ) โ 2 #
0) |
58 | 56, 57, 3 | exprecapd 10664 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โ) โ ((1 /
2)โ๐) = (1 /
(2โ๐))) |
59 | 58 | oveq2d 5893 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1
โ ((1 / 2)โ๐)) =
(1 โ (1 / (2โ๐)))) |
60 | | 1mhlfehlf 9139 |
. . . . . . 7
โข (1
โ (1 / 2)) = (1 / 2) |
61 | 60 | a1i 9 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1
โ (1 / 2)) = (1 / 2)) |
62 | 59, 61 | oveq12d 5895 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ ((1
โ ((1 / 2)โ๐)) /
(1 โ (1 / 2))) = ((1 โ (1 / (2โ๐))) / (1 / 2))) |
63 | | simpr 110 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ ๐ด โ
โ) |
64 | 63, 56, 57 | divrecap2d 8753 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ด / 2) = ((1 / 2) ยท ๐ด)) |
65 | 62, 64 | oveq12d 5895 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ (((1
โ ((1 / 2)โ๐)) /
(1 โ (1 / 2))) ยท (๐ด / 2)) = (((1 โ (1 / (2โ๐))) / (1 / 2)) ยท ((1 / 2)
ยท ๐ด))) |
66 | | ax-1cn 7906 |
. . . . . . 7
โข 1 โ
โ |
67 | | nnnn0 9185 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ0) |
68 | 67 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ด โ โ) โ ๐ โ
โ0) |
69 | | nnexpcl 10535 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
70 | 5, 68, 69 | sylancr 414 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โ) โ
(2โ๐) โ
โ) |
71 | 70 | nnrecred 8968 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ) โ (1 /
(2โ๐)) โ
โ) |
72 | 71 | recnd 7988 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โ) โ (1 /
(2โ๐)) โ
โ) |
73 | | subcl 8158 |
. . . . . . 7
โข ((1
โ โ โง (1 / (2โ๐)) โ โ) โ (1 โ (1 /
(2โ๐))) โ
โ) |
74 | 66, 72, 73 | sylancr 414 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1
โ (1 / (2โ๐)))
โ โ) |
75 | 20 | a1i 9 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1 / 2)
โ โ) |
76 | 56, 57 | recap0d 8741 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1 / 2)
# 0) |
77 | 74, 75, 76 | divclapd 8749 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ ((1
โ (1 / (2โ๐))) /
(1 / 2)) โ โ) |
78 | 77, 75, 63 | mulassd 7983 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ ((((1
โ (1 / (2โ๐))) /
(1 / 2)) ยท (1 / 2)) ยท ๐ด) = (((1 โ (1 / (2โ๐))) / (1 / 2)) ยท ((1 / 2)
ยท ๐ด))) |
79 | 74, 75, 76 | divcanap1d 8750 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ (((1
โ (1 / (2โ๐))) /
(1 / 2)) ยท (1 / 2)) = (1 โ (1 / (2โ๐)))) |
80 | 79 | oveq1d 5892 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ ((((1
โ (1 / (2โ๐))) /
(1 / 2)) ยท (1 / 2)) ยท ๐ด) = ((1 โ (1 / (2โ๐))) ยท ๐ด)) |
81 | 65, 78, 80 | 3eqtr2d 2216 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ (((1
โ ((1 / 2)โ๐)) /
(1 โ (1 / 2))) ยท (๐ด / 2)) = ((1 โ (1 / (2โ๐))) ยท ๐ด)) |
82 | | halfre 9134 |
. . . . . . 7
โข (1 / 2)
โ โ |
83 | | 1re 7958 |
. . . . . . 7
โข 1 โ
โ |
84 | | halflt1 9138 |
. . . . . . 7
โข (1 / 2)
< 1 |
85 | 82, 83, 84 | ltapii 8594 |
. . . . . 6
โข (1 / 2) #
1 |
86 | 85 | a1i 9 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ (1 / 2)
# 1) |
87 | 75, 86, 68 | geoserap 11517 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ (0...(๐ โ 1))((1 / 2)โ๐) = ((1 โ ((1 /
2)โ๐)) / (1 โ (1
/ 2)))) |
88 | 87 | oveq1d 5892 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ
(ฮฃ๐ โ
(0...(๐ โ 1))((1 /
2)โ๐) ยท (๐ด / 2)) = (((1 โ ((1 /
2)โ๐)) / (1 โ (1
/ 2))) ยท (๐ด /
2))) |
89 | | mullid 7957 |
. . . . . . 7
โข (๐ด โ โ โ (1
ยท ๐ด) = ๐ด) |
90 | 89 | adantl 277 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (1
ยท ๐ด) = ๐ด) |
91 | 90 | eqcomd 2183 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ ๐ด = (1 ยท ๐ด)) |
92 | 70 | nncnd 8935 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ
(2โ๐) โ
โ) |
93 | 70 | nnap0d 8967 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ
(2โ๐) #
0) |
94 | 63, 92, 93 | divrecap2d 8753 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ด / (2โ๐)) = ((1 / (2โ๐)) ยท ๐ด)) |
95 | 91, 94 | oveq12d 5895 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ด โ (๐ด / (2โ๐))) = ((1 ยท ๐ด) โ ((1 / (2โ๐)) ยท ๐ด))) |
96 | 66 | a1i 9 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ 1 โ
โ) |
97 | 96, 72, 63 | subdird 8374 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ ((1
โ (1 / (2โ๐)))
ยท ๐ด) = ((1 ยท
๐ด) โ ((1 /
(2โ๐)) ยท ๐ด))) |
98 | 95, 97 | eqtr4d 2213 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ด โ (๐ด / (2โ๐))) = ((1 โ (1 / (2โ๐))) ยท ๐ด)) |
99 | 81, 88, 98 | 3eqtr4d 2220 |
. 2
โข ((๐ โ โ โง ๐ด โ โ) โ
(ฮฃ๐ โ
(0...(๐ โ 1))((1 /
2)โ๐) ยท (๐ด / 2)) = (๐ด โ (๐ด / (2โ๐)))) |
100 | 16, 55, 99 | 3eqtrd 2214 |
1
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ (1...๐)(๐ด / (2โ๐)) = (๐ด โ (๐ด / (2โ๐)))) |