MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pntibndlem2 Structured version   Unicode version

Theorem pntibndlem2 22840
Description: Lemma for pntibnd 22842. The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)
Hypotheses
Ref Expression
pntibnd.r  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
pntibndlem1.1  |-  ( ph  ->  A  e.  RR+ )
pntibndlem1.l  |-  L  =  ( ( 1  / 
4 )  /  ( A  +  3 ) )
pntibndlem3.2  |-  ( ph  ->  A. x  e.  RR+  ( abs `  ( ( R `  x )  /  x ) )  <_  A )
pntibndlem3.3  |-  ( ph  ->  B  e.  RR+ )
pntibndlem3.k  |-  K  =  ( exp `  ( B  /  ( E  / 
2 ) ) )
pntibndlem3.c  |-  C  =  ( ( 2  x.  B )  +  ( log `  2 ) )
pntibndlem3.4  |-  ( ph  ->  E  e.  ( 0 (,) 1 ) )
pntibndlem3.6  |-  ( ph  ->  Z  e.  RR+ )
pntibndlem2.10  |-  ( ph  ->  N  e.  NN )
pntibndlem2.5  |-  ( ph  ->  T  e.  RR+ )
pntibndlem2.6  |-  ( ph  ->  A. x  e.  ( 1 (,) +oo ) A. y  e.  (
x [,] ( 2  x.  x ) ) ( (ψ `  y
)  -  (ψ `  x ) )  <_ 
( ( 2  x.  ( y  -  x
) )  +  ( T  x.  ( x  /  ( log `  x
) ) ) ) )
pntibndlem2.7  |-  X  =  ( ( exp `  ( T  /  ( E  / 
4 ) ) )  +  Z )
pntibndlem2.8  |-  ( ph  ->  M  e.  ( ( exp `  ( C  /  E ) ) [,) +oo ) )
pntibndlem2.9  |-  ( ph  ->  Y  e.  ( X (,) +oo ) )
pntibndlem2.11  |-  ( ph  ->  ( ( Y  < 
N  /\  N  <_  ( ( M  /  2
)  x.  Y ) )  /\  ( abs `  ( ( R `  N )  /  N
) )  <_  ( E  /  2 ) ) )
Assertion
Ref Expression
pntibndlem2  |-  ( ph  ->  E. z  e.  RR+  ( ( Y  < 
z  /\  ( (
1  +  ( L  x.  E ) )  x.  z )  < 
( M  x.  Y
) )  /\  A. u  e.  ( z [,] ( ( 1  +  ( L  x.  E
) )  x.  z
) ) ( abs `  ( ( R `  u )  /  u
) )  <_  E
) )
Distinct variable groups:    u, a, x, y, z, E    u, L, x, z    N, a, u, x, y, z   
u, A, x    u, C, x, y    u, R, x, y, z    z, M    x, T, y    z, Y    u, Z, x, y    ph, u
Allowed substitution hints:    ph( x, y, z, a)    A( y, z, a)    B( x, y, z, u, a)    C( z, a)    R( a)    T( z, u, a)    K( x, y, z, u, a)    L( y, a)    M( x, y, u, a)    X( x, y, z, u, a)    Y( x, y, u, a)    Z( z, a)

Proof of Theorem pntibndlem2
StepHypRef Expression
1 pntibndlem2.10 . . 3  |-  ( ph  ->  N  e.  NN )
21nnrpd 11026 . 2  |-  ( ph  ->  N  e.  RR+ )
3 pntibndlem2.11 . . . . 5  |-  ( ph  ->  ( ( Y  < 
N  /\  N  <_  ( ( M  /  2
)  x.  Y ) )  /\  ( abs `  ( ( R `  N )  /  N
) )  <_  ( E  /  2 ) ) )
43simpld 459 . . . 4  |-  ( ph  ->  ( Y  <  N  /\  N  <_  ( ( M  /  2 )  x.  Y ) ) )
54simpld 459 . . 3  |-  ( ph  ->  Y  <  N )
6 1red 9401 . . . . . 6  |-  ( ph  ->  1  e.  RR )
7 ioossre 11357 . . . . . . . 8  |-  ( 0 (,) 1 )  C_  RR
8 pntibnd.r . . . . . . . . 9  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
9 pntibndlem1.1 . . . . . . . . 9  |-  ( ph  ->  A  e.  RR+ )
10 pntibndlem1.l . . . . . . . . 9  |-  L  =  ( ( 1  / 
4 )  /  ( A  +  3 ) )
118, 9, 10pntibndlem1 22838 . . . . . . . 8  |-  ( ph  ->  L  e.  ( 0 (,) 1 ) )
127, 11sseldi 3354 . . . . . . 7  |-  ( ph  ->  L  e.  RR )
13 pntibndlem3.4 . . . . . . . 8  |-  ( ph  ->  E  e.  ( 0 (,) 1 ) )
147, 13sseldi 3354 . . . . . . 7  |-  ( ph  ->  E  e.  RR )
1512, 14remulcld 9414 . . . . . 6  |-  ( ph  ->  ( L  x.  E
)  e.  RR )
166, 15readdcld 9413 . . . . 5  |-  ( ph  ->  ( 1  +  ( L  x.  E ) )  e.  RR )
171nnred 10337 . . . . 5  |-  ( ph  ->  N  e.  RR )
1816, 17remulcld 9414 . . . 4  |-  ( ph  ->  ( ( 1  +  ( L  x.  E
) )  x.  N
)  e.  RR )
19 2re 10391 . . . . 5  |-  2  e.  RR
20 remulcl 9367 . . . . 5  |-  ( ( 2  e.  RR  /\  N  e.  RR )  ->  ( 2  x.  N
)  e.  RR )
2119, 17, 20sylancr 663 . . . 4  |-  ( ph  ->  ( 2  x.  N
)  e.  RR )
22 pntibndlem3.c . . . . . . . . . 10  |-  C  =  ( ( 2  x.  B )  +  ( log `  2 ) )
23 pntibndlem3.3 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  RR+ )
2423rpred 11027 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
25 remulcl 9367 . . . . . . . . . . . 12  |-  ( ( 2  e.  RR  /\  B  e.  RR )  ->  ( 2  x.  B
)  e.  RR )
2619, 24, 25sylancr 663 . . . . . . . . . . 11  |-  ( ph  ->  ( 2  x.  B
)  e.  RR )
27 2rp 10996 . . . . . . . . . . . . 13  |-  2  e.  RR+
2827a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  2  e.  RR+ )
2928relogcld 22072 . . . . . . . . . . 11  |-  ( ph  ->  ( log `  2
)  e.  RR )
3026, 29readdcld 9413 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2  x.  B )  +  ( log `  2 ) )  e.  RR )
3122, 30syl5eqel 2527 . . . . . . . . 9  |-  ( ph  ->  C  e.  RR )
32 eliooord 11355 . . . . . . . . . . . 12  |-  ( E  e.  ( 0 (,) 1 )  ->  (
0  <  E  /\  E  <  1 ) )
3313, 32syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( 0  <  E  /\  E  <  1
) )
3433simpld 459 . . . . . . . . . 10  |-  ( ph  ->  0  <  E )
3514, 34elrpd 11025 . . . . . . . . 9  |-  ( ph  ->  E  e.  RR+ )
3631, 35rerpdivcld 11054 . . . . . . . 8  |-  ( ph  ->  ( C  /  E
)  e.  RR )
3736reefcld 13373 . . . . . . 7  |-  ( ph  ->  ( exp `  ( C  /  E ) )  e.  RR )
38 pnfxr 11092 . . . . . . 7  |- +oo  e.  RR*
39 icossre 11376 . . . . . . 7  |-  ( ( ( exp `  ( C  /  E ) )  e.  RR  /\ +oo  e.  RR* )  ->  (
( exp `  ( C  /  E ) ) [,) +oo )  C_  RR )
4037, 38, 39sylancl 662 . . . . . 6  |-  ( ph  ->  ( ( exp `  ( C  /  E ) ) [,) +oo )  C_  RR )
41 pntibndlem2.8 . . . . . 6  |-  ( ph  ->  M  e.  ( ( exp `  ( C  /  E ) ) [,) +oo ) )
4240, 41sseldd 3357 . . . . 5  |-  ( ph  ->  M  e.  RR )
43 ioossre 11357 . . . . . 6  |-  ( X (,) +oo )  C_  RR
44 pntibndlem2.9 . . . . . 6  |-  ( ph  ->  Y  e.  ( X (,) +oo ) )
4543, 44sseldi 3354 . . . . 5  |-  ( ph  ->  Y  e.  RR )
4642, 45remulcld 9414 . . . 4  |-  ( ph  ->  ( M  x.  Y
)  e.  RR )
4719a1i 11 . . . . 5  |-  ( ph  ->  2  e.  RR )
48 eliooord 11355 . . . . . . . . . . . . 13  |-  ( L  e.  ( 0 (,) 1 )  ->  (
0  <  L  /\  L  <  1 ) )
4911, 48syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  <  L  /\  L  <  1
) )
5049simpld 459 . . . . . . . . . . 11  |-  ( ph  ->  0  <  L )
5112, 50elrpd 11025 . . . . . . . . . 10  |-  ( ph  ->  L  e.  RR+ )
5251rpge0d 11031 . . . . . . . . 9  |-  ( ph  ->  0  <_  L )
5349simprd 463 . . . . . . . . 9  |-  ( ph  ->  L  <  1 )
5435rpge0d 11031 . . . . . . . . 9  |-  ( ph  ->  0  <_  E )
5533simprd 463 . . . . . . . . 9  |-  ( ph  ->  E  <  1 )
5612, 6, 14, 6, 52, 53, 54, 55ltmul12ad 10274 . . . . . . . 8  |-  ( ph  ->  ( L  x.  E
)  <  ( 1  x.  1 ) )
57 1t1e1 10469 . . . . . . . 8  |-  ( 1  x.  1 )  =  1
5856, 57syl6breq 4331 . . . . . . 7  |-  ( ph  ->  ( L  x.  E
)  <  1 )
5915, 6, 6, 58ltadd2dd 9530 . . . . . 6  |-  ( ph  ->  ( 1  +  ( L  x.  E ) )  <  ( 1  +  1 ) )
60 df-2 10380 . . . . . 6  |-  2  =  ( 1  +  1 )
6159, 60syl6breqr 4332 . . . . 5  |-  ( ph  ->  ( 1  +  ( L  x.  E ) )  <  2 )
6216, 47, 2, 61ltmul1dd 11078 . . . 4  |-  ( ph  ->  ( ( 1  +  ( L  x.  E
) )  x.  N
)  <  ( 2  x.  N ) )
634simprd 463 . . . . . 6  |-  ( ph  ->  N  <_  ( ( M  /  2 )  x.  Y ) )
6442recnd 9412 . . . . . . 7  |-  ( ph  ->  M  e.  CC )
6545recnd 9412 . . . . . . 7  |-  ( ph  ->  Y  e.  CC )
66 rpcnne0 11008 . . . . . . . 8  |-  ( 2  e.  RR+  ->  ( 2  e.  CC  /\  2  =/=  0 ) )
6727, 66mp1i 12 . . . . . . 7  |-  ( ph  ->  ( 2  e.  CC  /\  2  =/=  0 ) )
68 div23 10013 . . . . . . 7  |-  ( ( M  e.  CC  /\  Y  e.  CC  /\  (
2  e.  CC  /\  2  =/=  0 ) )  ->  ( ( M  x.  Y )  / 
2 )  =  ( ( M  /  2
)  x.  Y ) )
6964, 65, 67, 68syl3anc 1218 . . . . . 6  |-  ( ph  ->  ( ( M  x.  Y )  /  2
)  =  ( ( M  /  2 )  x.  Y ) )
7063, 69breqtrrd 4318 . . . . 5  |-  ( ph  ->  N  <_  ( ( M  x.  Y )  /  2 ) )
7117, 46, 28lemuldiv2d 11073 . . . . 5  |-  ( ph  ->  ( ( 2  x.  N )  <_  ( M  x.  Y )  <->  N  <_  ( ( M  x.  Y )  / 
2 ) ) )
7270, 71mpbird 232 . . . 4  |-  ( ph  ->  ( 2  x.  N
)  <_  ( M  x.  Y ) )
7318, 21, 46, 62, 72ltletrd 9531 . . 3  |-  ( ph  ->  ( ( 1  +  ( L  x.  E
) )  x.  N
)  <  ( M  x.  Y ) )
74 pntibndlem3.2 . . . . . . . . . . . 12  |-  ( ph  ->  A. x  e.  RR+  ( abs `  ( ( R `  x )  /  x ) )  <_  A )
75 pntibndlem3.k . . . . . . . . . . . 12  |-  K  =  ( exp `  ( B  /  ( E  / 
2 ) ) )
768, 9, 10, 74, 23, 75, 22, 13, 9, 1pntibndlem2a 22839 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  e.  RR  /\  N  <_  u  /\  u  <_  (
( 1  +  ( L  x.  E ) )  x.  N ) ) )
7776simp1d 1000 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  e.  RR )
782adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  e.  RR+ )
7976simp2d 1001 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  <_  u )
8077, 78, 79rpgecld 11062 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  e.  RR+ )
818pntrf 22812 . . . . . . . . . 10  |-  R : RR+
--> RR
8281ffvelrni 5842 . . . . . . . . 9  |-  ( u  e.  RR+  ->  ( R `
 u )  e.  RR )
8380, 82syl 16 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  u )  e.  RR )
8483, 80rerpdivcld 11054 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  u )  e.  RR )
8584recnd 9412 . . . . . 6  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  u )  e.  CC )
8685abscld 12922 . . . . 5  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  /  u
) )  e.  RR )
8781ffvelrni 5842 . . . . . . . . . . . 12  |-  ( N  e.  RR+  ->  ( R `
 N )  e.  RR )
882, 87syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( R `  N
)  e.  RR )
8988, 1nndivred 10370 . . . . . . . . . 10  |-  ( ph  ->  ( ( R `  N )  /  N
)  e.  RR )
9089adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  N )  /  N )  e.  RR )
9190recnd 9412 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  N )  /  N )  e.  CC )
9285, 91subcld 9719 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  /  u )  -  ( ( R `
 N )  /  N ) )  e.  CC )
9392abscld 12922 . . . . . 6  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( ( R `
 u )  /  u )  -  (
( R `  N
)  /  N ) ) )  e.  RR )
9491abscld 12922 . . . . . 6  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  N )  /  N
) )  e.  RR )
9593, 94readdcld 9413 . . . . 5  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( ( R `  u )  /  u )  -  ( ( R `  N )  /  N
) ) )  +  ( abs `  (
( R `  N
)  /  N ) ) )  e.  RR )
9614adantr 465 . . . . 5  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  E  e.  RR )
9785, 91abs2difd 12943 . . . . . 6  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  /  u ) )  -  ( abs `  ( ( R `  N )  /  N ) ) )  <_  ( abs `  ( ( ( R `
 u )  /  u )  -  (
( R `  N
)  /  N ) ) ) )
9886, 94, 93lesubaddd 9936 . . . . . 6  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( abs `  (
( R `  u
)  /  u ) )  -  ( abs `  ( ( R `  N )  /  N
) ) )  <_ 
( abs `  (
( ( R `  u )  /  u
)  -  ( ( R `  N )  /  N ) ) )  <->  ( abs `  (
( R `  u
)  /  u ) )  <_  ( ( abs `  ( ( ( R `  u )  /  u )  -  ( ( R `  N )  /  N
) ) )  +  ( abs `  (
( R `  N
)  /  N ) ) ) ) )
9997, 98mpbid 210 . . . . 5  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  /  u
) )  <_  (
( abs `  (
( ( R `  u )  /  u
)  -  ( ( R `  N )  /  N ) ) )  +  ( abs `  ( ( R `  N )  /  N
) ) ) )
10096rehalfcld 10571 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( E  /  2 )  e.  RR )
10117adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  e.  RR )
10277, 101resubcld 9776 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  -  N )  e.  RR )
103102, 78rerpdivcld 11054 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  e.  RR )
104 3re 10395 . . . . . . . . . . . 12  |-  3  e.  RR
105104a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  3  e.  RR )
10686, 105readdcld 9413 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  /  u ) )  +  3 )  e.  RR )
107103, 106remulcld 9414 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( abs `  ( ( R `  u )  /  u
) )  +  3 ) )  e.  RR )
108 pntibndlem2.5 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  RR+ )
109108rpred 11027 . . . . . . . . . . 11  |-  ( ph  ->  T  e.  RR )
110109adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  T  e.  RR )
111 1red 9401 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  1  e.  RR )
112 4nn 10481 . . . . . . . . . . . . . . . . . 18  |-  4  e.  NN
113 nnrp 11000 . . . . . . . . . . . . . . . . . 18  |-  ( 4  e.  NN  ->  4  e.  RR+ )
114112, 113mp1i 12 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  4  e.  RR+ )
11535, 114rpdivcld 11044 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E  /  4
)  e.  RR+ )
116108, 115rpdivcld 11044 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( T  /  ( E  /  4 ) )  e.  RR+ )
117116rpred 11027 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  /  ( E  /  4 ) )  e.  RR )
118117reefcld 13373 . . . . . . . . . . . . 13  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  e.  RR )
119118adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( exp `  ( T  /  ( E  /  4 ) ) )  e.  RR )
120 efgt1 13400 . . . . . . . . . . . . . 14  |-  ( ( T  /  ( E  /  4 ) )  e.  RR+  ->  1  < 
( exp `  ( T  /  ( E  / 
4 ) ) ) )
121116, 120syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  1  <  ( exp `  ( T  /  ( E  /  4 ) ) ) )
122121adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  1  <  ( exp `  ( T  /  ( E  / 
4 ) ) ) )
123 pntibndlem2.7 . . . . . . . . . . . . . . . 16  |-  X  =  ( ( exp `  ( T  /  ( E  / 
4 ) ) )  +  Z )
124 pntibndlem3.6 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Z  e.  RR+ )
125124rpred 11027 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Z  e.  RR )
126118, 125readdcld 9413 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( exp `  ( T  /  ( E  / 
4 ) ) )  +  Z )  e.  RR )
127123, 126syl5eqel 2527 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
128118, 124ltaddrpd 11056 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  <  ( ( exp `  ( T  /  ( E  /  4 ) ) )  +  Z ) )
129128, 123syl6breqr 4332 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  <  X )
130 eliooord 11355 . . . . . . . . . . . . . . . . 17  |-  ( Y  e.  ( X (,) +oo )  ->  ( X  <  Y  /\  Y  < +oo ) )
13144, 130syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  <  Y  /\  Y  < +oo )
)
132131simpld 459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  <  Y )
133118, 127, 45, 129, 132lttrd 9532 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  <  Y )
134118, 45, 17, 133, 5lttrd 9532 . . . . . . . . . . . . 13  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  <  N )
135134adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( exp `  ( T  /  ( E  /  4 ) ) )  <  N )
136111, 119, 101, 122, 135lttrd 9532 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  1  <  N )
137101, 136rplogcld 22078 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( log `  N )  e.  RR+ )
138110, 137rerpdivcld 11054 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  RR )
139107, 138readdcld 9413 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( ( abs `  ( ( R `  u )  /  u ) )  +  3 ) )  +  ( T  / 
( log `  N
) ) )  e.  RR )
140 peano2re 9542 . . . . . . . . . . . 12  |-  ( ( abs `  ( ( R `  u )  /  u ) )  e.  RR  ->  (
( abs `  (
( R `  u
)  /  u ) )  +  1 )  e.  RR )
14186, 140syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  /  u ) )  +  1 )  e.  RR )
142103, 141remulcld 9414 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( abs `  ( ( R `  u )  /  u
) )  +  1 ) )  e.  RR )
143 chpcl 22462 . . . . . . . . . . . . 13  |-  ( u  e.  RR  ->  (ψ `  u )  e.  RR )
14477, 143syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  u
)  e.  RR )
145 chpcl 22462 . . . . . . . . . . . . 13  |-  ( N  e.  RR  ->  (ψ `  N )  e.  RR )
146101, 145syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  N
)  e.  RR )
147144, 146resubcld 9776 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (ψ `  u )  -  (ψ `  N ) )  e.  RR )
148147, 78rerpdivcld 11054 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  /  N )  e.  RR )
149142, 148readdcld 9413 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( ( abs `  ( ( R `  u )  /  u ) )  +  1 ) )  +  ( ( (ψ `  u )  -  (ψ `  N ) )  /  N ) )  e.  RR )
150103, 86remulcld 9414 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( abs `  (
( R `  u
)  /  u ) ) )  e.  RR )
15188adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  N )  e.  RR )
15283, 151resubcld 9776 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  -  ( R `  N ) )  e.  RR )
153152recnd 9412 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  -  ( R `  N ) )  e.  CC )
154153abscld 12922 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  -  ( R `  N )
) )  e.  RR )
155154, 78rerpdivcld 11054 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  -  ( R `  N ) ) )  /  N
)  e.  RR )
156150, 155readdcld 9413 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( abs `  ( ( R `  u )  /  u
) ) )  +  ( ( abs `  (
( R `  u
)  -  ( R `
 N ) ) )  /  N ) )  e.  RR )
157103, 84remulcld 9414 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  RR )
158157renegcld 9775 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  -u ( ( ( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  RR )
159158recnd 9412 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  -u ( ( ( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  CC )
160152, 78rerpdivcld 11054 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  -  ( R `
 N ) )  /  N )  e.  RR )
161160recnd 9412 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  -  ( R `
 N ) )  /  N )  e.  CC )
162159, 161abstrid 12942 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( -u ( ( ( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  +  ( ( ( R `
 u )  -  ( R `  N ) )  /  N ) ) )  <_  (
( abs `  -u (
( ( u  -  N )  /  N
)  x.  ( ( R `  u )  /  u ) ) )  +  ( abs `  ( ( ( R `
 u )  -  ( R `  N ) )  /  N ) ) ) )
16377recnd 9412 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  e.  CC )
164101recnd 9412 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  e.  CC )
16578rpne0d 11032 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  =/=  0 )
166163, 164, 164, 165divsubdird 10146 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  =  ( ( u  /  N )  -  ( N  /  N ) ) )
167164, 165dividd 10105 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  /  N )  =  1 )
168167oveq2d 6107 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  /  N )  -  ( N  /  N ) )  =  ( ( u  /  N )  -  1 ) )
169166, 168eqtrd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  =  ( ( u  /  N )  -  1 ) )
170169oveq1d 6106 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  =  ( ( ( u  /  N )  - 
1 )  x.  (
( R `  u
)  /  u ) ) )
17177, 78rerpdivcld 11054 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  /  N )  e.  RR )
172171recnd 9412 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  /  N )  e.  CC )
173 1cnd 9402 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  1  e.  CC )
174172, 173, 85subdird 9801 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  /  N
)  -  1 )  x.  ( ( R `
 u )  /  u ) )  =  ( ( ( u  /  N )  x.  ( ( R `  u )  /  u
) )  -  (
1  x.  ( ( R `  u )  /  u ) ) ) )
17580rpcnne0d 11036 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  e.  CC  /\  u  =/=  0 ) )
17678rpcnne0d 11036 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  e.  CC  /\  N  =/=  0 ) )
17783recnd 9412 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  u )  e.  CC )
178 dmdcan 10041 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( u  e.  CC  /\  u  =/=  0 )  /\  ( N  e.  CC  /\  N  =/=  0 )  /\  ( R `  u )  e.  CC )  ->  (
( u  /  N
)  x.  ( ( R `  u )  /  u ) )  =  ( ( R `
 u )  /  N ) )
179175, 176, 177, 178syl3anc 1218 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  /  N )  x.  ( ( R `
 u )  /  u ) )  =  ( ( R `  u )  /  N
) )
18085mulid2d 9404 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 1  x.  ( ( R `
 u )  /  u ) )  =  ( ( R `  u )  /  u
) )
181179, 180oveq12d 6109 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  /  N
)  x.  ( ( R `  u )  /  u ) )  -  ( 1  x.  ( ( R `  u )  /  u
) ) )  =  ( ( ( R `
 u )  /  N )  -  (
( R `  u
)  /  u ) ) )
182170, 174, 1813eqtrd 2479 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  =  ( ( ( R `
 u )  /  N )  -  (
( R `  u
)  /  u ) ) )
183182negeqd 9604 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  -u ( ( ( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  = 
-u ( ( ( R `  u )  /  N )  -  ( ( R `  u )  /  u
) ) )
18483, 78rerpdivcld 11054 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  N )  e.  RR )
185184recnd 9412 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  N )  e.  CC )
186185, 85negsubdi2d 9735 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  -u ( ( ( R `  u
)  /  N )  -  ( ( R `
 u )  /  u ) )  =  ( ( ( R `
 u )  /  u )  -  (
( R `  u
)  /  N ) ) )
187183, 186eqtrd 2475 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  -u ( ( ( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  =  ( ( ( R `
 u )  /  u )  -  (
( R `  u
)  /  N ) ) )
188151recnd 9412 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  N )  e.  CC )
189177, 188, 164, 165divsubdird 10146 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  -  ( R `
 N ) )  /  N )  =  ( ( ( R `
 u )  /  N )  -  (
( R `  N
)  /  N ) ) )
190187, 189oveq12d 6109 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( -u (
( ( u  -  N )  /  N
)  x.  ( ( R `  u )  /  u ) )  +  ( ( ( R `  u )  -  ( R `  N ) )  /  N ) )  =  ( ( ( ( R `  u )  /  u )  -  ( ( R `  u )  /  N
) )  +  ( ( ( R `  u )  /  N
)  -  ( ( R `  N )  /  N ) ) ) )
19185, 185, 91npncand 9743 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( R `  u )  /  u
)  -  ( ( R `  u )  /  N ) )  +  ( ( ( R `  u )  /  N )  -  ( ( R `  N )  /  N
) ) )  =  ( ( ( R `
 u )  /  u )  -  (
( R `  N
)  /  N ) ) )
192190, 191eqtrd 2475 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( -u (
( ( u  -  N )  /  N
)  x.  ( ( R `  u )  /  u ) )  +  ( ( ( R `  u )  -  ( R `  N ) )  /  N ) )  =  ( ( ( R `
 u )  /  u )  -  (
( R `  N
)  /  N ) ) )
193192fveq2d 5695 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( -u ( ( ( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  +  ( ( ( R `
 u )  -  ( R `  N ) )  /  N ) ) )  =  ( abs `  ( ( ( R `  u
)  /  u )  -  ( ( R `
 N )  /  N ) ) ) )
194157recnd 9412 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  CC )
195194absnegd 12935 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  -u ( ( ( u  -  N )  /  N )  x.  (
( R `  u
)  /  u ) ) )  =  ( abs `  ( ( ( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) ) ) )
196103recnd 9412 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  e.  CC )
197196, 85absmuld 12940 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( ( u  -  N )  /  N )  x.  (
( R `  u
)  /  u ) ) )  =  ( ( abs `  (
( u  -  N
)  /  N ) )  x.  ( abs `  ( ( R `  u )  /  u
) ) ) )
19877, 101subge0d 9929 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 0  <_  ( u  -  N )  <->  N  <_  u ) )
19979, 198mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  0  <_  ( u  -  N ) )
200102, 78, 199divge0d 11063 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  0  <_  ( ( u  -  N
)  /  N ) )
201103, 200absidd 12909 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( u  -  N )  /  N
) )  =  ( ( u  -  N
)  /  N ) )
202201oveq1d 6106 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( u  -  N )  /  N ) )  x.  ( abs `  (
( R `  u
)  /  u ) ) )  =  ( ( ( u  -  N )  /  N
)  x.  ( abs `  ( ( R `  u )  /  u
) ) ) )
203195, 197, 2023eqtrd 2479 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  -u ( ( ( u  -  N )  /  N )  x.  (
( R `  u
)  /  u ) ) )  =  ( ( ( u  -  N )  /  N
)  x.  ( abs `  ( ( R `  u )  /  u
) ) ) )
204153, 164, 165absdivd 12941 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( ( R `
 u )  -  ( R `  N ) )  /  N ) )  =  ( ( abs `  ( ( R `  u )  -  ( R `  N ) ) )  /  ( abs `  N
) ) )
20578rprege0d 11034 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  e.  RR  /\  0  <_  N ) )
206 absid 12785 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  RR  /\  0  <_  N )  -> 
( abs `  N
)  =  N )
207205, 206syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  N )  =  N )
208207oveq2d 6107 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  -  ( R `  N ) ) )  /  ( abs `  N ) )  =  ( ( abs `  ( ( R `  u )  -  ( R `  N )
) )  /  N
) )
209204, 208eqtrd 2475 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( ( R `
 u )  -  ( R `  N ) )  /  N ) )  =  ( ( abs `  ( ( R `  u )  -  ( R `  N ) ) )  /  N ) )
