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

Theorem pntibndlem2 20740
Description: Lemma for pntibnd 20742. 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 10389 . 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 8837 . . . . . . 7  |-  1  e.  RR
76a1i 10 . . . . . 6  |-  ( ph  ->  1  e.  RR )
8 ioossre 10712 . . . . . . . 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 20738 . . . . . . . 8  |-  ( ph  ->  L  e.  ( 0 (,) 1 ) )
138, 12sseldi 3178 . . . . . . 7  |-  ( ph  ->  L  e.  RR )
14 pntibndlem3.4 . . . . . . . 8  |-  ( ph  ->  E  e.  ( 0 (,) 1 ) )
158, 14sseldi 3178 . . . . . . 7  |-  ( ph  ->  E  e.  RR )
1613, 15remulcld 8863 . . . . . 6  |-  ( ph  ->  ( L  x.  E
)  e.  RR )
177, 16readdcld 8862 . . . . 5  |-  ( ph  ->  ( 1  +  ( L  x.  E ) )  e.  RR )
181nnred 9761 . . . . 5  |-  ( ph  ->  N  e.  RR )
1917, 18remulcld 8863 . . . 4  |-  ( ph  ->  ( ( 1  +  ( L  x.  E
) )  x.  N
)  e.  RR )
20 2re 9815 . . . . 5  |-  2  e.  RR
21 remulcl 8822 . . . . 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 10390 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
26 remulcl 8822 . . . . . . . . . . . 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 10359 . . . . . . . . . . . . 13  |-  2  e.  RR+
2928a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  2  e.  RR+ )
3029relogcld 19974 . . . . . . . . . . 11  |-  ( ph  ->  ( log `  2
)  e.  RR )
3127, 30readdcld 8862 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2  x.  B )  +  ( log `  2 ) )  e.  RR )
3223, 31syl5eqel 2367 . . . . . . . . 9  |-  ( ph  ->  C  e.  RR )
33 eliooord 10710 . . . . . . . . . . . 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 10388 . . . . . . . . 9  |-  ( ph  ->  E  e.  RR+ )
3732, 36rerpdivcld 10417 . . . . . . . 8  |-  ( ph  ->  ( C  /  E
)  e.  RR )
3837reefcld 12369 . . . . . . 7  |-  ( ph  ->  ( exp `  ( C  /  E ) )  e.  RR )
39 pnfxr 10455 . . . . . . 7  |-  +oo  e.  RR*
40 icossre 10730 . . . . . . 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 3181 . . . . 5  |-  ( ph  ->  M  e.  RR )
44 ioossre 10712 . . . . . 6  |-  ( X (,)  +oo )  C_  RR
45 pntibndlem2.9 . . . . . 6  |-  ( ph  ->  Y  e.  ( X (,)  +oo ) )
4644, 45sseldi 3178 . . . . 5  |-  ( ph  ->  Y  e.  RR )
4743, 46remulcld 8863 . . . 4  |-  ( ph  ->  ( M  x.  Y
)  e.  RR )
4820a1i 10 . . . . 5  |-  ( ph  ->  2  e.  RR )
49 eliooord 10710 . . . . . . . . . . . . 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 10388 . . . . . . . . . 10  |-  ( ph  ->  L  e.  RR+ )
5352rpge0d 10394 . . . . . . . . 9  |-  ( ph  ->  0  <_  L )
5450simprd 449 . . . . . . . . 9  |-  ( ph  ->  L  <  1 )
5536rpge0d 10394 . . . . . . . . 9  |-  ( ph  ->  0  <_  E )
5634simprd 449 . . . . . . . . 9  |-  ( ph  ->  E  <  1 )
5713, 7, 15, 7, 53, 54, 55, 56ltmul12ad 9698 . . . . . . . 8  |-  ( ph  ->  ( L  x.  E
)  <  ( 1  x.  1 ) )
58 1t1e1 9870 . . . . . . . 8  |-  ( 1  x.  1 )  =  1
5957, 58syl6breq 4062 . . . . . . 7  |-  ( ph  ->  ( L  x.  E
)  <  1 )
6016, 7, 7, 59ltadd2dd 8975 . . . . . 6  |-  ( ph  ->  ( 1  +  ( L  x.  E ) )  <  ( 1  +  1 ) )
61 df-2 9804 . . . . . 6  |-  2  =  ( 1  +  1 )
6260, 61syl6breqr 4063 . . . . 5  |-  ( ph  ->  ( 1  +  ( L  x.  E ) )  <  2 )
6317, 48, 2, 62ltmul1dd 10441 . . . 4  |-  ( ph  ->  ( ( 1  +  ( L  x.  E
) )  x.  N
)  <  ( 2  x.  N ) )
644simprd 449 . . . . . 6  |-  ( ph  ->  N  <_  ( ( M  /  2 )  x.  Y ) )
6543recnd 8861 . . . . . . 7  |-  ( ph  ->  M  e.  CC )
6646recnd 8861 . . . . . . 7  |-  ( ph  ->  Y  e.  CC )
67 rpcnne0 10371 . . . . . . . 8  |-  ( 2  e.  RR+  ->  ( 2  e.  CC  /\  2  =/=  0 ) )
6828, 67mp1i 11 . . . . . . 7  |-  ( ph  ->  ( 2  e.  CC  /\  2  =/=  0 ) )
69 div23 9443 . . . . . . 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 4049 . . . . 5  |-  ( ph  ->  N  <_  ( ( M  x.  Y )  /  2 ) )
7218, 47, 29lemuldiv2d 10436 . . . . 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 8976 . . 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 20739 . . . . . . . . . . 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 10425 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  e.  RR+ )
829pntrf 20712 . . . . . . . . . 10  |-  R : RR+
--> RR
8382ffvelrni 5664 . . . . . . . . 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 10417 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  u )  e.  RR )
8685recnd 8861 . . . . . 6  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  u )  e.  CC )
8786abscld 11918 . . . . 5  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  /  u
) )  e.  RR )
8882ffvelrni 5664 . . . . . . . . . . . 12  |-  ( N  e.  RR+  ->  ( R `
 N )  e.  RR )
