Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . 3
โข (๐ โ โ โฆ
((-1โ(๐ โ 1))
ยท (((1 / ((2 ยท ๐) + 1))โ๐) / ๐))) = (๐ โ โ โฆ ((-1โ(๐ โ 1)) ยท (((1 / ((2
ยท ๐) +
1))โ๐) / ๐))) |
2 | | eqid 2732 |
. . 3
โข (๐ โ โ โฆ (((1 /
((2 ยท ๐) +
1))โ๐) / ๐)) = (๐ โ โ โฆ (((1 / ((2 ยท
๐) + 1))โ๐) / ๐)) |
3 | | eqid 2732 |
. . 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 2732 |
. . 3
โข (๐ โ โ0
โฆ ((2 ยท ๐) +
1)) = (๐ โ
โ0 โฆ ((2 ยท ๐) + 1)) |
6 | | 2re 12285 |
. . . . . . 7
โข 2 โ
โ |
7 | 6 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ 2 โ
โ) |
8 | | nnre 12218 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
9 | 7, 8 | remulcld 11243 |
. . . . 5
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
10 | | 0le2 12313 |
. . . . . . 7
โข 0 โค
2 |
11 | 10 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ 0 โค
2) |
12 | | 0red 11216 |
. . . . . . 7
โข (๐ โ โ โ 0 โ
โ) |
13 | | nngt0 12242 |
. . . . . . 7
โข (๐ โ โ โ 0 <
๐) |
14 | 12, 8, 13 | ltled 11361 |
. . . . . 6
โข (๐ โ โ โ 0 โค
๐) |
15 | 7, 8, 11, 14 | mulge0d 11790 |
. . . . 5
โข (๐ โ โ โ 0 โค (2
ยท ๐)) |
16 | 9, 15 | ge0p1rpd 13045 |
. . . 4
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ+) |
17 | 16 | rpreccld 13025 |
. . 3
โข (๐ โ โ โ (1 / ((2
ยท ๐) + 1)) โ
โ+) |
18 | | 1red 11214 |
. . . . . 6
โข (๐ โ โ โ 1 โ
โ) |
19 | 18 | renegcld 11640 |
. . . . 5
โข (๐ โ โ โ -1 โ
โ) |
20 | 17 | rpred 13015 |
. . . . 5
โข (๐ โ โ โ (1 / ((2
ยท ๐) + 1)) โ
โ) |
21 | | neg1lt0 12328 |
. . . . . 6
โข -1 <
0 |
22 | 21 | a1i 11 |
. . . . 5
โข (๐ โ โ โ -1 <
0) |
23 | 17 | rpgt0d 13018 |
. . . . 5
โข (๐ โ โ โ 0 < (1
/ ((2 ยท ๐) +
1))) |
24 | 19, 12, 20, 22, 23 | lttrd 11374 |
. . . 4
โข (๐ โ โ โ -1 <
(1 / ((2 ยท ๐) +
1))) |
25 | | 1rp 12977 |
. . . . . 6
โข 1 โ
โ+ |
26 | 25 | a1i 11 |
. . . . 5
โข (๐ โ โ โ 1 โ
โ+) |
27 | | 1cnd 11208 |
. . . . . . 7
โข (๐ โ โ โ 1 โ
โ) |
28 | 27 | div1d 11981 |
. . . . . 6
โข (๐ โ โ โ (1 / 1) =
1) |
29 | | 2rp 12978 |
. . . . . . . . 9
โข 2 โ
โ+ |
30 | 29 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ 2 โ
โ+) |
31 | | nnrp 12984 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ+) |
32 | 30, 31 | rpmulcld 13031 |
. . . . . . 7
โข (๐ โ โ โ (2
ยท ๐) โ
โ+) |
33 | 18, 32 | ltaddrp2d 13049 |
. . . . . 6
โข (๐ โ โ โ 1 <
((2 ยท ๐) +
1)) |
34 | 28, 33 | eqbrtrd 5170 |
. . . . 5
โข (๐ โ โ โ (1 / 1)
< ((2 ยท ๐) +
1)) |
35 | 26, 16, 34 | ltrec1d 13035 |
. . . 4
โข (๐ โ โ โ (1 / ((2
ยท ๐) + 1)) <
1) |
36 | 20, 18 | absltd 15375 |
. . . 4
โข (๐ โ โ โ
((absโ(1 / ((2 ยท ๐) + 1))) < 1 โ (-1 < (1 / ((2
ยท ๐) + 1)) โง (1
/ ((2 ยท ๐) + 1))
< 1))) |
37 | 24, 35, 36 | mpbir2and 711 |
. . 3
โข (๐ โ โ โ
(absโ(1 / ((2 ยท ๐) + 1))) < 1) |
38 | 1, 2, 3, 4, 5, 17,
37 | stirlinglem5 44784 |
. 2
โข (๐ โ โ โ seq0( + ,
๐ป) โ (logโ((1 +
(1 / ((2 ยท ๐) + 1)))
/ (1 โ (1 / ((2 ยท ๐) + 1)))))) |
39 | | 2cnd 12289 |
. . . . . . . . . 10
โข (๐ โ โ โ 2 โ
โ) |
40 | | nncn 12219 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
41 | 39, 40 | mulcld 11233 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
42 | 41, 27 | addcld 11232 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
43 | 9, 18 | readdcld 11242 |
. . . . . . . . . 10
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
44 | | 2pos 12314 |
. . . . . . . . . . . 12
โข 0 <
2 |
45 | 44 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ โ 0 <
2) |
46 | 7, 8, 45, 13 | mulgt0d 11368 |
. . . . . . . . . 10
โข (๐ โ โ โ 0 < (2
ยท ๐)) |
47 | 9 | ltp1d 12143 |
. . . . . . . . . 10
โข (๐ โ โ โ (2
ยท ๐) < ((2
ยท ๐) +
1)) |
48 | 12, 9, 43, 46, 47 | lttrd 11374 |
. . . . . . . . 9
โข (๐ โ โ โ 0 <
((2 ยท ๐) +
1)) |
49 | 48 | gt0ne0d 11777 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
0) |
50 | 42, 49 | dividd 11987 |
. . . . . . 7
โข (๐ โ โ โ (((2
ยท ๐) + 1) / ((2
ยท ๐) + 1)) =
1) |
51 | 50 | eqcomd 2738 |
. . . . . 6
โข (๐ โ โ โ 1 = (((2
ยท ๐) + 1) / ((2
ยท ๐) +
1))) |
52 | 51 | oveq1d 7423 |
. . . . 5
โข (๐ โ โ โ (1 + (1 /
((2 ยท ๐) + 1))) =
((((2 ยท ๐) + 1) /
((2 ยท ๐) + 1)) + (1
/ ((2 ยท ๐) +
1)))) |
53 | 51 | oveq1d 7423 |
. . . . 5
โข (๐ โ โ โ (1
โ (1 / ((2 ยท ๐) + 1))) = ((((2 ยท ๐) + 1) / ((2 ยท ๐) + 1)) โ (1 / ((2 ยท ๐) + 1)))) |
54 | 52, 53 | oveq12d 7426 |
. . . 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 12027 |
. . . . . . 7
โข (๐ โ โ โ ((((2
ยท ๐) + 1) + 1) / ((2
ยท ๐) + 1)) = ((((2
ยท ๐) + 1) / ((2
ยท ๐) + 1)) + (1 /
((2 ยท ๐) +
1)))) |
56 | 55 | eqcomd 2738 |
. . . . . 6
โข (๐ โ โ โ ((((2
ยท ๐) + 1) / ((2
ยท ๐) + 1)) + (1 /
((2 ยท ๐) + 1))) =
((((2 ยท ๐) + 1) + 1)
/ ((2 ยท ๐) +
1))) |
57 | 42, 27, 42, 49 | divsubdird 12028 |
. . . . . . 7
โข (๐ โ โ โ ((((2
ยท ๐) + 1) โ 1)
/ ((2 ยท ๐) + 1)) =
((((2 ยท ๐) + 1) /
((2 ยท ๐) + 1))
โ (1 / ((2 ยท ๐) + 1)))) |
58 | 57 | eqcomd 2738 |
. . . . . 6
โข (๐ โ โ โ ((((2
ยท ๐) + 1) / ((2
ยท ๐) + 1)) โ
(1 / ((2 ยท ๐) + 1)))
= ((((2 ยท ๐) + 1)
โ 1) / ((2 ยท ๐) + 1))) |
59 | 56, 58 | oveq12d 7426 |
. . . . 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 11235 |
. . . . . . . 8
โข (๐ โ โ โ (((2
ยท ๐) + 1) + 1) = ((2
ยท ๐) + (1 +
1))) |
61 | | 1p1e2 12336 |
. . . . . . . . . 10
โข (1 + 1) =
2 |
62 | 61 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ โ (1 + 1) =
2) |
63 | 62 | oveq2d 7424 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + (1 + 1)) =
((2 ยท ๐) +
2)) |
64 | 39 | mulridd 11230 |
. . . . . . . . . . 11
โข (๐ โ โ โ (2
ยท 1) = 2) |
65 | 64 | eqcomd 2738 |
. . . . . . . . . 10
โข (๐ โ โ โ 2 = (2
ยท 1)) |
66 | 65 | oveq2d 7424 |
. . . . . . . . 9
โข (๐ โ โ โ ((2
ยท ๐) + 2) = ((2
ยท ๐) + (2 ยท
1))) |
67 | 39, 40, 27 | adddid 11237 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท (๐ + 1)) = ((2
ยท ๐) + (2 ยท
1))) |
68 | 66, 67 | eqtr4d 2775 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) + 2) = (2
ยท (๐ +
1))) |
69 | 60, 63, 68 | 3eqtrd 2776 |
. . . . . . 7
โข (๐ โ โ โ (((2
ยท ๐) + 1) + 1) = (2
ยท (๐ +
1))) |
70 | 69 | oveq1d 7423 |
. . . . . 6
โข (๐ โ โ โ ((((2
ยท ๐) + 1) + 1) / ((2
ยท ๐) + 1)) = ((2
ยท (๐ + 1)) / ((2
ยท ๐) +
1))) |
71 | 41, 27 | pncand 11571 |
. . . . . . 7
โข (๐ โ โ โ (((2
ยท ๐) + 1) โ 1)
= (2 ยท ๐)) |
72 | 71 | oveq1d 7423 |
. . . . . 6
โข (๐ โ โ โ ((((2
ยท ๐) + 1) โ 1)
/ ((2 ยท ๐) + 1)) =
((2 ยท ๐) / ((2
ยท ๐) +
1))) |
73 | 70, 72 | oveq12d 7426 |
. . . . 5
โข (๐ โ โ โ (((((2
ยท ๐) + 1) + 1) / ((2
ยท ๐) + 1)) / ((((2
ยท ๐) + 1) โ 1)
/ ((2 ยท ๐) + 1))) =
(((2 ยท (๐ + 1)) /
((2 ยท ๐) + 1)) / ((2
ยท ๐) / ((2 ยท
๐) + 1)))) |
74 | 59, 73 | eqtrd 2772 |
. . . 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 11232 |
. . . . . . 7
โข (๐ โ โ โ (๐ + 1) โ
โ) |
76 | 39, 75 | mulcld 11233 |
. . . . . 6
โข (๐ โ โ โ (2
ยท (๐ + 1)) โ
โ) |
77 | 46 | gt0ne0d 11777 |
. . . . . 6
โข (๐ โ โ โ (2
ยท ๐) โ
0) |
78 | 76, 41, 42, 77, 49 | divcan7d 12017 |
. . . . 5
โข (๐ โ โ โ (((2
ยท (๐ + 1)) / ((2
ยท ๐) + 1)) / ((2
ยท ๐) / ((2 ยท
๐) + 1))) = ((2 ยท
(๐ + 1)) / (2 ยท
๐))) |
79 | 45 | gt0ne0d 11777 |
. . . . . . 7
โข (๐ โ โ โ 2 โ
0) |
80 | 13 | gt0ne0d 11777 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ 0) |
81 | 39, 39, 75, 40, 79, 80 | divmuldivd 12030 |
. . . . . 6
โข (๐ โ โ โ ((2 / 2)
ยท ((๐ + 1) / ๐)) = ((2 ยท (๐ + 1)) / (2 ยท ๐))) |
82 | 81 | eqcomd 2738 |
. . . . 5
โข (๐ โ โ โ ((2
ยท (๐ + 1)) / (2
ยท ๐)) = ((2 / 2)
ยท ((๐ + 1) / ๐))) |
83 | 39, 79 | dividd 11987 |
. . . . . . 7
โข (๐ โ โ โ (2 / 2) =
1) |
84 | 83 | oveq1d 7423 |
. . . . . 6
โข (๐ โ โ โ ((2 / 2)
ยท ((๐ + 1) / ๐)) = (1 ยท ((๐ + 1) / ๐))) |
85 | 75, 40, 80 | divcld 11989 |
. . . . . . 7
โข (๐ โ โ โ ((๐ + 1) / ๐) โ โ) |
86 | 85 | mullidd 11231 |
. . . . . 6
โข (๐ โ โ โ (1
ยท ((๐ + 1) / ๐)) = ((๐ + 1) / ๐)) |
87 | 84, 86 | eqtrd 2772 |
. . . . 5
โข (๐ โ โ โ ((2 / 2)
ยท ((๐ + 1) / ๐)) = ((๐ + 1) / ๐)) |
88 | 78, 82, 87 | 3eqtrd 2776 |
. . . 4
โข (๐ โ โ โ (((2
ยท (๐ + 1)) / ((2
ยท ๐) + 1)) / ((2
ยท ๐) / ((2 ยท
๐) + 1))) = ((๐ + 1) / ๐)) |
89 | 54, 74, 88 | 3eqtrd 2776 |
. . 3
โข (๐ โ โ โ ((1 + (1
/ ((2 ยท ๐) + 1))) /
(1 โ (1 / ((2 ยท ๐) + 1)))) = ((๐ + 1) / ๐)) |
90 | 89 | fveq2d 6895 |
. 2
โข (๐ โ โ โ
(logโ((1 + (1 / ((2 ยท ๐) + 1))) / (1 โ (1 / ((2 ยท
๐) + 1))))) =
(logโ((๐ + 1) / ๐))) |
91 | 38, 90 | breqtrd 5174 |
1
โข (๐ โ โ โ seq0( + ,
๐ป) โ
(logโ((๐ + 1) / ๐))) |