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

Theorem pntibndlem2 20756
Description: Lemma for pntibnd 20758. 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 10405 . 2  |-  ( ph  ->  N  e.  RR+ )
3 pntibndlem2.11 . . . . 5  |-  ( ph  ->  ( ( Y  < 
N  /\  N  <_  ( ( M  /  2
)  x.  Y ) )  /\  ( abs `  ( ( R `  N )  /  N
) )  <_  ( E  /  2 ) ) )
43simpld 445 . . . 4  |-  ( ph  ->  ( Y  <  N  /\  N  <_  ( ( M  /  2 )  x.  Y ) ) )
54simpld 445 . . 3  |-  ( ph  ->  Y  <  N )
6 1re 8853 . . . . . . 7  |-  1  e.  RR
76a1i 10 . . . . . 6  |-  ( ph  ->  1  e.  RR )
8 ioossre 10728 . . . . . . . 8  |-  ( 0 (,) 1 )  C_  RR
9 pntibnd.r . . . . . . . . 9  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
10 pntibndlem1.1 . . . . . . . . 9  |-  ( ph  ->  A  e.  RR+ )
11 pntibndlem1.l . . . . . . . . 9  |-  L  =  ( ( 1  / 
4 )  /  ( A  +  3 ) )
129, 10, 11pntibndlem1 20754 . . . . . . . 8  |-  ( ph  ->  L  e.  ( 0 (,) 1 ) )
138, 12sseldi 3191 . . . . . . 7  |-  ( ph  ->  L  e.  RR )
14 pntibndlem3.4 . . . . . . . 8  |-  ( ph  ->  E  e.  ( 0 (,) 1 ) )
158, 14sseldi 3191 . . . . . . 7  |-  ( ph  ->  E  e.  RR )
1613, 15remulcld 8879 . . . . . 6  |-  ( ph  ->  ( L  x.  E
)  e.  RR )
177, 16readdcld 8878 . . . . 5  |-  ( ph  ->  ( 1  +  ( L  x.  E ) )  e.  RR )
181nnred 9777 . . . . 5  |-  ( ph  ->  N  e.  RR )
1917, 18remulcld 8879 . . . 4  |-  ( ph  ->  ( ( 1  +  ( L  x.  E
) )  x.  N
)  e.  RR )
20 2re 9831 . . . . 5  |-  2  e.  RR
21 remulcl 8838 . . . . 5  |-  ( ( 2  e.  RR  /\  N  e.  RR )  ->  ( 2  x.  N
)  e.  RR )
2220, 18, 21sylancr 644 . . . 4  |-  ( ph  ->  ( 2  x.  N
)  e.  RR )
23 pntibndlem3.c . . . . . . . . . 10  |-  C  =  ( ( 2  x.  B )  +  ( log `  2 ) )
24 pntibndlem3.3 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  RR+ )
2524rpred 10406 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
26 remulcl 8838 . . . . . . . . . . . 12  |-  ( ( 2  e.  RR  /\  B  e.  RR )  ->  ( 2  x.  B
)  e.  RR )
2720, 25, 26sylancr 644 . . . . . . . . . . 11  |-  ( ph  ->  ( 2  x.  B
)  e.  RR )
28 2rp 10375 . . . . . . . . . . . . 13  |-  2  e.  RR+
2928a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  2  e.  RR+ )
3029relogcld 19990 . . . . . . . . . . 11  |-  ( ph  ->  ( log `  2
)  e.  RR )
3127, 30readdcld 8878 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2  x.  B )  +  ( log `  2 ) )  e.  RR )
3223, 31syl5eqel 2380 . . . . . . . . 9  |-  ( ph  ->  C  e.  RR )
33 eliooord 10726 . . . . . . . . . . . 12  |-  ( E  e.  ( 0 (,) 1 )  ->  (
0  <  E  /\  E  <  1 ) )
3414, 33syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( 0  <  E  /\  E  <  1
) )
3534simpld 445 . . . . . . . . . 10  |-  ( ph  ->  0  <  E )
3615, 35elrpd 10404 . . . . . . . . 9  |-  ( ph  ->  E  e.  RR+ )
3732, 36rerpdivcld 10433 . . . . . . . 8  |-  ( ph  ->  ( C  /  E
)  e.  RR )
3837reefcld 12385 . . . . . . 7  |-  ( ph  ->  ( exp `  ( C  /  E ) )  e.  RR )
39 pnfxr 10471 . . . . . . 7  |-  +oo  e.  RR*
40 icossre 10746 . . . . . . 7  |-  ( ( ( exp `  ( C  /  E ) )  e.  RR  /\  +oo  e.  RR* )  ->  (
( exp `  ( C  /  E ) ) [,)  +oo )  C_  RR )
4138, 39, 40sylancl 643 . . . . . 6  |-  ( ph  ->  ( ( exp `  ( C  /  E ) ) [,)  +oo )  C_  RR )
42 pntibndlem2.8 . . . . . 6  |-  ( ph  ->  M  e.  ( ( exp `  ( C  /  E ) ) [,)  +oo ) )
4341, 42sseldd 3194 . . . . 5  |-  ( ph  ->  M  e.  RR )
44 ioossre 10728 . . . . . 6  |-  ( X (,)  +oo )  C_  RR
45 pntibndlem2.9 . . . . . 6  |-  ( ph  ->  Y  e.  ( X (,)  +oo ) )
4644, 45sseldi 3191 . . . . 5  |-  ( ph  ->  Y  e.  RR )
4743, 46remulcld 8879 . . . 4  |-  ( ph  ->  ( M  x.  Y
)  e.  RR )
4820a1i 10 . . . . 5  |-  ( ph  ->  2  e.  RR )
49 eliooord 10726 . . . . . . . . . . . . 13  |-  ( L  e.  ( 0 (,) 1 )  ->  (
0  <  L  /\  L  <  1 ) )
5012, 49syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  <  L  /\  L  <  1
) )
5150simpld 445 . . . . . . . . . . 11  |-  ( ph  ->  0  <  L )
5213, 51elrpd 10404 . . . . . . . . . 10  |-  ( ph  ->  L  e.  RR+ )
5352rpge0d 10410 . . . . . . . . 9  |-  ( ph  ->  0  <_  L )
5450simprd 449 . . . . . . . . 9  |-  ( ph  ->  L  <  1 )
5536rpge0d 10410 . . . . . . . . 9  |-  ( ph  ->  0  <_  E )
5634simprd 449 . . . . . . . . 9  |-  ( ph  ->  E  <  1 )
5713, 7, 15, 7, 53, 54, 55, 56ltmul12ad 9714 . . . . . . . 8  |-  ( ph  ->  ( L  x.  E
)  <  ( 1  x.  1 ) )
58 1t1e1 9886 . . . . . . . 8  |-  ( 1  x.  1 )  =  1
5957, 58syl6breq 4078 . . . . . . 7  |-  ( ph  ->  ( L  x.  E
)  <  1 )
6016, 7, 7, 59ltadd2dd 8991 . . . . . 6  |-  ( ph  ->  ( 1  +  ( L  x.  E ) )  <  ( 1  +  1 ) )
61 df-2 9820 . . . . . 6  |-  2  =  ( 1  +  1 )
6260, 61syl6breqr 4079 . . . . 5  |-  ( ph  ->  ( 1  +  ( L  x.  E ) )  <  2 )
6317, 48, 2, 62ltmul1dd 10457 . . . 4  |-  ( ph  ->  ( ( 1  +  ( L  x.  E
) )  x.  N
)  <  ( 2  x.  N ) )
644simprd 449 . . . . . 6  |-  ( ph  ->  N  <_  ( ( M  /  2 )  x.  Y ) )
6543recnd 8877 . . . . . . 7  |-  ( ph  ->  M  e.  CC )
6646recnd 8877 . . . . . . 7  |-  ( ph  ->  Y  e.  CC )
67 rpcnne0 10387 . . . . . . . 8  |-  ( 2  e.  RR+  ->  ( 2  e.  CC  /\  2  =/=  0 ) )
6828, 67mp1i 11 . . . . . . 7  |-  ( ph  ->  ( 2  e.  CC  /\  2  =/=  0 ) )
69 div23 9459 . . . . . . 7  |-  ( ( M  e.  CC  /\  Y  e.  CC  /\  (
2  e.  CC  /\  2  =/=  0 ) )  ->  ( ( M  x.  Y )  / 
2 )  =  ( ( M  /  2
)  x.  Y ) )
7065, 66, 68, 69syl3anc 1182 . . . . . 6  |-  ( ph  ->  ( ( M  x.  Y )  /  2
)  =  ( ( M  /  2 )  x.  Y ) )
7164, 70breqtrrd 4065 . . . . 5  |-  ( ph  ->  N  <_  ( ( M  x.  Y )  /  2 ) )
7218, 47, 29lemuldiv2d 10452 . . . . 5  |-  ( ph  ->  ( ( 2  x.  N )  <_  ( M  x.  Y )  <->  N  <_  ( ( M  x.  Y )  / 
2 ) ) )
7371, 72mpbird 223 . . . 4  |-  ( ph  ->  ( 2  x.  N
)  <_  ( M  x.  Y ) )
7419, 22, 47, 63, 73ltletrd 8992 . . 3  |-  ( ph  ->  ( ( 1  +  ( L  x.  E
) )  x.  N
)  <  ( M  x.  Y ) )
75 pntibndlem3.2 . . . . . . . . . . . 12  |-  ( ph  ->  A. x  e.  RR+  ( abs `  ( ( R `  x )  /  x ) )  <_  A )
76 pntibndlem3.k . . . . . . . . . . . 12  |-  K  =  ( exp `  ( B  /  ( E  / 
2 ) ) )
779, 10, 11, 75, 24, 76, 23, 14, 10, 1pntibndlem2a 20755 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  e.  RR  /\  N  <_  u  /\  u  <_  (
( 1  +  ( L  x.  E ) )  x.  N ) ) )
7877simp1d 967 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  e.  RR )
792adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  e.  RR+ )
8077simp2d 968 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  <_  u )
8178, 79, 80rpgecld 10441 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  e.  RR+ )
829pntrf 20728 . . . . . . . . . 10  |-  R : RR+
--> RR
8382ffvelrni 5680 . . . . . . . . 9  |-  ( u  e.  RR+  ->  ( R `
 u )  e.  RR )
