Step |
Hyp |
Ref |
Expression |
1 |
|
pntlem1.r |
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) ) |
2 |
|
pntlem1.a |
|- ( ph -> A e. RR+ ) |
3 |
|
pntlem1.b |
|- ( ph -> B e. RR+ ) |
4 |
|
pntlem1.l |
|- ( ph -> L e. ( 0 (,) 1 ) ) |
5 |
|
pntlem1.d |
|- D = ( A + 1 ) |
6 |
|
pntlem1.f |
|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) |
7 |
|
pntlem1.u |
|- ( ph -> U e. RR+ ) |
8 |
|
pntlem1.u2 |
|- ( ph -> U <_ A ) |
9 |
|
pntlem1.e |
|- E = ( U / D ) |
10 |
|
pntlem1.k |
|- K = ( exp ` ( B / E ) ) |
11 |
|
pntlem1.y |
|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) ) |
12 |
|
pntlem1.x |
|- ( ph -> ( X e. RR+ /\ Y < X ) ) |
13 |
|
pntlem1.c |
|- ( ph -> C e. RR+ ) |
14 |
|
pntlem1.w |
|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) ) |
15 |
|
pntlem1.z |
|- ( ph -> Z e. ( W [,) +oo ) ) |
16 |
|
pntlem1.m |
|- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 ) |
17 |
|
pntlem1.n |
|- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) |
18 |
|
pntlem1.U |
|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U ) |
19 |
7
|
adantr |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> U e. RR+ ) |
20 |
19
|
rpred |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> U e. RR ) |
21 |
|
simprl |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> J e. NN ) |
22 |
20 21
|
nndivred |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( U / J ) e. RR ) |
23 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
pntlemb |
|- ( ph -> ( Z e. RR+ /\ ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) /\ ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) ) |
24 |
23
|
simp1d |
|- ( ph -> Z e. RR+ ) |
25 |
24
|
adantr |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> Z e. RR+ ) |
26 |
21
|
nnrpd |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> J e. RR+ ) |
27 |
25 26
|
rpdivcld |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( Z / J ) e. RR+ ) |
28 |
1
|
pntrf |
|- R : RR+ --> RR |
29 |
28
|
ffvelrni |
|- ( ( Z / J ) e. RR+ -> ( R ` ( Z / J ) ) e. RR ) |
30 |
27 29
|
syl |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( R ` ( Z / J ) ) e. RR ) |
31 |
30 25
|
rerpdivcld |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( R ` ( Z / J ) ) / Z ) e. RR ) |
32 |
31
|
recnd |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( R ` ( Z / J ) ) / Z ) e. CC ) |
33 |
32
|
abscld |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) e. RR ) |
34 |
22 33
|
resubcld |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( U / J ) - ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) ) e. RR ) |
35 |
26
|
relogcld |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( log ` J ) e. RR ) |
36 |
30
|
recnd |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( R ` ( Z / J ) ) e. CC ) |
37 |
25
|
rpcnne0d |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( Z e. CC /\ Z =/= 0 ) ) |
38 |
26
|
rpcnne0d |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( J e. CC /\ J =/= 0 ) ) |
39 |
|
divdiv2 |
|- ( ( ( R ` ( Z / J ) ) e. CC /\ ( Z e. CC /\ Z =/= 0 ) /\ ( J e. CC /\ J =/= 0 ) ) -> ( ( R ` ( Z / J ) ) / ( Z / J ) ) = ( ( ( R ` ( Z / J ) ) x. J ) / Z ) ) |
40 |
36 37 38 39
|
syl3anc |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( R ` ( Z / J ) ) / ( Z / J ) ) = ( ( ( R ` ( Z / J ) ) x. J ) / Z ) ) |
41 |
21
|
nncnd |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> J e. CC ) |
42 |
|
div23 |
|- ( ( ( R ` ( Z / J ) ) e. CC /\ J e. CC /\ ( Z e. CC /\ Z =/= 0 ) ) -> ( ( ( R ` ( Z / J ) ) x. J ) / Z ) = ( ( ( R ` ( Z / J ) ) / Z ) x. J ) ) |
43 |
36 41 37 42
|
syl3anc |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( ( R ` ( Z / J ) ) x. J ) / Z ) = ( ( ( R ` ( Z / J ) ) / Z ) x. J ) ) |
44 |
40 43
|
eqtrd |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( R ` ( Z / J ) ) / ( Z / J ) ) = ( ( ( R ` ( Z / J ) ) / Z ) x. J ) ) |
45 |
44
|
fveq2d |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( R ` ( Z / J ) ) / ( Z / J ) ) ) = ( abs ` ( ( ( R ` ( Z / J ) ) / Z ) x. J ) ) ) |
46 |
32 41
|
absmuld |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( ( R ` ( Z / J ) ) / Z ) x. J ) ) = ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. ( abs ` J ) ) ) |
47 |
26
|
rprege0d |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( J e. RR /\ 0 <_ J ) ) |
48 |
|
absid |
|- ( ( J e. RR /\ 0 <_ J ) -> ( abs ` J ) = J ) |
49 |
47 48
|
syl |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` J ) = J ) |
50 |
49
|
oveq2d |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. ( abs ` J ) ) = ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. J ) ) |
51 |
45 46 50
|
3eqtrd |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( R ` ( Z / J ) ) / ( Z / J ) ) ) = ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. J ) ) |
52 |
|
fveq2 |
|- ( z = ( Z / J ) -> ( R ` z ) = ( R ` ( Z / J ) ) ) |
53 |
|
id |
|- ( z = ( Z / J ) -> z = ( Z / J ) ) |
54 |
52 53
|
oveq12d |
|- ( z = ( Z / J ) -> ( ( R ` z ) / z ) = ( ( R ` ( Z / J ) ) / ( Z / J ) ) ) |
55 |
54
|
fveq2d |
|- ( z = ( Z / J ) -> ( abs ` ( ( R ` z ) / z ) ) = ( abs ` ( ( R ` ( Z / J ) ) / ( Z / J ) ) ) ) |
56 |
55
|
breq1d |
|- ( z = ( Z / J ) -> ( ( abs ` ( ( R ` z ) / z ) ) <_ U <-> ( abs ` ( ( R ` ( Z / J ) ) / ( Z / J ) ) ) <_ U ) ) |
57 |
18
|
adantr |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U ) |
58 |
27
|
rpred |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( Z / J ) e. RR ) |
59 |
|
simprr |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> J <_ ( Z / Y ) ) |
60 |
26
|
rpred |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> J e. RR ) |
61 |
25
|
rpred |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> Z e. RR ) |
62 |
11
|
simpld |
|- ( ph -> Y e. RR+ ) |
63 |
62
|
adantr |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> Y e. RR+ ) |
64 |
60 61 63
|
lemuldiv2d |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( Y x. J ) <_ Z <-> J <_ ( Z / Y ) ) ) |
65 |
59 64
|
mpbird |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( Y x. J ) <_ Z ) |
66 |
63
|
rpred |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> Y e. RR ) |
67 |
66 61 26
|
lemuldivd |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( Y x. J ) <_ Z <-> Y <_ ( Z / J ) ) ) |
68 |
65 67
|
mpbid |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> Y <_ ( Z / J ) ) |
69 |
|
elicopnf |
|- ( Y e. RR -> ( ( Z / J ) e. ( Y [,) +oo ) <-> ( ( Z / J ) e. RR /\ Y <_ ( Z / J ) ) ) ) |
70 |
66 69
|
syl |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( Z / J ) e. ( Y [,) +oo ) <-> ( ( Z / J ) e. RR /\ Y <_ ( Z / J ) ) ) ) |
71 |
58 68 70
|
mpbir2and |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( Z / J ) e. ( Y [,) +oo ) ) |
72 |
56 57 71
|
rspcdva |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( R ` ( Z / J ) ) / ( Z / J ) ) ) <_ U ) |
73 |
51 72
|
eqbrtrrd |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. J ) <_ U ) |
74 |
33 20 26
|
lemuldivd |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. J ) <_ U <-> ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) <_ ( U / J ) ) ) |
75 |
73 74
|
mpbid |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) <_ ( U / J ) ) |
76 |
22 33
|
subge0d |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( 0 <_ ( ( U / J ) - ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) ) <-> ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) <_ ( U / J ) ) ) |
77 |
75 76
|
mpbird |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> 0 <_ ( ( U / J ) - ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) ) ) |
78 |
|
log1 |
|- ( log ` 1 ) = 0 |
79 |
|
nnge1 |
|- ( J e. NN -> 1 <_ J ) |
80 |
79
|
ad2antrl |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> 1 <_ J ) |
81 |
|
1rp |
|- 1 e. RR+ |
82 |
|
logleb |
|- ( ( 1 e. RR+ /\ J e. RR+ ) -> ( 1 <_ J <-> ( log ` 1 ) <_ ( log ` J ) ) ) |
83 |
81 26 82
|
sylancr |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( 1 <_ J <-> ( log ` 1 ) <_ ( log ` J ) ) ) |
84 |
80 83
|
mpbid |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( log ` 1 ) <_ ( log ` J ) ) |
85 |
78 84
|
eqbrtrrid |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> 0 <_ ( log ` J ) ) |
86 |
34 35 77 85
|
mulge0d |
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> 0 <_ ( ( ( U / J ) - ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) ) x. ( log ` J ) ) ) |