210203, 209oveq12d 6109 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  -u ( ( ( u  -  N )  /  N )  x.  ( ( R `  u )  /  u
) ) )  +  ( abs `  (
( ( R `  u )  -  ( R `  N )
)  /  N ) ) )  =  ( ( ( ( u  -  N )  /  N )  x.  ( abs `  ( ( R `
 u )  /  u ) ) )  +  ( ( abs `  ( ( R `  u )  -  ( R `  N )
) )  /  N
) ) )
211162, 193, 2103brtr3d 4321 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( ( R `
 u )  /  u )  -  (
( R `  N
)  /  N ) ) )  <_  (
( ( ( u  -  N )  /  N )  x.  ( abs `  ( ( R `
 u )  /  u ) ) )  +  ( ( abs `  ( ( R `  u )  -  ( R `  N )
) )  /  N
) ) )
212102, 147readdcld 9413 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  +  ( (ψ `  u )  -  (ψ `  N ) ) )  e.  RR )
213212, 78rerpdivcld 11054 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) )  /  N )  e.  RR )
214147recnd 9412 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (ψ `  u )  -  (ψ `  N ) )  e.  CC )
215164, 163subcld 9719 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  -  u )  e.  CC )
216214, 215abstrid 12942 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )  <_ 
( ( abs `  (
(ψ `  u )  -  (ψ `  N )
) )  +  ( abs `  ( N  -  u ) ) ) )
2178pntrval 22811 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  RR+  ->  ( R `
 u )  =  ( (ψ `  u
)  -  u ) )
21880, 217syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  u )  =  ( (ψ `  u )  -  u ) )
2198pntrval 22811 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  RR+  ->  ( R `
 N )  =  ( (ψ `  N
)  -  N ) )
22078, 219syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  N )  =  ( (ψ `  N )  -  N ) )
221218, 220oveq12d 6109 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  -  ( R `  N ) )  =  ( ( (ψ `  u )  -  u
)  -  ( (ψ `  N )  -  N
) ) )
222144recnd 9412 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  u
)  e.  CC )
223146recnd 9412 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  N
)  e.  CC )
224 subadd4 9653 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (ψ `  u
)  e.  CC  /\  (ψ `  N )  e.  CC )  /\  (
u  e.  CC  /\  N  e.  CC )
)  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  -  ( u  -  N ) )  =  ( ( (ψ `  u )  +  N
)  -  ( (ψ `  N )  +  u
) ) )
225 sub4 9654 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (ψ `  u
)  e.  CC  /\  (ψ `  N )  e.  CC )  /\  (
u  e.  CC  /\  N  e.  CC )
)  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  -  ( u  -  N ) )  =  ( ( (ψ `  u )  -  u
)  -  ( (ψ `  N )  -  N
) ) )
226 addsub4 9652 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (ψ `  u
)  e.  CC  /\  N  e.  CC )  /\  ( (ψ `  N
)  e.  CC  /\  u  e.  CC )
)  ->  ( (
(ψ `  u )  +  N )  -  (
(ψ `  N )  +  u ) )  =  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )
227226an42s 823 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (ψ `  u
)  e.  CC  /\  (ψ `  N )  e.  CC )  /\  (
u  e.  CC  /\  N  e.  CC )
)  ->  ( (
(ψ `  u )  +  N )  -  (
(ψ `  N )  +  u ) )  =  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )
228224, 225, 2273eqtr3d 2483 . . . . . . . . . . . . . . . . 17  |-  ( ( ( (ψ `  u
)  e.  CC  /\  (ψ `  N )  e.  CC )  /\  (
u  e.  CC  /\  N  e.  CC )
)  ->  ( (
(ψ `  u )  -  u )  -  (
(ψ `  N )  -  N ) )  =  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )
229222, 223, 163, 164, 228syl22anc 1219 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  u )  -  (
(ψ `  N )  -  N ) )  =  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )
230221, 229eqtr2d 2476 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  +  ( N  -  u ) )  =  ( ( R `
 u )  -  ( R `  N ) ) )