8481, 83syl 15 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  u )  e.  RR )
8584, 81rerpdivcld 10433 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  u )  e.  RR )
8685recnd 8877 . . . . . 6  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  u )  e.  CC )
8786abscld 11934 . . . . 5  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  /  u
) )  e.  RR )
8882ffvelrni 5680 . . . . . . . . . . . 12  |-  ( N  e.  RR+  ->  ( R `
 N )  e.  RR )
892, 88syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( R `  N
)  e.  RR )
9089, 1nndivred 9810 . . . . . . . . . 10  |-  ( ph  ->  ( ( R `  N )  /  N
)  e.  RR )
9190adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  N )  /  N )  e.  RR )
9291recnd 8877 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  N )  /  N )  e.  CC )
9386, 92subcld 9173 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  /  u )  -  ( ( R `
 N )  /  N ) )  e.  CC )
9493abscld 11934 . . . . . 6  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( ( R `
 u )  /  u )  -  (
( R `  N
)  /  N ) ) )  e.  RR )
9592abscld 11934 . . . . . 6  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  N )  /  N
) )  e.  RR )
9694, 95readdcld 8878 . . . . 5  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( ( R `  u )  /  u )  -  ( ( R `  N )  /  N
) ) )  +  ( abs `  (
( R `  N
)  /  N ) ) )  e.  RR )
9715adantr 451 . . . . 5  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  E  e.  RR )
9886, 92abs2difd 11955 . . . . . 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 ) ) ) )
9987, 95, 94lesubaddd 9385 . . . . . 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 ) ) ) ) )
10098, 99mpbid 201 . . . . 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
) ) ) )
10197rehalfcld 9974 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( E  /  2 )  e.  RR )
10218adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  e.  RR )
10378, 102resubcld 9227 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  -  N )  e.  RR )
104103, 79rerpdivcld 10433 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  e.  RR )
105 3re 9833 . . . . . . . . . . . 12  |-  3  e.  RR
106105a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  3  e.  RR )
10787, 106readdcld 8878 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  /  u ) )  +  3 )  e.  RR )
108104, 107remulcld 8879 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( abs `  ( ( R `  u )  /  u
) )  +  3 ) )  e.  RR )
109 pntibndlem2.5 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  RR+ )
110109rpred 10406 . . . . . . . . . . 11  |-  ( ph  ->  T  e.  RR )
111110adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  T  e.  RR )
1126a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  1  e.  RR )
113 4nn 9895 . . . . . . . . . . . . . . . . . 18  |-  4  e.  NN
114 nnrp 10379 . . . . . . . . . . . . . . . . . 18  |-  ( 4  e.  NN  ->  4  e.  RR+ )
115113, 114mp1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  4  e.  RR+ )
11636, 115rpdivcld 10423 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E  /  4
)  e.  RR+ )
117109, 116rpdivcld 10423 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( T  /  ( E  /  4 ) )  e.  RR+ )
118117rpred 10406 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  /  ( E  /  4 ) )  e.  RR )
119118reefcld 12385 . . . . . . . . . . . . 13  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  e.  RR )
120119adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( exp `  ( T  /  ( E  /  4 ) ) )  e.  RR )
121 efgt1 12412 . . . . . . . . . . . . . 14  |-  ( ( T  /  ( E  /  4 ) )  e.  RR+  ->  1  < 
( exp `  ( T  /  ( E  / 
4 ) ) ) )
122117, 121syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  1  <  ( exp `  ( T  /  ( E  /  4 ) ) ) )
123122adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  1  <  ( exp `  ( T  /  ( E  / 
4 ) ) ) )
124 pntibndlem2.7 . . . . . . . . . . . . . . . 16  |-  X  =  ( ( exp `  ( T  /  ( E  / 
4 ) ) )  +  Z )
125 pntibndlem3.6 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Z  e.  RR+ )
126125rpred 10406 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Z  e.  RR )
127119, 126readdcld 8878 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( exp `  ( T  /  ( E  / 
4 ) ) )  +  Z )  e.  RR )
128124, 127syl5eqel 2380 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
129119, 125ltaddrpd 10435 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  <  ( ( exp `  ( T  /  ( E  /  4 ) ) )  +  Z ) )
130129, 124syl6breqr 4079 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  <  X )
131 eliooord 10726 . . . . . . . . . . . . . . . . 17  |-  ( Y  e.  ( X (,)  +oo )  ->  ( X  <  Y  /\  Y  <  +oo ) )
13245, 131syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  <  Y  /\  Y  <  +oo )
)
133132simpld 445 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  <  Y )
134119, 128, 46, 130, 133lttrd 8993 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  <  Y )
135119, 46, 18, 134, 5lttrd 8993 . . . . . . . . . . . . 13  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  <  N )
136135adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( exp `  ( T  /  ( E  /  4 ) ) )  <  N )
137112, 120, 102, 123, 136lttrd 8993 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  1  <  N )
138102, 137rplogcld 19996 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( log `  N )  e.  RR+ )
139111, 138rerpdivcld 10433 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  RR )
140108, 139readdcld 8878 . . . . . . . 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 )
141 peano2re 9001 . . . . . . . . . . . 12  |-  ( ( abs `  ( ( R `  u )  /  u ) )  e.  RR  ->  (
( abs `  (
( R `  u
)  /  u ) )  +  1 )  e.  RR )
14287, 141syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  /  u ) )  +  1 )  e.  RR )
143104, 142remulcld 8879 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( abs `  ( ( R `  u )  /  u
) )  +  1 ) )  e.  RR )
144 chpcl 20378 . . . . . . . . . . . . 13  |-  ( u  e.  RR  ->  (ψ `  u )  e.  RR )
14578, 144syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  u
)  e.  RR )
146 chpcl 20378 . . . . . . . . . . . . 13  |-  ( N  e.  RR  ->  (ψ `  N )  e.  RR )
147102, 146syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  N
)  e.  RR )
148145, 147resubcld 9227 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (ψ `  u )  -  (ψ `  N ) )  e.  RR )
149148, 79rerpdivcld 10433 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  /  N )  e.  RR )
150143, 149readdcld 8878 . . . . . . . . 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 )
151104, 87remulcld 8879 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( abs `  (
( R `  u
)  /  u ) ) )  e.  RR )
15289adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  N )  e.  RR )
15384, 152resubcld 9227 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  -  ( R `  N ) )  e.  RR )
154153recnd 8877 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  -  ( R `  N ) )  e.  CC )
155154abscld 11934 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  -  ( R `  N )
) )  e.  RR )
156155, 79rerpdivcld 10433 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  -  ( R `  N ) ) )  /  N
)  e.  RR )
157151, 156readdcld 8878 . . . . . . . . . 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 )
158104, 85remulcld 8879 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  RR )
159158renegcld 9226 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  -u ( ( ( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  RR )
160159recnd 8877 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  -u ( ( ( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  CC )
161153, 79rerpdivcld 10433 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  -  ( R `
 N ) )  /  N )  e.  RR )
