Step |
Hyp |
Ref |
Expression |
1 |
|
stirlinglem11.1 |
โข ๐ด = ( ๐ โ โ โฆ ( ( ! โ ๐ ) / ( ( โ โ ( 2 ยท ๐ ) ) ยท ( ( ๐ / e ) โ ๐ ) ) ) ) |
2 |
|
stirlinglem11.2 |
โข ๐ต = ( ๐ โ โ โฆ ( log โ ( ๐ด โ ๐ ) ) ) |
3 |
|
stirlinglem11.3 |
โข ๐พ = ( ๐ โ โ โฆ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) ) |
4 |
|
0red |
โข ( ๐ โ โ โ 0 โ โ ) |
5 |
3
|
a1i |
โข ( ๐ โ โ โ ๐พ = ( ๐ โ โ โฆ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) ) ) |
6 |
|
simpr |
โข ( ( ๐ โ โ โง ๐ = 1 ) โ ๐ = 1 ) |
7 |
6
|
oveq2d |
โข ( ( ๐ โ โ โง ๐ = 1 ) โ ( 2 ยท ๐ ) = ( 2 ยท 1 ) ) |
8 |
7
|
oveq1d |
โข ( ( ๐ โ โ โง ๐ = 1 ) โ ( ( 2 ยท ๐ ) + 1 ) = ( ( 2 ยท 1 ) + 1 ) ) |
9 |
8
|
oveq2d |
โข ( ( ๐ โ โ โง ๐ = 1 ) โ ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) = ( 1 / ( ( 2 ยท 1 ) + 1 ) ) ) |
10 |
7
|
oveq2d |
โข ( ( ๐ โ โ โง ๐ = 1 ) โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) = ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท 1 ) ) ) |
11 |
9 10
|
oveq12d |
โข ( ( ๐ โ โ โง ๐ = 1 ) โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) = ( ( 1 / ( ( 2 ยท 1 ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท 1 ) ) ) ) |
12 |
|
1nn |
โข 1 โ โ |
13 |
12
|
a1i |
โข ( ๐ โ โ โ 1 โ โ ) |
14 |
|
2cnd |
โข ( ๐ โ โ โ 2 โ โ ) |
15 |
|
1cnd |
โข ( ๐ โ โ โ 1 โ โ ) |
16 |
14 15
|
mulcld |
โข ( ๐ โ โ โ ( 2 ยท 1 ) โ โ ) |
17 |
16 15
|
addcld |
โข ( ๐ โ โ โ ( ( 2 ยท 1 ) + 1 ) โ โ ) |
18 |
|
2t1e2 |
โข ( 2 ยท 1 ) = 2 |
19 |
18
|
oveq1i |
โข ( ( 2 ยท 1 ) + 1 ) = ( 2 + 1 ) |
20 |
|
2p1e3 |
โข ( 2 + 1 ) = 3 |
21 |
19 20
|
eqtri |
โข ( ( 2 ยท 1 ) + 1 ) = 3 |
22 |
|
3ne0 |
โข 3 โ 0 |
23 |
21 22
|
eqnetri |
โข ( ( 2 ยท 1 ) + 1 ) โ 0 |
24 |
23
|
a1i |
โข ( ๐ โ โ โ ( ( 2 ยท 1 ) + 1 ) โ 0 ) |
25 |
17 24
|
reccld |
โข ( ๐ โ โ โ ( 1 / ( ( 2 ยท 1 ) + 1 ) ) โ โ ) |
26 |
|
nncn |
โข ( ๐ โ โ โ ๐ โ โ ) |
27 |
14 26
|
mulcld |
โข ( ๐ โ โ โ ( 2 ยท ๐ ) โ โ ) |
28 |
27 15
|
addcld |
โข ( ๐ โ โ โ ( ( 2 ยท ๐ ) + 1 ) โ โ ) |
29 |
|
1red |
โข ( ๐ โ โ โ 1 โ โ ) |
30 |
|
2re |
โข 2 โ โ |
31 |
30
|
a1i |
โข ( ๐ โ โ โ 2 โ โ ) |
32 |
|
nnre |
โข ( ๐ โ โ โ ๐ โ โ ) |
33 |
31 32
|
remulcld |
โข ( ๐ โ โ โ ( 2 ยท ๐ ) โ โ ) |
34 |
33 29
|
readdcld |
โข ( ๐ โ โ โ ( ( 2 ยท ๐ ) + 1 ) โ โ ) |
35 |
|
0lt1 |
โข 0 < 1 |
36 |
35
|
a1i |
โข ( ๐ โ โ โ 0 < 1 ) |
37 |
|
2rp |
โข 2 โ โ+ |
38 |
37
|
a1i |
โข ( ๐ โ โ โ 2 โ โ+ ) |
39 |
|
nnrp |
โข ( ๐ โ โ โ ๐ โ โ+ ) |
40 |
38 39
|
rpmulcld |
โข ( ๐ โ โ โ ( 2 ยท ๐ ) โ โ+ ) |
41 |
29 40
|
ltaddrp2d |
โข ( ๐ โ โ โ 1 < ( ( 2 ยท ๐ ) + 1 ) ) |
42 |
4 29 34 36 41
|
lttrd |
โข ( ๐ โ โ โ 0 < ( ( 2 ยท ๐ ) + 1 ) ) |
43 |
42
|
gt0ne0d |
โข ( ๐ โ โ โ ( ( 2 ยท ๐ ) + 1 ) โ 0 ) |
44 |
28 43
|
reccld |
โข ( ๐ โ โ โ ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ โ ) |
45 |
|
2nn0 |
โข 2 โ โ0 |
46 |
45
|
a1i |
โข ( ๐ โ โ โ 2 โ โ0 ) |
47 |
|
1nn0 |
โข 1 โ โ0 |
48 |
47
|
a1i |
โข ( ๐ โ โ โ 1 โ โ0 ) |
49 |
46 48
|
nn0mulcld |
โข ( ๐ โ โ โ ( 2 ยท 1 ) โ โ0 ) |
50 |
44 49
|
expcld |
โข ( ๐ โ โ โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท 1 ) ) โ โ ) |
51 |
25 50
|
mulcld |
โข ( ๐ โ โ โ ( ( 1 / ( ( 2 ยท 1 ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท 1 ) ) ) โ โ ) |
52 |
5 11 13 51
|
fvmptd |
โข ( ๐ โ โ โ ( ๐พ โ 1 ) = ( ( 1 / ( ( 2 ยท 1 ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท 1 ) ) ) ) |
53 |
|
1re |
โข 1 โ โ |
54 |
30 53
|
remulcli |
โข ( 2 ยท 1 ) โ โ |
55 |
54 53
|
readdcli |
โข ( ( 2 ยท 1 ) + 1 ) โ โ |
56 |
55 23
|
rereccli |
โข ( 1 / ( ( 2 ยท 1 ) + 1 ) ) โ โ |
57 |
56
|
a1i |
โข ( ๐ โ โ โ ( 1 / ( ( 2 ยท 1 ) + 1 ) ) โ โ ) |
58 |
34 43
|
rereccld |
โข ( ๐ โ โ โ ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ โ ) |
59 |
58 49
|
reexpcld |
โข ( ๐ โ โ โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท 1 ) ) โ โ ) |
60 |
57 59
|
remulcld |
โข ( ๐ โ โ โ ( ( 1 / ( ( 2 ยท 1 ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท 1 ) ) ) โ โ ) |
61 |
52 60
|
eqeltrd |
โข ( ๐ โ โ โ ( ๐พ โ 1 ) โ โ ) |
62 |
1
|
stirlinglem2 |
โข ( ๐ โ โ โ ( ๐ด โ ๐ ) โ โ+ ) |
63 |
62
|
relogcld |
โข ( ๐ โ โ โ ( log โ ( ๐ด โ ๐ ) ) โ โ ) |
64 |
|
nfcv |
โข โฒ ๐ ๐ |
65 |
|
nfcv |
โข โฒ ๐ log |
66 |
|
nfmpt1 |
โข โฒ ๐ ( ๐ โ โ โฆ ( ( ! โ ๐ ) / ( ( โ โ ( 2 ยท ๐ ) ) ยท ( ( ๐ / e ) โ ๐ ) ) ) ) |
67 |
1 66
|
nfcxfr |
โข โฒ ๐ ๐ด |
68 |
67 64
|
nffv |
โข โฒ ๐ ( ๐ด โ ๐ ) |
69 |
65 68
|
nffv |
โข โฒ ๐ ( log โ ( ๐ด โ ๐ ) ) |
70 |
|
2fveq3 |
โข ( ๐ = ๐ โ ( log โ ( ๐ด โ ๐ ) ) = ( log โ ( ๐ด โ ๐ ) ) ) |
71 |
64 69 70 2
|
fvmptf |
โข ( ( ๐ โ โ โง ( log โ ( ๐ด โ ๐ ) ) โ โ ) โ ( ๐ต โ ๐ ) = ( log โ ( ๐ด โ ๐ ) ) ) |
72 |
63 71
|
mpdan |
โข ( ๐ โ โ โ ( ๐ต โ ๐ ) = ( log โ ( ๐ด โ ๐ ) ) ) |
73 |
72 63
|
eqeltrd |
โข ( ๐ โ โ โ ( ๐ต โ ๐ ) โ โ ) |
74 |
|
peano2nn |
โข ( ๐ โ โ โ ( ๐ + 1 ) โ โ ) |
75 |
1
|
stirlinglem2 |
โข ( ( ๐ + 1 ) โ โ โ ( ๐ด โ ( ๐ + 1 ) ) โ โ+ ) |
76 |
74 75
|
syl |
โข ( ๐ โ โ โ ( ๐ด โ ( ๐ + 1 ) ) โ โ+ ) |
77 |
76
|
relogcld |
โข ( ๐ โ โ โ ( log โ ( ๐ด โ ( ๐ + 1 ) ) ) โ โ ) |
78 |
|
nfcv |
โข โฒ ๐ ( ๐ + 1 ) |
79 |
67 78
|
nffv |
โข โฒ ๐ ( ๐ด โ ( ๐ + 1 ) ) |
80 |
65 79
|
nffv |
โข โฒ ๐ ( log โ ( ๐ด โ ( ๐ + 1 ) ) ) |
81 |
|
2fveq3 |
โข ( ๐ = ( ๐ + 1 ) โ ( log โ ( ๐ด โ ๐ ) ) = ( log โ ( ๐ด โ ( ๐ + 1 ) ) ) ) |
82 |
78 80 81 2
|
fvmptf |
โข ( ( ( ๐ + 1 ) โ โ โง ( log โ ( ๐ด โ ( ๐ + 1 ) ) ) โ โ ) โ ( ๐ต โ ( ๐ + 1 ) ) = ( log โ ( ๐ด โ ( ๐ + 1 ) ) ) ) |
83 |
74 77 82
|
syl2anc |
โข ( ๐ โ โ โ ( ๐ต โ ( ๐ + 1 ) ) = ( log โ ( ๐ด โ ( ๐ + 1 ) ) ) ) |
84 |
83 77
|
eqeltrd |
โข ( ๐ โ โ โ ( ๐ต โ ( ๐ + 1 ) ) โ โ ) |
85 |
73 84
|
resubcld |
โข ( ๐ โ โ โ ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) โ โ ) |
86 |
31 29
|
remulcld |
โข ( ๐ โ โ โ ( 2 ยท 1 ) โ โ ) |
87 |
|
0le2 |
โข 0 โค 2 |
88 |
87
|
a1i |
โข ( ๐ โ โ โ 0 โค 2 ) |
89 |
|
0le1 |
โข 0 โค 1 |
90 |
89
|
a1i |
โข ( ๐ โ โ โ 0 โค 1 ) |
91 |
31 29 88 90
|
mulge0d |
โข ( ๐ โ โ โ 0 โค ( 2 ยท 1 ) ) |
92 |
86 91
|
ge0p1rpd |
โข ( ๐ โ โ โ ( ( 2 ยท 1 ) + 1 ) โ โ+ ) |
93 |
92
|
rpreccld |
โข ( ๐ โ โ โ ( 1 / ( ( 2 ยท 1 ) + 1 ) ) โ โ+ ) |
94 |
39
|
rpge0d |
โข ( ๐ โ โ โ 0 โค ๐ ) |
95 |
31 32 88 94
|
mulge0d |
โข ( ๐ โ โ โ 0 โค ( 2 ยท ๐ ) ) |
96 |
33 95
|
ge0p1rpd |
โข ( ๐ โ โ โ ( ( 2 ยท ๐ ) + 1 ) โ โ+ ) |
97 |
96
|
rpreccld |
โข ( ๐ โ โ โ ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ โ+ ) |
98 |
|
2z |
โข 2 โ โค |
99 |
98
|
a1i |
โข ( ๐ โ โ โ 2 โ โค ) |
100 |
|
1z |
โข 1 โ โค |
101 |
100
|
a1i |
โข ( ๐ โ โ โ 1 โ โค ) |
102 |
99 101
|
zmulcld |
โข ( ๐ โ โ โ ( 2 ยท 1 ) โ โค ) |
103 |
97 102
|
rpexpcld |
โข ( ๐ โ โ โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท 1 ) ) โ โ+ ) |
104 |
93 103
|
rpmulcld |
โข ( ๐ โ โ โ ( ( 1 / ( ( 2 ยท 1 ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท 1 ) ) ) โ โ+ ) |
105 |
52 104
|
eqeltrd |
โข ( ๐ โ โ โ ( ๐พ โ 1 ) โ โ+ ) |
106 |
105
|
rpgt0d |
โข ( ๐ โ โ โ 0 < ( ๐พ โ 1 ) ) |
107 |
85 61
|
resubcld |
โข ( ๐ โ โ โ ( ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) โ ( ๐พ โ 1 ) ) โ โ ) |
108 |
|
eqid |
โข ( โคโฅ โ ( 1 + 1 ) ) = ( โคโฅ โ ( 1 + 1 ) ) |
109 |
101
|
peano2zd |
โข ( ๐ โ โ โ ( 1 + 1 ) โ โค ) |
110 |
|
nnuz |
โข โ = ( โคโฅ โ 1 ) |
111 |
3
|
a1i |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ๐พ = ( ๐ โ โ โฆ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) ) ) |
112 |
|
oveq2 |
โข ( ๐ = ๐ โ ( 2 ยท ๐ ) = ( 2 ยท ๐ ) ) |
113 |
112
|
oveq1d |
โข ( ๐ = ๐ โ ( ( 2 ยท ๐ ) + 1 ) = ( ( 2 ยท ๐ ) + 1 ) ) |
114 |
113
|
oveq2d |
โข ( ๐ = ๐ โ ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) = ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ) |
115 |
112
|
oveq2d |
โข ( ๐ = ๐ โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) = ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) |
116 |
114 115
|
oveq12d |
โข ( ๐ = ๐ โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) = ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) ) |
117 |
116
|
adantl |
โข ( ( ( ๐ โ โ โง ๐ โ โ ) โง ๐ = ๐ ) โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) = ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) ) |
118 |
|
simpr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ๐ โ โ ) |
119 |
|
2cnd |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ 2 โ โ ) |
120 |
|
nncn |
โข ( ๐ โ โ โ ๐ โ โ ) |
121 |
120
|
adantl |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ๐ โ โ ) |
122 |
119 121
|
mulcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 2 ยท ๐ ) โ โ ) |
123 |
|
1cnd |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ 1 โ โ ) |
124 |
122 123
|
addcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 2 ยท ๐ ) + 1 ) โ โ ) |
125 |
|
0red |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ 0 โ โ ) |
126 |
|
1red |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ 1 โ โ ) |
127 |
30
|
a1i |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ 2 โ โ ) |
128 |
|
nnre |
โข ( ๐ โ โ โ ๐ โ โ ) |
129 |
128
|
adantl |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ๐ โ โ ) |
130 |
127 129
|
remulcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 2 ยท ๐ ) โ โ ) |
131 |
130 126
|
readdcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 2 ยท ๐ ) + 1 ) โ โ ) |
132 |
35
|
a1i |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ 0 < 1 ) |
133 |
37
|
a1i |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ 2 โ โ+ ) |
134 |
|
nnrp |
โข ( ๐ โ โ โ ๐ โ โ+ ) |
135 |
134
|
adantl |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ๐ โ โ+ ) |
136 |
133 135
|
rpmulcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 2 ยท ๐ ) โ โ+ ) |
137 |
126 136
|
ltaddrp2d |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ 1 < ( ( 2 ยท ๐ ) + 1 ) ) |
138 |
125 126 131 132 137
|
lttrd |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ 0 < ( ( 2 ยท ๐ ) + 1 ) ) |
139 |
138
|
gt0ne0d |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 2 ยท ๐ ) + 1 ) โ 0 ) |
140 |
124 139
|
reccld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ โ ) |
141 |
26
|
adantr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ๐ โ โ ) |
142 |
119 141
|
mulcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 2 ยท ๐ ) โ โ ) |
143 |
142 123
|
addcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 2 ยท ๐ ) + 1 ) โ โ ) |
144 |
43
|
adantr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 2 ยท ๐ ) + 1 ) โ 0 ) |
145 |
143 144
|
reccld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ โ ) |
146 |
45
|
a1i |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ 2 โ โ0 ) |
147 |
|
nnnn0 |
โข ( ๐ โ โ โ ๐ โ โ0 ) |
148 |
147
|
adantl |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ๐ โ โ0 ) |
149 |
146 148
|
nn0mulcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 2 ยท ๐ ) โ โ0 ) |
150 |
145 149
|
expcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) โ โ ) |
151 |
140 150
|
mulcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) โ โ ) |
152 |
111 117 118 151
|
fvmptd |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ๐พ โ ๐ ) = ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) ) |
153 |
|
0red |
โข ( ๐ โ โ โ 0 โ โ ) |
154 |
|
1red |
โข ( ๐ โ โ โ 1 โ โ ) |
155 |
30
|
a1i |
โข ( ๐ โ โ โ 2 โ โ ) |
156 |
155 128
|
remulcld |
โข ( ๐ โ โ โ ( 2 ยท ๐ ) โ โ ) |
157 |
156 154
|
readdcld |
โข ( ๐ โ โ โ ( ( 2 ยท ๐ ) + 1 ) โ โ ) |
158 |
35
|
a1i |
โข ( ๐ โ โ โ 0 < 1 ) |
159 |
37
|
a1i |
โข ( ๐ โ โ โ 2 โ โ+ ) |
160 |
159 134
|
rpmulcld |
โข ( ๐ โ โ โ ( 2 ยท ๐ ) โ โ+ ) |
161 |
154 160
|
ltaddrp2d |
โข ( ๐ โ โ โ 1 < ( ( 2 ยท ๐ ) + 1 ) ) |
162 |
153 154 157 158 161
|
lttrd |
โข ( ๐ โ โ โ 0 < ( ( 2 ยท ๐ ) + 1 ) ) |
163 |
162
|
gt0ne0d |
โข ( ๐ โ โ โ ( ( 2 ยท ๐ ) + 1 ) โ 0 ) |
164 |
163
|
adantl |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 2 ยท ๐ ) + 1 ) โ 0 ) |
165 |
124 164
|
reccld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ โ ) |
166 |
165 150
|
mulcld |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) โ โ ) |
167 |
152 166
|
eqeltrd |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ๐พ โ ๐ ) โ โ ) |
168 |
|
eqid |
โข ( ๐ โ โ โฆ ( ( ( ( 1 + ( 2 ยท ๐ ) ) / 2 ) ยท ( log โ ( ( ๐ + 1 ) / ๐ ) ) ) โ 1 ) ) = ( ๐ โ โ โฆ ( ( ( ( 1 + ( 2 ยท ๐ ) ) / 2 ) ยท ( log โ ( ( ๐ + 1 ) / ๐ ) ) ) โ 1 ) ) |
169 |
1 2 168 3
|
stirlinglem9 |
โข ( ๐ โ โ โ seq 1 ( + , ๐พ ) โ ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) ) |
170 |
110 13 167 169
|
clim2ser |
โข ( ๐ โ โ โ seq ( 1 + 1 ) ( + , ๐พ ) โ ( ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) โ ( seq 1 ( + , ๐พ ) โ 1 ) ) ) |
171 |
|
peano2nn |
โข ( 1 โ โ โ ( 1 + 1 ) โ โ ) |
172 |
|
uznnssnn |
โข ( ( 1 + 1 ) โ โ โ ( โคโฅ โ ( 1 + 1 ) ) โ โ ) |
173 |
12 171 172
|
mp2b |
โข ( โคโฅ โ ( 1 + 1 ) ) โ โ |
174 |
173
|
a1i |
โข ( ๐ โ โ โ ( โคโฅ โ ( 1 + 1 ) ) โ โ ) |
175 |
174
|
sseld |
โข ( ๐ โ โ โ ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ ๐ โ โ ) ) |
176 |
175
|
imdistani |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( ๐ โ โ โง ๐ โ โ ) ) |
177 |
176 152
|
syl |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( ๐พ โ ๐ ) = ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) ) |
178 |
30
|
a1i |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ 2 โ โ ) |
179 |
|
eluzelre |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ ๐ โ โ ) |
180 |
178 179
|
remulcld |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ ( 2 ยท ๐ ) โ โ ) |
181 |
|
1red |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ 1 โ โ ) |
182 |
180 181
|
readdcld |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ ( ( 2 ยท ๐ ) + 1 ) โ โ ) |
183 |
173
|
sseli |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ ๐ โ โ ) |
184 |
183 163
|
syl |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ ( ( 2 ยท ๐ ) + 1 ) โ 0 ) |
185 |
182 184
|
rereccld |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ โ ) |
186 |
185
|
adantl |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ โ ) |
187 |
34
|
adantr |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( ( 2 ยท ๐ ) + 1 ) โ โ ) |
188 |
43
|
adantr |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( ( 2 ยท ๐ ) + 1 ) โ 0 ) |
189 |
187 188
|
rereccld |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ โ ) |
190 |
176 149
|
syl |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( 2 ยท ๐ ) โ โ0 ) |
191 |
189 190
|
reexpcld |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) โ โ ) |
192 |
186 191
|
remulcld |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) โ โ ) |
193 |
177 192
|
eqeltrd |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( ๐พ โ ๐ ) โ โ ) |
194 |
|
1red |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 1 โ โ ) |
195 |
30
|
a1i |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 2 โ โ ) |
196 |
176 129
|
syl |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ๐ โ โ ) |
197 |
195 196
|
remulcld |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( 2 ยท ๐ ) โ โ ) |
198 |
87
|
a1i |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 0 โค 2 ) |
199 |
|
0red |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ 0 โ โ ) |
200 |
87
|
a1i |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ 0 โค 2 ) |
201 |
|
1p1e2 |
โข ( 1 + 1 ) = 2 |
202 |
|
eluzle |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ ( 1 + 1 ) โค ๐ ) |
203 |
201 202
|
eqbrtrrid |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ 2 โค ๐ ) |
204 |
199 178 179 200 203
|
letrd |
โข ( ๐ โ ( โคโฅ โ ( 1 + 1 ) ) โ 0 โค ๐ ) |
205 |
204
|
adantl |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 0 โค ๐ ) |
206 |
195 196 198 205
|
mulge0d |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 0 โค ( 2 ยท ๐ ) ) |
207 |
197 206
|
ge0p1rpd |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( ( 2 ยท ๐ ) + 1 ) โ โ+ ) |
208 |
89
|
a1i |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 0 โค 1 ) |
209 |
194 207 208
|
divge0d |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 0 โค ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ) |
210 |
32
|
adantr |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ๐ โ โ ) |
211 |
195 210
|
remulcld |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( 2 ยท ๐ ) โ โ ) |
212 |
94
|
adantr |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 0 โค ๐ ) |
213 |
195 210 198 212
|
mulge0d |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 0 โค ( 2 ยท ๐ ) ) |
214 |
211 213
|
ge0p1rpd |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ ( ( 2 ยท ๐ ) + 1 ) โ โ+ ) |
215 |
194 214 208
|
divge0d |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 0 โค ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ) |
216 |
189 190 215
|
expge0d |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 0 โค ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) |
217 |
186 191 209 216
|
mulge0d |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 0 โค ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) ยท ( ( 1 / ( ( 2 ยท ๐ ) + 1 ) ) โ ( 2 ยท ๐ ) ) ) ) |
218 |
217 177
|
breqtrrd |
โข ( ( ๐ โ โ โง ๐ โ ( โคโฅ โ ( 1 + 1 ) ) ) โ 0 โค ( ๐พ โ ๐ ) ) |
219 |
108 109 170 193 218
|
iserge0 |
โข ( ๐ โ โ โ 0 โค ( ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) โ ( seq 1 ( + , ๐พ ) โ 1 ) ) ) |
220 |
|
seq1 |
โข ( 1 โ โค โ ( seq 1 ( + , ๐พ ) โ 1 ) = ( ๐พ โ 1 ) ) |
221 |
100 220
|
mp1i |
โข ( ๐ โ โ โ ( seq 1 ( + , ๐พ ) โ 1 ) = ( ๐พ โ 1 ) ) |
222 |
221
|
oveq2d |
โข ( ๐ โ โ โ ( ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) โ ( seq 1 ( + , ๐พ ) โ 1 ) ) = ( ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) โ ( ๐พ โ 1 ) ) ) |
223 |
219 222
|
breqtrd |
โข ( ๐ โ โ โ 0 โค ( ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) โ ( ๐พ โ 1 ) ) ) |
224 |
4 107 61 223
|
leadd1dd |
โข ( ๐ โ โ โ ( 0 + ( ๐พ โ 1 ) ) โค ( ( ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) โ ( ๐พ โ 1 ) ) + ( ๐พ โ 1 ) ) ) |
225 |
52 51
|
eqeltrd |
โข ( ๐ โ โ โ ( ๐พ โ 1 ) โ โ ) |
226 |
225
|
addlidd |
โข ( ๐ โ โ โ ( 0 + ( ๐พ โ 1 ) ) = ( ๐พ โ 1 ) ) |
227 |
73
|
recnd |
โข ( ๐ โ โ โ ( ๐ต โ ๐ ) โ โ ) |
228 |
84
|
recnd |
โข ( ๐ โ โ โ ( ๐ต โ ( ๐ + 1 ) ) โ โ ) |
229 |
227 228
|
subcld |
โข ( ๐ โ โ โ ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) โ โ ) |
230 |
229 225
|
npcand |
โข ( ๐ โ โ โ ( ( ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) โ ( ๐พ โ 1 ) ) + ( ๐พ โ 1 ) ) = ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) ) |
231 |
224 226 230
|
3brtr3d |
โข ( ๐ โ โ โ ( ๐พ โ 1 ) โค ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) ) |
232 |
4 61 85 106 231
|
ltletrd |
โข ( ๐ โ โ โ 0 < ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) ) |
233 |
84 73
|
posdifd |
โข ( ๐ โ โ โ ( ( ๐ต โ ( ๐ + 1 ) ) < ( ๐ต โ ๐ ) โ 0 < ( ( ๐ต โ ๐ ) โ ( ๐ต โ ( ๐ + 1 ) ) ) ) ) |
234 |
232 233
|
mpbird |
โข ( ๐ โ โ โ ( ๐ต โ ( ๐ + 1 ) ) < ( ๐ต โ ๐ ) ) |