892, 88syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( R `  N
)  e.  RR )
9089, 1nndivred 9794 . . . . . . . . . 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 8861 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  N )  /  N )  e.  CC )
9386, 92subcld 9157 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  /  u )  -  ( ( R `
 N )  /  N ) )  e.  CC )
9493abscld 11918 . . . . . 6  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( ( R `
 u )  /  u )  -  (
( R `  N
)  /  N ) ) )  e.  RR )
9592abscld 11918 . . . . . 6  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  N )  /  N
) )  e.  RR )
9694, 95readdcld 8862 . . . . 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 11939 . . . . . 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 9369 . . . . . 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 9958 . . . . . . 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 9211 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  -  N )  e.  RR )
104103, 79rerpdivcld 10417 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  e.  RR )
105 3re 9817 . . . . . . . . . . . 12  |-  3  e.  RR
106105a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  3  e.  RR )
10787, 106readdcld 8862 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  /  u ) )  +  3 )  e.  RR )
108104, 107remulcld 8863 . . . . . . . . 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 10390 . . . . . . . . . . 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 9879 . . . . . . . . . . . . . . . . . 18  |-  4  e.  NN
114 nnrp 10363 . . . . . . . . . . . . . . . . . 18  |-  ( 4  e.  NN  ->  4  e.  RR+ )
115113, 114mp1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  4  e.  RR+ )
11636, 115rpdivcld 10407 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E  /  4
)  e.  RR+ )
117109, 116rpdivcld 10407 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( T  /  ( E  /  4 ) )  e.  RR+ )
118117rpred 10390 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  /  ( E  /  4 ) )  e.  RR )
119118reefcld 12369 . . . . . . . . . . . . 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 12396 . . . . . . . . . . . . . 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 10390 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Z  e.  RR )
127119, 126readdcld 8862 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( exp `  ( T  /  ( E  / 
4 ) ) )  +  Z )  e.  RR )
128124, 127syl5eqel 2367 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
129119, 125ltaddrpd 10419 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  <  ( ( exp `  ( T  /  ( E  /  4 ) ) )  +  Z ) )
130129, 124syl6breqr 4063 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  <  X )
131 eliooord 10710 . . . . . . . . . . . . . . . . 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 8977 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( exp `  ( T  /  ( E  / 
4 ) ) )  <  Y )
135119, 46, 18, 134, 5lttrd 8977 . . . . . . . . . . . . 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 8977 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  1  <  N )
138102, 137rplogcld 19980 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( log `  N )  e.  RR+ )
139111, 138rerpdivcld 10417 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  RR )
140108, 139readdcld 8862 . . . . . . . 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 8985 . . . . . . . . . . . 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 8863 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( abs `  ( ( R `  u )  /  u
) )  +  1 ) )  e.  RR )
144 chpcl 20362 . . . . . . . . . . . . 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 20362 . . . . . . . . . . . . 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 9211 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (ψ `  u )  -  (ψ `  N ) )  e.  RR )
149148, 79rerpdivcld 10417 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  /  N )  e.  RR )
150143, 149readdcld 8862 . . . . . . . . 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 8863 . . . . . . . . . . 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 9211 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  -  ( R `  N ) )  e.  RR )
154153recnd 8861 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  -  ( R `  N ) )  e.  CC )
155154abscld 11918 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  -  ( R `  N )
) )  e.  RR )
156155, 79rerpdivcld 10417 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  -  ( R `  N ) ) )  /  N
)  e.  RR )
157151, 156readdcld 8862 . . . . . . . . . 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 8863 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  RR )
159158renegcld 9210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  -u ( ( ( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  RR )
160159recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  -u ( ( ( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  CC )
161153, 79rerpdivcld 10417 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  -  ( R `
 N ) )  /  N )  e.  RR )
162161recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  -  ( R `
 N ) )  /  N )  e.  CC )
163160, 162abstrid 11938 . . . . . . . . . . 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 8861 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  e.  CC )
165102recnd 8861 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  e.  CC )
16679rpne0d 10395 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  N  =/=  0 )
167164, 165, 165, 166divsubdird 9575 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  =  ( ( u  /  N )  -  ( N  /  N ) ) )
168165, 166dividd 9534 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  /  N )  =  1 )
169168oveq2d 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  /  N )  -  ( N  /  N ) )  =  ( ( u  /  N )  -  1 ) )
170167, 169eqtrd 2315 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  =  ( ( u  /  N )  -  1 ) )
171170oveq1d 5873 . . . . . . . . . . . . . . . . 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 10417 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  /  N )  e.  RR )
173172recnd 8861 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  /  N )  e.  CC )
174 ax-1cn 8795 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  CC
175174a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  1  e.  CC )
176173, 175, 86subdird 9236 . . . . . . . . . . . . . . . . 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 10399 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  e.  CC  /\  u  =/=  0 ) )
17879rpcnne0d 10399 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  e.  CC  /\  N  =/=  0 ) )
17984recnd 8861 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  u )  e.  CC )
180 dmdcan 9470 . . . . . . . . . . . . . . . . . . 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 8853 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 1  x.  ( ( R `
 u )  /  u ) )  =  ( ( R `  u )  /  u
) )
183181, 182oveq12d 5876 . . . . . . . . . . . . . . . . 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 2319 . . . . . . . . . . . . . . . 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 9046 . . . . . . . . . . . . . . 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 10417 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  N )  e.  RR )
187186recnd 8861 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  /  N )  e.  CC )
188187, 86negsubdi2d 9173 . . . . . . . . . . . . . . 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 2315 . . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( R `  N )  e.  CC )
191179, 190, 165, 166divsubdird 9575 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( R `  u
)  -  ( R `
 N ) )  /  N )  =  ( ( ( R `
 u )  /  N )  -  (
( R `  N
)  /  N ) ) )
192189, 191oveq12d 5876 . . . . . . . . . . . . 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 9181 . . . . . . . . . . . . 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 2315 . . . . . . . . . . . 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 5529 . . . . . . . . . . 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 8861 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( R `
 u )  /  u ) )  e.  CC )
