Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
โข (๐ โ โ โฆ
((-1โ(๐ โ 1))
ยท (((1 / ((2 ยท ๐) + 1))โ๐) / ๐))) = (๐ โ โ โฆ ((-1โ(๐ โ 1)) ยท (((1 / ((2
ยท ๐) +
1))โ๐) / ๐))) |
2 | | eqid 2737 |
. . 3
โข (๐ โ โ โฆ (((1 /
((2 ยท ๐) +
1))โ๐) / ๐)) = (๐ โ โ โฆ (((1 / ((2 ยท
๐) + 1))โ๐) / ๐)) |
3 | | eqid 2737 |
. . 3
โข (๐ โ โ โฆ
(((-1โ(๐ โ 1))
ยท (((1 / ((2 ยท ๐) + 1))โ๐) / ๐)) + (((1 / ((2 ยท ๐) + 1))โ๐) / ๐))) = (๐ โ โ โฆ (((-1โ(๐ โ 1)) ยท (((1 / ((2
ยท ๐) +
1))โ๐) / ๐)) + (((1 / ((2 ยท ๐) + 1))โ๐) / ๐))) |
4 | | stirlinglem6.1 |
. . 3
โข ๐ป = (๐ โ โ0 โฆ (2
ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))))) |
5 | | eqid 2737 |
. . 3
โข (๐ โ โ0
โฆ ((2 ยท ๐) +
1)) = (๐ โ
โ0 โฆ ((2 ยท ๐) + 1)) |
6 | | 2re 12234 |
. . . . . . 7
โข 2 โ
โ |
7 | 6 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ 2 โ
โ) |
8 | | nnre 12167 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
9 | 7, 8 | remulcld 11192 |
. . . . 5
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
10 | | 0le2 12262 |
. . . . . . 7
โข 0 โค
2 |
11 | 10 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ 0 โค
2) |
12 | | 0red 11165 |
. . . . . . 7
โข (๐ โ โ โ 0 โ
โ) |
13 | | nngt0 12191 |
. . . . . . 7
โข (๐ โ โ โ 0 <
๐) |
14 | 12, 8, 13 | ltled 11310 |
. . . . . 6
โข (๐ โ โ โ 0 โค
๐) |
15 | 7, 8, 11, 14 | mulge0d 11739 |
. . . . 5
โข (๐ โ โ โ 0 โค (2
ยท ๐)) |
16 | 9, 15 | ge0p1rpd 12994 |
. . . 4
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ+) |
17 | 16 | rpreccld 12974 |
. . 3
โข (๐ โ โ โ (1 / ((2
ยท ๐) + 1)) โ
โ+) |
18 | | 1red 11163 |
. . . . . 6
โข (๐ โ โ โ 1 โ
โ) |
19 | 18 | renegcld 11589 |
. . . . 5
โข (๐ โ โ โ -1 โ
โ) |
20 | 17 | rpred 12964 |
. . . . 5
โข (๐ โ โ โ (1 / ((2
ยท ๐) + 1)) โ
โ) |
21 | | neg1lt0 12277 |
. . . . . 6
โข -1 <
0 |
22 | 21 | a1i 11 |
. . . . 5
โข (๐ โ โ โ -1 <
0) |
23 | 17 | rpgt0d 12967 |
. . . . 5
โข (๐ โ โ โ 0 < (1
/ ((2 ยท ๐) +
1))) |
24 | 19, 12, 20, 22, 23 | lttrd 11323 |
. . . 4
โข (๐ โ โ โ -1 <
(1 / ((2 ยท ๐) +
1))) |
25 | | 1rp 12926 |
. . . . . 6
โข 1 โ
โ+ |
26 | 25 | a1i 11 |
. . . . 5
โข (๐ โ โ โ 1 โ
โ+) |
27 | | 1cnd 11157 |
. . . . . . 7
โข (๐ โ โ โ 1 โ
โ) |
28 | 27 | div1d 11930 |
. . . . . 6
โข (๐ โ โ โ (1 / 1) =
1) |
29 | | 2rp 12927 |
. . . . . . . . 9
โข 2 โ
โ+ |
30 | 29 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ 2 โ
โ+) |
31 | | nnrp 12933 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ+) |
32 | 30, 31 | rpmulcld 12980 |
. . . . . . 7
โข (๐ โ โ โ (2
ยท ๐) โ
โ+) |
33 | 18, 32 | ltaddrp2d 12998 |
. . . . . 6
โข (๐ โ โ โ 1 <
((2 ยท ๐) +
1)) |
34 | 28, 33 | eqbrtrd 5132 |
. . . . 5
โข (๐ โ โ โ (1 / 1)
< ((2 ยท ๐) +
1)) |
35 | 26, 16, 34 | ltrec1d 12984 |
. . . 4
โข (๐ โ โ โ (1 / ((2
ยท ๐) + 1)) <
1) |
36 | 20, 18 | absltd 15321 |
. . . 4
โข (๐ โ โ โ
((absโ(1 / ((2 ยท ๐) + 1))) < 1 โ (-1 < (1 / ((2
ยท ๐) + 1)) โง (1
/ ((2 ยท ๐) + 1))
< 1))) |
37 | 24, 35, 36 | mpbir2and 712 |
. . 3
โข (๐ โ โ โ
(absโ(1 / ((2 ยท ๐) + 1))) < 1) |
38 | 1, 2, 3, 4, 5, 17,
37 | stirlinglem5 44393 |
. 2
โข (๐ โ โ โ seq0( + ,
๐ป) โ (logโ((1 +
(1 / ((2 ยท ๐) + 1)))
/ (1 โ (1 / ((2 ยท ๐) + 1)))))) |
39 | | 2cnd 12238 |
. . . . . . . . . 10
โข (๐ โ โ โ 2 โ
โ) |
40 | | nncn 12168 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
41 | 39, 40 | mulcld 11182 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
42 | 41, 27 | addcld 11181 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
43 | 9, 18 | readdcld 11191 |
. . . . . . . . . 10
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
44 | | 2pos 12263 |
. . . . . . . . . . . 12
โข 0 <
2 |
45 | 44 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ โ 0 <
2) |
46 | 7, 8, 45, 13 | mulgt0d 11317 |
. . . . . . . . . 10
โข (๐ โ โ โ 0 < (2
ยท ๐)) |
47 | 9 | ltp1d 12092 |
. . . . . . . . . 10
โข (๐ โ โ โ (2
ยท ๐) < ((2
ยท ๐) +
1)) |
48 | 12, 9, 43, 46, 47 | lttrd 11323 |
. . . . . . . . 9
โข (๐ โ โ โ 0 <
((2 ยท ๐) +
1)) |
49 | 48 | gt0ne0d 11726 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
0) |
50 | 42, 49 | dividd 11936 |
. . . . . . 7
โข (๐ โ โ โ (((2
ยท ๐) + 1) / ((2
ยท ๐) + 1)) =
1) |
51 | 50 | eqcomd 2743 |
. . . . . 6
โข (๐ โ โ โ 1 = (((2
ยท ๐) + 1) / ((2
ยท ๐) +
1))) |
52 | 51 | oveq1d 7377 |
. . . . 5
โข (๐ โ โ โ (1 + (1 /
((2 ยท ๐) + 1))) =
((((2 ยท ๐) + 1) /
((2 ยท ๐) + 1)) + (1
/ ((2 ยท ๐) +
1)))) |
53 | 51 | oveq1d 7377 |
. . . . 5
โข (๐ โ โ โ (1
โ (1 / ((2 ยท ๐) + 1))) = ((((2 ยท ๐) + 1) / ((2 ยท ๐) + 1)) โ (1 / ((2 ยท ๐) + 1)))) |
54 | 52, 53 | oveq12d 7380 |
. . . 4
โข (๐ โ โ โ ((1 + (1
/ ((2 ยท ๐) + 1))) /
(1 โ (1 / ((2 ยท ๐) + 1)))) = (((((2 ยท ๐) + 1) / ((2 ยท ๐) + 1)) + (1 / ((2 ยท
๐) + 1))) / ((((2 ยท
๐) + 1) / ((2 ยท
๐) + 1)) โ (1 / ((2
ยท ๐) +
1))))) |
55 | 42, 27, 42, 49 | divdird 11976 |
. . . . . . 7
โข (๐ โ โ โ ((((2
ยท ๐) + 1) + 1) / ((2
ยท ๐) + 1)) = ((((2
ยท ๐) + 1) / ((2
ยท ๐) + 1)) + (1 /
((2 ยท ๐) +
1)))) |
56 | 55 | eqcomd 2743 |
. . . . . 6
โข (๐ โ โ โ ((((2
ยท ๐) + 1) / ((2
ยท ๐) + 1)) + (1 /
((2 ยท ๐) + 1))) =
((((2 ยท ๐) + 1) + 1)
/ ((2 ยท ๐) +
1))) |
57 | 42, 27, 42, 49 | divsubdird 11977 |
. . . . . . 7
โข (๐ โ โ โ ((((2
ยท ๐) + 1) โ 1)
/ ((2 ยท ๐) + 1)) =
((((2 ยท ๐) + 1) /
((2 ยท ๐) + 1))
โ (1 / ((2 ยท ๐) + 1)))) |
58 | 57 | eqcomd 2743 |
. . . . . 6
โข (๐ โ โ โ ((((2
ยท ๐) + 1) / ((2
ยท ๐) + 1)) โ
(1 / ((2 ยท ๐) + 1)))
= ((((2 ยท ๐) + 1)
โ 1) / ((2 ยท ๐) + 1))) |
59 | 56, 58 | oveq12d 7380 |
. . . . 5
โข (๐ โ โ โ (((((2
ยท ๐) + 1) / ((2
ยท ๐) + 1)) + (1 /
((2 ยท ๐) + 1))) /
((((2 ยท ๐) + 1) /
((2 ยท ๐) + 1))
โ (1 / ((2 ยท ๐) + 1)))) = (((((2 ยท ๐) + 1) + 1) / ((2 ยท ๐) + 1)) / ((((2 ยท ๐) + 1) โ 1) / ((2 ยท
๐) + 1)))) |
60 | 41, 27, 27 | addassd 11184 |
. . . . . . . 8
โข (๐ โ โ โ (((2
ยท ๐) + 1) + 1) = ((2
ยท ๐) + (1 +
1))) |
61 | | 1p1e2 12285 |
. . . . . . . . . 10
โข (1 + 1) =
2 |
62 | 61 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ โ (1 + 1) =
2) |
63 | 62 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + (1 + 1)) =
((2 ยท ๐) +
2)) |
64 | 39 | mulid1d 11179 |
. . . . . . . . . . 11
โข (๐ โ โ โ (2
ยท 1) = 2) |
65 | 64 | eqcomd 2743 |
. . . . . . . . . 10
โข (๐ โ โ โ 2 = (2
ยท 1)) |
66 | 65 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ โ โ ((2
ยท ๐) + 2) = ((2
ยท ๐) + (2 ยท
1))) |
67 | 39, 40, 27 | adddid 11186 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท (๐ + 1)) = ((2
ยท ๐) + (2 ยท
1))) |
68 | 66, 67 | eqtr4d 2780 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + 2) = (2
ยท (๐ +
1))) |
69 | 60, 63, 68 | 3eqtrd 2781 |
. . . . . . 7
โข (๐ โ โ โ (((2
ยท ๐) + 1) + 1) = (2
ยท (๐ +
1))) |
70 | 69 | oveq1d 7377 |
. . . . . 6
โข (๐ โ โ โ ((((2
ยท ๐) + 1) + 1) / ((2
ยท ๐) + 1)) = ((2
ยท (๐ + 1)) / ((2
ยท ๐) +
1))) |
71 | 41, 27 | pncand 11520 |
. . . . . . 7
โข (๐ โ โ โ (((2
ยท ๐) + 1) โ 1)
= (2 ยท ๐)) |
72 | 71 | oveq1d 7377 |
. . . . . 6
โข (๐ โ โ โ ((((2
ยท ๐) + 1) โ 1)
/ ((2 ยท ๐) + 1)) =
((2 ยท ๐) / ((2
ยท ๐) +
1))) |
73 | 70, 72 | oveq12d 7380 |
. . . . 5
โข (๐ โ โ โ (((((2
ยท ๐) + 1) + 1) / ((2
ยท ๐) + 1)) / ((((2
ยท ๐) + 1) โ 1)
/ ((2 ยท ๐) + 1))) =
(((2 ยท (๐ + 1)) /
((2 ยท ๐) + 1)) / ((2
ยท ๐) / ((2 ยท
๐) + 1)))) |
74 | 59, 73 | eqtrd 2777 |
. . . 4
โข (๐ โ โ โ (((((2
ยท ๐) + 1) / ((2
ยท ๐) + 1)) + (1 /
((2 ยท ๐) + 1))) /
((((2 ยท ๐) + 1) /
((2 ยท ๐) + 1))
โ (1 / ((2 ยท ๐) + 1)))) = (((2 ยท (๐ + 1)) / ((2 ยท ๐) + 1)) / ((2 ยท ๐) / ((2 ยท ๐) + 1)))) |
75 | 40, 27 | addcld 11181 |
. . . . . . 7
โข (๐ โ โ โ (๐ + 1) โ
โ) |
76 | 39, 75 | mulcld 11182 |
. . . . . 6
โข (๐ โ โ โ (2
ยท (๐ + 1)) โ
โ) |
77 | 46 | gt0ne0d 11726 |
. . . . . 6
โข (๐ โ โ โ (2
ยท ๐) โ
0) |
78 | 76, 41, 42, 77, 49 | divcan7d 11966 |
. . . . 5
โข (๐ โ โ โ (((2
ยท (๐ + 1)) / ((2
ยท ๐) + 1)) / ((2
ยท ๐) / ((2 ยท
๐) + 1))) = ((2 ยท
(๐ + 1)) / (2 ยท
๐))) |
79 | 45 | gt0ne0d 11726 |
. . . . . . 7
โข (๐ โ โ โ 2 โ
0) |
80 | 13 | gt0ne0d 11726 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ 0) |
81 | 39, 39, 75, 40, 79, 80 | divmuldivd 11979 |
. . . . . 6
โข (๐ โ โ โ ((2 / 2)
ยท ((๐ + 1) / ๐)) = ((2 ยท (๐ + 1)) / (2 ยท ๐))) |
82 | 81 | eqcomd 2743 |
. . . . 5
โข (๐ โ โ โ ((2
ยท (๐ + 1)) / (2
ยท ๐)) = ((2 / 2)
ยท ((๐ + 1) / ๐))) |
83 | 39, 79 | dividd 11936 |
. . . . . . 7
โข (๐ โ โ โ (2 / 2) =
1) |
84 | 83 | oveq1d 7377 |
. . . . . 6
โข (๐ โ โ โ ((2 / 2)
ยท ((๐ + 1) / ๐)) = (1 ยท ((๐ + 1) / ๐))) |
85 | 75, 40, 80 | divcld 11938 |
. . . . . . 7
โข (๐ โ โ โ ((๐ + 1) / ๐) โ โ) |
86 | 85 | mulid2d 11180 |
. . . . . 6
โข (๐ โ โ โ (1
ยท ((๐ + 1) / ๐)) = ((๐ + 1) / ๐)) |
87 | 84, 86 | eqtrd 2777 |
. . . . 5
โข (๐ โ โ โ ((2 / 2)
ยท ((๐ + 1) / ๐)) = ((๐ + 1) / ๐)) |
88 | 78, 82, 87 | 3eqtrd 2781 |
. . . 4
โข (๐ โ โ โ (((2
ยท (๐ + 1)) / ((2
ยท ๐) + 1)) / ((2
ยท ๐) / ((2 ยท
๐) + 1))) = ((๐ + 1) / ๐)) |
89 | 54, 74, 88 | 3eqtrd 2781 |
. . 3
โข (๐ โ โ โ ((1 + (1
/ ((2 ยท ๐) + 1))) /
(1 โ (1 / ((2 ยท ๐) + 1)))) = ((๐ + 1) / ๐)) |
90 | 89 | fveq2d 6851 |
. 2
โข (๐ โ โ โ
(logโ((1 + (1 / ((2 ยท ๐) + 1))) / (1 โ (1 / ((2 ยท
๐) + 1))))) =
(logโ((๐ + 1) / ๐))) |
91 | 38, 90 | breqtrd 5136 |
1
โข (๐ โ โ โ seq0( + ,
๐ป) โ
(logโ((๐ + 1) / ๐))) |