Step | Hyp | Ref
| Expression |
1 | | eqidd 2178 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ1))
โ (๐บโ๐) = (๐บโ๐)) |
2 | | cvgcmp2nlemabs.m |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
3 | | cvgcmp2nlemabs.n |
. . . . . . . . . 10
โข (๐ โ ๐ โ (โคโฅโ๐)) |
4 | | eluznn 9602 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ) |
5 | 2, 3, 4 | syl2anc 411 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
6 | | elnnuz 9566 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
7 | 5, 6 | sylib 122 |
. . . . . . . 8
โข (๐ โ ๐ โ
(โคโฅโ1)) |
8 | | elnnuz 9566 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
9 | | cvgcmp2n.cl |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (๐บโ๐) โ โ) |
10 | 9 | recnd 7988 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (๐บโ๐) โ โ) |
11 | 8, 10 | sylan2br 288 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ1))
โ (๐บโ๐) โ
โ) |
12 | 1, 7, 11 | fsum3ser 11407 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ (1...๐)(๐บโ๐) = (seq1( + , ๐บ)โ๐)) |
13 | | nnuz 9565 |
. . . . . . . . 9
โข โ =
(โคโฅโ1) |
14 | 2, 13 | eleqtrdi 2270 |
. . . . . . . 8
โข (๐ โ ๐ โ
(โคโฅโ1)) |
15 | 1, 14, 11 | fsum3ser 11407 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ (1...๐)(๐บโ๐) = (seq1( + , ๐บ)โ๐)) |
16 | 12, 15 | oveq12d 5895 |
. . . . . 6
โข (๐ โ (ฮฃ๐ โ (1...๐)(๐บโ๐) โ ฮฃ๐ โ (1...๐)(๐บโ๐)) = ((seq1( + , ๐บ)โ๐) โ (seq1( + , ๐บ)โ๐))) |
17 | 2 | nnred 8934 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
18 | 17 | ltp1d 8889 |
. . . . . . . . . 10
โข (๐ โ ๐ < (๐ + 1)) |
19 | | fzdisj 10054 |
. . . . . . . . . 10
โข (๐ < (๐ + 1) โ ((1...๐) โฉ ((๐ + 1)...๐)) = โ
) |
20 | 18, 19 | syl 14 |
. . . . . . . . 9
โข (๐ โ ((1...๐) โฉ ((๐ + 1)...๐)) = โ
) |
21 | | eluzle 9542 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ๐) โ ๐ โค ๐) |
22 | 3, 21 | syl 14 |
. . . . . . . . . . 11
โข (๐ โ ๐ โค ๐) |
23 | | elfz1b 10092 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ (๐ โ โ โง ๐ โ โ โง ๐ โค ๐)) |
24 | 2, 5, 22, 23 | syl3anbrc 1181 |
. . . . . . . . . 10
โข (๐ โ ๐ โ (1...๐)) |
25 | | fzsplit 10053 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ (1...๐) = ((1...๐) โช ((๐ + 1)...๐))) |
26 | 24, 25 | syl 14 |
. . . . . . . . 9
โข (๐ โ (1...๐) = ((1...๐) โช ((๐ + 1)...๐))) |
27 | | 1zzd 9282 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โค) |
28 | 5 | nnzd 9376 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โค) |
29 | 27, 28 | fzfigd 10433 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ Fin) |
30 | | elfznn 10056 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ ๐ โ โ) |
31 | 30, 10 | sylan2 286 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...๐)) โ (๐บโ๐) โ โ) |
32 | 20, 26, 29, 31 | fsumsplit 11417 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (1...๐)(๐บโ๐) = (ฮฃ๐ โ (1...๐)(๐บโ๐) + ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐))) |
33 | 32 | eqcomd 2183 |
. . . . . . 7
โข (๐ โ (ฮฃ๐ โ (1...๐)(๐บโ๐) + ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐)) = ฮฃ๐ โ (1...๐)(๐บโ๐)) |
34 | 29, 31 | fsumcl 11410 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (1...๐)(๐บโ๐) โ โ) |
35 | 2 | nnzd 9376 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โค) |
36 | 27, 35 | fzfigd 10433 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ Fin) |
37 | | elfznn 10056 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ ๐ โ โ) |
38 | 37, 10 | sylan2 286 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...๐)) โ (๐บโ๐) โ โ) |
39 | 36, 38 | fsumcl 11410 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (1...๐)(๐บโ๐) โ โ) |
40 | 35 | peano2zd 9380 |
. . . . . . . . . 10
โข (๐ โ (๐ + 1) โ โค) |
41 | 40, 28 | fzfigd 10433 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1)...๐) โ Fin) |
42 | 2 | peano2nnd 8936 |
. . . . . . . . . . 11
โข (๐ โ (๐ + 1) โ โ) |
43 | | elfzuz 10023 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + 1)...๐) โ ๐ โ (โคโฅโ(๐ + 1))) |
44 | | eluznn 9602 |
. . . . . . . . . . 11
โข (((๐ + 1) โ โ โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โ) |
45 | 42, 43, 44 | syl2an 289 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ ๐ โ โ) |
46 | 45, 10 | syldan 282 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ (๐บโ๐) โ โ) |
47 | 41, 46 | fsumcl 11410 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐) โ โ) |
48 | 34, 39, 47 | subaddd 8288 |
. . . . . . 7
โข (๐ โ ((ฮฃ๐ โ (1...๐)(๐บโ๐) โ ฮฃ๐ โ (1...๐)(๐บโ๐)) = ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐) โ (ฮฃ๐ โ (1...๐)(๐บโ๐) + ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐)) = ฮฃ๐ โ (1...๐)(๐บโ๐))) |
49 | 33, 48 | mpbird 167 |
. . . . . 6
โข (๐ โ (ฮฃ๐ โ (1...๐)(๐บโ๐) โ ฮฃ๐ โ (1...๐)(๐บโ๐)) = ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐)) |
50 | 16, 49 | eqtr3d 2212 |
. . . . 5
โข (๐ โ ((seq1( + , ๐บ)โ๐) โ (seq1( + , ๐บ)โ๐)) = ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐)) |
51 | 45, 9 | syldan 282 |
. . . . . 6
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ (๐บโ๐) โ โ) |
52 | 41, 51 | fsumrecl 11411 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐) โ โ) |
53 | 50, 52 | eqeltrd 2254 |
. . . 4
โข (๐ โ ((seq1( + , ๐บ)โ๐) โ (seq1( + , ๐บ)โ๐)) โ โ) |
54 | 42 | nnzd 9376 |
. . . . . . 7
โข (๐ โ (๐ + 1) โ โค) |
55 | 54, 28 | fzfigd 10433 |
. . . . . 6
โข (๐ โ ((๐ + 1)...๐) โ Fin) |
56 | | cvgcmp2n.ge0 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ 0 โค (๐บโ๐)) |
57 | 45, 56 | syldan 282 |
. . . . . 6
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ 0 โค (๐บโ๐)) |
58 | 55, 51, 57 | fsumge0 11469 |
. . . . 5
โข (๐ โ 0 โค ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐)) |
59 | 58, 50 | breqtrrd 4033 |
. . . 4
โข (๐ โ 0 โค ((seq1( + , ๐บ)โ๐) โ (seq1( + , ๐บ)โ๐))) |
60 | 53, 59 | absidd 11178 |
. . 3
โข (๐ โ (absโ((seq1( + ,
๐บ)โ๐) โ (seq1( + , ๐บ)โ๐))) = ((seq1( + , ๐บ)โ๐) โ (seq1( + , ๐บ)โ๐))) |
61 | 60, 50 | eqtrd 2210 |
. 2
โข (๐ โ (absโ((seq1( + ,
๐บ)โ๐) โ (seq1( + , ๐บ)โ๐))) = ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐)) |
62 | | halfre 9134 |
. . . . . . 7
โข (1 / 2)
โ โ |
63 | 62 | a1i 9 |
. . . . . 6
โข (๐ โ (1 / 2) โ
โ) |
64 | 42 | nnnn0d 9231 |
. . . . . 6
โข (๐ โ (๐ + 1) โ
โ0) |
65 | 63, 64 | reexpcld 10673 |
. . . . 5
โข (๐ โ ((1 / 2)โ(๐ + 1)) โ
โ) |
66 | 5 | peano2nnd 8936 |
. . . . . . 7
โข (๐ โ (๐ + 1) โ โ) |
67 | 66 | nnnn0d 9231 |
. . . . . 6
โข (๐ โ (๐ + 1) โ
โ0) |
68 | 63, 67 | reexpcld 10673 |
. . . . 5
โข (๐ โ ((1 / 2)โ(๐ + 1)) โ
โ) |
69 | 65, 68 | resubcld 8340 |
. . . 4
โข (๐ โ (((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) โ
โ) |
70 | | 1mhlfehlf 9139 |
. . . . . 6
โข (1
โ (1 / 2)) = (1 / 2) |
71 | | 2rp 9660 |
. . . . . . 7
โข 2 โ
โ+ |
72 | | rpreccl 9682 |
. . . . . . 7
โข (2 โ
โ+ โ (1 / 2) โ โ+) |
73 | 71, 72 | ax-mp 5 |
. . . . . 6
โข (1 / 2)
โ โ+ |
74 | 70, 73 | eqeltri 2250 |
. . . . 5
โข (1
โ (1 / 2)) โ โ+ |
75 | 74 | a1i 9 |
. . . 4
โข (๐ โ (1 โ (1 / 2)) โ
โ+) |
76 | 69, 75 | rerpdivcld 9730 |
. . 3
โข (๐ โ ((((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) / (1
โ (1 / 2))) โ โ) |
77 | 71 | a1i 9 |
. . . . 5
โข (๐ โ 2 โ
โ+) |
78 | 2 | nnrpd 9696 |
. . . . 5
โข (๐ โ ๐ โ
โ+) |
79 | 77, 78 | rpdivcld 9716 |
. . . 4
โข (๐ โ (2 / ๐) โ
โ+) |
80 | 79 | rpred 9698 |
. . 3
โข (๐ โ (2 / ๐) โ โ) |
81 | 71 | a1i 9 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ 2 โ
โ+) |
82 | 45 | nnzd 9376 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ ๐ โ โค) |
83 | 81, 82 | rpexpcld 10680 |
. . . . . . . 8
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ (2โ๐) โ
โ+) |
84 | 83 | rprecred 9710 |
. . . . . . 7
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ (1 / (2โ๐)) โ โ) |
85 | | cvgcmp2n.lt |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (๐บโ๐) โค (1 / (2โ๐))) |
86 | 45, 85 | syldan 282 |
. . . . . . 7
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ (๐บโ๐) โค (1 / (2โ๐))) |
87 | 41, 51, 84, 86 | fsumle 11473 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐) โค ฮฃ๐ โ ((๐ + 1)...๐)(1 / (2โ๐))) |
88 | | 2cnd 8994 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ 2 โ โ) |
89 | 81 | rpap0d 9704 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ 2 # 0) |
90 | 88, 89, 82 | exprecapd 10664 |
. . . . . . . 8
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ ((1 / 2)โ๐) = (1 / (2โ๐))) |
91 | 90 | eqcomd 2183 |
. . . . . . 7
โข ((๐ โง ๐ โ ((๐ + 1)...๐)) โ (1 / (2โ๐)) = ((1 / 2)โ๐)) |
92 | 91 | sumeq2dv 11378 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ ((๐ + 1)...๐)(1 / (2โ๐)) = ฮฃ๐ โ ((๐ + 1)...๐)((1 / 2)โ๐)) |
93 | 87, 92 | breqtrd 4031 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐) โค ฮฃ๐ โ ((๐ + 1)...๐)((1 / 2)โ๐)) |
94 | | fzval3 10206 |
. . . . . . 7
โข (๐ โ โค โ ((๐ + 1)...๐) = ((๐ + 1)..^(๐ + 1))) |
95 | 28, 94 | syl 14 |
. . . . . 6
โข (๐ โ ((๐ + 1)...๐) = ((๐ + 1)..^(๐ + 1))) |
96 | 95 | sumeq1d 11376 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ((๐ + 1)...๐)((1 / 2)โ๐) = ฮฃ๐ โ ((๐ + 1)..^(๐ + 1))((1 / 2)โ๐)) |
97 | 93, 96 | breqtrd 4031 |
. . . 4
โข (๐ โ ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐) โค ฮฃ๐ โ ((๐ + 1)..^(๐ + 1))((1 / 2)โ๐)) |
98 | | halfcn 9135 |
. . . . . 6
โข (1 / 2)
โ โ |
99 | 98 | a1i 9 |
. . . . 5
โข (๐ โ (1 / 2) โ
โ) |
100 | | 1re 7958 |
. . . . . . 7
โข 1 โ
โ |
101 | | halflt1 9138 |
. . . . . . 7
โข (1 / 2)
< 1 |
102 | 62, 100, 101 | ltapii 8594 |
. . . . . 6
โข (1 / 2) #
1 |
103 | 102 | a1i 9 |
. . . . 5
โข (๐ โ (1 / 2) #
1) |
104 | | eluzp1p1 9555 |
. . . . . 6
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ
(โคโฅโ(๐ + 1))) |
105 | 3, 104 | syl 14 |
. . . . 5
โข (๐ โ (๐ + 1) โ
(โคโฅโ(๐ + 1))) |
106 | 99, 103, 64, 105 | geosergap 11516 |
. . . 4
โข (๐ โ ฮฃ๐ โ ((๐ + 1)..^(๐ + 1))((1 / 2)โ๐) = ((((1 / 2)โ(๐ + 1)) โ ((1 / 2)โ(๐ + 1))) / (1 โ (1 /
2)))) |
107 | 97, 106 | breqtrd 4031 |
. . 3
โข (๐ โ ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐) โค ((((1 / 2)โ(๐ + 1)) โ ((1 / 2)โ(๐ + 1))) / (1 โ (1 /
2)))) |
108 | 73 | a1i 9 |
. . . . . . . 8
โข (๐ โ (1 / 2) โ
โ+) |
109 | 28 | peano2zd 9380 |
. . . . . . . 8
โข (๐ โ (๐ + 1) โ โค) |
110 | 108, 109 | rpexpcld 10680 |
. . . . . . 7
โข (๐ โ ((1 / 2)โ(๐ + 1)) โ
โ+) |
111 | 110 | rpred 9698 |
. . . . . 6
โข (๐ โ ((1 / 2)โ(๐ + 1)) โ
โ) |
112 | 65, 111 | resubcld 8340 |
. . . . 5
โข (๐ โ (((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) โ
โ) |
113 | 2 | nnrecred 8968 |
. . . . 5
โข (๐ โ (1 / ๐) โ โ) |
114 | 65, 110 | ltsubrpd 9731 |
. . . . . 6
โข (๐ โ (((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) < ((1
/ 2)โ(๐ +
1))) |
115 | | 2cnd 8994 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
116 | 77 | rpap0d 9704 |
. . . . . . . 8
โข (๐ โ 2 # 0) |
117 | 115, 116,
40 | exprecapd 10664 |
. . . . . . 7
โข (๐ โ ((1 / 2)โ(๐ + 1)) = (1 / (2โ(๐ + 1)))) |
118 | 42 | nnred 8934 |
. . . . . . . . 9
โข (๐ โ (๐ + 1) โ โ) |
119 | 77, 40 | rpexpcld 10680 |
. . . . . . . . . 10
โข (๐ โ (2โ(๐ + 1)) โ
โ+) |
120 | 119 | rpred 9698 |
. . . . . . . . 9
โข (๐ โ (2โ(๐ + 1)) โ โ) |
121 | | 2z 9283 |
. . . . . . . . . . . 12
โข 2 โ
โค |
122 | | uzid 9544 |
. . . . . . . . . . . 12
โข (2 โ
โค โ 2 โ (โคโฅโ2)) |
123 | 121, 122 | ax-mp 5 |
. . . . . . . . . . 11
โข 2 โ
(โคโฅโ2) |
124 | 123 | a1i 9 |
. . . . . . . . . 10
โข (๐ โ 2 โ
(โคโฅโ2)) |
125 | | bernneq3 10645 |
. . . . . . . . . 10
โข ((2
โ (โคโฅโ2) โง (๐ + 1) โ โ0) โ
(๐ + 1) < (2โ(๐ + 1))) |
126 | 124, 64, 125 | syl2anc 411 |
. . . . . . . . 9
โข (๐ โ (๐ + 1) < (2โ(๐ + 1))) |
127 | 17, 118, 120, 18, 126 | lttrd 8085 |
. . . . . . . 8
โข (๐ โ ๐ < (2โ(๐ + 1))) |
128 | 78, 119 | ltrecd 9717 |
. . . . . . . 8
โข (๐ โ (๐ < (2โ(๐ + 1)) โ (1 / (2โ(๐ + 1))) < (1 / ๐))) |
129 | 127, 128 | mpbid 147 |
. . . . . . 7
โข (๐ โ (1 / (2โ(๐ + 1))) < (1 / ๐)) |
130 | 117, 129 | eqbrtrd 4027 |
. . . . . 6
โข (๐ โ ((1 / 2)โ(๐ + 1)) < (1 / ๐)) |
131 | 112, 65, 113, 114, 130 | lttrd 8085 |
. . . . 5
โข (๐ โ (((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) < (1 /
๐)) |
132 | 112, 113,
77, 131 | ltmul1dd 9754 |
. . . 4
โข (๐ โ ((((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) ยท
2) < ((1 / ๐) ยท
2)) |
133 | 70 | oveq2i 5888 |
. . . . . 6
โข ((((1 /
2)โ(๐ + 1)) โ
((1 / 2)โ(๐ + 1))) /
(1 โ (1 / 2))) = ((((1 / 2)โ(๐ + 1)) โ ((1 / 2)โ(๐ + 1))) / (1 /
2)) |
134 | 112 | recnd 7988 |
. . . . . . 7
โข (๐ โ (((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) โ
โ) |
135 | | 1cnd 7975 |
. . . . . . 7
โข (๐ โ 1 โ
โ) |
136 | | 1ap0 8549 |
. . . . . . . 8
โข 1 #
0 |
137 | 136 | a1i 9 |
. . . . . . 7
โข (๐ โ 1 # 0) |
138 | 134, 135,
115, 137, 116 | divdivap2d 8782 |
. . . . . 6
โข (๐ โ ((((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) / (1 /
2)) = (((((1 / 2)โ(๐ +
1)) โ ((1 / 2)โ(๐ + 1))) ยท 2) / 1)) |
139 | 133, 138 | eqtrid 2222 |
. . . . 5
โข (๐ โ ((((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) / (1
โ (1 / 2))) = (((((1 / 2)โ(๐ + 1)) โ ((1 / 2)โ(๐ + 1))) ยท 2) /
1)) |
140 | 134, 115 | mulcld 7980 |
. . . . . 6
โข (๐ โ ((((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) ยท
2) โ โ) |
141 | 140 | div1d 8739 |
. . . . 5
โข (๐ โ (((((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) ยท
2) / 1) = ((((1 / 2)โ(๐ + 1)) โ ((1 / 2)โ(๐ + 1))) ยท
2)) |
142 | 139, 141 | eqtrd 2210 |
. . . 4
โข (๐ โ ((((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) / (1
โ (1 / 2))) = ((((1 / 2)โ(๐ + 1)) โ ((1 / 2)โ(๐ + 1))) ยท
2)) |
143 | 17 | recnd 7988 |
. . . . 5
โข (๐ โ ๐ โ โ) |
144 | 2 | nnap0d 8967 |
. . . . 5
โข (๐ โ ๐ # 0) |
145 | 115, 143,
144 | divrecap2d 8753 |
. . . 4
โข (๐ โ (2 / ๐) = ((1 / ๐) ยท 2)) |
146 | 132, 142,
145 | 3brtr4d 4037 |
. . 3
โข (๐ โ ((((1 / 2)โ(๐ + 1)) โ ((1 /
2)โ(๐ + 1))) / (1
โ (1 / 2))) < (2 / ๐)) |
147 | 52, 76, 80, 107, 146 | lelttrd 8084 |
. 2
โข (๐ โ ฮฃ๐ โ ((๐ + 1)...๐)(๐บโ๐) < (2 / ๐)) |
148 | 61, 147 | eqbrtrd 4027 |
1
โข (๐ โ (absโ((seq1( + ,
๐บ)โ๐) โ (seq1( + , ๐บ)โ๐))) < (2 / ๐)) |