197196absnegd 11931 . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  /  N )  e.  CC )
199198, 86absmuld 11936 . . . . . . . . . . . . 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 9362 . . . . . . . . . . . . . . . . 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 10426 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  0  <_  ( ( u  -  N
)  /  N ) )
203104, 202absidd 11905 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( u  -  N )  /  N
) )  =  ( ( u  -  N
)  /  N ) )
204203oveq1d 5873 . . . . . . . . . . . . 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 2319 . . . . . . . . . . . 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 11937 . . . . . . . . . . . . 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 10397 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  e.  RR  /\  0  <_  N ) )
208 absid 11781 . . . . . . . . . . . . . . 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 5874 . . . . . . . . . . . . 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 2315 . . . . . . . . . . . 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 5876 . . . . . . . . . . 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 4052 . . . . . . . . . 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 8862 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
u  -  N )  +  ( (ψ `  u )  -  (ψ `  N ) ) )  e.  RR )
215214, 79rerpdivcld 10417 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) )  /  N )  e.  RR )
216148recnd 8861 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (ψ `  u )  -  (ψ `  N ) )  e.  CC )
217165, 164subcld 9157 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  -  u )  e.  CC )
218216, 217abstrid 11938 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )  <_ 
( ( abs `  (
(ψ `  u )  -  (ψ `  N )
) )  +  ( abs `  ( N  -  u ) ) ) )
2199pntrval 20711 . . . . . . . . . . . . . . . . . 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 20711 . . . . . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( R `  u )  -  ( R `  N ) )  =  ( ( (ψ `  u )  -  u
)  -  ( (ψ `  N )  -  N
) ) )
224145recnd 8861 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  u
)  e.  CC )
225147recnd 8861 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  (ψ `  N
)  e.  CC )
226 subadd4 9091 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (ψ `  u
)  e.  CC  /\  (ψ `  N )  e.  CC )  /\  (
u  e.  CC  /\  N  e.  CC )
)  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  -  ( u  -  N ) )  =  ( ( (ψ `  u )  +  N
)  -  ( (ψ `  N )  +  u
) ) )
227 sub4 9092 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (ψ `  u
)  e.  CC  /\  (ψ `  N )  e.  CC )  /\  (
u  e.  CC  /\  N  e.  CC )
)  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  -  ( u  -  N ) )  =  ( ( (ψ `  u )  -  u
)  -  ( (ψ `  N )  -  N
) ) )
228 addsub4 9090 . . . . . . . . . . . . . . . . . . 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 2323 . . . . . . . . . . . . . . . . 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 2316 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  +  ( N  -  u ) )  =  ( ( R `
 u )  -  ( R `  N ) ) )
233232fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( (ψ `  u )  -  (ψ `  N ) )  +  ( N  -  u
) ) )  =  ( abs `  (
( R `  u
)  -  ( R `
 N ) ) ) )
