Step |
Hyp |
Ref |
Expression |
1 |
|
pntlem1.r |
โข ๐
= ( ๐ โ โ+ โฆ ( ( ฯ โ ๐ ) โ ๐ ) ) |
2 |
|
pntlem1.a |
โข ( ๐ โ ๐ด โ โ+ ) |
3 |
|
pntlem1.b |
โข ( ๐ โ ๐ต โ โ+ ) |
4 |
|
pntlem1.l |
โข ( ๐ โ ๐ฟ โ ( 0 (,) 1 ) ) |
5 |
|
pntlem1.d |
โข ๐ท = ( ๐ด + 1 ) |
6 |
|
pntlem1.f |
โข ๐น = ( ( 1 โ ( 1 / ๐ท ) ) ยท ( ( ๐ฟ / ( ; 3 2 ยท ๐ต ) ) / ( ๐ท โ 2 ) ) ) |
7 |
|
pntlem1.u |
โข ( ๐ โ ๐ โ โ+ ) |
8 |
|
pntlem1.u2 |
โข ( ๐ โ ๐ โค ๐ด ) |
9 |
|
pntlem1.e |
โข ๐ธ = ( ๐ / ๐ท ) |
10 |
|
pntlem1.k |
โข ๐พ = ( exp โ ( ๐ต / ๐ธ ) ) |
11 |
|
pntlem1.y |
โข ( ๐ โ ( ๐ โ โ+ โง 1 โค ๐ ) ) |
12 |
|
pntlem1.x |
โข ( ๐ โ ( ๐ โ โ+ โง ๐ < ๐ ) ) |
13 |
|
pntlem1.c |
โข ( ๐ โ ๐ถ โ โ+ ) |
14 |
|
pntlem1.w |
โข ๐ = ( ( ( ๐ + ( 4 / ( ๐ฟ ยท ๐ธ ) ) ) โ 2 ) + ( ( ( ๐ ยท ( ๐พ โ 2 ) ) โ 4 ) + ( exp โ ( ( ( ; 3 2 ยท ๐ต ) / ( ( ๐ โ ๐ธ ) ยท ( ๐ฟ ยท ( ๐ธ โ 2 ) ) ) ) ยท ( ( ๐ ยท 3 ) + ๐ถ ) ) ) ) ) |
15 |
|
pntlem1.z |
โข ( ๐ โ ๐ โ ( ๐ [,) +โ ) ) |
16 |
|
pntlem1.m |
โข ๐ = ( ( โ โ ( ( log โ ๐ ) / ( log โ ๐พ ) ) ) + 1 ) |
17 |
|
pntlem1.n |
โข ๐ = ( โ โ ( ( ( log โ ๐ ) / ( log โ ๐พ ) ) / 2 ) ) |
18 |
|
pntlem1.U |
โข ( ๐ โ โ ๐ง โ ( ๐ [,) +โ ) ( abs โ ( ( ๐
โ ๐ง ) / ๐ง ) ) โค ๐ ) |
19 |
|
pntlem1.K |
โข ( ๐ โ โ ๐ฆ โ ( ๐ (,) +โ ) โ ๐ง โ โ+ ( ( ๐ฆ < ๐ง โง ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ง ) < ( ๐พ ยท ๐ฆ ) ) โง โ ๐ข โ ( ๐ง [,] ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ง ) ) ( abs โ ( ( ๐
โ ๐ข ) / ๐ข ) ) โค ๐ธ ) ) |
20 |
|
pntlem1.o |
โข ๐ = ( ( ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) ) |
21 |
|
pntlem1.v |
โข ( ๐ โ ๐ โ โ+ ) |
22 |
|
pntlem1.V |
โข ( ๐ โ ( ( ( ๐พ โ ๐ฝ ) < ๐ โง ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) < ( ๐พ ยท ( ๐พ โ ๐ฝ ) ) ) โง โ ๐ข โ ( ๐ [,] ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ( abs โ ( ( ๐
โ ๐ข ) / ๐ข ) ) โค ๐ธ ) ) |
23 |
|
pntlem1.j |
โข ( ๐ โ ๐ฝ โ ( ๐ ..^ ๐ ) ) |
24 |
|
pntlem1.i |
โข ๐ผ = ( ( ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) + 1 ) ... ( โ โ ( ๐ / ๐ ) ) ) |
25 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
pntlemb |
โข ( ๐ โ ( ๐ โ โ+ โง ( 1 < ๐ โง e โค ( โ โ ๐ ) โง ( โ โ ๐ ) โค ( ๐ / ๐ ) ) โง ( ( 4 / ( ๐ฟ ยท ๐ธ ) ) โค ( โ โ ๐ ) โง ( ( ( log โ ๐ ) / ( log โ ๐พ ) ) + 2 ) โค ( ( ( log โ ๐ ) / ( log โ ๐พ ) ) / 4 ) โง ( ( ๐ ยท 3 ) + ๐ถ ) โค ( ( ( ๐ โ ๐ธ ) ยท ( ( ๐ฟ ยท ( ๐ธ โ 2 ) ) / ( ; 3 2 ยท ๐ต ) ) ) ยท ( log โ ๐ ) ) ) ) ) |
26 |
25
|
simp1d |
โข ( ๐ โ ๐ โ โ+ ) |
27 |
1 2 3 4 5 6 7 8 9 10
|
pntlemc |
โข ( ๐ โ ( ๐ธ โ โ+ โง ๐พ โ โ+ โง ( ๐ธ โ ( 0 (,) 1 ) โง 1 < ๐พ โง ( ๐ โ ๐ธ ) โ โ+ ) ) ) |
28 |
27
|
simp2d |
โข ( ๐ โ ๐พ โ โ+ ) |
29 |
|
elfzoelz |
โข ( ๐ฝ โ ( ๐ ..^ ๐ ) โ ๐ฝ โ โค ) |
30 |
23 29
|
syl |
โข ( ๐ โ ๐ฝ โ โค ) |
31 |
30
|
peano2zd |
โข ( ๐ โ ( ๐ฝ + 1 ) โ โค ) |
32 |
28 31
|
rpexpcld |
โข ( ๐ โ ( ๐พ โ ( ๐ฝ + 1 ) ) โ โ+ ) |
33 |
26 32
|
rpdivcld |
โข ( ๐ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) โ โ+ ) |
34 |
33
|
rpred |
โข ( ๐ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) โ โ ) |
35 |
34
|
flcld |
โข ( ๐ โ ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) โ โค ) |
36 |
|
1rp |
โข 1 โ โ+ |
37 |
1 2 3 4 5 6
|
pntlemd |
โข ( ๐ โ ( ๐ฟ โ โ+ โง ๐ท โ โ+ โง ๐น โ โ+ ) ) |
38 |
37
|
simp1d |
โข ( ๐ โ ๐ฟ โ โ+ ) |
39 |
27
|
simp1d |
โข ( ๐ โ ๐ธ โ โ+ ) |
40 |
38 39
|
rpmulcld |
โข ( ๐ โ ( ๐ฟ ยท ๐ธ ) โ โ+ ) |
41 |
|
rpaddcl |
โข ( ( 1 โ โ+ โง ( ๐ฟ ยท ๐ธ ) โ โ+ ) โ ( 1 + ( ๐ฟ ยท ๐ธ ) ) โ โ+ ) |
42 |
36 40 41
|
sylancr |
โข ( ๐ โ ( 1 + ( ๐ฟ ยท ๐ธ ) ) โ โ+ ) |
43 |
42 21
|
rpmulcld |
โข ( ๐ โ ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) โ โ+ ) |
44 |
26 43
|
rpdivcld |
โข ( ๐ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) โ โ+ ) |
45 |
44
|
rpred |
โข ( ๐ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) โ โ ) |
46 |
45
|
flcld |
โข ( ๐ โ ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) โ โค ) |
47 |
43
|
rpred |
โข ( ๐ โ ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) โ โ ) |
48 |
32
|
rpred |
โข ( ๐ โ ( ๐พ โ ( ๐ฝ + 1 ) ) โ โ ) |
49 |
22
|
simpld |
โข ( ๐ โ ( ( ๐พ โ ๐ฝ ) < ๐ โง ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) < ( ๐พ ยท ( ๐พ โ ๐ฝ ) ) ) ) |
50 |
49
|
simprd |
โข ( ๐ โ ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) < ( ๐พ ยท ( ๐พ โ ๐ฝ ) ) ) |
51 |
28
|
rpcnd |
โข ( ๐ โ ๐พ โ โ ) |
52 |
28 30
|
rpexpcld |
โข ( ๐ โ ( ๐พ โ ๐ฝ ) โ โ+ ) |
53 |
52
|
rpcnd |
โข ( ๐ โ ( ๐พ โ ๐ฝ ) โ โ ) |
54 |
51 53
|
mulcomd |
โข ( ๐ โ ( ๐พ ยท ( ๐พ โ ๐ฝ ) ) = ( ( ๐พ โ ๐ฝ ) ยท ๐พ ) ) |
55 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
|
pntlemg |
โข ( ๐ โ ( ๐ โ โ โง ๐ โ ( โคโฅ โ ๐ ) โง ( ( ( log โ ๐ ) / ( log โ ๐พ ) ) / 4 ) โค ( ๐ โ ๐ ) ) ) |
56 |
55
|
simp1d |
โข ( ๐ โ ๐ โ โ ) |
57 |
|
elfzouz |
โข ( ๐ฝ โ ( ๐ ..^ ๐ ) โ ๐ฝ โ ( โคโฅ โ ๐ ) ) |
58 |
23 57
|
syl |
โข ( ๐ โ ๐ฝ โ ( โคโฅ โ ๐ ) ) |
59 |
|
eluznn |
โข ( ( ๐ โ โ โง ๐ฝ โ ( โคโฅ โ ๐ ) ) โ ๐ฝ โ โ ) |
60 |
56 58 59
|
syl2anc |
โข ( ๐ โ ๐ฝ โ โ ) |
61 |
60
|
nnnn0d |
โข ( ๐ โ ๐ฝ โ โ0 ) |
62 |
51 61
|
expp1d |
โข ( ๐ โ ( ๐พ โ ( ๐ฝ + 1 ) ) = ( ( ๐พ โ ๐ฝ ) ยท ๐พ ) ) |
63 |
54 62
|
eqtr4d |
โข ( ๐ โ ( ๐พ ยท ( ๐พ โ ๐ฝ ) ) = ( ๐พ โ ( ๐ฝ + 1 ) ) ) |
64 |
50 63
|
breqtrd |
โข ( ๐ โ ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) < ( ๐พ โ ( ๐ฝ + 1 ) ) ) |
65 |
47 48 64
|
ltled |
โข ( ๐ โ ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) โค ( ๐พ โ ( ๐ฝ + 1 ) ) ) |
66 |
43 32 26
|
lediv2d |
โข ( ๐ โ ( ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) โค ( ๐พ โ ( ๐ฝ + 1 ) ) โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) โค ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) ) |
67 |
65 66
|
mpbid |
โข ( ๐ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) โค ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) |
68 |
|
flwordi |
โข ( ( ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) โ โ โง ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) โ โ โง ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) โค ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) โ ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) โค ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) ) |
69 |
34 45 67 68
|
syl3anc |
โข ( ๐ โ ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) โค ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) ) |
70 |
|
eluz2 |
โข ( ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) โ ( โคโฅ โ ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) ) โ ( ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) โ โค โง ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) โ โค โง ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) โค ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) ) ) |
71 |
35 46 69 70
|
syl3anbrc |
โข ( ๐ โ ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) โ ( โคโฅ โ ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) ) ) |
72 |
|
eluzp1p1 |
โข ( ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) โ ( โคโฅ โ ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) ) โ ( ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) + 1 ) โ ( โคโฅ โ ( ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) + 1 ) ) ) |
73 |
|
fzss1 |
โข ( ( ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) + 1 ) โ ( โคโฅ โ ( ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) + 1 ) ) โ ( ( ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) + 1 ) ... ( โ โ ( ๐ / ๐ ) ) ) โ ( ( ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โ โ ( ๐ / ๐ ) ) ) ) |
74 |
71 72 73
|
3syl |
โข ( ๐ โ ( ( ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) + 1 ) ... ( โ โ ( ๐ / ๐ ) ) ) โ ( ( ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โ โ ( ๐ / ๐ ) ) ) ) |
75 |
26 21
|
rpdivcld |
โข ( ๐ โ ( ๐ / ๐ ) โ โ+ ) |
76 |
75
|
rpred |
โข ( ๐ โ ( ๐ / ๐ ) โ โ ) |
77 |
76
|
flcld |
โข ( ๐ โ ( โ โ ( ๐ / ๐ ) ) โ โค ) |
78 |
26 52
|
rpdivcld |
โข ( ๐ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) โ โ+ ) |
79 |
78
|
rpred |
โข ( ๐ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) โ โ ) |
80 |
79
|
flcld |
โข ( ๐ โ ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) โ โค ) |
81 |
52
|
rpred |
โข ( ๐ โ ( ๐พ โ ๐ฝ ) โ โ ) |
82 |
21
|
rpred |
โข ( ๐ โ ๐ โ โ ) |
83 |
49
|
simpld |
โข ( ๐ โ ( ๐พ โ ๐ฝ ) < ๐ ) |
84 |
81 82 83
|
ltled |
โข ( ๐ โ ( ๐พ โ ๐ฝ ) โค ๐ ) |
85 |
52 21 26
|
lediv2d |
โข ( ๐ โ ( ( ๐พ โ ๐ฝ ) โค ๐ โ ( ๐ / ๐ ) โค ( ๐ / ( ๐พ โ ๐ฝ ) ) ) ) |
86 |
84 85
|
mpbid |
โข ( ๐ โ ( ๐ / ๐ ) โค ( ๐ / ( ๐พ โ ๐ฝ ) ) ) |
87 |
|
flwordi |
โข ( ( ( ๐ / ๐ ) โ โ โง ( ๐ / ( ๐พ โ ๐ฝ ) ) โ โ โง ( ๐ / ๐ ) โค ( ๐ / ( ๐พ โ ๐ฝ ) ) ) โ ( โ โ ( ๐ / ๐ ) ) โค ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) ) |
88 |
76 79 86 87
|
syl3anc |
โข ( ๐ โ ( โ โ ( ๐ / ๐ ) ) โค ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) ) |
89 |
|
eluz2 |
โข ( ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) โ ( โคโฅ โ ( โ โ ( ๐ / ๐ ) ) ) โ ( ( โ โ ( ๐ / ๐ ) ) โ โค โง ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) โ โค โง ( โ โ ( ๐ / ๐ ) ) โค ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) ) ) |
90 |
77 80 88 89
|
syl3anbrc |
โข ( ๐ โ ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) โ ( โคโฅ โ ( โ โ ( ๐ / ๐ ) ) ) ) |
91 |
|
fzss2 |
โข ( ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) โ ( โคโฅ โ ( โ โ ( ๐ / ๐ ) ) ) โ ( ( ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โ โ ( ๐ / ๐ ) ) ) โ ( ( ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) ) ) |
92 |
90 91
|
syl |
โข ( ๐ โ ( ( ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โ โ ( ๐ / ๐ ) ) ) โ ( ( ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) ) ) |
93 |
74 92
|
sstrd |
โข ( ๐ โ ( ( ( โ โ ( ๐ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐ ) ) ) + 1 ) ... ( โ โ ( ๐ / ๐ ) ) ) โ ( ( ( โ โ ( ๐ / ( ๐พ โ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โ โ ( ๐ / ( ๐พ โ ๐ฝ ) ) ) ) ) |
94 |
93 24 20
|
3sstr4g |
โข ( ๐ โ ๐ผ โ ๐ ) |