Step | Hyp | Ref
| Expression |
1 | | nnuz 12811 |
. . . 4
โข โ =
(โคโฅโ1) |
2 | | 1zzd 12539 |
. . . 4
โข (๐ โ โ โ 1 โ
โค) |
3 | | 1e0p1 12665 |
. . . . . . . 8
โข 1 = (0 +
1) |
4 | 3 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 1 = (0 +
1)) |
5 | 4 | seqeq1d 13918 |
. . . . . 6
โข (๐ โ โ โ seq1( + ,
๐ป) = seq(0 + 1)( + , ๐ป)) |
6 | | nn0uz 12810 |
. . . . . . 7
โข
โ0 = (โคโฅโ0) |
7 | | 0nn0 12433 |
. . . . . . . 8
โข 0 โ
โ0 |
8 | 7 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 0 โ
โ0) |
9 | | stirlinglem7.3 |
. . . . . . . . 9
โข ๐ป = (๐ โ โ0 โฆ (2
ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))))) |
10 | | oveq2 7366 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
11 | 10 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((2 ยท ๐) + 1) = ((2 ยท ๐) + 1)) |
12 | 11 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (1 / ((2 ยท ๐) + 1)) = (1 / ((2 ยท ๐) + 1))) |
13 | 11 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1)) = ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))) |
14 | 12, 13 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))) = ((1 / ((2 ยท
๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) +
1)))) |
15 | 14 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ = ๐ โ (2 ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) + 1)))) = (2
ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))))) |
16 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โ
โ0) |
17 | | 2cnd 12236 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ0)
โ 2 โ โ) |
18 | | 2cnd 12236 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ 2 โ โ) |
19 | | nn0cn 12428 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ ๐ โ
โ) |
20 | 18, 19 | mulcld 11180 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (2 ยท ๐)
โ โ) |
21 | | 1cnd 11155 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ 1 โ โ) |
22 | 20, 21 | addcld 11179 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ ((2 ยท ๐) + 1)
โ โ) |
23 | 22 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ0)
โ ((2 ยท ๐) + 1)
โ โ) |
24 | | 0red 11163 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ 0 โ โ) |
25 | | 2re 12232 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โ |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ 2 โ โ) |
27 | | nn0re 12427 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ ๐ โ
โ) |
28 | 26, 27 | remulcld 11190 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ (2 ยท ๐)
โ โ) |
29 | | 1red 11161 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ 1 โ โ) |
30 | | 0le2 12260 |
. . . . . . . . . . . . . . . . . 18
โข 0 โค
2 |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ 0 โค 2) |
32 | | nn0ge0 12443 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ 0 โค ๐) |
33 | 26, 27, 31, 32 | mulge0d 11737 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ 0 โค (2 ยท ๐)) |
34 | | 0lt1 11682 |
. . . . . . . . . . . . . . . . 17
โข 0 <
1 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ 0 < 1) |
36 | 28, 29, 33, 35 | addgegt0d 11733 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ 0 < ((2 ยท ๐) + 1)) |
37 | 24, 36 | ltned 11296 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ 0 โ ((2 ยท ๐) + 1)) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ0)
โ 0 โ ((2 ยท ๐) + 1)) |
39 | 38 | necomd 2996 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ0)
โ ((2 ยท ๐) + 1)
โ 0) |
40 | 23, 39 | reccld 11929 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ0)
โ (1 / ((2 ยท ๐)
+ 1)) โ โ) |
41 | | nncn 12166 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โ) |
42 | 41 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โ
โ) |
43 | 17, 42 | mulcld 11180 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ0)
โ (2 ยท ๐)
โ โ) |
44 | | 1cnd 11155 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ0)
โ 1 โ โ) |
45 | 43, 44 | addcld 11179 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ0)
โ ((2 ยท ๐) + 1)
โ โ) |
46 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 2 โ
โ) |
47 | | nnre 12165 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ
โ) |
48 | 46, 47 | remulcld 11190 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
49 | | 1red 11161 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 1 โ
โ) |
50 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 0 โค
2) |
51 | | 0red 11163 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ 0 โ
โ) |
52 | | nngt0 12189 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ 0 <
๐) |
53 | 51, 47, 52 | ltled 11308 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 0 โค
๐) |
54 | 46, 47, 50, 53 | mulge0d 11737 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 0 โค (2
ยท ๐)) |
55 | 34 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 0 <
1) |
56 | 48, 49, 54, 55 | addgegt0d 11733 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ 0 <
((2 ยท ๐) +
1)) |
57 | 56 | gt0ne0d 11724 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
0) |
58 | 57 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ0)
โ ((2 ยท ๐) + 1)
โ 0) |
59 | 45, 58 | reccld 11929 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ0)
โ (1 / ((2 ยท ๐)
+ 1)) โ โ) |
60 | | 2nn0 12435 |
. . . . . . . . . . . . . . 15
โข 2 โ
โ0 |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ0)
โ 2 โ โ0) |
62 | 61, 16 | nn0mulcld 12483 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ0)
โ (2 ยท ๐)
โ โ0) |
63 | | 1nn0 12434 |
. . . . . . . . . . . . . 14
โข 1 โ
โ0 |
64 | 63 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ0)
โ 1 โ โ0) |
65 | 62, 64 | nn0addcld 12482 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ0)
โ ((2 ยท ๐) + 1)
โ โ0) |
66 | 59, 65 | expcld 14057 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ0)
โ ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1)) โ โ) |
67 | 40, 66 | mulcld 11180 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ0)
โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))) โ
โ) |
68 | 17, 67 | mulcld 11180 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ0)
โ (2 ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1)))) โ
โ) |
69 | 9, 15, 16, 68 | fvmptd3 6972 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ปโ๐) = (2 ยท ((1 / ((2
ยท ๐) + 1)) ยท
((1 / ((2 ยท ๐) +
1))โ((2 ยท ๐) +
1))))) |
70 | 69, 68 | eqeltrd 2834 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ปโ๐) โ
โ) |
71 | 9 | stirlinglem6 44406 |
. . . . . . 7
โข (๐ โ โ โ seq0( + ,
๐ป) โ
(logโ((๐ + 1) / ๐))) |
72 | 6, 8, 70, 71 | clim2ser 15545 |
. . . . . 6
โข (๐ โ โ โ seq(0 +
1)( + , ๐ป) โ
((logโ((๐ + 1) /
๐)) โ (seq0( + ,
๐ป)โ0))) |
73 | 5, 72 | eqbrtrd 5128 |
. . . . 5
โข (๐ โ โ โ seq1( + ,
๐ป) โ
((logโ((๐ + 1) /
๐)) โ (seq0( + ,
๐ป)โ0))) |
74 | | 0z 12515 |
. . . . . . . 8
โข 0 โ
โค |
75 | | seq1 13925 |
. . . . . . . 8
โข (0 โ
โค โ (seq0( + , ๐ป)โ0) = (๐ปโ0)) |
76 | 74, 75 | mp1i 13 |
. . . . . . 7
โข (๐ โ โ โ (seq0( +
, ๐ป)โ0) = (๐ปโ0)) |
77 | 9 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ ๐ป = (๐ โ โ0 โฆ (2
ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1)))))) |
78 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ = 0) โ ๐ = 0) |
79 | 78 | oveq2d 7374 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ = 0) โ (2 ยท ๐) = (2 ยท
0)) |
80 | 79 | oveq1d 7373 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ = 0) โ ((2 ยท ๐) + 1) = ((2 ยท 0) +
1)) |
81 | 80 | oveq2d 7374 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ = 0) โ (1 / ((2 ยท
๐) + 1)) = (1 / ((2
ยท 0) + 1))) |
82 | 80 | oveq2d 7374 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ = 0) โ ((1 / ((2 ยท
๐) + 1))โ((2 ยท
๐) + 1)) = ((1 / ((2
ยท ๐) + 1))โ((2
ยท 0) + 1))) |
83 | 81, 82 | oveq12d 7376 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ = 0) โ ((1 / ((2 ยท
๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) + 1))) = ((1 /
((2 ยท 0) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท 0) +
1)))) |
84 | 83 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ = 0) โ (2 ยท ((1 /
((2 ยท ๐) + 1))
ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1)))) = (2 ยท ((1 / ((2 ยท 0)
+ 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท 0) +
1))))) |
85 | | 2cnd 12236 |
. . . . . . . . 9
โข (๐ โ โ โ 2 โ
โ) |
86 | | 0cnd 11153 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ 0 โ
โ) |
87 | 85, 86 | mulcld 11180 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (2
ยท 0) โ โ) |
88 | | 1cnd 11155 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 1 โ
โ) |
89 | 87, 88 | addcld 11179 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((2
ยท 0) + 1) โ โ) |
90 | 85 | mul01d 11359 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (2
ยท 0) = 0) |
91 | 90 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ 0 = (2
ยท 0)) |
92 | 91 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (0 + 1) =
((2 ยท 0) + 1)) |
93 | 4, 92 | eqtrd 2773 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ 1 = ((2
ยท 0) + 1)) |
94 | 55, 93 | breqtrd 5132 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 0 <
((2 ยท 0) + 1)) |
95 | 94 | gt0ne0d 11724 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((2
ยท 0) + 1) โ 0) |
96 | 89, 95 | reccld 11929 |
. . . . . . . . . 10
โข (๐ โ โ โ (1 / ((2
ยท 0) + 1)) โ โ) |
97 | 85, 41 | mulcld 11180 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
98 | 97, 88 | addcld 11179 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
99 | 98, 57 | reccld 11929 |
. . . . . . . . . . 11
โข (๐ โ โ โ (1 / ((2
ยท ๐) + 1)) โ
โ) |
100 | 93, 63 | eqeltrrdi 2843 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((2
ยท 0) + 1) โ โ0) |
101 | 99, 100 | expcld 14057 |
. . . . . . . . . 10
โข (๐ โ โ โ ((1 / ((2
ยท ๐) + 1))โ((2
ยท 0) + 1)) โ โ) |
102 | 96, 101 | mulcld 11180 |
. . . . . . . . 9
โข (๐ โ โ โ ((1 / ((2
ยท 0) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท 0) + 1))) โ
โ) |
103 | 85, 102 | mulcld 11180 |
. . . . . . . 8
โข (๐ โ โ โ (2
ยท ((1 / ((2 ยท 0) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท 0) +
1)))) โ โ) |
104 | 77, 84, 8, 103 | fvmptd 6956 |
. . . . . . 7
โข (๐ โ โ โ (๐ปโ0) = (2 ยท ((1 /
((2 ยท 0) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท 0) +
1))))) |
105 | 90 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((2
ยท 0) + 1) = (0 + 1)) |
106 | 105, 3 | eqtr4di 2791 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((2
ยท 0) + 1) = 1) |
107 | 106 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (1 / ((2
ยท 0) + 1)) = (1 / 1)) |
108 | 88 | div1d 11928 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (1 / 1) =
1) |
109 | 107, 108 | eqtrd 2773 |
. . . . . . . . . . 11
โข (๐ โ โ โ (1 / ((2
ยท 0) + 1)) = 1) |
110 | 106 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((1 / ((2
ยท ๐) + 1))โ((2
ยท 0) + 1)) = ((1 / ((2 ยท ๐) + 1))โ1)) |
111 | 99 | exp1d 14052 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((1 / ((2
ยท ๐) + 1))โ1) =
(1 / ((2 ยท ๐) +
1))) |
112 | 110, 111 | eqtrd 2773 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((1 / ((2
ยท ๐) + 1))โ((2
ยท 0) + 1)) = (1 / ((2 ยท ๐) + 1))) |
113 | 109, 112 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ โ โ โ ((1 / ((2
ยท 0) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท 0) + 1))) = (1
ยท (1 / ((2 ยท ๐) + 1)))) |
114 | 99 | mulid2d 11178 |
. . . . . . . . . 10
โข (๐ โ โ โ (1
ยท (1 / ((2 ยท ๐) + 1))) = (1 / ((2 ยท ๐) + 1))) |
115 | 113, 114 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ โ โ ((1 / ((2
ยท 0) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท 0) + 1))) = (1 /
((2 ยท ๐) +
1))) |
116 | 115 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ โ โ (2
ยท ((1 / ((2 ยท 0) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท 0) +
1)))) = (2 ยท (1 / ((2 ยท ๐) + 1)))) |
117 | 85, 88, 98, 57 | divassd 11971 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท 1) / ((2 ยท ๐) + 1)) = (2 ยท (1 / ((2 ยท
๐) + 1)))) |
118 | 85 | mulid1d 11177 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท 1) = 2) |
119 | 118 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท 1) / ((2 ยท ๐) + 1)) = (2 / ((2 ยท ๐) + 1))) |
120 | 116, 117,
119 | 3eqtr2d 2779 |
. . . . . . 7
โข (๐ โ โ โ (2
ยท ((1 / ((2 ยท 0) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท 0) +
1)))) = (2 / ((2 ยท ๐) + 1))) |
121 | 76, 104, 120 | 3eqtrd 2777 |
. . . . . 6
โข (๐ โ โ โ (seq0( +
, ๐ป)โ0) = (2 / ((2
ยท ๐) +
1))) |
122 | 121 | oveq2d 7374 |
. . . . 5
โข (๐ โ โ โ
((logโ((๐ + 1) /
๐)) โ (seq0( + ,
๐ป)โ0)) =
((logโ((๐ + 1) /
๐)) โ (2 / ((2
ยท ๐) +
1)))) |
123 | 73, 122 | breqtrd 5132 |
. . . 4
โข (๐ โ โ โ seq1( + ,
๐ป) โ
((logโ((๐ + 1) /
๐)) โ (2 / ((2
ยท ๐) +
1)))) |
124 | 88, 97 | addcld 11179 |
. . . . 5
โข (๐ โ โ โ (1 + (2
ยท ๐)) โ
โ) |
125 | 124 | halfcld 12403 |
. . . 4
โข (๐ โ โ โ ((1 + (2
ยท ๐)) / 2) โ
โ) |
126 | | seqex 13914 |
. . . . 5
โข seq1( + ,
๐พ) โ
V |
127 | 126 | a1i 11 |
. . . 4
โข (๐ โ โ โ seq1( + ,
๐พ) โ
V) |
128 | | elnnuz 12812 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
129 | 128 | biimpi 215 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
130 | 129 | adantl 483 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
(โคโฅโ1)) |
131 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
132 | 131 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((2 ยท ๐) + 1) = ((2 ยท ๐) + 1)) |
133 | 132 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ = ๐ โ (1 / ((2 ยท ๐) + 1)) = (1 / ((2 ยท ๐) + 1))) |
134 | 132 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ = ๐ โ ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1)) = ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))) |
135 | 133, 134 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = ๐ โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))) = ((1 / ((2 ยท
๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) +
1)))) |
136 | 135 | oveq2d 7374 |
. . . . . . 7
โข (๐ = ๐ โ (2 ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) + 1)))) = (2
ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))))) |
137 | | elfzuz 13443 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ ๐ โ
(โคโฅโ1)) |
138 | | elnnuz 12812 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
139 | 138 | biimpri 227 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ1) โ ๐ โ โ) |
140 | | nnnn0 12425 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ0) |
141 | 137, 139,
140 | 3syl 18 |
. . . . . . . 8
โข (๐ โ (1...๐) โ ๐ โ โ0) |
142 | 141 | adantl 483 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ๐ โ โ0) |
143 | | 2cnd 12236 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ 2 โ โ) |
144 | 142 | nn0cnd 12480 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ๐ โ โ) |
145 | 143, 144 | mulcld 11180 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (2 ยท ๐) โ โ) |
146 | | 1cnd 11155 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ 1 โ โ) |
147 | 145, 146 | addcld 11179 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ โ) |
148 | | elfznn 13476 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ ๐ โ โ) |
149 | | 0red 11163 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ 0 โ
โ) |
150 | | 1red 11161 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ 1 โ
โ) |
151 | 25 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 2 โ
โ) |
152 | | nnre 12165 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โ) |
153 | 151, 152 | remulcld 11190 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
154 | 153, 150 | readdcld 11189 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
155 | 34 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ 0 <
1) |
156 | | 2rp 12925 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ+ |
157 | 156 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 2 โ
โ+) |
158 | | nnrp 12931 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โ+) |
159 | 157, 158 | rpmulcld 12978 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (2
ยท ๐) โ
โ+) |
160 | 150, 159 | ltaddrp2d 12996 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ 1 <
((2 ยท ๐) +
1)) |
161 | 149, 150,
154, 155, 160 | lttrd 11321 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ 0 <
((2 ยท ๐) +
1)) |
162 | 161 | gt0ne0d 11724 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
0) |
163 | 148, 162 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ ((2 ยท ๐) + 1) โ 0) |
164 | 163 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ 0) |
165 | 147, 164 | reccld 11929 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (1 / ((2 ยท ๐) + 1)) โ
โ) |
166 | 99 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (1 / ((2 ยท ๐) + 1)) โ โ) |
167 | 60 | a1i 11 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ 2 โ
โ0) |
168 | 167, 142 | nn0mulcld 12483 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (2 ยท ๐) โ
โ0) |
169 | 63 | a1i 11 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ 1 โ
โ0) |
170 | 168, 169 | nn0addcld 12482 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ
โ0) |
171 | 166, 170 | expcld 14057 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1)) โ
โ) |
172 | 165, 171 | mulcld 11180 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) + 1))) โ
โ) |
173 | 143, 172 | mulcld 11180 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (2 ยท ((1 / ((2 ยท
๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) + 1)))) โ
โ) |
174 | 9, 136, 142, 173 | fvmptd3 6972 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (๐ปโ๐) = (2 ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) +
1))))) |
175 | 174, 173 | eqeltrd 2834 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (๐ปโ๐) โ โ) |
176 | | addcl 11138 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + ๐) โ โ) |
177 | 176 | adantl 483 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ + ๐) โ โ) |
178 | 130, 175,
177 | seqcl 13934 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (seq1( +
, ๐ป)โ๐) โ
โ) |
179 | | 1cnd 11155 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ 1
โ โ) |
180 | | 2cnd 12236 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ 2
โ โ) |
181 | 41 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
182 | 180, 181 | mulcld 11180 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (2
ยท ๐) โ
โ) |
183 | 179, 182 | addcld 11179 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (1 + (2
ยท ๐)) โ
โ) |
184 | 183 | halfcld 12403 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((1 +
(2 ยท ๐)) / 2) โ
โ) |
185 | | simprl 770 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
186 | | simprr 772 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
187 | 184, 185,
186 | adddid 11184 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (((1 +
(2 ยท ๐)) / 2)
ยท (๐ + ๐)) = ((((1 + (2 ยท ๐)) / 2) ยท ๐) + (((1 + (2 ยท ๐)) / 2) ยท ๐))) |
188 | | stirlinglem7.2 |
. . . . . . 7
โข ๐พ = (๐ โ โ โฆ ((1 / ((2 ยท
๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ(2
ยท ๐)))) |
189 | 131 | oveq2d 7374 |
. . . . . . . 8
โข (๐ = ๐ โ ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)) = ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐))) |
190 | 133, 189 | oveq12d 7376 |
. . . . . . 7
โข (๐ = ๐ โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐))) = ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ(2
ยท ๐)))) |
191 | 148 | adantl 483 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ๐ โ โ) |
192 | 166, 168 | expcld 14057 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)) โ
โ) |
193 | 165, 192 | mulcld 11180 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ(2
ยท ๐))) โ
โ) |
194 | 188, 190,
191, 193 | fvmptd3 6972 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (๐พโ๐) = ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)))) |
195 | 124 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (1 + (2 ยท ๐)) โ โ) |
196 | | 2ne0 12262 |
. . . . . . . . 9
โข 2 โ
0 |
197 | 196 | a1i 11 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ 2 โ 0) |
198 | 195, 143,
173, 197 | div32d 11959 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((1 + (2 ยท ๐)) / 2) ยท (2 ยท ((1
/ ((2 ยท ๐) + 1))
ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))))) = ((1 + (2 ยท ๐)) ยท ((2 ยท ((1 /
((2 ยท ๐) + 1))
ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1)))) / 2))) |
199 | 172, 143,
197 | divcan3d 11941 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((2 ยท ((1 / ((2 ยท
๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) + 1)))) / 2) =
((1 / ((2 ยท ๐) + 1))
ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1)))) |
200 | 199 | oveq2d 7374 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 + (2 ยท ๐)) ยท ((2 ยท ((1 / ((2 ยท
๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) + 1)))) / 2)) =
((1 + (2 ยท ๐))
ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))))) |
201 | 195, 165,
171 | mul12d 11369 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 + (2 ยท ๐)) ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) + 1)))) = ((1 /
((2 ยท ๐) + 1))
ยท ((1 + (2 ยท ๐)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))))) |
202 | 98 | ad2antrr 725 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ โ) |
203 | 57 | ad2antrr 725 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ 0) |
204 | 170 | nn0zd 12530 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((2 ยท ๐) + 1) โ โค) |
205 | 202, 203,
204 | exprecd 14065 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1)) = (1 / (((2 ยท
๐) + 1)โ((2 ยท
๐) + 1)))) |
206 | 205 | oveq2d 7374 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 + (2 ยท ๐)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))) = ((1 + (2 ยท
๐)) ยท (1 / (((2
ยท ๐) + 1)โ((2
ยท ๐) +
1))))) |
207 | 202, 170 | expcld 14057 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((2 ยท ๐) + 1)โ((2 ยท ๐) + 1)) โ โ) |
208 | 202, 203,
204 | expne0d 14063 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((2 ยท ๐) + 1)โ((2 ยท ๐) + 1)) โ 0) |
209 | 195, 207,
208 | divrecd 11939 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 + (2 ยท ๐)) / (((2 ยท ๐) + 1)โ((2 ยท ๐) + 1))) = ((1 + (2 ยท ๐)) ยท (1 / (((2 ยท
๐) + 1)โ((2 ยท
๐) +
1))))) |
210 | 41 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ๐ โ โ) |
211 | 143, 210 | mulcld 11180 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (2 ยท ๐) โ โ) |
212 | 146, 211 | addcomd 11362 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (1 + (2 ยท ๐)) = ((2 ยท ๐) + 1)) |
213 | 202, 168 | expcld 14057 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((2 ยท ๐) + 1)โ(2 ยท ๐)) โ โ) |
214 | 213, 202 | mulcomd 11181 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((((2 ยท ๐) + 1)โ(2 ยท ๐)) ยท ((2 ยท ๐) + 1)) = (((2 ยท ๐) + 1) ยท (((2 ยท ๐) + 1)โ(2 ยท ๐)))) |
215 | 212, 214 | oveq12d 7376 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 + (2 ยท ๐)) / ((((2 ยท ๐) + 1)โ(2 ยท ๐)) ยท ((2 ยท ๐) + 1))) = (((2 ยท ๐) + 1) / (((2 ยท ๐) + 1) ยท (((2 ยท ๐) + 1)โ(2 ยท ๐))))) |
216 | 202, 168 | expp1d 14058 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((2 ยท ๐) + 1)โ((2 ยท ๐) + 1)) = ((((2 ยท ๐) + 1)โ(2 ยท ๐)) ยท ((2 ยท ๐) + 1))) |
217 | 216 | oveq2d 7374 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 + (2 ยท ๐)) / (((2 ยท ๐) + 1)โ((2 ยท ๐) + 1))) = ((1 + (2 ยท ๐)) / ((((2 ยท ๐) + 1)โ(2 ยท ๐)) ยท ((2 ยท ๐) + 1)))) |
218 | | 2z 12540 |
. . . . . . . . . . . . . . 15
โข 2 โ
โค |
219 | 218 | a1i 11 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ 2 โ โค) |
220 | 142 | nn0zd 12530 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ๐ โ โค) |
221 | 219, 220 | zmulcld 12618 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (2 ยท ๐) โ โค) |
222 | 202, 203,
221 | expne0d 14063 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((2 ยท ๐) + 1)โ(2 ยท ๐)) โ 0) |
223 | 202, 202,
213, 203, 222 | divdiv1d 11967 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((((2 ยท ๐) + 1) / ((2 ยท ๐) + 1)) / (((2 ยท ๐) + 1)โ(2 ยท ๐))) = (((2 ยท ๐) + 1) / (((2 ยท ๐) + 1) ยท (((2 ยท ๐) + 1)โ(2 ยท ๐))))) |
224 | 215, 217,
223 | 3eqtr4d 2783 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 + (2 ยท ๐)) / (((2 ยท ๐) + 1)โ((2 ยท ๐) + 1))) = ((((2 ยท ๐) + 1) / ((2 ยท ๐) + 1)) / (((2 ยท ๐) + 1)โ(2 ยท ๐)))) |
225 | 206, 209,
224 | 3eqtr2d 2779 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 + (2 ยท ๐)) ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))) = ((((2 ยท ๐) + 1) / ((2 ยท ๐) + 1)) / (((2 ยท ๐) + 1)โ(2 ยท ๐)))) |
226 | 225 | oveq2d 7374 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1)) ยท ((1 + (2
ยท ๐)) ยท ((1 /
((2 ยท ๐) +
1))โ((2 ยท ๐) +
1)))) = ((1 / ((2 ยท ๐) + 1)) ยท ((((2 ยท ๐) + 1) / ((2 ยท ๐) + 1)) / (((2 ยท ๐) + 1)โ(2 ยท ๐))))) |
227 | 202, 203 | dividd 11934 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((2 ยท ๐) + 1) / ((2 ยท ๐) + 1)) = 1) |
228 | | 1exp 14003 |
. . . . . . . . . . . . 13
โข ((2
ยท ๐) โ โค
โ (1โ(2 ยท ๐)) = 1) |
229 | 221, 228 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (1โ(2 ยท ๐)) = 1) |
230 | 227, 229 | eqtr4d 2776 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((2 ยท ๐) + 1) / ((2 ยท ๐) + 1)) = (1โ(2 ยท ๐))) |
231 | 230 | oveq1d 7373 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((((2 ยท ๐) + 1) / ((2 ยท ๐) + 1)) / (((2 ยท ๐) + 1)โ(2 ยท ๐))) = ((1โ(2 ยท ๐)) / (((2 ยท ๐) + 1)โ(2 ยท ๐)))) |
232 | 146, 202,
203, 168 | expdivd 14071 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)) = ((1โ(2 ยท ๐)) / (((2 ยท ๐) + 1)โ(2 ยท ๐)))) |
233 | 231, 232 | eqtr4d 2776 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((((2 ยท ๐) + 1) / ((2 ยท ๐) + 1)) / (((2 ยท ๐) + 1)โ(2 ยท ๐))) = ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐))) |
234 | 233 | oveq2d 7374 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 / ((2 ยท ๐) + 1)) ยท ((((2 ยท
๐) + 1) / ((2 ยท
๐) + 1)) / (((2 ยท
๐) + 1)โ(2 ยท
๐)))) = ((1 / ((2 ยท
๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ(2
ยท ๐)))) |
235 | 201, 226,
234 | 3eqtrd 2777 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((1 + (2 ยท ๐)) ยท ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) + 1)))) = ((1 /
((2 ยท ๐) + 1))
ยท ((1 / ((2 ยท ๐) + 1))โ(2 ยท ๐)))) |
236 | 198, 200,
235 | 3eqtrd 2777 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((1 + (2 ยท ๐)) / 2) ยท (2 ยท ((1
/ ((2 ยท ๐) + 1))
ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))))) = ((1 / ((2 ยท ๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ(2
ยท ๐)))) |
237 | 174 | eqcomd 2739 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (2 ยท ((1 / ((2 ยท
๐) + 1)) ยท ((1 / ((2
ยท ๐) + 1))โ((2
ยท ๐) + 1)))) =
(๐ปโ๐)) |
238 | 237 | oveq2d 7374 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((1 + (2 ยท ๐)) / 2) ยท (2 ยท ((1
/ ((2 ยท ๐) + 1))
ยท ((1 / ((2 ยท ๐) + 1))โ((2 ยท ๐) + 1))))) = (((1 + (2 ยท ๐)) / 2) ยท (๐ปโ๐))) |
239 | 194, 236,
238 | 3eqtr2d 2779 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (๐พโ๐) = (((1 + (2 ยท ๐)) / 2) ยท (๐ปโ๐))) |
240 | 177, 187,
130, 175, 239 | seqdistr 13965 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (seq1( +
, ๐พ)โ๐) = (((1 + (2 ยท ๐)) / 2) ยท (seq1( + ,
๐ป)โ๐))) |
241 | 1, 2, 123, 125, 127, 178, 240 | climmulc2 15525 |
. . 3
โข (๐ โ โ โ seq1( + ,
๐พ) โ (((1 + (2
ยท ๐)) / 2) ยท
((logโ((๐ + 1) /
๐)) โ (2 / ((2
ยท ๐) +
1))))) |
242 | 88, 97 | addcomd 11362 |
. . . . . 6
โข (๐ โ โ โ (1 + (2
ยท ๐)) = ((2 ยท
๐) + 1)) |
243 | 242 | oveq1d 7373 |
. . . . 5
โข (๐ โ โ โ ((1 + (2
ยท ๐)) / 2) = (((2
ยท ๐) + 1) /
2)) |
244 | 243 | oveq1d 7373 |
. . . 4
โข (๐ โ โ โ (((1 + (2
ยท ๐)) / 2) ยท
((logโ((๐ + 1) /
๐)) โ (2 / ((2
ยท ๐) + 1)))) = ((((2
ยท ๐) + 1) / 2)
ยท ((logโ((๐ +
1) / ๐)) โ (2 / ((2
ยท ๐) +
1))))) |
245 | 243, 125 | eqeltrrd 2835 |
. . . . 5
โข (๐ โ โ โ (((2
ยท ๐) + 1) / 2)
โ โ) |
246 | 41, 88 | addcld 11179 |
. . . . . . 7
โข (๐ โ โ โ (๐ + 1) โ
โ) |
247 | | nnne0 12192 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ 0) |
248 | 246, 41, 247 | divcld 11936 |
. . . . . 6
โข (๐ โ โ โ ((๐ + 1) / ๐) โ โ) |
249 | 47, 49 | readdcld 11189 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ + 1) โ
โ) |
250 | 47 | ltp1d 12090 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ < (๐ + 1)) |
251 | 51, 47, 249, 52, 250 | lttrd 11321 |
. . . . . . . 8
โข (๐ โ โ โ 0 <
(๐ + 1)) |
252 | 251 | gt0ne0d 11724 |
. . . . . . 7
โข (๐ โ โ โ (๐ + 1) โ 0) |
253 | 246, 41, 252, 247 | divne0d 11952 |
. . . . . 6
โข (๐ โ โ โ ((๐ + 1) / ๐) โ 0) |
254 | 248, 253 | logcld 25942 |
. . . . 5
โข (๐ โ โ โ
(logโ((๐ + 1) / ๐)) โ
โ) |
255 | 85, 98, 57 | divcld 11936 |
. . . . 5
โข (๐ โ โ โ (2 / ((2
ยท ๐) + 1)) โ
โ) |
256 | 245, 254,
255 | subdid 11616 |
. . . 4
โข (๐ โ โ โ ((((2
ยท ๐) + 1) / 2)
ยท ((logโ((๐ +
1) / ๐)) โ (2 / ((2
ยท ๐) + 1)))) =
(((((2 ยท ๐) + 1) /
2) ยท (logโ((๐
+ 1) / ๐))) โ ((((2
ยท ๐) + 1) / 2)
ยท (2 / ((2 ยท ๐) + 1))))) |
257 | 97, 88 | addcomd 11362 |
. . . . . . 7
โข (๐ โ โ โ ((2
ยท ๐) + 1) = (1 + (2
ยท ๐))) |
258 | 257 | oveq1d 7373 |
. . . . . 6
โข (๐ โ โ โ (((2
ยท ๐) + 1) / 2) = ((1
+ (2 ยท ๐)) /
2)) |
259 | 258 | oveq1d 7373 |
. . . . 5
โข (๐ โ โ โ ((((2
ยท ๐) + 1) / 2)
ยท (logโ((๐ +
1) / ๐))) = (((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐)))) |
260 | 196 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ 2 โ
0) |
261 | 98, 85, 57, 260 | divcan6d 11955 |
. . . . 5
โข (๐ โ โ โ ((((2
ยท ๐) + 1) / 2)
ยท (2 / ((2 ยท ๐) + 1))) = 1) |
262 | 259, 261 | oveq12d 7376 |
. . . 4
โข (๐ โ โ โ (((((2
ยท ๐) + 1) / 2)
ยท (logโ((๐ +
1) / ๐))) โ ((((2
ยท ๐) + 1) / 2)
ยท (2 / ((2 ยท ๐) + 1)))) = ((((1 + (2 ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1)) |
263 | 244, 256,
262 | 3eqtrd 2777 |
. . 3
โข (๐ โ โ โ (((1 + (2
ยท ๐)) / 2) ยท
((logโ((๐ + 1) /
๐)) โ (2 / ((2
ยท ๐) + 1)))) = ((((1
+ (2 ยท ๐)) / 2)
ยท (logโ((๐ +
1) / ๐))) โ
1)) |
264 | 241, 263 | breqtrd 5132 |
. 2
โข (๐ โ โ โ seq1( + ,
๐พ) โ ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1)) |
265 | | stirlinglem7.1 |
. . 3
โข ๐ฝ = (๐ โ โ โฆ ((((1 + (2 ยท
๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1)) |
266 | | oveq2 7366 |
. . . . . . 7
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
267 | 266 | oveq2d 7374 |
. . . . . 6
โข (๐ = ๐ โ (1 + (2 ยท ๐)) = (1 + (2 ยท ๐))) |
268 | 267 | oveq1d 7373 |
. . . . 5
โข (๐ = ๐ โ ((1 + (2 ยท ๐)) / 2) = ((1 + (2 ยท ๐)) / 2)) |
269 | | oveq1 7365 |
. . . . . . 7
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
270 | | id 22 |
. . . . . . 7
โข (๐ = ๐ โ ๐ = ๐) |
271 | 269, 270 | oveq12d 7376 |
. . . . . 6
โข (๐ = ๐ โ ((๐ + 1) / ๐) = ((๐ + 1) / ๐)) |
272 | 271 | fveq2d 6847 |
. . . . 5
โข (๐ = ๐ โ (logโ((๐ + 1) / ๐)) = (logโ((๐ + 1) / ๐))) |
273 | 268, 272 | oveq12d 7376 |
. . . 4
โข (๐ = ๐ โ (((1 + (2 ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) = (((1 + (2 ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐)))) |
274 | 273 | oveq1d 7373 |
. . 3
โข (๐ = ๐ โ ((((1 + (2 ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) = ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1)) |
275 | | id 22 |
. . 3
โข (๐ โ โ โ ๐ โ
โ) |
276 | 125, 254 | mulcld 11180 |
. . . 4
โข (๐ โ โ โ (((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ
โ) |
277 | 276, 88 | subcld 11517 |
. . 3
โข (๐ โ โ โ ((((1 +
(2 ยท ๐)) / 2)
ยท (logโ((๐ +
1) / ๐))) โ 1) โ
โ) |
278 | 265, 274,
275, 277 | fvmptd3 6972 |
. 2
โข (๐ โ โ โ (๐ฝโ๐) = ((((1 + (2 ยท ๐)) / 2) ยท (logโ((๐ + 1) / ๐))) โ 1)) |
279 | 264, 278 | breqtrrd 5134 |
1
โข (๐ โ โ โ seq1( + ,
๐พ) โ (๐ฝโ๐)) |