162161recnd 8877 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  -  ( R `
 N ) )  /  N )  e.  CC )
163160, 162abstrid 11954 . . . . . . . . . . 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 ) ) ) )
16478recnd 8877 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  e.  CC )
165102recnd 8877 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  e.  CC )
16679rpne0d 10411 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  =/=  0 )
167164, 165, 165, 166divsubdird 9591 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  =  ( ( u  /  N )  -  ( N  /  N ) ) )
168165, 166dividd 9550 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  /  N )  =  1 )
169168oveq2d 5890 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  /  N )  -  ( N  /  N ) )  =  ( ( u  /  N )  -  1 ) )
170167, 169eqtrd 2328 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  =  ( ( u  /  N )  -  1 ) )
171170oveq1d 5889 . . . . . . . . . . . . . . . . 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 ) ) )
17278, 79rerpdivcld 10433 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  /  N )  e.  RR )
173172recnd 8877 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  /  N )  e.  CC )
174 ax-1cn 8811 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  CC
175174a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  1  e.  CC )
176173, 175, 86subdird 9252 . . . . . . . . . . . . . . . . 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 ) ) ) )
17781rpcnne0d 10415 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  e.  CC  /\  u  =/=  0 ) )
17879rpcnne0d 10415 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  e.  CC  /\  N  =/=  0 ) )
17984recnd 8877 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  u )  e.  CC )
180 dmdcan 9486 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( u  e.  CC  /\  u  =/=  0 )  /\  ( N  e.  CC  /\  N  =/=  0 )  /\  ( R `  u )  e.  CC )  ->  (
( u  /  N
)  x.  ( ( R `  u )  /  u ) )  =  ( ( R `
 u )  /  N ) )