234 chpwordi 20395 . . . . . . . . . . . . . . . . . 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 11914 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( (ψ `  u
)  -  (ψ `  N ) ) )  =  ( (ψ `  u )  -  (ψ `  N ) ) )
237102, 78, 80abssuble0d 11915 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( N  -  u
) )  =  ( u  -  N ) )
238236, 237oveq12d 5876 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( (ψ `  u )  -  (ψ `  N ) ) )  +  ( abs `  ( N  -  u )
) )  =  ( ( (ψ `  u
)  -  (ψ `  N ) )  +  ( u  -  N
) ) )
239103recnd 8861 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  -  N )  e.  CC )
240216, 239addcomd 9014 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  +  ( u  -  N ) )  =  ( ( u  -  N )  +  ( (ψ `  u
)  -  (ψ `  N ) ) ) )
241238, 240eqtrd 2315 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( (ψ `  u )  -  (ψ `  N ) ) )  +  ( abs `  ( N  -  u )
) )  =  ( ( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) ) )
242218, 233, 2413brtr3d 4052 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  -  ( R `  N )
) )  <_  (
( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) ) )
243155, 214, 79, 242lediv1dd 10444 . . . . . . . . . . . 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 9387 . . . . . . . . . . 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 8861 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( abs `  (
( R `  u
)  /  u ) ) )  e.  CC )
246149recnd 8861 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
(ψ `  u )  -  (ψ `  N )
)  /  N )  e.  CC )
247245, 198, 246addassd 8857 . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( abs `  ( ( R `  u )  /  u
) )  e.  CC )
249198, 248, 175adddid 8859 . . . . . . . . . . . . . 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 8852 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  1 )  =  ( ( u  -  N )  /  N
) )
251250oveq2d 5874 . . . . . . . . . . . . . 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 2315 . . . . . . . . . . . . 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 5873 . . . . . . . . . . . 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 9574 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  +  ( (ψ `  u )  -  (ψ `  N ) ) )  /  N )  =  ( ( ( u  -  N )  /  N )  +  ( ( (ψ `  u
)  -  (ψ `  N ) )  /  N ) ) )
255254oveq2d 5874 . . . . . . . . . . . 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 2325 . . . . . . . . . . 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 4049 . . . . . . . . . 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 8973 . . . . . . . . 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 8822 . . . . . . . . . . . . 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 8862 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
2  x.  ( ( u  -  N )  /  N ) )  +  ( T  / 
( log `  N
) ) )  e.  RR )
262 remulcl 8822 . . . . . . . . . . . . . . 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 10417 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( N  /  ( log `  N
) )  e.  RR )
265111, 264remulcld 8863 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  e.  RR )
266263, 265readdcld 8862 . . . . . . . . . . . . 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 8910 . . . . . . . . . . . . . . . . . . . 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 10429 . . . . . . . . . . . . . . . . 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 8973 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  u  <_  ( 2  x.  N ) )
279 elicc2 10715 . . . . . . . . . . . . . . . 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 8876 . . . . . . . . . . . . . . . . . 18  |-  RR  C_  RR*
283282, 6sselii 3177 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR*
284 elioopnf 10737 . . . . . . . . . . . . . . . . 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 5866 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  N  ->  (
2  x.  x )  =  ( 2  x.  N ) )
291289, 290oveq12d 5876 . . . . . . . . . . . . . . . . 17  |-  ( x  =  N  ->  (
x [,] ( 2  x.  x ) )  =  ( N [,] ( 2  x.  N
) ) )
292 fveq2 5525 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  N  ->  (ψ `  x )  =  (ψ `  N ) )
293292oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  N  ->  (
(ψ `  y )  -  (ψ `  x )
)  =  ( (ψ `  y )  -  (ψ `  N ) ) )
294 oveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  N  ->  (
y  -  x )  =  ( y  -  N ) )
295294oveq2d 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  N  ->  (
2  x.  ( y  -  x ) )  =  ( 2  x.  ( y  -  N
) ) )
296 fveq2 5525 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  N  ->  ( log `  x )  =  ( log `  N
) )
297289, 296oveq12d 5876 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  N  ->  (
x  /  ( log `  x ) )  =  ( N  /  ( log `  N ) ) )
298297oveq2d 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  N  ->  ( T  x.  ( x  /  ( log `  x
) ) )  =  ( T  x.  ( N  /  ( log `  N
) ) ) )
299295, 298oveq12d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  N  ->  (
( 2  x.  (
y  -  x ) )  +  ( T  x.  ( x  / 
( log `  x
) ) ) )  =  ( ( 2  x.  ( y  -  N ) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) )
300293, 299breq12d 4036 . . . . . . . . . . . . . . . . 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 2748 . . . . . . . . . . . . . . . 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 2880 . . . . . . . . . . . . . . 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 5525 . . . . . . . . . . . . . . . . 17  |-  ( y  =  u  ->  (ψ `  y )  =  (ψ `  u ) )
305304oveq1d 5873 . . . . . . . . . . . . . . . 16  |-  ( y  =  u  ->  (
(ψ `  y )  -  (ψ `  N )
)  =  ( (ψ `  u )  -  (ψ `  N ) ) )
306 oveq1 5865 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  u  ->  (
y  -  N )  =  ( u  -  N ) )
307306oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( y  =  u  ->  (
2  x.  ( y  -  N ) )  =  ( 2  x.  ( u  -  N
) ) )
308307oveq1d 5873 . . . . . . . . . . . . . . . 16  |-  ( y  =  u  ->  (
( 2  x.  (
y  -  N ) )  +  ( T  x.  ( N  / 
( log `  N
) ) ) )  =  ( ( 2  x.  ( u  -  N ) )  +  ( T  x.  ( N  /  ( log `  N
) ) ) ) )
309305, 308breq12d 4036 . . . . . . . . . . . . . . 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 2880 . . . . . . . . . . . . . 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 10444 . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . 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 10390 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  T  e.  RR )
316315, 264remulcld 8863 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  e.  RR )
317316recnd 8861 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  x.  ( N  /  ( log `  N ) ) )  e.  CC )
318 divdir 9447 . . . . . . . . . . . . . 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 9816 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
321320a1i 10 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  2  e.  CC )
322321, 239, 165, 166divassd 9571 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
2  x.  ( u  -  N ) )  /  N )  =  ( 2  x.  (
( u  -  N
)  /  N ) ) )
323111recnd 8861 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  T  e.  CC )
324138rpcnne0d 10399 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( log `  N )  e.  CC  /\  ( log `  N )  =/=  0
) )
325 div12 9446 . . . . . . . . . . . . . . . . 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 5873 . . . . . . . . . . . . . . 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 10407 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  RR+ )
329328rpcnd 10392 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  CC )
330329, 165, 166divcan3d 9541 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( N  x.  ( T  /  ( log `  N
) ) )  /  N )  =  ( T  /  ( log `  N ) ) )
331327, 330eqtrd 2315 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( T  x.  ( N  /  ( log `  N
) ) )  /  N )  =  ( T  /  ( log `  N ) ) )
332322, 331oveq12d 5876 . . . . . . . . . . . . 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 2315 . . . . . . . . . . . 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 4047 . . . . . . . . . . 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 9387 . . . . . . . . . 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 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  -  N
)  /  N )  x.  ( ( abs `  ( ( R `  u )  /  u
) )  +  1 ) )  e.  CC )
337260recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( 2  x.  ( ( u  -  N )  /  N ) )  e.  CC )
338139recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( T  /  ( log `  N
) )  e.  CC )
339336, 337, 338addassd 8857 . . . . . . . . . . 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 8823 . . . . . . . . . . . . . . 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 5874 . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( abs `  ( ( R `
 u )  /  u ) )  +  1 )  e.  CC )
