Step | Hyp | Ref
| Expression |
1 | | nnuz 9562 |
. . 3
โข โ =
(โคโฅโ1) |
2 | | 1zzd 9279 |
. . 3
โข (๐ด โ โ โ 1 โ
โค) |
3 | | halfcn 9132 |
. . . . . . 7
โข (1 / 2)
โ โ |
4 | 3 | a1i 9 |
. . . . . 6
โข (๐ด โ โ โ (1 / 2)
โ โ) |
5 | | halfre 9131 |
. . . . . . . . 9
โข (1 / 2)
โ โ |
6 | | halfge0 9134 |
. . . . . . . . 9
โข 0 โค (1
/ 2) |
7 | | absid 11079 |
. . . . . . . . 9
โข (((1 / 2)
โ โ โง 0 โค (1 / 2)) โ (absโ(1 / 2)) = (1 /
2)) |
8 | 5, 6, 7 | mp2an 426 |
. . . . . . . 8
โข
(absโ(1 / 2)) = (1 / 2) |
9 | | halflt1 9135 |
. . . . . . . 8
โข (1 / 2)
< 1 |
10 | 8, 9 | eqbrtri 4024 |
. . . . . . 7
โข
(absโ(1 / 2)) < 1 |
11 | 10 | a1i 9 |
. . . . . 6
โข (๐ด โ โ โ
(absโ(1 / 2)) < 1) |
12 | 4, 11 | expcnv 11511 |
. . . . 5
โข (๐ด โ โ โ (๐ โ โ0
โฆ ((1 / 2)โ๐))
โ 0) |
13 | | id 19 |
. . . . 5
โข (๐ด โ โ โ ๐ด โ
โ) |
14 | | geo2lim.1 |
. . . . . . 7
โข ๐น = (๐ โ โ โฆ (๐ด / (2โ๐))) |
15 | | nnex 8924 |
. . . . . . . 8
โข โ
โ V |
16 | 15 | mptex 5742 |
. . . . . . 7
โข (๐ โ โ โฆ (๐ด / (2โ๐))) โ V |
17 | 14, 16 | eqeltri 2250 |
. . . . . 6
โข ๐น โ V |
18 | 17 | a1i 9 |
. . . . 5
โข (๐ด โ โ โ ๐น โ V) |
19 | | nnnn0 9182 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ0) |
20 | 19 | adantl 277 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ0) |
21 | 3 | a1i 9 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ (1 / 2)
โ โ) |
22 | 21, 20 | expcld 10653 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ ((1 /
2)โ๐) โ
โ) |
23 | | oveq2 5882 |
. . . . . . . 8
โข (๐ = ๐ โ ((1 / 2)โ๐) = ((1 / 2)โ๐)) |
24 | | eqid 2177 |
. . . . . . . 8
โข (๐ โ โ0
โฆ ((1 / 2)โ๐)) =
(๐ โ
โ0 โฆ ((1 / 2)โ๐)) |
25 | 23, 24 | fvmptg 5592 |
. . . . . . 7
โข ((๐ โ โ0
โง ((1 / 2)โ๐)
โ โ) โ ((๐
โ โ0 โฆ ((1 / 2)โ๐))โ๐) = ((1 / 2)โ๐)) |
26 | 20, 22, 25 | syl2anc 411 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ โ โ0
โฆ ((1 / 2)โ๐))โ๐) = ((1 / 2)โ๐)) |
27 | 26, 22 | eqeltrd 2254 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ โ โ0
โฆ ((1 / 2)โ๐))โ๐) โ โ) |
28 | | simpl 109 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ด โ
โ) |
29 | | 2nn 9079 |
. . . . . . . . 9
โข 2 โ
โ |
30 | | nnexpcl 10532 |
. . . . . . . . 9
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
31 | 29, 20, 30 | sylancr 414 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ
(2โ๐) โ
โ) |
32 | 31 | nncnd 8932 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ
(2โ๐) โ
โ) |
33 | 31 | nnap0d 8964 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ
(2โ๐) #
0) |
34 | 28, 32, 33 | divrecapd 8749 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด / (2โ๐)) = (๐ด ยท (1 / (2โ๐)))) |
35 | | simpr 110 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
36 | 28, 32, 33 | divclapd 8746 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด / (2โ๐)) โ โ) |
37 | | oveq2 5882 |
. . . . . . . . 9
โข (๐ = ๐ โ (2โ๐) = (2โ๐)) |
38 | 37 | oveq2d 5890 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ด / (2โ๐)) = (๐ด / (2โ๐))) |
39 | 38, 14 | fvmptg 5592 |
. . . . . . 7
โข ((๐ โ โ โง (๐ด / (2โ๐)) โ โ) โ (๐นโ๐) = (๐ด / (2โ๐))) |
40 | 35, 36, 39 | syl2anc 411 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ (๐นโ๐) = (๐ด / (2โ๐))) |
41 | | 2cn 8989 |
. . . . . . . . 9
โข 2 โ
โ |
42 | | 2ap0 9011 |
. . . . . . . . 9
โข 2 #
0 |
43 | | nnz 9271 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
44 | 43 | adantl 277 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โค) |
45 | | exprecap 10560 |
. . . . . . . . 9
โข ((2
โ โ โง 2 # 0 โง ๐ โ โค) โ ((1 / 2)โ๐) = (1 / (2โ๐))) |
46 | 41, 42, 44, 45 | mp3an12i 1341 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ ((1 /
2)โ๐) = (1 /
(2โ๐))) |
47 | 26, 46 | eqtrd 2210 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ โ โ0
โฆ ((1 / 2)โ๐))โ๐) = (1 / (2โ๐))) |
48 | 47 | oveq2d 5890 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด ยท ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐)) = (๐ด ยท (1 / (2โ๐)))) |
49 | 34, 40, 48 | 3eqtr4d 2220 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ (๐นโ๐) = (๐ด ยท ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐))) |
50 | 1, 2, 12, 13, 18, 27, 49 | climmulc2 11338 |
. . . 4
โข (๐ด โ โ โ ๐น โ (๐ด ยท 0)) |
51 | | mul01 8345 |
. . . 4
โข (๐ด โ โ โ (๐ด ยท 0) =
0) |
52 | 50, 51 | breqtrd 4029 |
. . 3
โข (๐ด โ โ โ ๐น โ 0) |
53 | | seqex 10446 |
. . . 4
โข seq1( + ,
๐น) โ
V |
54 | 53 | a1i 9 |
. . 3
โข (๐ด โ โ โ seq1( + ,
๐น) โ
V) |
55 | 40, 36 | eqeltrd 2254 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ) โ (๐นโ๐) โ โ) |
56 | 40 | oveq2d 5890 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด โ (๐นโ๐)) = (๐ด โ (๐ด / (2โ๐)))) |
57 | | geo2sum 11521 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ) โ
ฮฃ๐ โ (1...๐)(๐ด / (2โ๐)) = (๐ด โ (๐ด / (2โ๐)))) |
58 | 57 | ancoms 268 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ) โ
ฮฃ๐ โ (1...๐)(๐ด / (2โ๐)) = (๐ด โ (๐ด / (2โ๐)))) |
59 | | elnnuz 9563 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
60 | 59 | biimpri 133 |
. . . . . . 7
โข (๐ โ
(โคโฅโ1) โ ๐ โ โ) |
61 | 60 | adantl 277 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ
(โคโฅโ1)) โ ๐ โ โ) |
62 | | simpll 527 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ
(โคโฅโ1)) โ ๐ด โ โ) |
63 | 41 | a1i 9 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ
(โคโฅโ1)) โ 2 โ โ) |
64 | 61 | nnnn0d 9228 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ
(โคโฅโ1)) โ ๐ โ โ0) |
65 | 63, 64 | expcld 10653 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ
(โคโฅโ1)) โ (2โ๐) โ โ) |
66 | 42 | a1i 9 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ
(โคโฅโ1)) โ 2 # 0) |
67 | 61 | nnzd 9373 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ
(โคโฅโ1)) โ ๐ โ โค) |
68 | 63, 66, 67 | expap0d 10659 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ
(โคโฅโ1)) โ (2โ๐) # 0) |
69 | 62, 65, 68 | divclapd 8746 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ
(โคโฅโ1)) โ (๐ด / (2โ๐)) โ โ) |
70 | | oveq2 5882 |
. . . . . . . 8
โข (๐ = ๐ โ (2โ๐) = (2โ๐)) |
71 | 70 | oveq2d 5890 |
. . . . . . 7
โข (๐ = ๐ โ (๐ด / (2โ๐)) = (๐ด / (2โ๐))) |
72 | 71, 14 | fvmptg 5592 |
. . . . . 6
โข ((๐ โ โ โง (๐ด / (2โ๐)) โ โ) โ (๐นโ๐) = (๐ด / (2โ๐))) |
73 | 61, 69, 72 | syl2anc 411 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ
(โคโฅโ1)) โ (๐นโ๐) = (๐ด / (2โ๐))) |
74 | 35, 1 | eleqtrdi 2270 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
(โคโฅโ1)) |
75 | 73, 74, 69 | fsum3ser 11404 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ) โ
ฮฃ๐ โ (1...๐)(๐ด / (2โ๐)) = (seq1( + , ๐น)โ๐)) |
76 | 56, 58, 75 | 3eqtr2rd 2217 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ) โ (seq1( +
, ๐น)โ๐) = (๐ด โ (๐นโ๐))) |
77 | 1, 2, 52, 13, 54, 55, 76 | climsubc2 11340 |
. 2
โข (๐ด โ โ โ seq1( + ,
๐น) โ (๐ด โ 0)) |
78 | | subid1 8176 |
. 2
โข (๐ด โ โ โ (๐ด โ 0) = ๐ด) |
79 | 77, 78 | breqtrd 4029 |
1
โข (๐ด โ โ โ seq1( + ,
๐น) โ ๐ด) |