181177, 178, 179, 180syl3anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  /  N )  x.  ( ( R `
 u )  /  u ) )  =  ( ( R `  u )  /  N
) )
18286mulid2d 8869 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 1  x.  ( ( R `
 u )  /  u ) )  =  ( ( R `  u )  /  u
) )
183181, 182oveq12d 5892 . . . . . . . . . . . . . . . . 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 ) ) )
184171, 176, 1833eqtrd 2332 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  =  ( ( ( R `
 u )  /  N )  -  (
( R `  u
)  /  u ) ) )
185184negeqd 9062 . . . . . . . . . . . . . . 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
) ) )
18684, 79rerpdivcld 10433 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  N )  e.  RR )
187186recnd 8877 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  N )  e.  CC )
188187, 86negsubdi2d 9189 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  -u ( ( ( R `  u
)  /  N )  -  ( ( R `
 u )  /  u ) )  =  ( ( ( R `
 u )  /  u )  -  (
( R `  u
)  /  N ) ) )
189185, 188eqtrd 2328 . . . . . . . . . . . . . 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 ) ) )
190152recnd 8877 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  N )  e.  CC )
191179, 190, 165, 166divsubdird 9591 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  -  ( R `
 N ) )  /  N )  =  ( ( ( R `
 u )  /  N )  -  (
( R `  N
)  /  N ) ) )
192189, 191oveq12d 5892 . . . . . . . . . . . . 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 ) ) ) )
19386, 187, 92npncand 9197 . . . . . . . . . . . . 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 ) ) )
194192, 193eqtrd 2328 . . . . . . . . . . . 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 ) ) )
195194fveq2d 5545 . . . . . . . . . . 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 ) ) ) )
196158recnd 8877 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  CC )
197196absnegd 11947 . . . . . . . . . . . . 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 ) ) ) )
198104recnd 8877 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  e.  CC )
199198, 86absmuld 11952 . . . . . . . . . . . . 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
) ) ) )
20078, 102subge0d 9378 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 0  <_  ( u  -  N )  <->  N  <_  u ) )
20180, 200mpbird 223 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  0  <_  ( u  -  N ) )
202103, 79, 201divge0d 10442 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  0  <_  ( ( u  -  N
)  /  N ) )
203104, 202absidd 11921 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( u  -  N )  /  N
) )  =  ( ( u  -  N
)  /  N ) )
204203oveq1d 5889 . . . . . . . . . . . . 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
) ) ) )
205197, 199, 2043eqtrd 2332 . . . . . . . . . . . 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
) ) ) )
206154, 165, 166absdivd 11953 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( ( R `
 u )  -  ( R `  N ) )  /  N ) )  =  ( ( abs `  ( ( R `  u )  -  ( R `  N ) ) )  /  ( abs `  N
) ) )
20779rprege0d 10413 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  e.  RR  /\  0  <_  N ) )
208 absid 11797 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  RR  /\  0  <_  N )  -> 
( abs `  N
)  =  N )
209207, 208syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  N )  =  N )
210209oveq2d 5890 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  -  ( R `  N ) ) )  /  ( abs `  N ) )  =  ( ( abs `  ( ( R `  u )  -  ( R `  N )
) )  /  N
) )
211206, 210eqtrd 2328 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( ( R `
 u )  -  ( R `  N ) )  /  N ) )  =  ( ( abs `  ( ( R `  u )  -  ( R `  N ) ) )  /  N ) )