231230fveq2d 5695 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )  =  ( abs `  (
( R `  u
)  -  ( R `
 N ) ) ) )
232 chpwordi 22495 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  RR  /\  u  e.  RR  /\  N  <_  u )  ->  (ψ `  N )  <_  (ψ `  u ) )
233101, 77, 79, 232syl3anc 1218 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  N
)  <_  (ψ `  u
) )
234146, 144, 233abssubge0d 12918 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( (ψ `  u
)  -  (ψ `  N ) ) )  =  ( (ψ `  u )  -  (ψ `  N ) ) )
235101, 77, 79abssuble0d 12919 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( N  -  u
) )  =  ( u  -  N ) )
236234, 235oveq12d 6109 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( (ψ `  u )  -  (ψ `  N ) ) )  +  ( abs `  ( N  -  u )
) )  =  ( ( (ψ `  u
)  -  (ψ `  N ) )  +  ( u  -  N
) ) )
237102recnd 9412 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  -  N )  e.  CC )
238214, 237addcomd 9571 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  +  ( u  -  N ) )  =  ( ( u  -  N )  +  ( (ψ `  u
)  -  (ψ `  N ) ) ) )
239236, 238eqtrd 2475 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( (ψ `  u )  -  (ψ `  N ) ) )  +  ( abs `  ( N  -  u )
) )  =  ( ( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) ) )
240216, 231, 2393brtr3d 4321 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  -  ( R `  N )
) )  <_  (
( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) ) )
241154, 212, 78, 240lediv1dd 11081 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  -  ( R `  N ) ) )  /  N
)  <_  ( (
( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) )  /  N ) )
242155, 213, 150, 241leadd2dd 9954 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( abs `  ( ( R `  u )  /  u
) ) )  +  ( ( abs `  (
( R `  u
)  -  ( R `
 N ) ) )  /  N ) )  <_  ( (
( ( u  -  N )  /  N
)  x.  ( abs `  ( ( R `  u )  /  u
) ) )  +  ( ( ( u  -  N )  +  ( (ψ `  u
)  -  (ψ `  N ) ) )  /  N ) ) )
243150recnd 9412 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( abs `  (
( R `  u
)  /  u ) ) )  e.  CC )
244148recnd 9412 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  /  N )  e.  CC )
245243, 196, 244addassd 9408 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( ( u  -  N )  /  N )  x.  ( abs `  ( ( R `
 u )  /  u ) ) )  +  ( ( u  -  N )  /  N ) )  +  ( ( (ψ `  u )  -  (ψ `  N ) )  /  N ) )  =  ( ( ( ( u  -  N )  /  N )  x.  ( abs `  (
( R `  u
)  /  u ) ) )  +  ( ( ( u  -  N )  /  N
)  +  ( ( (ψ `  u )  -  (ψ `  N )
)  /  N ) ) ) )
24686recnd 9412 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  /  u
) )  e.  CC )
247196, 246, 173adddid 9410 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( abs `  ( ( R `  u )  /  u
) )  +  1 ) )  =  ( ( ( ( u  -  N )  /  N )  x.  ( abs `  ( ( R `
 u )  /  u ) ) )  +  ( ( ( u  -  N )  /  N )  x.  1 ) ) )
248196mulid1d 9403 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  1 )  =  ( ( u  -  N )  /  N
) )
249248oveq2d 6107 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( abs `  ( ( R `  u )  /  u
) ) )  +  ( ( ( u  -  N )  /  N )  x.  1 ) )  =  ( ( ( ( u  -  N )  /  N )  x.  ( abs `  ( ( R `
 u )  /  u ) ) )  +  ( ( u  -  N )  /  N ) ) )
250247, 249eqtrd 2475 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( abs `  ( ( R `  u )  /  u
) )  +  1 ) )  =  ( ( ( ( u  -  N )  /  N )  x.  ( abs `  ( ( R `
 u )  /  u ) ) )  +  ( ( u  -  N )  /  N ) ) )
251250oveq1d 6106 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( ( abs `  ( ( R `  u )  /  u ) )  +  1 ) )  +  ( ( (ψ `  u )  -  (ψ `  N ) )  /  N ) )  =  ( ( ( ( ( u  -  N
)  /  N )  x.  ( abs `  (
( R `  u
)  /  u ) ) )  +  ( ( u  -  N
)  /  N ) )  +  ( ( (ψ `  u )  -  (ψ `  N )
)  /  N ) ) )
252237, 214, 164, 165divdird 10145 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) )  /  N )  =  ( ( ( u  -  N )  /  N )  +  ( ( (ψ `  u
)  -  (ψ `  N ) )  /  N ) ) )
253252oveq2d 6107 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( abs `  ( ( R `  u )  /  u
) ) )  +  ( ( ( u  -  N )  +  ( (ψ `  u
)  -  (ψ `  N ) ) )  /  N ) )  =  ( ( ( ( u  -  N
)  /  N )  x.  ( abs `  (
( R `  u
)  /  u ) ) )  +  ( ( ( u  -  N )  /  N
)  +  ( ( (ψ `  u )  -  (ψ `  N )
)  /  N ) ) ) )
254245, 251, 2533eqtr4d 2485 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( ( abs `  ( ( R `  u )  /  u ) )  +  1 ) )  +  ( ( (ψ `  u )  -  (ψ `  N ) )  /  N ) )  =  ( ( ( ( u  -  N )  /  N )  x.  ( abs `  (
( R `  u
)  /  u ) ) )  +  ( ( ( u  -  N )  +  ( (ψ `  u )  -  (ψ `  N )
) )  /  N
) ) )
255242, 254breqtrrd 4318 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( abs `  ( ( R `  u )  /  u
) ) )  +  ( ( abs `  (
( R `  u
)  -  ( R `
 N ) ) )  /  N ) )  <_  ( (
( ( u  -  N )  /  N
)  x.  ( ( abs `  ( ( R `  u )  /  u ) )  +  1 ) )  +  ( ( (ψ `  u )  -  (ψ `  N ) )  /  N ) ) )
25693, 156, 149, 211, 255letrd 9528 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( ( R `
 u )  /  u )  -  (
( R `  N
)  /  N ) ) )  <_  (
( ( ( u  -  N )  /  N )  x.  (
( abs `  (
( R `  u
)  /  u ) )  +  1 ) )  +  ( ( (ψ `  u )  -  (ψ `  N )
)  /  N ) ) )
257 remulcl 9367 . . . . . . . . . . . . 13  |-  ( ( 2  e.  RR  /\  ( ( u  -  N )  /  N
)  e.  RR )  ->  ( 2  x.  ( ( u  -  N )  /  N
) )  e.  RR )
25819, 103, 257sylancr 663 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  ( ( u  -  N )  /  N ) )  e.  RR )
259258, 138readdcld 9413 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
2  x.  ( ( u  -  N )  /  N ) )  +  ( T  / 
( log `  N
) ) )  e.  RR )
260 remulcl 9367 . . . . . . . . . . . . . . 15  |-  ( ( 2  e.  RR  /\  ( u  -  N
)  e.  RR )  ->  ( 2  x.  ( u  -  N
) )  e.  RR )
26119, 102, 260sylancr 663 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  ( u  -  N ) )  e.  RR )
262101, 137rerpdivcld 11054 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  /  ( log `  N
) )  e.  RR )
263110, 262remulcld 9414 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  e.  RR )
264261, 263readdcld 9413 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
2  x.  ( u  -  N ) )  +  ( T  x.  ( N  /  ( log `  N ) ) ) )  e.  RR )
26518adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
1  +  ( L  x.  E ) )  x.  N )  e.  RR )
26621adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  N )  e.  RR )
26776simp3d 1002 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  <_  ( ( 1  +  ( L  x.  E ) )  x.  N ) )
268 ltle 9463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1  +  ( L  x.  E ) )  e.  RR  /\  2  e.  RR )  ->  ( ( 1  +  ( L  x.  E
) )  <  2  ->  ( 1  +  ( L  x.  E ) )  <_  2 ) )
26916, 19, 268sylancl 662 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1  +  ( L  x.  E
) )  <  2  ->  ( 1  +  ( L  x.  E ) )  <_  2 ) )
27061, 269mpd 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1  +  ( L  x.  E ) )  <_  2 )
271270adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 1  +  ( L  x.  E ) )  <_ 
2 )
27216adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 1  +  ( L  x.  E ) )  e.  RR )
27319a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  2  e.  RR )
274272, 273, 78lemul1d 11066 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
1  +  ( L  x.  E ) )  <_  2  <->  ( (
1  +  ( L  x.  E ) )  x.  N )  <_ 
( 2  x.  N
) ) )
275271, 274mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
1  +  ( L  x.  E ) )  x.  N )  <_ 
( 2  x.  N
) )
27677, 265, 266, 267, 275letrd 9528 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  <_  ( 2  x.  N ) )
277 elicc2 11360 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  RR  /\  ( 2  x.  N
)  e.  RR )  ->  ( u  e.  ( N [,] (
2  x.  N ) )  <->  ( u  e.  RR  /\  N  <_  u  /\  u  <_  (
2  x.  N ) ) ) )
278101, 266, 277syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  e.  ( N [,] (
2  x.  N ) )  <->  ( u  e.  RR  /\  N  <_  u  /\  u  <_  (
2  x.  N ) ) ) )
27977, 79, 276, 278mpbir3and 1171 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  e.  ( N [,] ( 2  x.  N ) ) )
280 1re 9385 . . . . . . . . . . . . . . . . . 18  |-  1  e.  RR
281280rexri 9436 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR*
282 elioopnf 11383 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  RR*  ->  ( N  e.  ( 1 (,) +oo )  <->  ( N  e.  RR  /\  1  < 
N ) ) )
283281, 282ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( 1 (,) +oo )  <->  ( N  e.  RR  /\  1  < 
N ) )
284101, 136, 283sylanbrc 664 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  e.  ( 1 (,) +oo ) )
285 pntibndlem2.6 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. x  e.  ( 1 (,) +oo ) A. y  e.  (
x [,] ( 2  x.  x ) ) ( (ψ `  y
)  -  (ψ `  x ) )  <_ 
( ( 2  x.  ( y  -  x
) )  +  ( T  x.  ( x  /  ( log `  x
) ) ) ) )
286285adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  A. x  e.  ( 1 (,) +oo ) A. y  e.  ( x [,] ( 2  x.  x ) ) ( (ψ `  y
)  -  (ψ `  x ) )  <_ 
( ( 2  x.  ( y  -  x
) )  +  ( T  x.  ( x  /  ( log `  x
) ) ) ) )
287 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  N  ->  x  =  N )
288 oveq2 6099 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  N  ->  (
2  x.  x )  =  ( 2  x.  N ) )
289287, 288oveq12d 6109 . . . . . . . . . . . . . . . . 17  |-  ( x  =  N  ->  (
x [,] ( 2  x.  x ) )  =  ( N [,] ( 2  x.  N
) ) )
290 fveq2 5691 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  N  ->  (ψ `  x )  =  (ψ `  N ) )
291290oveq2d 6107 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  N  ->  (
(ψ `  y )  -  (ψ `  x )
)  =  ( (ψ `  y )  -  (ψ `  N ) ) )
292 oveq2 6099 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  N  ->  (
y  -  x )  =  ( y  -  N ) )
293292oveq2d 6107 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  N  ->  (
2  x.  ( y  -  x ) )  =  ( 2  x.  ( y  -  N
) ) )
294 fveq2 5691 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  N  ->  ( log `  x )  =  ( log `  N
) )
295287, 294oveq12d 6109 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  N  ->  (
x  /  ( log `  x ) )  =  ( N  /  ( log `  N ) ) )
296295oveq2d 6107 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  N  ->  ( T  x.  ( x  /  ( log `  x
) ) )  =  ( T  x.  ( N  /  ( log `  N
) ) ) )
297293, 296oveq12d 6109 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  N  ->  (
( 2  x.  (
y  -  x ) )  +  ( T  x.  ( x  / 
( log `  x
) ) ) )  =  ( ( 2  x.  ( y  -  N ) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) )
298291, 297breq12d 4305 . . . . . . . . . . . . . . . . 17  |-  ( x  =  N  ->  (
( (ψ `  y
)  -  (ψ `  x ) )  <_ 
( ( 2  x.  ( y  -  x
) )  +  ( T  x.  ( x  /  ( log `  x
) ) ) )  <-> 
( (ψ `  y
)  -  (ψ `  N ) )  <_ 
( ( 2  x.  ( y  -  N
) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) ) )
299289, 298raleqbidv 2931 . . . . . . . . . . . . . . . 16  |-  ( x  =  N  ->  ( A. y  e.  (
x [,] ( 2  x.  x ) ) ( (ψ `  y
)  -  (ψ `  x ) )  <_ 
( ( 2  x.  ( y  -  x
) )  +  ( T  x.  ( x  /  ( log `  x
) ) ) )  <->  A. y  e.  ( N [,] ( 2  x.  N ) ) ( (ψ `  y )  -  (ψ `  N )
)  <_  ( (
2  x.  ( y  -  N ) )  +  ( T  x.  ( N  /  ( log `  N ) ) ) ) ) )
300299rspcv 3069 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( 1 (,) +oo )  ->  ( A. x  e.  ( 1 (,) +oo ) A. y  e.  ( x [,] ( 2  x.  x
) ) ( (ψ `  y )  -  (ψ `  x ) )  <_ 
( ( 2  x.  ( y  -  x
) )  +  ( T  x.  ( x  /  ( log `  x
) ) ) )  ->  A. y  e.  ( N [,] ( 2  x.  N ) ) ( (ψ `  y
)  -  (ψ `  N ) )  <_ 
( ( 2  x.  ( y  -  N
) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) ) )
301284, 286, 300sylc 60 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  A. y  e.  ( N [,] (
2  x.  N ) ) ( (ψ `  y )  -  (ψ `  N ) )  <_ 
( ( 2  x.  ( y  -  N
) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) )
302 fveq2 5691 . . . . . . . . . . . . . . . . 17  |-  ( y  =  u  ->  (ψ `  y )  =  (ψ `  u ) )
303302oveq1d 6106 . . . . . . . . . . . . . . . 16  |-  ( y  =  u  ->  (
(ψ `  y )  -  (ψ `  N )
)  =  ( (ψ `  u )  -  (ψ `  N ) ) )
304 oveq1 6098 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  u  ->  (
y  -  N )  =  ( u  -  N ) )
305304oveq2d 6107 . . . . . . . . . . . . . . . . 17  |-  ( y  =  u  ->  (
2  x.  ( y  -  N ) )  =  ( 2  x.  ( u  -  N
) ) )
306305oveq1d 6106 . . . . . . . . . . . . . . . 16  |-  ( y  =  u  ->  (
( 2  x.  (
y  -  N ) )  +  ( T  x.  ( N  / 
( log `  N
) ) ) )  =  ( ( 2  x.  ( u  -  N ) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) )
307303, 306breq12d 4305 . . . . . . . . . . . . . . 15  |-  ( y  =  u  ->  (
( (ψ `  y
)  -  (ψ `  N ) )  <_ 
( ( 2  x.  ( y  -  N
) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) )  <-> 
( (ψ `  u
)  -  (ψ `  N ) )  <_ 
( ( 2  x.  ( u  -  N
) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) ) )
308307rspcv 3069 . . . . . . . . . . . . . 14  |-  ( u  e.  ( N [,] ( 2  x.  N
) )  ->  ( A. y  e.  ( N [,] ( 2  x.  N ) ) ( (ψ `  y )  -  (ψ `  N )
)  <_  ( (
2  x.  ( y  -  N ) )  +  ( T  x.  ( N  /  ( log `  N ) ) ) )  ->  (
(ψ `  u )  -  (ψ `  N )
)  <_  ( (
2  x.  ( u  -  N ) )  +  ( T  x.  ( N  /  ( log `  N ) ) ) ) ) )
309279, 301, 308sylc 60 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (ψ `  u )  -  (ψ `  N ) )  <_ 
( ( 2  x.  ( u  -  N
) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) )
310147, 264, 78, 309lediv1dd 11081 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  /  N )  <_  ( ( ( 2  x.  ( u  -  N ) )  +  ( T  x.  ( N  /  ( log `  N ) ) ) )  /  N
) )
311261recnd 9412 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  ( u  -  N ) )  e.  CC )
312108adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  T  e.  RR+ )
313312rpred 11027 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  T  e.  RR )
314313, 262remulcld 9414 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  e.  RR )
315314recnd 9412 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  e.  CC )
316 divdir 10017 . . . . . . . . . . . . . 14  |-  ( ( ( 2  x.  (
u  -  N ) )  e.  CC  /\  ( T  x.  ( N  /  ( log `  N
) ) )  e.  CC  /\  ( N  e.  CC  /\  N  =/=  0 ) )  -> 
( ( ( 2  x.  ( u  -  N ) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) )  /  N )  =  ( ( ( 2  x.  ( u  -  N ) )  /  N )  +  ( ( T  x.  ( N  /  ( log `  N
) ) )  /  N ) ) )
317311, 315, 176, 316syl3anc 1218 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( 2  x.  (
u  -  N ) )  +  ( T  x.  ( N  / 
( log `  N
) ) ) )  /  N )  =  ( ( ( 2  x.  ( u  -  N ) )  /  N )  +  ( ( T  x.  ( N  /  ( log `  N
) ) )  /  N ) ) )
318 2cnd 10394 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  2  e.  CC )
319318, 237, 164, 165divassd 10142 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
2  x.  ( u  -  N ) )  /  N )  =  ( 2  x.  (
( u  -  N
)  /  N ) ) )
320110recnd 9412 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  T  e.  CC )
321137rpcnne0d 11036 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( log `  N )  e.  CC  /\  ( log `  N )  =/=  0
) )
322 div12 10016 . . . . . . . . . . . . . . . . 17  |-  ( ( T  e.  CC  /\  N  e.  CC  /\  (
( log `  N
)  e.  CC  /\  ( log `  N )  =/=  0 ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  =  ( N  x.  ( T  / 
( log `  N
) ) ) )
323320, 164, 321, 322syl3anc 1218 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  =  ( N  x.  ( T  / 
( log `  N
) ) ) )
324323oveq1d 6106 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( T  x.  ( N  /  ( log `  N
) ) )  /  N )  =  ( ( N  x.  ( T  /  ( log `  N
) ) )  /  N ) )
325312, 137rpdivcld 11044 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  RR+ )
326325rpcnd 11029 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  CC )
327326, 164, 165divcan3d 10112 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( N  x.  ( T  /  ( log `  N
) ) )  /  N )  =  ( T  /  ( log `  N ) ) )
328324, 327eqtrd 2475 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( T  x.  ( N  /  ( log `  N
) ) )  /  N )  =  ( T  /  ( log `  N ) ) )
329319, 328oveq12d 6109 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( 2  x.  (
u  -  N ) )  /  N )  +  ( ( T  x.  ( N  / 
( log `  N
) ) )  /  N ) )  =  ( ( 2  x.  ( ( u  -  N )  /  N
) )  +  ( T  /  ( log `  N ) ) ) )
330317, 329eqtrd 2475 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( 2  x.  (
u  -  N ) )  +  ( T  x.  ( N  / 
( log `  N
) ) ) )  /  N )  =  ( ( 2  x.  ( ( u  -  N )  /  N
) )  +  ( T  /  ( log `  N ) ) ) )
331310, 330breqtrd 4316 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  /  N )  <_  ( ( 2  x.  ( ( u  -  N )  /  N ) )  +  ( T  /  ( log `  N ) ) ) )
332148, 259, 142, 331leadd2dd 9954 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( ( abs `  ( ( R `  u )  /  u ) )  +  1 ) )  +  ( ( (ψ `  u )  -  (ψ `  N ) )  /  N ) )  <_ 
( ( ( ( u  -  N )  /  N )  x.  ( ( abs `  (
( R `  u
)  /  u ) )  +  1 ) )  +  ( ( 2  x.  ( ( u  -  N )  /  N ) )  +  ( T  / 
( log `  N
) ) ) ) )
333142recnd 9412 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( abs `  ( ( R `  u )  /  u
) )  +  1 ) )  e.  CC )
334258recnd 9412 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  ( ( u  -  N )  /  N ) )  e.  CC )
335138recnd 9412 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  CC )
336333, 334, 335addassd 9408 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( ( u  -  N )  /  N )  x.  (
( abs `  (
( R `  u
)  /  u ) )  +  1 ) )  +  ( 2  x.  ( ( u  -  N )  /  N ) ) )  +  ( T  / 
( log `  N
) ) )  =  ( ( ( ( u  -  N )  /  N )  x.  ( ( abs `  (
( R `  u
)  /  u ) )  +  1 ) )  +  ( ( 2  x.  ( ( u  -  N )  /  N ) )  +  ( T  / 
( log `  N
) ) ) ) )
337 2cn 10392 . . . . . . . . . . . . . . 15  |-  2  e.  CC
338 mulcom 9368 . . . . . . . . . . . . . . 15  |-  ( ( 2  e.  CC  /\  ( ( u  -  N )  /  N
)  e.  CC )  ->  ( 2  x.  ( ( u  -  N )  /  N
) )  =  ( ( ( u  -  N )  /  N
)  x.  2 ) )
339337, 196, 338sylancr 663 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  ( ( u  -  N )  /  N ) )  =  ( ( ( u  -  N )  /  N )  x.  2 ) )
340339oveq2d 6107 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( ( abs `  ( ( R `  u )  /  u ) )  +  1 ) )  +  ( 2  x.  ( ( u  -  N )  /  N
) ) )  =  ( ( ( ( u  -  N )  /  N )  x.  ( ( abs `  (
( R `  u
)  /  u ) )  +  1 ) )  +  ( ( ( u  -  N
)  /  N )  x.  2 ) ) )
341141recnd 9412 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  /  u ) )  +  1 )  e.  CC )
342196, 341, 318adddid 9410 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( ( abs `  ( ( R `  u )  /  u ) )  +  1 )  +  2 ) )  =  ( ( ( ( u  -  N )  /  N )  x.  ( ( abs `  (
( R `  u
)  /  u ) )  +  1 ) )  +  ( ( ( u  -  N
)  /  N )  x.  2 ) ) )
343246, 173, 318addassd 9408 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( abs `  (
( R `  u
)  /  u ) )  +  1 )  +  2 )  =  ( ( abs `  (
( R `  u
)  /  u ) )  +  ( 1  +  2 ) ) )
344 1p2e3 10446 . . . . . . . . . . . . . . . 16  |-  ( 1  +  2 )  =  3
345344oveq2i 6102 . . . . . . . . . . . . . . 15  |-  ( ( abs `  ( ( R `  u )  /  u ) )  +  ( 1  +  2 ) )  =  ( ( abs `  (
( R `  u
)  /  u ) )  +  3 )
346343, 345syl6eq 2491 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( abs `  (
( R `  u
)  /  u ) )  +  1 )  +  2 )  =  ( ( abs `  (
( R `  u
)  /  u ) )  +  3 ) )
347346oveq2d 6107 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( ( abs `  ( ( R `  u )  /  u ) )  +  1 )  +  2 ) )  =  ( ( ( u  -  N )  /  N )  x.  (
( abs `  (
( R `  u
)  /  u ) )  +  3 ) ) )
348340, 342, 3473eqtr2d 2481 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( ( abs `  ( ( R `  u )  /  u ) )  +  1 ) )  +  ( 2  x.  ( ( u  -  N )  /  N
) ) )  =  ( ( ( u  -  N )  /  N )  x.  (
( abs `  (
( R `  u
)  /  u ) )  +  3 ) ) )
349348oveq1d 6106 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( ( u  -  N )  /  N )  x.  (
( abs `  (
( R `  u
)  /  u ) )  +  1 ) )  +  ( 2  x.  ( ( u  -  N )  /  N ) ) )  +  ( T  / 
( log `  N
) ) )  =  ( ( ( ( u  -  N )  /  N )  x.  ( ( abs `  (
( R `  u
)  /  u ) )  +  3 ) )  +  ( T  /  ( log `  N
) ) ) )
350336, 349eqtr3d 2477 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( ( abs `  ( ( R `  u )  /  u ) )  +  1 ) )  +  ( ( 2  x.  ( ( u  -  N )  /  N ) )  +  ( T  /  ( log `  N ) ) ) )  =  ( ( ( ( u  -  N )  /  N )  x.  (
( abs `  (
( R `  u
)  /  u ) )  +  3 ) )  +  ( T  /  ( log `  N
) ) ) )
351332, 350breqtrd 4316 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( ( u  -  N )  /  N
)  x.  ( ( abs `  ( ( R `  u )  /  u ) )  +  1 ) )  +  ( ( (ψ `  u )  -  (ψ `  N ) )  /  N ) )  <_ 
( ( ( ( u  -  N )  /  N )  x.  ( ( abs `  (
( R `  u
)  /  u ) )  +  3 ) )  +  ( T  /  ( log `  N
) ) ) )
35293, 149, 139, 256, 351letrd 9528 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( ( R `
 u )  /  u )  -  (
( R `  N
)  /  N ) ) )  <_  (
( ( ( u  -  N )  /  N )  x.  (
( abs `  (
( R `  u
)  /  u ) )  +  3 ) )  +  ( T  /  ( log `  N
) ) ) )
353100rehalfcld 10571 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( E  /  2 )  / 
2 )  e.  RR )
35477, 272, 78ledivmul2d 11077 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  /  N )  <_  ( 1  +  ( L  x.  E
) )  <->  u  <_  ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )
355267, 354mpbird 232 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  /  N )  <_  (
1  +  ( L  x.  E ) ) )
356 ax-1cn 9340 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
35715adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( L  x.  E )  e.  RR )
358357recnd 9412 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( L  x.  E )  e.  CC )
359 addcom 9555 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  CC  /\  ( L  x.  E
)  e.  CC )  ->  ( 1  +  ( L  x.  E
) )  =  ( ( L  x.  E
)  +  1 ) )
360356, 358, 359sylancr 663 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 1  +  ( L  x.  E ) )  =  ( ( L  x.  E )  +  1 ) )
361355, 360breqtrd 4316 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  /  N )  <_  (
( L  x.  E
)  +  1 ) )
362171, 111, 357lesubaddd 9936 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  /  N
)  -  1 )  <_  ( L  x.  E )  <->  ( u  /  N )  <_  (
( L  x.  E
)  +  1 ) ) )
363361, 362mpbird 232 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  /  N )  -  1 )  <_ 
( L  x.  E
) )
364169, 363eqbrtrd 4312 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( (