344198, 343, 321adddid 8859 . . . . . . . . . . . . 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 8857 . . . . . . . . . . . . . . 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 9847 . . . . . . . . . . . . . . . . 17  |-  ( 2  +  1 )  =  3
347320, 174, 346addcomli 9004 . . . . . . . . . . . . . . . 16  |-  ( 1  +  2 )  =  3
348347oveq2i 5869 . . . . . . . . . . . . . . 15  |-  ( ( abs `  ( ( R `  u )  /  u ) )  +  ( 1  +  2 ) )  =  ( ( abs `  (
( R `  u
)  /  u ) )  +  3 )
349345, 348syl6eq 2331 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( abs `  (
( R `  u
)  /  u ) )  +  1 )  +  2 )  =  ( ( abs `  (
( R `  u
)  /  u ) )  +  3 ) )
350349oveq2d 5874 . . . . . . . . . . . . 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 2321 . . . . . . . . . . . 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 5873 . . . . . . . . . . 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 2317 . . . . . . . . . 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 4047 . . . . . . . . 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 8973 . . . . . . . 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 9958 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( ( E  /  2 )  / 
2 )  e.  RR )
35778, 274, 79ledivmul2d 10440 . . . . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( L  x.  E )  e.  CC )
361 addcom 8998 . . . . . . . . . . . . . . . 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 4047 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( u  /  N )  <_  (
( L  x.  E
)  +  1 ) )
364172, 112, 359lesubaddd 9369 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( N [,] ( ( 1  +  ( L  x.  E ) )  x.  N ) ) )  ->  ( (
( u  /  N
)  -  1 )  <_  ( L  x.  E )  <->