212205, 211oveq12d 5892 . . . . . . . . . . 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
) ) )
213163, 195, 2123brtr3d 4068 . . . . . . . . . 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
) ) )
214103, 148readdcld 8878 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  +  ( (ψ `  u )  -  (ψ `  N ) ) )  e.  RR )
215214, 79rerpdivcld 10433 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) )  /  N )  e.  RR )
216148recnd 8877 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (ψ `  u )  -  (ψ `  N ) )  e.  CC )
217165, 164subcld 9173 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  -  u )  e.  CC )
218216, 217abstrid 11954 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )  <_ 
( ( abs `  (
(ψ `  u )  -  (ψ `  N )
) )  +  ( abs `  ( N  -  u ) ) ) )
2199pntrval 20727 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  RR+  ->  ( R `
 u )  =  ( (ψ `  u
)  -  u ) )
22081, 219syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  u )  =  ( (ψ `  u )  -  u ) )
2219pntrval 20727 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  RR+  ->  ( R `
 N )  =  ( (ψ `  N
)  -  N ) )
22279, 221syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  N )  =  ( (ψ `  N )  -  N ) )
223220, 222oveq12d 5892 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  -  ( R `  N ) )  =  ( ( (ψ `  u )  -  u
)  -  ( (ψ `  N )  -  N
) ) )
224145recnd 8877 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  u
)  e.  CC )
225147recnd 8877 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  N
)  e.  CC )
226 subadd4 9107 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (ψ `  u
)  e.  CC  /\  (ψ `  N )  e.  CC )  /\  (
u  e.  CC  /\  N  e.  CC )
)  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  -  ( u  -  N ) )  =  ( ( (ψ `  u )  +  N
)  -  ( (ψ `  N )  +  u
) ) )
227 sub4 9108 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (ψ `  u
)  e.  CC  /\  (ψ `  N )  e.  CC )  /\  (
u  e.  CC  /\  N  e.  CC )
)  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  -  ( u  -  N ) )  =  ( ( (ψ `  u )  -  u
)  -  ( (ψ `  N )  -  N
) ) )
228 addsub4 9106 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (ψ `  u
)  e.  CC  /\  N  e.  CC )  /\  ( (ψ `  N
)  e.  CC  /\  u  e.  CC )
)  ->  ( (
(ψ `  u )  +  N )  -  (
(ψ `  N )  +  u ) )  =  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )
229228an42s 800 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (ψ `  u
)  e.  CC  /\  (ψ `  N )  e.  CC )  /\  (
u  e.  CC  /\  N  e.  CC )
)  ->  ( (
(ψ `  u )  +  N )  -  (
(ψ `  N )  +  u ) )  =  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )
230226, 227, 2293eqtr3d 2336 . . . . . . . . . . . . . . . . 17  |-  ( ( ( (ψ `  u
)  e.  CC  /\  (ψ `  N )  e.  CC )  /\  (
u  e.  CC  /\  N  e.  CC )
)  ->  ( (
(ψ `  u )  -  u )  -  (
(ψ `  N )  -  N ) )  =  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )
231224, 225, 164, 165, 230syl22anc 1183 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  u )  -  (
(ψ `  N )  -  N ) )  =  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )
232223, 231eqtr2d 2329 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  +  ( N  -  u ) )  =  ( ( R `
 u )  -  ( R `  N ) ) )
