Step | Hyp | Ref
| Expression |
1 | | nnuz 12811 |
. 2
โข โ =
(โคโฅโ1) |
2 | | 1zzd 12539 |
. 2
โข (๐ โ โ โ 1 โ
โค) |
3 | | stirlinglem10.1 |
. . 3
โข ๐ด = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
4 | | stirlinglem10.2 |
. . 3
โข ๐ต = (๐ โ โ โฆ (logโ(๐ดโ๐))) |
5 | | eqid 2733 |
. . 3
โข (๐ โ โ โฆ ((((1 +
(2 ยท ๐)) / 2)
ยท (logโ((๐ +
1) / ๐))) โ 1)) =
(๐ โ โ โฆ
((((1 + (2 ยท ๐)) /
2) ยท (logโ((๐
+ 1) / ๐))) โ
1)) |
6 | | stirlinglem10.4 |
. . 3
โข ๐พ = (๐ โ โ โฆ ((1 / ((2 ยท
๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ(2
ยท ๐)))) |
7 | 3, 4, 5, 6 | stirlinglem9 44409 |
. 2
โข (๐ โ โ โ seq1( + ,
๐พ) โ ((๐ตโ๐) โ (๐ตโ(๐ + 1)))) |
8 | | 2cnd 12236 |
. . . . . . . 8
โข (๐ โ โ โ 2 โ
โ) |
9 | | nncn 12166 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
10 | 8, 9 | mulcld 11180 |
. . . . . . 7
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
11 | | 1cnd 11155 |
. . . . . . 7
โข (๐ โ โ โ 1 โ
โ) |
12 | 10, 11 | addcld 11179 |
. . . . . 6
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
13 | 12 | sqcld 14055 |
. . . . 5
โข (๐ โ โ โ (((2
ยท ๐) + 1)โ2)
โ โ) |
14 | | 0red 11163 |
. . . . . . . 8
โข (๐ โ โ โ 0 โ
โ) |
15 | | 1red 11161 |
. . . . . . . 8
โข (๐ โ โ โ 1 โ
โ) |
16 | | 2re 12232 |
. . . . . . . . . . 11
โข 2 โ
โ |
17 | 16 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ โ 2 โ
โ) |
18 | | nnre 12165 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
19 | 17, 18 | remulcld 11190 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
20 | 19, 15 | readdcld 11189 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
21 | | 0lt1 11682 |
. . . . . . . . 9
โข 0 <
1 |
22 | 21 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ 0 <
1) |
23 | | 2rp 12925 |
. . . . . . . . . . 11
โข 2 โ
โ+ |
24 | 23 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ โ 2 โ
โ+) |
25 | | nnrp 12931 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ+) |
26 | 24, 25 | rpmulcld 12978 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท ๐) โ
โ+) |
27 | 15, 26 | ltaddrp2d 12996 |
. . . . . . . 8
โข (๐ โ โ โ 1 <
((2 ยท ๐) +
1)) |
28 | 14, 15, 20, 22, 27 | lttrd 11321 |
. . . . . . 7
โข (๐ โ โ โ 0 <
((2 ยท ๐) +
1)) |
29 | 28 | gt0ne0d 11724 |
. . . . . 6
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
0) |
30 | | 2z 12540 |
. . . . . . 7
โข 2 โ
โค |
31 | 30 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ 2 โ
โค) |
32 | 12, 29, 31 | expne0d 14063 |
. . . . 5
โข (๐ โ โ โ (((2
ยท ๐) + 1)โ2)
โ 0) |
33 | 13, 32 | reccld 11929 |
. . . 4
โข (๐ โ โ โ (1 / (((2
ยท ๐) + 1)โ2))
โ โ) |
34 | 15 | renegcld 11587 |
. . . . . 6
โข (๐ โ โ โ -1 โ
โ) |
35 | 20 | resqcld 14036 |
. . . . . . 7
โข (๐ โ โ โ (((2
ยท ๐) + 1)โ2)
โ โ) |
36 | 35, 32 | rereccld 11987 |
. . . . . 6
โข (๐ โ โ โ (1 / (((2
ยท ๐) + 1)โ2))
โ โ) |
37 | | 1re 11160 |
. . . . . . . 8
โข 1 โ
โ |
38 | | lt0neg2 11667 |
. . . . . . . 8
โข (1 โ
โ โ (0 < 1 โ -1 < 0)) |
39 | 37, 38 | ax-mp 5 |
. . . . . . 7
โข (0 < 1
โ -1 < 0) |
40 | 22, 39 | sylib 217 |
. . . . . 6
โข (๐ โ โ โ -1 <
0) |
41 | 20, 29 | sqgt0d 14159 |
. . . . . . 7
โข (๐ โ โ โ 0 <
(((2 ยท ๐) +
1)โ2)) |
42 | 35, 41 | recgt0d 12094 |
. . . . . 6
โข (๐ โ โ โ 0 < (1
/ (((2 ยท ๐) +
1)โ2))) |
43 | 34, 14, 36, 40, 42 | lttrd 11321 |
. . . . 5
โข (๐ โ โ โ -1 <
(1 / (((2 ยท ๐) +
1)โ2))) |
44 | | 2nn 12231 |
. . . . . . . 8
โข 2 โ
โ |
45 | 44 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 2 โ
โ) |
46 | | expgt1 14012 |
. . . . . . 7
โข ((((2
ยท ๐) + 1) โ
โ โง 2 โ โ โง 1 < ((2 ยท ๐) + 1)) โ 1 < (((2 ยท ๐) + 1)โ2)) |
47 | 20, 45, 27, 46 | syl3anc 1372 |
. . . . . 6
โข (๐ โ โ โ 1 <
(((2 ยท ๐) +
1)โ2)) |
48 | 35, 41 | elrpd 12959 |
. . . . . . 7
โข (๐ โ โ โ (((2
ยท ๐) + 1)โ2)
โ โ+) |
49 | 48 | recgt1d 12976 |
. . . . . 6
โข (๐ โ โ โ (1 <
(((2 ยท ๐) +
1)โ2) โ (1 / (((2 ยท ๐) + 1)โ2)) < 1)) |
50 | 47, 49 | mpbid 231 |
. . . . 5
โข (๐ โ โ โ (1 / (((2
ยท ๐) + 1)โ2))
< 1) |
51 | 36, 15 | absltd 15320 |
. . . . 5
โข (๐ โ โ โ
((absโ(1 / (((2 ยท ๐) + 1)โ2))) < 1 โ (-1 < (1 /
(((2 ยท ๐) +
1)โ2)) โง (1 / (((2 ยท ๐) + 1)โ2)) < 1))) |
52 | 43, 50, 51 | mpbir2and 712 |
. . . 4
โข (๐ โ โ โ
(absโ(1 / (((2 ยท ๐) + 1)โ2))) < 1) |
53 | | 1nn0 12434 |
. . . . 5
โข 1 โ
โ0 |
54 | 53 | a1i 11 |
. . . 4
โข (๐ โ โ โ 1 โ
โ0) |
55 | | stirlinglem10.5 |
. . . . . 6
โข ๐ฟ = (๐ โ โ โฆ ((1 / (((2 ยท
๐) + 1)โ2))โ๐)) |
56 | 55 | a1i 11 |
. . . . 5
โข ((๐ โ โ โง ๐ โ
(โคโฅโ1)) โ ๐ฟ = (๐ โ โ โฆ ((1 / (((2 ยท
๐) + 1)โ2))โ๐))) |
57 | | simpr 486 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ
(โคโฅโ1)) โง ๐ = ๐) โ ๐ = ๐) |
58 | 57 | oveq2d 7374 |
. . . . 5
โข (((๐ โ โ โง ๐ โ
(โคโฅโ1)) โง ๐ = ๐) โ ((1 / (((2 ยท ๐) + 1)โ2))โ๐) = ((1 / (((2 ยท ๐) + 1)โ2))โ๐)) |
59 | | elnnuz 12812 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
60 | 59 | biimpri 227 |
. . . . . 6
โข (๐ โ
(โคโฅโ1) โ ๐ โ โ) |
61 | 60 | adantl 483 |
. . . . 5
โข ((๐ โ โ โง ๐ โ
(โคโฅโ1)) โ ๐ โ โ) |
62 | 33 | adantr 482 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ
(โคโฅโ1)) โ (1 / (((2 ยท ๐) + 1)โ2)) โ
โ) |
63 | 61 | nnnn0d 12478 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ
(โคโฅโ1)) โ ๐ โ โ0) |
64 | 62, 63 | expcld 14057 |
. . . . 5
โข ((๐ โ โ โง ๐ โ
(โคโฅโ1)) โ ((1 / (((2 ยท ๐) + 1)โ2))โ๐) โ โ) |
65 | 56, 58, 61, 64 | fvmptd 6956 |
. . . 4
โข ((๐ โ โ โง ๐ โ
(โคโฅโ1)) โ (๐ฟโ๐) = ((1 / (((2 ยท ๐) + 1)โ2))โ๐)) |
66 | 33, 52, 54, 65 | geolim2 15761 |
. . 3
โข (๐ โ โ โ seq1( + ,
๐ฟ) โ (((1 / (((2
ยท ๐) +
1)โ2))โ1) / (1 โ (1 / (((2 ยท ๐) + 1)โ2))))) |
67 | 33 | exp1d 14052 |
. . . . 5
โข (๐ โ โ โ ((1 /
(((2 ยท ๐) +
1)โ2))โ1) = (1 / (((2 ยท ๐) + 1)โ2))) |
68 | 13, 32 | dividd 11934 |
. . . . . . . 8
โข (๐ โ โ โ ((((2
ยท ๐) + 1)โ2) /
(((2 ยท ๐) +
1)โ2)) = 1) |
69 | 68 | eqcomd 2739 |
. . . . . . 7
โข (๐ โ โ โ 1 = ((((2
ยท ๐) + 1)โ2) /
(((2 ยท ๐) +
1)โ2))) |
70 | 69 | oveq1d 7373 |
. . . . . 6
โข (๐ โ โ โ (1
โ (1 / (((2 ยท ๐) + 1)โ2))) = (((((2 ยท ๐) + 1)โ2) / (((2 ยท
๐) + 1)โ2)) โ (1
/ (((2 ยท ๐) +
1)โ2)))) |
71 | 48 | rpcnne0d 12971 |
. . . . . . 7
โข (๐ โ โ โ ((((2
ยท ๐) + 1)โ2)
โ โ โง (((2 ยท ๐) + 1)โ2) โ 0)) |
72 | | divsubdir 11854 |
. . . . . . 7
โข (((((2
ยท ๐) + 1)โ2)
โ โ โง 1 โ โ โง ((((2 ยท ๐) + 1)โ2) โ โ โง (((2
ยท ๐) + 1)โ2)
โ 0)) โ (((((2 ยท ๐) + 1)โ2) โ 1) / (((2 ยท
๐) + 1)โ2)) = (((((2
ยท ๐) + 1)โ2) /
(((2 ยท ๐) +
1)โ2)) โ (1 / (((2 ยท ๐) + 1)โ2)))) |
73 | 13, 11, 71, 72 | syl3anc 1372 |
. . . . . 6
โข (๐ โ โ โ (((((2
ยท ๐) + 1)โ2)
โ 1) / (((2 ยท ๐) + 1)โ2)) = (((((2 ยท ๐) + 1)โ2) / (((2 ยท
๐) + 1)โ2)) โ (1
/ (((2 ยท ๐) +
1)โ2)))) |
74 | | ax-1cn 11114 |
. . . . . . . . . 10
โข 1 โ
โ |
75 | | binom2 14127 |
. . . . . . . . . 10
โข (((2
ยท ๐) โ โ
โง 1 โ โ) โ (((2 ยท ๐) + 1)โ2) = ((((2 ยท ๐)โ2) + (2 ยท ((2
ยท ๐) ยท 1))) +
(1โ2))) |
76 | 10, 74, 75 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ โ โ (((2
ยท ๐) + 1)โ2) =
((((2 ยท ๐)โ2) +
(2 ยท ((2 ยท ๐)
ยท 1))) + (1โ2))) |
77 | 76 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ โ โ ((((2
ยท ๐) + 1)โ2)
โ 1) = (((((2 ยท ๐)โ2) + (2 ยท ((2 ยท ๐) ยท 1))) + (1โ2))
โ 1)) |
78 | 8, 9 | sqmuld 14069 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((2
ยท ๐)โ2) =
((2โ2) ยท (๐โ2))) |
79 | | sq2 14107 |
. . . . . . . . . . . . . . 15
โข
(2โ2) = 4 |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(2โ2) = 4) |
81 | 80 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
((2โ2) ยท (๐โ2)) = (4 ยท (๐โ2))) |
82 | 78, 81 | eqtrd 2773 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((2
ยท ๐)โ2) = (4
ยท (๐โ2))) |
83 | 10 | mulid1d 11177 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((2
ยท ๐) ยท 1) =
(2 ยท ๐)) |
84 | 83 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (2
ยท ((2 ยท ๐)
ยท 1)) = (2 ยท (2 ยท ๐))) |
85 | 8, 8, 9 | mulassd 11183 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((2
ยท 2) ยท ๐) =
(2 ยท (2 ยท ๐))) |
86 | | 2t2e4 12322 |
. . . . . . . . . . . . . . 15
โข (2
ยท 2) = 4 |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (2
ยท 2) = 4) |
88 | 87 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((2
ยท 2) ยท ๐) =
(4 ยท ๐)) |
89 | 84, 85, 88 | 3eqtr2d 2779 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (2
ยท ((2 ยท ๐)
ยท 1)) = (4 ยท ๐)) |
90 | 82, 89 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ โ โ โ (((2
ยท ๐)โ2) + (2
ยท ((2 ยท ๐)
ยท 1))) = ((4 ยท (๐โ2)) + (4 ยท ๐))) |
91 | | 4cn 12243 |
. . . . . . . . . . . . 13
โข 4 โ
โ |
92 | 91 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 4 โ
โ) |
93 | 9 | sqcld 14055 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐โ2) โ
โ) |
94 | 92, 93, 9 | adddid 11184 |
. . . . . . . . . . 11
โข (๐ โ โ โ (4
ยท ((๐โ2) +
๐)) = ((4 ยท (๐โ2)) + (4 ยท ๐))) |
95 | 9 | sqvald 14054 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐โ2) = (๐ ยท ๐)) |
96 | 9 | mulid1d 11177 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
97 | 96 | eqcomd 2739 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ = (๐ ยท 1)) |
98 | 95, 97 | oveq12d 7376 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐โ2) + ๐) = ((๐ ยท ๐) + (๐ ยท 1))) |
99 | 9, 9, 11 | adddid 11184 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
100 | 98, 99 | eqtr4d 2776 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((๐โ2) + ๐) = (๐ ยท (๐ + 1))) |
101 | 100 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ โ โ (4
ยท ((๐โ2) +
๐)) = (4 ยท (๐ ยท (๐ + 1)))) |
102 | 90, 94, 101 | 3eqtr2d 2779 |
. . . . . . . . . 10
โข (๐ โ โ โ (((2
ยท ๐)โ2) + (2
ยท ((2 ยท ๐)
ยท 1))) = (4 ยท (๐ ยท (๐ + 1)))) |
103 | | sq1 14105 |
. . . . . . . . . . 11
โข
(1โ2) = 1 |
104 | 103 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ โ
(1โ2) = 1) |
105 | 102, 104 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ โ โ โ ((((2
ยท ๐)โ2) + (2
ยท ((2 ยท ๐)
ยท 1))) + (1โ2)) = ((4 ยท (๐ ยท (๐ + 1))) + 1)) |
106 | 105 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ โ โ (((((2
ยท ๐)โ2) + (2
ยท ((2 ยท ๐)
ยท 1))) + (1โ2)) โ 1) = (((4 ยท (๐ ยท (๐ + 1))) + 1) โ 1)) |
107 | 9, 11 | addcld 11179 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ + 1) โ
โ) |
108 | 9, 107 | mulcld 11180 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ ยท (๐ + 1)) โ โ) |
109 | 92, 108 | mulcld 11180 |
. . . . . . . . 9
โข (๐ โ โ โ (4
ยท (๐ ยท (๐ + 1))) โ
โ) |
110 | 109, 11 | pncand 11518 |
. . . . . . . 8
โข (๐ โ โ โ (((4
ยท (๐ ยท (๐ + 1))) + 1) โ 1) = (4
ยท (๐ ยท (๐ + 1)))) |
111 | 77, 106, 110 | 3eqtrd 2777 |
. . . . . . 7
โข (๐ โ โ โ ((((2
ยท ๐) + 1)โ2)
โ 1) = (4 ยท (๐
ยท (๐ +
1)))) |
112 | 111 | oveq1d 7373 |
. . . . . 6
โข (๐ โ โ โ (((((2
ยท ๐) + 1)โ2)
โ 1) / (((2 ยท ๐) + 1)โ2)) = ((4 ยท (๐ ยท (๐ + 1))) / (((2 ยท ๐) + 1)โ2))) |
113 | 70, 73, 112 | 3eqtr2d 2779 |
. . . . 5
โข (๐ โ โ โ (1
โ (1 / (((2 ยท ๐) + 1)โ2))) = ((4 ยท (๐ ยท (๐ + 1))) / (((2 ยท ๐) + 1)โ2))) |
114 | 67, 113 | oveq12d 7376 |
. . . 4
โข (๐ โ โ โ (((1 /
(((2 ยท ๐) +
1)โ2))โ1) / (1 โ (1 / (((2 ยท ๐) + 1)โ2)))) = ((1 / (((2 ยท
๐) + 1)โ2)) / ((4
ยท (๐ ยท (๐ + 1))) / (((2 ยท ๐) +
1)โ2)))) |
115 | | 4pos 12265 |
. . . . . . . . 9
โข 0 <
4 |
116 | 115 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ 0 <
4) |
117 | 116 | gt0ne0d 11724 |
. . . . . . 7
โข (๐ โ โ โ 4 โ
0) |
118 | | nnne0 12192 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ 0) |
119 | 18, 15 | readdcld 11189 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ + 1) โ
โ) |
120 | | nngt0 12189 |
. . . . . . . . . 10
โข (๐ โ โ โ 0 <
๐) |
121 | 18 | ltp1d 12090 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ < (๐ + 1)) |
122 | 14, 18, 119, 120, 121 | lttrd 11321 |
. . . . . . . . 9
โข (๐ โ โ โ 0 <
(๐ + 1)) |
123 | 122 | gt0ne0d 11724 |
. . . . . . . 8
โข (๐ โ โ โ (๐ + 1) โ 0) |
124 | 9, 107, 118, 123 | mulne0d 11812 |
. . . . . . 7
โข (๐ โ โ โ (๐ ยท (๐ + 1)) โ 0) |
125 | 92, 108, 117, 124 | mulne0d 11812 |
. . . . . 6
โข (๐ โ โ โ (4
ยท (๐ ยท (๐ + 1))) โ 0) |
126 | 11, 13, 109, 13, 32, 32, 125 | divdivdivd 11983 |
. . . . 5
โข (๐ โ โ โ ((1 /
(((2 ยท ๐) +
1)โ2)) / ((4 ยท (๐ ยท (๐ + 1))) / (((2 ยท ๐) + 1)โ2))) = ((1 ยท (((2
ยท ๐) + 1)โ2)) /
((((2 ยท ๐) +
1)โ2) ยท (4 ยท (๐ ยท (๐ + 1)))))) |
127 | 11, 13 | mulcomd 11181 |
. . . . . 6
โข (๐ โ โ โ (1
ยท (((2 ยท ๐) +
1)โ2)) = ((((2 ยท ๐) + 1)โ2) ยท 1)) |
128 | 127 | oveq1d 7373 |
. . . . 5
โข (๐ โ โ โ ((1
ยท (((2 ยท ๐) +
1)โ2)) / ((((2 ยท ๐) + 1)โ2) ยท (4 ยท (๐ ยท (๐ + 1))))) = (((((2 ยท ๐) + 1)โ2) ยท 1) /
((((2 ยท ๐) +
1)โ2) ยท (4 ยท (๐ ยท (๐ + 1)))))) |
129 | 11 | mulid1d 11177 |
. . . . . . . . . 10
โข (๐ โ โ โ (1
ยท 1) = 1) |
130 | 129 | eqcomd 2739 |
. . . . . . . . 9
โข (๐ โ โ โ 1 = (1
ยท 1)) |
131 | 130 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ โ โ (1 / (4
ยท (๐ ยท (๐ + 1)))) = ((1 ยท 1) / (4
ยท (๐ ยท (๐ + 1))))) |
132 | 11, 92, 11, 108, 117, 124 | divmuldivd 11977 |
. . . . . . . 8
โข (๐ โ โ โ ((1 / 4)
ยท (1 / (๐ ยท
(๐ + 1)))) = ((1 ยท
1) / (4 ยท (๐
ยท (๐ +
1))))) |
133 | 131, 132 | eqtr4d 2776 |
. . . . . . 7
โข (๐ โ โ โ (1 / (4
ยท (๐ ยท (๐ + 1)))) = ((1 / 4) ยท (1
/ (๐ ยท (๐ + 1))))) |
134 | 68, 133 | oveq12d 7376 |
. . . . . 6
โข (๐ โ โ โ (((((2
ยท ๐) + 1)โ2) /
(((2 ยท ๐) +
1)โ2)) ยท (1 / (4 ยท (๐ ยท (๐ + 1))))) = (1 ยท ((1 / 4) ยท (1
/ (๐ ยท (๐ + 1)))))) |
135 | 13, 13, 11, 109, 32, 125 | divmuldivd 11977 |
. . . . . 6
โข (๐ โ โ โ (((((2
ยท ๐) + 1)โ2) /
(((2 ยท ๐) +
1)โ2)) ยท (1 / (4 ยท (๐ ยท (๐ + 1))))) = (((((2 ยท ๐) + 1)โ2) ยท 1) /
((((2 ยท ๐) +
1)โ2) ยท (4 ยท (๐ ยท (๐ + 1)))))) |
136 | 92, 117 | reccld 11929 |
. . . . . . . 8
โข (๐ โ โ โ (1 / 4)
โ โ) |
137 | 108, 124 | reccld 11929 |
. . . . . . . 8
โข (๐ โ โ โ (1 /
(๐ ยท (๐ + 1))) โ
โ) |
138 | 136, 137 | mulcld 11180 |
. . . . . . 7
โข (๐ โ โ โ ((1 / 4)
ยท (1 / (๐ ยท
(๐ + 1)))) โ
โ) |
139 | 138 | mulid2d 11178 |
. . . . . 6
โข (๐ โ โ โ (1
ยท ((1 / 4) ยท (1 / (๐ ยท (๐ + 1))))) = ((1 / 4) ยท (1 / (๐ ยท (๐ + 1))))) |
140 | 134, 135,
139 | 3eqtr3d 2781 |
. . . . 5
โข (๐ โ โ โ (((((2
ยท ๐) + 1)โ2)
ยท 1) / ((((2 ยท ๐) + 1)โ2) ยท (4 ยท (๐ ยท (๐ + 1))))) = ((1 / 4) ยท (1 / (๐ ยท (๐ + 1))))) |
141 | 126, 128,
140 | 3eqtrd 2777 |
. . . 4
โข (๐ โ โ โ ((1 /
(((2 ยท ๐) +
1)โ2)) / ((4 ยท (๐ ยท (๐ + 1))) / (((2 ยท ๐) + 1)โ2))) = ((1 / 4) ยท (1 /
(๐ ยท (๐ + 1))))) |
142 | 114, 141 | eqtrd 2773 |
. . 3
โข (๐ โ โ โ (((1 /
(((2 ยท ๐) +
1)โ2))โ1) / (1 โ (1 / (((2 ยท ๐) + 1)โ2)))) = ((1 / 4) ยท (1 /
(๐ ยท (๐ + 1))))) |
143 | 66, 142 | breqtrd 5132 |
. 2
โข (๐ โ โ โ seq1( + ,
๐ฟ) โ ((1 / 4)
ยท (1 / (๐ ยท
(๐ +
1))))) |
144 | 59 | biimpi 215 |
. . . 4
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
145 | 144 | adantl 483 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
(โคโฅโ1)) |
146 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
147 | 146 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐ โ ((2 ยท ๐) + 1) = ((2 ยท ๐) + 1)) |
148 | 147 | oveq2d 7374 |
. . . . . . 7
โข (๐ = ๐ โ (1 / ((2 ยท ๐) + 1)) = (1 / ((2 ยท ๐) + 1))) |
149 | 146 | oveq2d 7374 |
. . . . . . 7
โข (๐ = ๐ โ ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)) = ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐))) |
150 | 148, 149 | oveq12d 7376 |
. . . . . 6
โข (๐ = ๐ โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐))) = ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ(2
ยท ๐)))) |
151 | | elfznn 13476 |
. . . . . . 7
โข (๐ โ (1...๐) โ ๐ โ โ) |
152 | 151 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ๐ โ โ) |
153 | | 2cnd 12236 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 2 โ โ) |
154 | 152 | nncnd 12174 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ๐ โ โ) |
155 | 153, 154 | mulcld 11180 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (2 ยท ๐) โ โ) |
156 | | 1cnd 11155 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 1 โ โ) |
157 | 155, 156 | addcld 11179 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ โ) |
158 | | 0red 11163 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 0 โ
โ) |
159 | | 1red 11161 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 1 โ
โ) |
160 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ 2 โ
โ) |
161 | | nnre 12165 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
162 | 160, 161 | remulcld 11190 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
163 | 162, 159 | readdcld 11189 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
164 | 21 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 0 <
1) |
165 | 23 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ 2 โ
โ+) |
166 | | nnrp 12931 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ+) |
167 | 165, 166 | rpmulcld 12978 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (2
ยท ๐) โ
โ+) |
168 | 159, 167 | ltaddrp2d 12996 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 1 <
((2 ยท ๐) +
1)) |
169 | 158, 159,
163, 164, 168 | lttrd 11321 |
. . . . . . . . . . 11
โข (๐ โ โ โ 0 <
((2 ยท ๐) +
1)) |
170 | 151, 169 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ 0 < ((2 ยท ๐) + 1)) |
171 | 170 | gt0ne0d 11724 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ ((2 ยท ๐) + 1) โ 0) |
172 | 171 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ 0) |
173 | 157, 172 | reccld 11929 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1 / ((2 ยท ๐) + 1)) โ
โ) |
174 | 9 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ๐ โ โ) |
175 | 153, 174 | mulcld 11180 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (2 ยท ๐) โ โ) |
176 | 175, 156 | addcld 11179 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ โ) |
177 | 29 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ 0) |
178 | 176, 177 | reccld 11929 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1 / ((2 ยท ๐) + 1)) โ โ) |
179 | | 2nn0 12435 |
. . . . . . . . . 10
โข 2 โ
โ0 |
180 | 179 | a1i 11 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 2 โ
โ0) |
181 | 152 | nnnn0d 12478 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ๐ โ โ0) |
182 | 180, 181 | nn0mulcld 12483 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (2 ยท ๐) โ
โ0) |
183 | 178, 182 | expcld 14057 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)) โ
โ) |
184 | 173, 183 | mulcld 11180 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ(2
ยท ๐))) โ
โ) |
185 | 6, 150, 152, 184 | fvmptd3 6972 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (๐พโ๐) = ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)))) |
186 | 185 | adantlr 714 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (๐พโ๐) = ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)))) |
187 | 169 | gt0ne0d 11724 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
0) |
188 | 163, 187 | rereccld 11987 |
. . . . . . 7
โข (๐ โ โ โ (1 / ((2
ยท ๐) + 1)) โ
โ) |
189 | 151, 188 | syl 17 |
. . . . . 6
โข (๐ โ (1...๐) โ (1 / ((2 ยท ๐) + 1)) โ โ) |
190 | 189 | adantl 483 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (1 / ((2 ยท ๐) + 1)) โ
โ) |
191 | 20, 29 | rereccld 11987 |
. . . . . . . 8
โข (๐ โ โ โ (1 / ((2
ยท ๐) + 1)) โ
โ) |
192 | 191 | adantr 482 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1 / ((2 ยท ๐) + 1)) โ โ) |
193 | 192, 182 | reexpcld 14074 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)) โ
โ) |
194 | 193 | adantlr 714 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)) โ
โ) |
195 | 190, 194 | remulcld 11190 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ(2
ยท ๐))) โ
โ) |
196 | 186, 195 | eqeltrd 2834 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (๐พโ๐) โ โ) |
197 | | readdcl 11139 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + ๐) โ โ) |
198 | 197 | adantl 483 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ + ๐) โ โ) |
199 | 145, 196,
198 | seqcl 13934 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ (seq1( +
, ๐พ)โ๐) โ
โ) |
200 | | oveq2 7366 |
. . . . . 6
โข (๐ = ๐ โ ((1 / (((2 ยท ๐) + 1)โ2))โ๐) = ((1 / (((2 ยท ๐) + 1)โ2))โ๐)) |
201 | 33 | adantr 482 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1 / (((2 ยท ๐) + 1)โ2)) โ
โ) |
202 | 201, 181 | expcld 14057 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / (((2 ยท ๐) + 1)โ2))โ๐) โ
โ) |
203 | 55, 200, 152, 202 | fvmptd3 6972 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (๐ฟโ๐) = ((1 / (((2 ยท ๐) + 1)โ2))โ๐)) |
204 | 36 | adantr 482 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1 / (((2 ยท ๐) + 1)โ2)) โ
โ) |
205 | 204, 181 | reexpcld 14074 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / (((2 ยท ๐) + 1)โ2))โ๐) โ
โ) |
206 | 203, 205 | eqeltrd 2834 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (๐ฟโ๐) โ โ) |
207 | 206 | adantlr 714 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (๐ฟโ๐) โ โ) |
208 | 145, 207,
198 | seqcl 13934 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ (seq1( +
, ๐ฟ)โ๐) โ
โ) |
209 | 30 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ 2 โ โค) |
210 | | elfzelz 13447 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ๐ โ โค) |
211 | 209, 210 | zmulcld 12618 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ (2 ยท ๐) โ โค) |
212 | | 1exp 14003 |
. . . . . . . . . . . 12
โข ((2
ยท ๐) โ โค
โ (1โ(2 ยท ๐)) = 1) |
213 | 211, 212 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ (1โ(2 ยท ๐)) = 1) |
214 | | 1exp 14003 |
. . . . . . . . . . . 12
โข (๐ โ โค โ
(1โ๐) =
1) |
215 | 210, 214 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ (1โ๐) = 1) |
216 | 213, 215 | eqtr4d 2776 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ (1โ(2 ยท ๐)) = (1โ๐)) |
217 | 216 | adantl 483 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1โ(2 ยท ๐)) = (1โ๐)) |
218 | 176, 181,
180 | expmuld 14060 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (((2 ยท ๐) + 1)โ(2 ยท ๐)) = ((((2 ยท ๐) + 1)โ2)โ๐)) |
219 | 217, 218 | oveq12d 7376 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1โ(2 ยท ๐)) / (((2 ยท ๐) + 1)โ(2 ยท ๐))) = ((1โ๐) / ((((2 ยท ๐) + 1)โ2)โ๐))) |
220 | 156, 176,
177, 182 | expdivd 14071 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)) = ((1โ(2 ยท ๐)) / (((2 ยท ๐) + 1)โ(2 ยท ๐)))) |
221 | 176 | sqcld 14055 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (((2 ยท ๐) + 1)โ2) โ
โ) |
222 | 30 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 2 โ โค) |
223 | 176, 177,
222 | expne0d 14063 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (((2 ยท ๐) + 1)โ2) โ 0) |
224 | 156, 221,
223, 181 | expdivd 14071 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / (((2 ยท ๐) + 1)โ2))โ๐) = ((1โ๐) / ((((2 ยท ๐) + 1)โ2)โ๐))) |
225 | 219, 220,
224 | 3eqtr4d 2783 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)) = ((1 / (((2 ยท ๐) + 1)โ2))โ๐)) |
226 | 225 | oveq2d 7374 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ(2
ยท ๐))) = ((1 / ((2
ยท ๐) + 1)) ยท
((1 / (((2 ยท ๐) +
1)โ2))โ๐))) |
227 | | 1rp 12924 |
. . . . . . . . . . 11
โข 1 โ
โ+ |
228 | 227 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 1 โ
โ+) |
229 | 16 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 2 โ โ) |
230 | 152 | nnred 12173 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ๐ โ โ) |
231 | 229, 230 | remulcld 11190 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (2 ยท ๐) โ โ) |
232 | 180 | nn0ge0d 12481 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 0 โค 2) |
233 | 181 | nn0ge0d 12481 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 0 โค ๐) |
234 | 229, 230,
232, 233 | mulge0d 11737 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 0 โค (2 ยท ๐)) |
235 | 231, 234 | ge0p1rpd 12992 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ
โ+) |
236 | | 1red 11161 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 1 โ โ) |
237 | 228 | rpge0d 12966 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 0 โค 1) |
238 | 159, 163,
168 | ltled 11308 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 1 โค
((2 ยท ๐) +
1)) |
239 | 151, 238 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ 1 โค ((2 ยท ๐) + 1)) |
240 | 239 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 1 โค ((2 ยท ๐) + 1)) |
241 | 228, 235,
236, 237, 240 | lediv2ad 12984 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1 / ((2 ยท ๐) + 1)) โค (1 /
1)) |
242 | 156 | div1d 11928 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1 / 1) = 1) |
243 | 241, 242 | breqtrd 5132 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1 / ((2 ยท ๐) + 1)) โค 1) |
244 | 152, 188 | syl 17 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1 / ((2 ยท ๐) + 1)) โ
โ) |
245 | 18 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ๐ โ โ) |
246 | 229, 245 | remulcld 11190 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (2 ยท ๐) โ โ) |
247 | 14, 18, 120 | ltled 11308 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ 0 โค
๐) |
248 | 247 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 0 โค ๐) |
249 | 229, 245,
232, 248 | mulge0d 11737 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ (1...๐)) โ 0 โค (2 ยท ๐)) |
250 | 246, 249 | ge0p1rpd 12992 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ
โ+) |
251 | 250, 222 | rpexpcld 14156 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (((2 ยท ๐) + 1)โ2) โ
โ+) |
252 | 251 | rpreccld 12972 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1 / (((2 ยท ๐) + 1)โ2)) โ
โ+) |
253 | 210 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ๐ โ โค) |
254 | 252, 253 | rpexpcld 14156 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / (((2 ยท ๐) + 1)โ2))โ๐) โ
โ+) |
255 | 244, 236,
254 | lemul1d 13005 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1)) โค 1 โ ((1 / ((2
ยท ๐) + 1)) ยท
((1 / (((2 ยท ๐) +
1)โ2))โ๐)) โค
(1 ยท ((1 / (((2 ยท ๐) + 1)โ2))โ๐)))) |
256 | 243, 255 | mpbid 231 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / (((2
ยท ๐) +
1)โ2))โ๐)) โค
(1 ยท ((1 / (((2 ยท ๐) + 1)โ2))โ๐))) |
257 | 202 | mulid2d 11178 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (1 ยท ((1 / (((2 ยท
๐) + 1)โ2))โ๐)) = ((1 / (((2 ยท ๐) + 1)โ2))โ๐)) |
258 | 256, 257 | breqtrd 5132 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / (((2
ยท ๐) +
1)โ2))โ๐)) โค
((1 / (((2 ยท ๐) +
1)โ2))โ๐)) |
259 | 226, 258 | eqbrtrd 5128 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ(2
ยท ๐))) โค ((1 /
(((2 ยท ๐) +
1)โ2))โ๐)) |
260 | 259, 185,
203 | 3brtr4d 5138 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...๐)) โ (๐พโ๐) โค (๐ฟโ๐)) |
261 | 260 | adantlr 714 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (๐พโ๐) โค (๐ฟโ๐)) |
262 | 145, 196,
207, 261 | serle 13969 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ (seq1( +
, ๐พ)โ๐) โค (seq1( + , ๐ฟ)โ๐)) |
263 | 1, 2, 7, 143, 199, 208, 262 | climle 15528 |
1
โข (๐ โ โ โ ((๐ตโ๐) โ (๐ตโ(๐ + 1))) โค ((1 / 4) ยท (1 / (๐ ยท (๐ + 1))))) |