233232fveq2d 5545 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )  =  ( abs `  (
( R `  u
)  -  ( R `
 N ) ) ) )
234 chpwordi 20411 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  RR  /\  u  e.  RR  /\  N  <_  u )  ->  (ψ `  N )  <_  (ψ `  u ) )
235102, 78, 80, 234syl3anc 1182 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  N
)  <_  (ψ `  u
) )
236147, 145, 235abssubge0d 11930 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( (ψ `  u
)  -  (ψ `  N ) ) )  =  ( (ψ `  u )  -  (ψ `  N ) ) )
237102, 78, 80abssuble0d 11931 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( N  -  u
) )  =  ( u  -  N ) )
238236, 237oveq12d 5892 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( (ψ `  u )  -  (ψ `  N ) ) )  +  ( abs `  ( N  -  u )
) )  =  ( ( (ψ `  u
)  -  (ψ `  N ) )  +  ( u  -  N
) ) )
239103recnd 8877 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  -  N )  e.  CC )
240216, 239addcomd 9030 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  +  ( u  -  N ) )  =  ( ( u  -  N )  +  ( (ψ `  u
)  -  (ψ `  N ) ) ) )
241238, 240eqtrd 2328 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( (ψ `  u )  -  (ψ `  N ) ) )  +  ( abs `  ( N  -  u )
) )  =  ( ( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) ) )
242218, 233, 2413brtr3d 4068 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  -  ( R `  N )
) )  <_  (
( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) ) )
243155, 214, 79, 242lediv1dd 10460 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  -  ( R `  N ) ) )  /  N
)  <_  ( (
( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) )  /  N ) )
244156, 215, 151, 243leadd2dd 9403 . . . . . . . . . . 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 ) ) )
245151recnd 8877 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( abs `  (
( R `  u
)  /  u ) ) )  e.  CC )
246149recnd 8877 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  /  N )  e.  CC )
247245, 198, 246addassd 8873 . . . . . . . . . . . 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 ) ) ) )
24887recnd 8877 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  /  u
) )  e.  CC )
249198, 248, 175adddid 8875 . . . . . . . . . . . . . 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 ) ) )
250198mulid1d 8868 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  1 )  =  ( ( u  -  N )  /  N
) )
251250oveq2d 5890 . . . . . . . . . . . . . 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 ) ) )
252249, 251eqtrd 2328 . . . . . . . . . . . . 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 ) ) )
253252oveq1d 5889 . . . . . . . . . . . 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 ) ) )
254239, 216, 165, 166divdird 9590 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) )  /  N )  =  ( ( ( u  -  N )  /  N )  +  ( ( (ψ `  u
)  -  (ψ `  N ) )  /  N ) ) )
255254oveq2d 5890 . . . . . . . . . . . 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 ) ) ) )
256247, 253, 2553eqtr4d 2338 . . . . . . . . . . 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
) ) )
257244, 256breqtrrd 4065 . . . . . . . . . 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 ) ) )
25894, 157, 150, 213, 257letrd 8989 . . . . . . . . 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 ) ) )
259 remulcl 8838 . . . . . . . . . . . . 13  |-  ( ( 2  e.  RR  /\  ( ( u  -  N )  /  N
)  e.  RR )  ->  ( 2  x.  ( ( u  -  N )  /  N
) )  e.  RR )
26020, 104, 259sylancr 644 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  ( ( u  -  N )  /  N ) )  e.  RR )
261260, 139readdcld 8878 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
2  x.  ( ( u  -  N )  /  N ) )  +  ( T  / 
( log `  N
) ) )  e.  RR )
262 remulcl 8838 . . . . . . . . . . . . . . 15  |-  ( ( 2  e.  RR  /\  ( u  -  N
)  e.  RR )  ->  ( 2  x.  ( u  -  N
) )  e.  RR )
26320, 103, 262sylancr 644 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  ( u  -  N ) )  e.  RR )
264102, 138rerpdivcld 10433 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  /  ( log `  N
) )  e.  RR )
265111, 264remulcld 8879 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  e.  RR )
266263, 265readdcld 8878 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
2  x.  ( u  -  N ) )  +  ( T  x.  ( N  /  ( log `  N ) ) ) )  e.  RR )
26719adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
1  +  ( L  x.  E ) )  x.  N )  e.  RR )
26822adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  N )  e.  RR )
26977simp3d 969 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  <_  ( ( 1  +  ( L  x.  E ) )  x.  N ) )
270 ltle 8926 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1  +  ( L  x.  E ) )  e.  RR  /\  2  e.  RR )  ->  ( ( 1  +  ( L  x.  E
) )  <  2  ->  ( 1  +  ( L  x.  E ) )  <_  2 ) )
27117, 20, 270sylancl 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1  +  ( L  x.  E
) )  <  2  ->  ( 1  +  ( L  x.  E ) )  <_  2 ) )
27262, 271mpd 14 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1  +  ( L  x.  E ) )  <_  2 )
273272adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 1  +  ( L  x.  E ) )  <_ 
2 )
27417adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 1  +  ( L  x.  E ) )  e.  RR )
27520a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  2  e.  RR )
276274, 275, 79lemul1d 10445 . . . . . . . . . . . . . . . . 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
) ) )
277273, 276mpbid 201 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
1  +  ( L  x.  E ) )  x.  N )  <_ 
( 2  x.  N
) )
27878, 267, 268, 269, 277letrd 8989 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  <_  ( 2  x.  N ) )
279 elicc2 10731 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  RR  /\  ( 2  x.  N
)  e.  RR )  ->  ( u  e.  ( N [,] (
2  x.  N ) )  <->  ( u  e.  RR  /\  N  <_  u  /\  u  <_  (
2  x.  N ) ) ) )
280102, 268, 279syl2anc 642 . . . . . . . . . . . . . . 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 ) ) ) )
28178, 80, 278, 280mpbir3and 1135 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  e.  ( N [,] ( 2  x.  N ) ) )
282 ressxr 8892 . . . . . . . . . . . . . . . . . 18  |-  RR  C_  RR*
283282, 6sselii 3190 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR*
284 elioopnf 10753 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  RR*  ->  ( N  e.  ( 1 (,) 
+oo )  <->  ( N  e.  RR  /\  1  < 
N ) ) )
285283, 284ax-mp 8 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( 1 (,) 
+oo )  <->  ( N  e.  RR  /\  1  < 
N ) )
286102, 137, 285sylanbrc 645 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  e.  ( 1 (,)  +oo ) )
287 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
) ) ) ) )
288287adantr 451 . . . . . . . . . . . . . . 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
) ) ) ) )
289 id 19 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  N  ->  x  =  N )
290 oveq2 5882 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  N  ->  (
2  x.  x )  =  ( 2  x.  N ) )
291289, 290oveq12d 5892 . . . . . . . . . . . . . . . . 17  |-  ( x  =  N  ->  (
x [,] ( 2  x.  x ) )  =  ( N [,] ( 2  x.  N
) ) )
292 fveq2 5541 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  N  ->  (ψ `  x )  =  (ψ `  N ) )
293292oveq2d 5890 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  N  ->  (
(ψ `  y )  -  (ψ `  x )
)  =  ( (ψ `  y )  -  (ψ `  N ) ) )
294 oveq2 5882 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  N  ->  (
y  -  x )  =  ( y  -  N ) )
295294oveq2d 5890 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  N  ->  (
2  x.  ( y  -  x ) )  =  ( 2  x.  ( y  -  N
) ) )
296 fveq2 5541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  N  ->  ( log `  x )  =  ( log `  N
) )
297289, 296oveq12d 5892 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  N  ->  (
x  /  ( log `  x ) )  =  ( N  /  ( log `  N ) ) )
298297oveq2d 5890 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  N  ->  ( T  x.  ( x  /  ( log `  x
) ) )  =  ( T  x.  ( N  /  ( log `  N
) ) ) )
299295, 298oveq12d 5892 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  N  ->  (
( 2  x.  (
y  -  x ) )  +  ( T  x.  ( x  / 
( log `  x
) ) ) )  =  ( ( 2  x.  ( y  -  N ) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) )
300293, 299breq12d 4052 . . . . . . . . . . . . . . . . 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
) ) ) ) ) )
301291, 300raleqbidv 2761 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
302301rspcv 2893 . . . . . . . . . . . . . . 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
) ) ) ) ) )
303286, 288, 302sylc 56 . . . . . . . . . . . . . 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
) ) ) ) )
304 fveq2 5541 . . . . . . . . . . . . . . . . 17  |-  ( y  =  u  ->  (ψ `  y )  =  (ψ `  u ) )
305304oveq1d 5889 . . . . . . . . . . . . . . . 16  |-  ( y  =  u  ->  (
(ψ `  y )  -  (ψ `  N )
)  =  ( (ψ `  u )  -  (ψ `  N ) ) )
306 oveq1 5881 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  u  ->  (
y  -  N )  =  ( u  -  N ) )
307306oveq2d 5890 . . . . . . . . . . . . . . . . 17  |-  ( y  =  u  ->  (
2  x.  ( y  -  N ) )  =  ( 2  x.  ( u  -  N
) ) )
308307oveq1d 5889 . . . . . . . . . . . . . . . 16  |-  ( y  =  u  ->  (
( 2  x.  (
y  -  N ) )  +  ( T  x.  ( N  / 
( log `  N
) ) ) )  =  ( ( 2  x.  ( u  -  N ) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) )
309305, 308breq12d 4052 . . . . . . . . . . . . . . 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
) ) ) ) ) )
310309rspcv 2893 . . . . . . . . . . . . . 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 ) ) ) ) ) )
311281, 303, 310sylc 56 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (ψ `  u )  -  (ψ `  N ) )  <_ 
( ( 2  x.  ( u  -  N
) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) )
312148, 266, 79, 311lediv1dd 10460 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  /  N )  <_  ( ( ( 2  x.  ( u  -  N ) )  +  ( T  x.  ( N  /  ( log `  N ) ) ) )  /  N
) )
313263recnd 8877 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  ( u  -  N ) )  e.  CC )
314109adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  T  e.  RR+ )
315314rpred 10406 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  T  e.  RR )
316315, 264remulcld 8879 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  e.  RR )
317316recnd 8877 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  e.  CC )
318 divdir 9463 . . . . . . . . . . . . . 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 ) ) )
319313, 317, 178, 318syl3anc 1182 . . . . . . . . . . . . 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 ) ) )
320 2cn 9832 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
321320a1i 10 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  2  e.  CC )
322321, 239, 165, 166divassd 9587 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
2  x.  ( u  -  N ) )  /  N )  =  ( 2  x.  (
( u  -  N
)  /  N ) ) )
323111recnd 8877 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  T  e.  CC )
324138rpcnne0d 10415 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( log `  N )  e.  CC  /\  ( log `  N )  =/=  0
) )
325 div12 9462 . . . . . . . . . . . . . . . . 17  |-  ( ( T  e.  CC  /\  N  e.  CC  /\  (
( log `  N
)  e.  CC  /\  ( log `  N )  =/=  0 ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  =  ( N  x.  ( T  / 
( log `  N
) ) ) )
326323, 165, 324, 325syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  =  ( N  x.  ( T  / 
( log `  N
) ) ) )
327326oveq1d 5889 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( T  x.  ( N  /  ( log `  N
) ) )  /  N )  =  ( ( N  x.  ( T  /  ( log `  N
) ) )  /  N ) )
328314, 138rpdivcld 10423 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  RR+ )
329328rpcnd 10408 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  CC )
330329, 165, 166divcan3d 9557 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( N  x.  ( T  /  ( log `  N
) ) )  /  N )  =  ( T  /  ( log `  N ) ) )
331327, 330eqtrd 2328 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( T  x.  ( N  /  ( log `  N
) ) )  /  N )  =  ( T  /  ( log `  N ) ) )
332322, 331oveq12d 5892 . . . . . . . . . . . . 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 ) ) ) )
333319, 332eqtrd 2328 . . . . . . . . . . . 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 ) ) ) )
334312, 333breqtrd 4063 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  /  N )  <_  ( ( 2  x.  ( ( u  -  N )  /  N ) )  +  ( T  /  ( log `  N ) ) ) )
335149, 261, 143, 334leadd2dd 9403 . . . . . . . . . 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
) ) ) ) )
336143recnd 8877 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( abs `  ( ( R `  u )  /  u
) )  +  1 ) )  e.  CC )
337260recnd 8877 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  ( ( u  -  N )  /  N ) )  e.  CC )
338139recnd 8877 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  CC )
339336, 337, 338addassd 8873 . . . . . . . . . . 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
) ) ) ) )
340 mulcom 8839 . . . . . . . . . . . . . . 15  |-  ( ( 2  e.  CC  /\  ( ( u  -  N )  /  N
)  e.  CC )  ->  ( 2  x.  ( ( u  -  N )  /  N
) )  =  ( ( ( u  -  N )  /  N
)  x.  2 ) )
341320, 198, 340sylancr 644 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  ( ( u  -  N )  /  N ) )  =  ( ( ( u  -  N )  /  N )  x.  2 ) )
342341oveq2d 5890 . . . . . . . . . . . . 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 ) ) )
343142recnd 8877 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  /  u ) )  +  1 )  e.  CC )
344198, 343, 321adddid 8875 . . . . . . . . . . . . 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 ) ) )
345248, 175, 321addassd 8873 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( abs `  (
( R `  u
)  /  u ) )  +  1 )  +  2 )  =  ( ( abs `  (
( R `  u
)  /  u ) )  +  ( 1  +  2 ) ) )
346 2p1e3 9863 . . . . . . . . . . . . . . . . 17  |-  ( 2  +  1 )  =  3
347320, 174, 346addcomli 9020 . . . . . . . . . . . . . . . 16  |-  ( 1  +  2 )  =  3
348347oveq2i 5885 . . . . . . . . . . . . . . 15  |-  ( ( abs `  ( ( R `  u )  /  u ) )  +  ( 1  +  2 ) )  =  ( ( abs `  (
( R `  u
)  /  u ) )  +  3 )
349345, 348syl6eq 2344 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( abs `  (
( R `  u
)  /  u ) )  +  1 )  +  2 )  =  ( ( abs `  (
( R `  u
)  /  u ) )  +  3 ) )
350349oveq2d 5890 . . . . . . . . . . . . 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 ) ) )
351342, 344, 3503eqtr2d 2334 . . . . . . . . . . . 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 ) ) )
352351oveq1d 5889 . . . . . . . . . . 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
) ) ) )
353339, 352eqtr3d 2330 . . . . . . . . . 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
) ) ) )
354335, 353breqtrd 4063 . . . . . . . . 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
) ) ) )
35594, 150, 140, 258, 354letrd 8989 . . . . . . . 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
) ) ) )
356101rehalfcld 9974 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( E  /  2 )  / 
2 )  e.  RR )
35778, 274, 79ledivmul2d 10456 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  /  N )  <_  ( 1  +  ( L  x.  E
) )  <->  u  <_  ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )
358269, 357mpbird 223 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  /  N )  <_  (
1  +  ( L  x.  E ) ) )
35916adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( L  x.  E )  e.  RR )
360359recnd 8877 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( L  x.  E )  e.  CC )
361 addcom 9014 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  CC  /\  ( L  x.  E
)  e.  CC )  ->  ( 1  +  ( L  x.  E
) )  =  ( ( L  x.  E
)  +  1 ) )
362174, 360, 361sylancr 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 1  +  ( L  x.  E ) )  =  ( ( L  x.  E )  +  1 ) )
363358, 362breqtrd 4063 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +