Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lgamgulmlem2 Structured version   Unicode version

Theorem lgamgulmlem2 24845
Description: Lemma for lgamgulm 24850. (Contributed by Mario Carneiro, 3-Jul-2017.)
Hypotheses
Ref Expression
lgamgulm.r  |-  ( ph  ->  R  e.  NN )
lgamgulm.u  |-  U  =  { x  e.  CC  |  ( ( abs `  x )  <_  R  /\  A. k  e.  NN0  ( 1  /  R
)  <_  ( abs `  ( x  +  k ) ) ) }
lgamgulm.n  |-  ( ph  ->  N  e.  NN )
lgamgulm.a  |-  ( ph  ->  A  e.  U )
lgamgulm.l  |-  ( ph  ->  ( 2  x.  R
)  <_  N )
Assertion
Ref Expression
lgamgulmlem2  |-  ( ph  ->  ( abs `  (
( A  /  N
)  -  ( log `  ( ( A  /  N )  +  1 ) ) ) )  <_  ( R  x.  ( ( 1  / 
( N  -  R
) )  -  (
1  /  N ) ) ) )
Distinct variable groups:    x, N    x, k, R    A, k, x    ph, x
Allowed substitution hints:    ph( k)    U( x, k)    N( k)

Proof of Theorem lgamgulmlem2
Dummy variables  y 
t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1elunit 11047 . . 3  |-  1  e.  ( 0 [,] 1
)
2 0elunit 11046 . . 3  |-  0  e.  ( 0 [,] 1
)
3 0re 9122 . . . . 5  |-  0  e.  RR
43a1i 11 . . . 4  |-  ( ph  ->  0  e.  RR )
5 1re 9121 . . . . 5  |-  1  e.  RR
65a1i 11 . . . 4  |-  ( ph  ->  1  e.  RR )
7 eqid 2442 . . . . 5  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
87subcn 18927 . . . . . 6  |-  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
98a1i 11 . . . . 5  |-  ( ph  ->  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
) )
107mulcn 18928 . . . . . . 7  |-  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
1110a1i 11 . . . . . 6  |-  ( ph  ->  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
) )
12 lgamgulm.r . . . . . . . . . . 11  |-  ( ph  ->  R  e.  NN )
13 lgamgulm.u . . . . . . . . . . 11  |-  U  =  { x  e.  CC  |  ( ( abs `  x )  <_  R  /\  A. k  e.  NN0  ( 1  /  R
)  <_  ( abs `  ( x  +  k ) ) ) }
1412, 13lgamgulmlem1 24844 . . . . . . . . . 10  |-  ( ph  ->  U  C_  ( CC  \  ( ZZ  \  NN ) ) )
15 lgamgulm.a . . . . . . . . . 10  |-  ( ph  ->  A  e.  U )
1614, 15sseldd 3335 . . . . . . . . 9  |-  ( ph  ->  A  e.  ( CC 
\  ( ZZ  \  NN ) ) )
1716eldifad 3318 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
18 lgamgulm.n . . . . . . . . . 10  |-  ( ph  ->  N  e.  NN )
1918nnred 10046 . . . . . . . . 9  |-  ( ph  ->  N  e.  RR )
2019recnd 9145 . . . . . . . 8  |-  ( ph  ->  N  e.  CC )
2118nnne0d 10075 . . . . . . . 8  |-  ( ph  ->  N  =/=  0 )
2217, 20, 21divcld 9821 . . . . . . 7  |-  ( ph  ->  ( A  /  N
)  e.  CC )
23 unitssre 11073 . . . . . . . . 9  |-  ( 0 [,] 1 )  C_  RR
24 ax-resscn 9078 . . . . . . . . 9  |-  RR  C_  CC
2523, 24sstri 3343 . . . . . . . 8  |-  ( 0 [,] 1 )  C_  CC
2625a1i 11 . . . . . . 7  |-  ( ph  ->  ( 0 [,] 1
)  C_  CC )
27 ssid 3353 . . . . . . . 8  |-  CC  C_  CC
2827a1i 11 . . . . . . 7  |-  ( ph  ->  CC  C_  CC )
29 cncfmptc 18972 . . . . . . 7  |-  ( ( ( A  /  N
)  e.  CC  /\  ( 0 [,] 1
)  C_  CC  /\  CC  C_  CC )  ->  (
t  e.  ( 0 [,] 1 )  |->  ( A  /  N ) )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )
3022, 26, 28, 29syl3anc 1185 . . . . . 6  |-  ( ph  ->  ( t  e.  ( 0 [,] 1 ) 
|->  ( A  /  N
) )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
31 cncfmptid 18973 . . . . . . 7  |-  ( ( ( 0 [,] 1
)  C_  CC  /\  CC  C_  CC )  ->  (
t  e.  ( 0 [,] 1 )  |->  t )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )
3225, 28, 31sylancr 646 . . . . . 6  |-  ( ph  ->  ( t  e.  ( 0 [,] 1 ) 
|->  t )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
337, 11, 30, 32cncfmpt2f 18975 . . . . 5  |-  ( ph  ->  ( t  e.  ( 0 [,] 1 ) 
|->  ( ( A  /  N )  x.  t
) )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
3422adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( A  /  N )  e.  CC )
35 simpr 449 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  t  e.  ( 0 [,] 1
) )
3623, 35sseldi 3332 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  t  e.  RR )
3736recnd 9145 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  t  e.  CC )
3834, 37mulcld 9139 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( A  /  N
)  x.  t )  e.  CC )
39 ax-1cn 9079 . . . . . . . . . . 11  |-  1  e.  CC
4039a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  1  e.  CC )
4138, 40addcld 9138 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( ( A  /  N )  x.  t
)  +  1 )  e.  CC )
42 rere 11958 . . . . . . . . . . . 12  |-  ( ( ( ( A  /  N )  x.  t
)  +  1 )  e.  RR  ->  (
Re `  ( (
( A  /  N
)  x.  t )  +  1 ) )  =  ( ( ( A  /  N )  x.  t )  +  1 ) )
4342adantl 454 . . . . . . . . . . 11  |-  ( ( ( ph  /\  t  e.  ( 0 [,] 1
) )  /\  (
( ( A  /  N )  x.  t
)  +  1 )  e.  RR )  -> 
( Re `  (
( ( A  /  N )  x.  t
)  +  1 ) )  =  ( ( ( A  /  N
)  x.  t )  +  1 ) )
4441recld 12030 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
Re `  ( (
( A  /  N
)  x.  t )  +  1 ) )  e.  RR )
4538recld 12030 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
Re `  ( ( A  /  N )  x.  t ) )  e.  RR )
4645recnd 9145 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
Re `  ( ( A  /  N )  x.  t ) )  e.  CC )
4746abscld 12269 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( abs `  ( Re `  ( ( A  /  N )  x.  t
) ) )  e.  RR )
4838abscld 12269 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( abs `  ( ( A  /  N )  x.  t ) )  e.  RR )
495a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  1  e.  RR )
50 absrele 12144 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A  /  N
)  x.  t )  e.  CC  ->  ( abs `  ( Re `  ( ( A  /  N )  x.  t
) ) )  <_ 
( abs `  (
( A  /  N
)  x.  t ) ) )
5138, 50syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( abs `  ( Re `  ( ( A  /  N )  x.  t
) ) )  <_ 
( abs `  (
( A  /  N
)  x.  t ) ) )
5249rehalfcld 10245 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
1  /  2 )  e.  RR )
5312nnred 10046 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  R  e.  RR )
5453adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  R  e.  RR )
5518adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  N  e.  NN )
5654, 55nndivred 10079 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( R  /  N )  e.  RR )
5722abscld 12269 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( abs `  ( A  /  N ) )  e.  RR )
5857adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( abs `  ( A  /  N ) )  e.  RR )
5934absge0d 12277 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  0  <_  ( abs `  ( A  /  N ) ) )
603, 5elicc2i 11007 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  e.  ( 0 [,] 1 )  <->  ( t  e.  RR  /\  0  <_ 
t  /\  t  <_  1 ) )
6160simp2bi 974 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  ( 0 [,] 1 )  ->  0  <_  t )
6261adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  0  <_  t )
6317, 20, 21absdivd 12288 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( abs `  ( A  /  N ) )  =  ( ( abs `  A )  /  ( abs `  N ) ) )
6418nnrpd 10678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  N  e.  RR+ )
6564rpge0d 10683 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  0  <_  N )
6619, 65absidd 12256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( abs `  N
)  =  N )
6766oveq2d 6126 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( abs `  A
)  /  ( abs `  N ) )  =  ( ( abs `  A
)  /  N ) )
6863, 67eqtr2d 2475 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( abs `  A
)  /  N )  =  ( abs `  ( A  /  N ) ) )
6917abscld 12269 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( abs `  A
)  e.  RR )
70 fveq2 5757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  A  ->  ( abs `  x )  =  ( abs `  A
) )
7170breq1d 4247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  A  ->  (
( abs `  x
)  <_  R  <->  ( abs `  A )  <_  R
) )
72 oveq1 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  =  A  ->  (
x  +  k )  =  ( A  +  k ) )
7372fveq2d 5761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  A  ->  ( abs `  ( x  +  k ) )  =  ( abs `  ( A  +  k )
) )
7473breq2d 4249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  A  ->  (
( 1  /  R
)  <_  ( abs `  ( x  +  k ) )  <->  ( 1  /  R )  <_ 
( abs `  ( A  +  k )
) ) )
7574ralbidv 2731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  A  ->  ( A. k  e.  NN0  ( 1  /  R
)  <_  ( abs `  ( x  +  k ) )  <->  A. k  e.  NN0  ( 1  /  R )  <_  ( abs `  ( A  +  k ) ) ) )
7671, 75anbi12d 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  =  A  ->  (
( ( abs `  x
)  <_  R  /\  A. k  e.  NN0  (
1  /  R )  <_  ( abs `  (
x  +  k ) ) )  <->  ( ( abs `  A )  <_  R  /\  A. k  e. 
NN0  ( 1  /  R )  <_  ( abs `  ( A  +  k ) ) ) ) )
7776, 13elrab2 3100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( A  e.  U  <->  ( A  e.  CC  /\  ( ( abs `  A )  <_  R  /\  A. k  e.  NN0  ( 1  /  R )  <_ 
( abs `  ( A  +  k )
) ) ) )
7877simprbi 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A  e.  U  ->  (
( abs `  A
)  <_  R  /\  A. k  e.  NN0  (
1  /  R )  <_  ( abs `  ( A  +  k )
) ) )
7915, 78syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( abs `  A
)  <_  R  /\  A. k  e.  NN0  (
1  /  R )  <_  ( abs `  ( A  +  k )
) ) )
8079simpld 447 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( abs `  A
)  <_  R )
8169, 53, 64, 80lediv1dd 10733 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( abs `  A
)  /  N )  <_  ( R  /  N ) )
8268, 81eqbrtrrd 4259 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( abs `  ( A  /  N ) )  <_  ( R  /  N ) )
8382adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( abs `  ( A  /  N ) )  <_ 
( R  /  N
) )
8460simp3bi 975 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  ( 0 [,] 1 )  ->  t  <_  1 )
8584adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  t  <_  1 )
8658, 56, 36, 49, 59, 62, 83, 85lemul12ad 9984 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( abs `  ( A  /  N ) )  x.  t )  <_ 
( ( R  /  N )  x.  1 ) )
8734, 37absmuld 12287 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( abs `  ( ( A  /  N )  x.  t ) )  =  ( ( abs `  ( A  /  N ) )  x.  ( abs `  t
) ) )
8836, 62absidd 12256 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( abs `  t )  =  t )
8988oveq2d 6126 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( abs `  ( A  /  N ) )  x.  ( abs `  t
) )  =  ( ( abs `  ( A  /  N ) )  x.  t ) )
9087, 89eqtr2d 2475 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( abs `  ( A  /  N ) )  x.  t )  =  ( abs `  (
( A  /  N
)  x.  t ) ) )
9156recnd 9145 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( R  /  N )  e.  CC )
9291mulid1d 9136 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( R  /  N
)  x.  1 )  =  ( R  /  N ) )
9386, 90, 923brtr3d 4266 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( abs `  ( ( A  /  N )  x.  t ) )  <_ 
( R  /  N
) )
94 lgamgulm.l . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( 2  x.  R
)  <_  N )
95 2rp 10648 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  2  e.  RR+
9695a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  2  e.  RR+ )
9753, 19, 96lemuldiv2d 10725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( 2  x.  R )  <_  N  <->  R  <_  ( N  / 
2 ) ) )
9894, 97mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  R  <_  ( N  /  2 ) )
99 2re 10100 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  2  e.  RR
10099a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  2  e.  RR )
101100recnd 9145 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  2  e.  CC )
102 2ne0 10114 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  2  =/=  0
103102a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  2  =/=  0 )
10420, 101, 103divrecd 9824 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( N  /  2
)  =  ( N  x.  ( 1  / 
2 ) ) )
10598, 104breqtrd 4261 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  R  <_  ( N  x.  ( 1  /  2
) ) )
1066rehalfcld 10245 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
10753, 106, 64ledivmuld 10728 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( R  /  N )  <_  (
1  /  2 )  <-> 
R  <_  ( N  x.  ( 1  /  2
) ) ) )
108105, 107mpbird 225 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( R  /  N
)  <_  ( 1  /  2 ) )
109108adantr 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( R  /  N )  <_ 
( 1  /  2
) )
11048, 56, 52, 93, 109letrd 9258 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( abs `  ( ( A  /  N )  x.  t ) )  <_ 
( 1  /  2
) )
111 halflt1 10220 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  /  2 )  <  1
112111a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
1  /  2 )  <  1 )
11348, 52, 49, 110, 112lelttrd 9259 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( abs `  ( ( A  /  N )  x.  t ) )  <  1 )
11447, 48, 49, 51, 113lelttrd 9259 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( abs `  ( Re `  ( ( A  /  N )  x.  t
) ) )  <  1 )
11545, 49absltd 12263 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( abs `  (
Re `  ( ( A  /  N )  x.  t ) ) )  <  1  <->  ( -u 1  <  ( Re `  (
( A  /  N
)  x.  t ) )  /\  ( Re
`  ( ( A  /  N )  x.  t ) )  <  1 ) ) )
116114, 115mpbid 203 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( -u 1  <  ( Re
`  ( ( A  /  N )  x.  t ) )  /\  ( Re `  ( ( A  /  N )  x.  t ) )  <  1 ) )
117116simpld 447 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  -u 1  <  ( Re `  (
( A  /  N
)  x.  t ) ) )
11849renegcld 9495 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  -u 1  e.  RR )
119118, 45posdifd 9644 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( -u 1  <  ( Re
`  ( ( A  /  N )  x.  t ) )  <->  0  <  ( ( Re `  (
( A  /  N
)  x.  t ) )  -  -u 1
) ) )
120117, 119mpbid 203 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  0  <  ( ( Re `  ( ( A  /  N )  x.  t
) )  -  -u 1
) )
12146, 40subnegd 9449 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( Re `  (
( A  /  N
)  x.  t ) )  -  -u 1
)  =  ( ( Re `  ( ( A  /  N )  x.  t ) )  +  1 ) )
122120, 121breqtrd 4261 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  0  <  ( ( Re `  ( ( A  /  N )  x.  t
) )  +  1 ) )
12338, 40readdd 12050 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
Re `  ( (
( A  /  N
)  x.  t )  +  1 ) )  =  ( ( Re
`  ( ( A  /  N )  x.  t ) )  +  ( Re `  1
) ) )
124 re1 11990 . . . . . . . . . . . . . . . 16  |-  ( Re
`  1 )  =  1
125124oveq2i 6121 . . . . . . . . . . . . . . 15  |-  ( ( Re `  ( ( A  /  N )  x.  t ) )  +  ( Re ` 
1 ) )  =  ( ( Re `  ( ( A  /  N )  x.  t
) )  +  1 )
126123, 125syl6eq 2490 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
Re `  ( (
( A  /  N
)  x.  t )  +  1 ) )  =  ( ( Re
`  ( ( A  /  N )  x.  t ) )  +  1 ) )
127122, 126breqtrrd 4263 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  0  <  ( Re `  (
( ( A  /  N )  x.  t
)  +  1 ) ) )
12844, 127elrpd 10677 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
Re `  ( (
( A  /  N
)  x.  t )  +  1 ) )  e.  RR+ )
129128adantr 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  t  e.  ( 0 [,] 1
) )  /\  (
( ( A  /  N )  x.  t
)  +  1 )  e.  RR )  -> 
( Re `  (
( ( A  /  N )  x.  t
)  +  1 ) )  e.  RR+ )
13043, 129eqeltrrd 2517 . . . . . . . . . 10  |-  ( ( ( ph  /\  t  e.  ( 0 [,] 1
) )  /\  (
( ( A  /  N )  x.  t
)  +  1 )  e.  RR )  -> 
( ( ( A  /  N )  x.  t )  +  1 )  e.  RR+ )
131130ex 425 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( ( ( A  /  N )  x.  t )  +  1 )  e.  RR  ->  ( ( ( A  /  N )  x.  t
)  +  1 )  e.  RR+ ) )
132 eqid 2442 . . . . . . . . . 10  |-  ( CC 
\  (  -oo (,] 0 ) )  =  ( CC  \  (  -oo (,] 0 ) )
133132ellogdm 20561 . . . . . . . . 9  |-  ( ( ( ( A  /  N )  x.  t
)  +  1 )  e.  ( CC  \ 
(  -oo (,] 0 ) )  <->  ( ( ( ( A  /  N
)  x.  t )  +  1 )  e.  CC  /\  ( ( ( ( A  /  N )  x.  t
)  +  1 )  e.  RR  ->  (
( ( A  /  N )  x.  t
)  +  1 )  e.  RR+ ) ) )
13441, 131, 133sylanbrc 647 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( ( A  /  N )  x.  t
)  +  1 )  e.  ( CC  \ 
(  -oo (,] 0 ) ) )
135 eqidd 2443 . . . . . . . 8  |-  ( ph  ->  ( t  e.  ( 0 [,] 1 ) 
|->  ( ( ( A  /  N )  x.  t )  +  1 ) )  =  ( t  e.  ( 0 [,] 1 )  |->  ( ( ( A  /  N )  x.  t
)  +  1 ) ) )
136132logcn 20569 . . . . . . . . . . 11  |-  ( log  |`  ( CC  \  (  -oo (,] 0 ) ) )  e.  ( ( CC  \  (  -oo (,] 0 ) ) -cn-> CC )
137136a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( log  |`  ( CC  \  (  -oo (,] 0 ) ) )  e.  ( ( CC 
\  (  -oo (,] 0 ) ) -cn-> CC ) )
138 cncff 18954 . . . . . . . . . 10  |-  ( ( log  |`  ( CC  \  (  -oo (,] 0
) ) )  e.  ( ( CC  \ 
(  -oo (,] 0 ) ) -cn-> CC )  ->  ( log  |`  ( CC  \ 
(  -oo (,] 0 ) ) ) : ( CC  \  (  -oo (,] 0 ) ) --> CC )
139137, 138syl 16 . . . . . . . . 9  |-  ( ph  ->  ( log  |`  ( CC  \  (  -oo (,] 0 ) ) ) : ( CC  \ 
(  -oo (,] 0 ) ) --> CC )
140139feqmptd 5808 . . . . . . . 8  |-  ( ph  ->  ( log  |`  ( CC  \  (  -oo (,] 0 ) ) )  =  ( y  e.  ( CC  \  (  -oo (,] 0 ) ) 
|->  ( ( log  |`  ( CC  \  (  -oo (,] 0 ) ) ) `
 y ) ) )
141 fveq2 5757 . . . . . . . 8  |-  ( y  =  ( ( ( A  /  N )  x.  t )  +  1 )  ->  (
( log  |`  ( CC 
\  (  -oo (,] 0 ) ) ) `
 y )  =  ( ( log  |`  ( CC  \  (  -oo (,] 0 ) ) ) `
 ( ( ( A  /  N )  x.  t )  +  1 ) ) )
142134, 135, 140, 141fmptco 5930 . . . . . . 7  |-  ( ph  ->  ( ( log  |`  ( CC  \  (  -oo (,] 0 ) ) )  o.  ( t  e.  ( 0 [,] 1
)  |->  ( ( ( A  /  N )  x.  t )  +  1 ) ) )  =  ( t  e.  ( 0 [,] 1
)  |->  ( ( log  |`  ( CC  \  (  -oo (,] 0 ) ) ) `  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) )
143 fvres 5774 . . . . . . . . 9  |-  ( ( ( ( A  /  N )  x.  t
)  +  1 )  e.  ( CC  \ 
(  -oo (,] 0 ) )  ->  ( ( log  |`  ( CC  \ 
(  -oo (,] 0 ) ) ) `  (
( ( A  /  N )  x.  t
)  +  1 ) )  =  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) ) )
144134, 143syl 16 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( log  |`  ( CC 
\  (  -oo (,] 0 ) ) ) `
 ( ( ( A  /  N )  x.  t )  +  1 ) )  =  ( log `  (
( ( A  /  N )  x.  t
)  +  1 ) ) )
145144mpteq2dva 4320 . . . . . . 7  |-  ( ph  ->  ( t  e.  ( 0 [,] 1 ) 
|->  ( ( log  |`  ( CC  \  (  -oo (,] 0 ) ) ) `
 ( ( ( A  /  N )  x.  t )  +  1 ) ) )  =  ( t  e.  ( 0 [,] 1
)  |->  ( log `  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) )
146142, 145eqtrd 2474 . . . . . 6  |-  ( ph  ->  ( ( log  |`  ( CC  \  (  -oo (,] 0 ) ) )  o.  ( t  e.  ( 0 [,] 1
)  |->  ( ( ( A  /  N )  x.  t )  +  1 ) ) )  =  ( t  e.  ( 0 [,] 1
)  |->  ( log `  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) )
147 eqid 2442 . . . . . . . . 9  |-  ( t  e.  ( 0 [,] 1 )  |->  ( ( ( A  /  N
)  x.  t )  +  1 ) )  =  ( t  e.  ( 0 [,] 1
)  |->  ( ( ( A  /  N )  x.  t )  +  1 ) )
148134, 147fmptd 5922 . . . . . . . 8  |-  ( ph  ->  ( t  e.  ( 0 [,] 1 ) 
|->  ( ( ( A  /  N )  x.  t )  +  1 ) ) : ( 0 [,] 1 ) --> ( CC  \  (  -oo (,] 0 ) ) )
149 difss 3460 . . . . . . . . 9  |-  ( CC 
\  (  -oo (,] 0 ) )  C_  CC
1507addcn 18926 . . . . . . . . . . 11  |-  +  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
151150a1i 11 . . . . . . . . . 10  |-  ( ph  ->  +  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
) )
15239a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  CC )
153 cncfmptc 18972 . . . . . . . . . . 11  |-  ( ( 1  e.  CC  /\  ( 0 [,] 1
)  C_  CC  /\  CC  C_  CC )  ->  (
t  e.  ( 0 [,] 1 )  |->  1 )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )
154152, 26, 28, 153syl3anc 1185 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  ( 0 [,] 1 ) 
|->  1 )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
1557, 151, 33, 154cncfmpt2f 18975 . . . . . . . . 9  |-  ( ph  ->  ( t  e.  ( 0 [,] 1 ) 
|->  ( ( ( A  /  N )  x.  t )  +  1 ) )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
156 cncffvrn 18959 . . . . . . . . 9  |-  ( ( ( CC  \  (  -oo (,] 0 ) ) 
C_  CC  /\  (
t  e.  ( 0 [,] 1 )  |->  ( ( ( A  /  N )  x.  t
)  +  1 ) )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )  -> 
( ( t  e.  ( 0 [,] 1
)  |->  ( ( ( A  /  N )  x.  t )  +  1 ) )  e.  ( ( 0 [,] 1 ) -cn-> ( CC 
\  (  -oo (,] 0 ) ) )  <-> 
( t  e.  ( 0 [,] 1 ) 
|->  ( ( ( A  /  N )  x.  t )  +  1 ) ) : ( 0 [,] 1 ) --> ( CC  \  (  -oo (,] 0 ) ) ) )
157149, 155, 156sylancr 646 . . . . . . . 8  |-  ( ph  ->  ( ( t  e.  ( 0 [,] 1
)  |->  ( ( ( A  /  N )  x.  t )  +  1 ) )  e.  ( ( 0 [,] 1 ) -cn-> ( CC 
\  (  -oo (,] 0 ) ) )  <-> 
( t  e.  ( 0 [,] 1 ) 
|->  ( ( ( A  /  N )  x.  t )  +  1 ) ) : ( 0 [,] 1 ) --> ( CC  \  (  -oo (,] 0 ) ) ) )
158148, 157mpbird 225 . . . . . . 7  |-  ( ph  ->  ( t  e.  ( 0 [,] 1 ) 
|->  ( ( ( A  /  N )  x.  t )  +  1 ) )  e.  ( ( 0 [,] 1
) -cn-> ( CC  \ 
(  -oo (,] 0 ) ) ) )
159158, 137cncfco 18968 . . . . . 6  |-  ( ph  ->  ( ( log  |`  ( CC  \  (  -oo (,] 0 ) ) )  o.  ( t  e.  ( 0 [,] 1
)  |->  ( ( ( A  /  N )  x.  t )  +  1 ) ) )  e.  ( ( 0 [,] 1 ) -cn-> CC ) )
160146, 159eqeltrrd 2517 . . . . 5  |-  ( ph  ->  ( t  e.  ( 0 [,] 1 ) 
|->  ( log `  (
( ( A  /  N )  x.  t
)  +  1 ) ) )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
1617, 9, 33, 160cncfmpt2f 18975 . . . 4  |-  ( ph  ->  ( t  e.  ( 0 [,] 1 ) 
|->  ( ( ( A  /  N )  x.  t )  -  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )
16224a1i 11 . . . . . . . 8  |-  ( ph  ->  RR  C_  CC )
16323a1i 11 . . . . . . . 8  |-  ( ph  ->  ( 0 [,] 1
)  C_  RR )
164132logdmn0 20562 . . . . . . . . . . 11  |-  ( ( ( ( A  /  N )  x.  t
)  +  1 )  e.  ( CC  \ 
(  -oo (,] 0 ) )  ->  ( (
( A  /  N
)  x.  t )  +  1 )  =/=  0 )
165134, 164syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( ( A  /  N )  x.  t
)  +  1 )  =/=  0 )
16641, 165logcld 20499 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) )  e.  CC )
16738, 166subcld 9442 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( 0 [,] 1
) )  ->  (
( ( A  /  N )  x.  t
)  -  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) ) )  e.  CC )
1687tgioo2 18865 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
169 iccntr 18883 . . . . . . . . 9  |-  ( ( 0  e.  RR  /\  1  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( 0 [,] 1 ) )  =  ( 0 (,) 1
) )
1703, 6, 169sylancr 646 . . . . . . . 8  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( 0 [,] 1 ) )  =  ( 0 (,) 1
) )
171162, 163, 167, 168, 7, 170dvmptntr 19888 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( ( ( A  /  N )  x.  t
)  -  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) )  =  ( RR 
_D  ( t  e.  ( 0 (,) 1
)  |->  ( ( ( A  /  N )  x.  t )  -  ( log `  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) ) ) )
172 reex 9112 . . . . . . . . . 10  |-  RR  e.  _V
173172prid1 3936 . . . . . . . . 9  |-  RR  e.  { RR ,  CC }
174173a1i 11 . . . . . . . 8  |-  ( ph  ->  RR  e.  { RR ,  CC } )
17517adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  A  e.  CC )
17620adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  N  e.  CC )
17721adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  N  =/=  0 )
178175, 176, 177divcld 9821 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( A  /  N )  e.  CC )
179 ioossicc 11027 . . . . . . . . . . 11  |-  ( 0 (,) 1 )  C_  ( 0 [,] 1
)
180179sseli 3330 . . . . . . . . . 10  |-  ( t  e.  ( 0 (,) 1 )  ->  t  e.  ( 0 [,] 1
) )
181180, 37sylan2 462 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  t  e.  CC )
182178, 181mulcld 9139 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( A  /  N
)  x.  t )  e.  CC )
18317adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  RR )  ->  A  e.  CC )
18420adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  RR )  ->  N  e.  CC )
18521adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  RR )  ->  N  =/=  0 )
186183, 184, 185divcld 9821 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  RR )  ->  ( A  /  N )  e.  CC )
187162sselda 3334 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  RR )  ->  t  e.  CC )
188186, 187mulcld 9139 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  RR )  ->  ( ( A  /  N )  x.  t )  e.  CC )
18939a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  RR )  ->  1  e.  CC )
190174dvmptid 19874 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  (
t  e.  RR  |->  t ) )  =  ( t  e.  RR  |->  1 ) )
191174, 187, 189, 190, 22dvmptcmul 19881 . . . . . . . . . 10  |-  ( ph  ->  ( RR  _D  (
t  e.  RR  |->  ( ( A  /  N
)  x.  t ) ) )  =  ( t  e.  RR  |->  ( ( A  /  N
)  x.  1 ) ) )
19222mulid1d 9136 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  /  N )  x.  1 )  =  ( A  /  N ) )
193192mpteq2dv 4321 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  RR  |->  ( ( A  /  N )  x.  1 ) )  =  ( t  e.  RR  |->  ( A  /  N ) ) )
194191, 193eqtrd 2474 . . . . . . . . 9  |-  ( ph  ->  ( RR  _D  (
t  e.  RR  |->  ( ( A  /  N
)  x.  t ) ) )  =  ( t  e.  RR  |->  ( A  /  N ) ) )
195179, 163syl5ss 3345 . . . . . . . . 9  |-  ( ph  ->  ( 0 (,) 1
)  C_  RR )
196 retop 18826 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  e.  Top
197 iooretop 18831 . . . . . . . . . . 11  |-  ( 0 (,) 1 )  e.  ( topGen `  ran  (,) )
198 isopn3i 17177 . . . . . . . . . . 11  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( 0 (,) 1 )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (
0 (,) 1 ) )  =  ( 0 (,) 1 ) )
199196, 197, 198mp2an 655 . . . . . . . . . 10  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( 0 (,) 1
) )  =  ( 0 (,) 1 )
200199a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( 0 (,) 1 ) )  =  ( 0 (,) 1
) )
201174, 188, 186, 194, 195, 168, 7, 200dvmptres2 19879 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N
)  x.  t ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( A  /  N ) ) )
202180, 166sylan2 462 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) )  e.  CC )
20339a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  1  e.  CC )
204182, 203addcld 9138 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( A  /  N )  x.  t
)  +  1 )  e.  CC )
205180, 165sylan2 462 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( A  /  N )  x.  t
)  +  1 )  =/=  0 )
206204, 205reccld 9814 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) )  e.  CC )
207206, 178mulcld 9139 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) )  e.  CC )
208 cnex 9102 . . . . . . . . . . 11  |-  CC  e.  _V
209208prid2 3937 . . . . . . . . . 10  |-  CC  e.  { RR ,  CC }
210209a1i 11 . . . . . . . . 9  |-  ( ph  ->  CC  e.  { RR ,  CC } )
211180, 134sylan2 462 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( A  /  N )  x.  t
)  +  1 )  e.  ( CC  \ 
(  -oo (,] 0 ) ) )
212 eldifi 3455 . . . . . . . . . . 11  |-  ( y  e.  ( CC  \ 
(  -oo (,] 0 ) )  ->  y  e.  CC )
213212adantl 454 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( CC  \  (  -oo (,] 0 ) ) )  ->  y  e.  CC )
214132logdmn0 20562 . . . . . . . . . . 11  |-  ( y  e.  ( CC  \ 
(  -oo (,] 0 ) )  ->  y  =/=  0 )
215214adantl 454 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( CC  \  (  -oo (,] 0 ) ) )  ->  y  =/=  0 )
216213, 215logcld 20499 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( CC  \  (  -oo (,] 0 ) ) )  ->  ( log `  y )  e.  CC )
217213, 215reccld 9814 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( CC  \  (  -oo (,] 0 ) ) )  ->  ( 1  /  y )  e.  CC )
218188, 189addcld 9138 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  RR )  ->  ( ( ( A  /  N
)  x.  t )  +  1 )  e.  CC )
219 0cn 9115 . . . . . . . . . . . . 13  |-  0  e.  CC
220219a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  RR )  ->  0  e.  CC )
221174, 152dvmptc 19875 . . . . . . . . . . . 12  |-  ( ph  ->  ( RR  _D  (
t  e.  RR  |->  1 ) )  =  ( t  e.  RR  |->  0 ) )
222174, 188, 186, 194, 189, 220, 221dvmptadd 19877 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  (
t  e.  RR  |->  ( ( ( A  /  N )  x.  t
)  +  1 ) ) )  =  ( t  e.  RR  |->  ( ( A  /  N
)  +  0 ) ) )
22322addid1d 9297 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A  /  N )  +  0 )  =  ( A  /  N ) )
224223mpteq2dv 4321 . . . . . . . . . . 11  |-  ( ph  ->  ( t  e.  RR  |->  ( ( A  /  N )  +  0 ) )  =  ( t  e.  RR  |->  ( A  /  N ) ) )
225222, 224eqtrd 2474 . . . . . . . . . 10  |-  ( ph  ->  ( RR  _D  (
t  e.  RR  |->  ( ( ( A  /  N )  x.  t
)  +  1 ) ) )  =  ( t  e.  RR  |->  ( A  /  N ) ) )
226174, 218, 186, 225, 195, 168, 7, 200dvmptres2 19879 . . . . . . . . 9  |-  ( ph  ->  ( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( ( ( A  /  N )  x.  t
)  +  1 ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( A  /  N ) ) )
227 fvres 5774 . . . . . . . . . . . . 13  |-  ( y  e.  ( CC  \ 
(  -oo (,] 0 ) )  ->  ( ( log  |`  ( CC  \ 
(  -oo (,] 0 ) ) ) `  y
)  =  ( log `  y ) )
228227mpteq2ia 4316 . . . . . . . . . . . 12  |-  ( y  e.  ( CC  \ 
(  -oo (,] 0 ) )  |->  ( ( log  |`  ( CC  \  (  -oo (,] 0 ) ) ) `  y ) )  =  ( y  e.  ( CC  \ 
(  -oo (,] 0 ) )  |->  ( log `  y
) )
229140, 228syl6req 2491 . . . . . . . . . . 11  |-  ( ph  ->  ( y  e.  ( CC  \  (  -oo (,] 0 ) )  |->  ( log `  y ) )  =  ( log  |`  ( CC  \  (  -oo (,] 0 ) ) ) )
230229oveq2d 6126 . . . . . . . . . 10  |-  ( ph  ->  ( CC  _D  (
y  e.  ( CC 
\  (  -oo (,] 0 ) )  |->  ( log `  y ) ) )  =  ( CC  _D  ( log  |`  ( CC  \  (  -oo (,] 0 ) ) ) ) )
231132dvlog 20573 . . . . . . . . . 10  |-  ( CC 
_D  ( log  |`  ( CC  \  (  -oo (,] 0 ) ) ) )  =  ( y  e.  ( CC  \ 
(  -oo (,] 0 ) )  |->  ( 1  / 
y ) )
232230, 231syl6eq 2490 . . . . . . . . 9  |-  ( ph  ->  ( CC  _D  (
y  e.  ( CC 
\  (  -oo (,] 0 ) )  |->  ( log `  y ) ) )  =  ( y  e.  ( CC 
\  (  -oo (,] 0 ) )  |->  ( 1  /  y ) ) )
233 fveq2 5757 . . . . . . . . 9  |-  ( y  =  ( ( ( A  /  N )  x.  t )  +  1 )  ->  ( log `  y )  =  ( log `  (
( ( A  /  N )  x.  t
)  +  1 ) ) )
234 oveq2 6118 . . . . . . . . 9  |-  ( y  =  ( ( ( A  /  N )  x.  t )  +  1 )  ->  (
1  /  y )  =  ( 1  / 
( ( ( A  /  N )  x.  t )  +  1 ) ) )
235174, 210, 211, 178, 216, 217, 226, 232, 233, 234dvmptco 19889 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( log `  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) )
236174, 182, 178, 201, 202, 207, 235dvmptsub 19884 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( ( ( A  /  N )  x.  t
)  -  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N )  -  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) ) ) )
237171, 236eqtrd 2474 . . . . . 6  |-  ( ph  ->  ( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( ( ( A  /  N )  x.  t
)  -  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N )  -  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) ) ) )
238237dmeqd 5101 . . . . 5  |-  ( ph  ->  dom  ( RR  _D  ( t  e.  ( 0 [,] 1 ) 
|->  ( ( ( A  /  N )  x.  t )  -  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) )  =  dom  ( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) )
239 ovex 6135 . . . . . 6  |-  ( ( A  /  N )  -  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) )  e. 
_V
240 eqid 2442 . . . . . 6  |-  ( t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N )  -  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) ) )  =  ( t  e.  ( 0 (,) 1
)  |->  ( ( A  /  N )  -  ( ( 1  / 
( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N ) ) ) )
241239, 240dmmpti 5603 . . . . 5  |-  dom  (
t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N
)  -  ( ( 1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) )  x.  ( A  /  N ) ) ) )  =  ( 0 (,) 1 )
242238, 241syl6eq 2490 . . . 4  |-  ( ph  ->  dom  ( RR  _D  ( t  e.  ( 0 [,] 1 ) 
|->  ( ( ( A  /  N )  x.  t )  -  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) )  =  ( 0 (,) 1 ) )
243100, 53remulcld 9147 . . . . . . . . 9  |-  ( ph  ->  ( 2  x.  R
)  e.  RR )
24412nnrpd 10678 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  RR+ )
24553, 244ltaddrpd 10708 . . . . . . . . . 10  |-  ( ph  ->  R  <  ( R  +  R ) )
24653recnd 9145 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  CC )
2472462timesd 10241 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  R
)  =  ( R  +  R ) )
248245, 247breqtrrd 4263 . . . . . . . . 9  |-  ( ph  ->  R  <  ( 2  x.  R ) )
24953, 243, 19, 248, 94ltletrd 9261 . . . . . . . 8  |-  ( ph  ->  R  <  N )
250 difrp 10676 . . . . . . . . 9  |-  ( ( R  e.  RR  /\  N  e.  RR )  ->  ( R  <  N  <->  ( N  -  R )  e.  RR+ ) )
25153, 19, 250syl2anc 644 . . . . . . . 8  |-  ( ph  ->  ( R  <  N  <->  ( N  -  R )  e.  RR+ ) )
252249, 251mpbid 203 . . . . . . 7  |-  ( ph  ->  ( N  -  R
)  e.  RR+ )
253252rprecred 10690 . . . . . 6  |-  ( ph  ->  ( 1  /  ( N  -  R )
)  e.  RR )
25418nnrecred 10076 . . . . . 6  |-  ( ph  ->  ( 1  /  N
)  e.  RR )
255253, 254resubcld 9496 . . . . 5  |-  ( ph  ->  ( ( 1  / 
( N  -  R
) )  -  (
1  /  N ) )  e.  RR )
25653, 255remulcld 9147 . . . 4  |-  ( ph  ->  ( R  x.  (
( 1  /  ( N  -  R )
)  -  ( 1  /  N ) ) )  e.  RR )
257237fveq1d 5759 . . . . . . 7  |-  ( ph  ->  ( ( RR  _D  ( t  e.  ( 0 [,] 1 ) 
|->  ( ( ( A  /  N )  x.  t )  -  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) ) `  y
)  =  ( ( t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N
)  -  ( ( 1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) )  x.  ( A  /  N ) ) ) ) `  y ) )
258257fveq2d 5761 . . . . . 6  |-  ( ph  ->  ( abs `  (
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( ( ( A  /  N )  x.  t
)  -  ( log `  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) ) `  y ) )  =  ( abs `  ( ( t  e.  ( 0 (,) 1
)  |->  ( ( A  /  N )  -  ( ( 1  / 
( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N ) ) ) ) `  y
) ) )
259258adantr 453 . . . . 5  |-  ( (
ph  /\  y  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( RR 
_D  ( t  e.  ( 0 [,] 1
)  |->  ( ( ( A  /  N )  x.  t )  -  ( log `  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) ) ) `  y ) )  =  ( abs `  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) `  y
) ) )
260 nfv 1630 . . . . . . 7  |-  F/ t ( ph  /\  y  e.  ( 0 (,) 1
) )
261 nfcv 2578 . . . . . . . . 9  |-  F/_ t abs
262 nffvmpt1 5765 . . . . . . . . 9  |-  F/_ t
( ( t  e.  ( 0 (,) 1
)  |->  ( ( A  /  N )  -  ( ( 1  / 
( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N ) ) ) ) `  y
)
263261, 262nffv 5764 . . . . . . . 8  |-  F/_ t
( abs `  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) `  y
) )
264 nfcv 2578 . . . . . . . 8  |-  F/_ t  <_
265 nfcv 2578 . . . . . . . 8  |-  F/_ t
( R  x.  (
( 1  /  ( N  -  R )
)  -  ( 1  /  N ) ) )
266263, 264, 265nfbr 4281 . . . . . . 7  |-  F/ t ( abs `  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) `  y
) )  <_  ( R  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) )
267260, 266nfim 1834 . . . . . 6  |-  F/ t ( ( ph  /\  y  e.  ( 0 (,) 1 ) )  ->  ( abs `  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) `  y
) )  <_  ( R  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) ) )
268 eleq1 2502 . . . . . . . 8  |-  ( t  =  y  ->  (
t  e.  ( 0 (,) 1 )  <->  y  e.  ( 0 (,) 1
) ) )
269268anbi2d 686 . . . . . . 7  |-  ( t  =  y  ->  (
( ph  /\  t  e.  ( 0 (,) 1
) )  <->  ( ph  /\  y  e.  ( 0 (,) 1 ) ) ) )
270 fveq2 5757 . . . . . . . . 9  |-  ( t  =  y  ->  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) `  t
)  =  ( ( t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N
)  -  ( ( 1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) )  x.  ( A  /  N ) ) ) ) `  y ) )
271270fveq2d 5761 . . . . . . . 8  |-  ( t  =  y  ->  ( abs `  ( ( t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N )  -  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) ) ) `
 t ) )  =  ( abs `  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) `  y
) ) )
272271breq1d 4247 . . . . . . 7  |-  ( t  =  y  ->  (
( abs `  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) `  t
) )  <_  ( R  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) )  <-> 
( abs `  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) `  y
) )  <_  ( R  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) ) ) )
273269, 272imbi12d 313 . . . . . 6  |-  ( t  =  y  ->  (
( ( ph  /\  t  e.  ( 0 (,) 1 ) )  ->  ( abs `  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) `  t
) )  <_  ( R  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) ) )  <->  ( ( ph  /\  y  e.  ( 0 (,) 1 ) )  ->  ( abs `  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) `  y
) )  <_  ( R  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) ) ) ) )
274 simpr 449 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  t  e.  ( 0 (,) 1
) )
275240fvmpt2 5841 . . . . . . . . . 10  |-  ( ( t  e.  ( 0 (,) 1 )  /\  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) )  e.  _V )  ->  ( ( t  e.  ( 0 (,) 1
)  |->  ( ( A  /  N )  -  ( ( 1  / 
( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N ) ) ) ) `  t
)  =  ( ( A  /  N )  -  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) ) )
276274, 239, 275sylancl 645 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( A  /  N )  -  (
( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  x.  ( A  /  N ) ) ) ) `  t
)  =  ( ( A  /  N )  -  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) ) )
277276fveq2d 5761 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N )  -  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) ) ) `
 t ) )  =  ( abs `  (
( A  /  N
)  -  ( ( 1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) )  x.  ( A  /  N ) ) ) ) )
278178, 203, 206subdid 9520 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( A  /  N
)  x.  ( 1  -  ( 1  / 
( ( ( A  /  N )  x.  t )  +  1 ) ) ) )  =  ( ( ( A  /  N )  x.  1 )  -  ( ( A  /  N )  x.  (
1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) ) )
279178mulid1d 9136 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( A  /  N
)  x.  1 )  =  ( A  /  N ) )
280178, 206mulcomd 9140 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( A  /  N
)  x.  ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) ) )  =  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) )
281279, 280oveq12d 6128 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( A  /  N )  x.  1 )  -  ( ( A  /  N )  x.  ( 1  / 
( ( ( A  /  N )  x.  t )  +  1 ) ) ) )  =  ( ( A  /  N )  -  ( ( 1  / 
( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N ) ) ) )
282278, 281eqtr2d 2475 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( A  /  N
)  -  ( ( 1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) )  x.  ( A  /  N ) ) )  =  ( ( A  /  N )  x.  ( 1  -  (
1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) ) )
283282fveq2d 5761 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( A  /  N )  -  ( ( 1  / 
( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N ) ) ) )  =  ( abs `  ( ( A  /  N )  x.  ( 1  -  ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) ) ) )
284175, 176, 177absdivd 12288 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( A  /  N ) )  =  ( ( abs `  A
)  /  ( abs `  N ) ) )
28519adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  N  e.  RR )
28665adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  0  <_  N )
287285, 286absidd 12256 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  N )  =  N )
288287oveq2d 6126 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( abs `  A
)  /  ( abs `  N ) )  =  ( ( abs `  A
)  /  N ) )
289284, 288eqtrd 2474 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( A  /  N ) )  =  ( ( abs `  A
)  /  N ) )
290289oveq1d 6125 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( abs `  ( A  /  N ) )  x.  ( abs `  (
1  -  ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) )  =  ( ( ( abs `  A
)  /  N )  x.  ( abs `  (
1  -  ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) ) )
291203, 206subcld 9442 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  -  ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) ) )  e.  CC )
292178, 291absmuld 12287 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( A  /  N )  x.  ( 1  -  (
1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) ) )  =  ( ( abs `  ( A  /  N ) )  x.  ( abs `  (
1  -  ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) ) )
29369adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  A )  e.  RR )
294293recnd 9145 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  A )  e.  CC )
295291abscld 12269 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( 1  -  ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) )  e.  RR )
296295recnd 9145 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( 1  -  ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) )  e.  CC )
297294, 296, 176, 177div23d 9858 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( abs `  A
)  x.  ( abs `  ( 1  -  (
1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) ) )  /  N )  =  ( ( ( abs `  A
)  /  N )  x.  ( abs `  (
1  -  ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) ) )
298290, 292, 2973eqtr4d 2484 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( A  /  N )  x.  ( 1  -  (
1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) ) )  =  ( ( ( abs `  A )  x.  ( abs `  ( 1  -  ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) ) )  /  N ) )
299277, 283, 2983eqtrd 2478 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N )  -  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) ) ) `
 t ) )  =  ( ( ( abs `  A )  x.  ( abs `  (
1  -  ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) )  /  N
) )
30053adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  R  e.  RR )
301253adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( N  -  R ) )  e.  RR )
302254adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  N )  e.  RR )
303301, 302resubcld 9496 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( 1  /  ( N  -  R )
)  -  ( 1  /  N ) )  e.  RR )
304285, 303remulcld 9147 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) )  e.  RR )
30517absge0d 12277 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  ( abs `  A ) )
306305adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  0  <_  ( abs `  A
) )
307291absge0d 12277 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  0  <_  ( abs `  (
1  -  ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) ) ) ) )
30880adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  A )  <_  R )
309252adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  -  R )  e.  RR+ )
310244adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  R  e.  RR+ )
311309, 310rpdivcld 10696 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  -  R
)  /  R )  e.  RR+ )
31216dmgmn0 24841 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  =/=  0 )
313312adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  A  =/=  0 )
314175, 176, 313, 177divne0d 9837 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( A  /  N )  =/=  0 )
315 eliooord 11001 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  ( 0 (,) 1 )  ->  (
0  <  t  /\  t  <  1 ) )
316315adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
0  <  t  /\  t  <  1 ) )
317316simpld 447 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  0  <  t )
318317gt0ne0d 9622 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  t  =/=  0 )
319178, 181, 314, 318mulne0d 9705 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( A  /  N
)  x.  t )  =/=  0 )
320182, 319reccld 9814 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( ( A  /  N )  x.  t ) )  e.  CC )
321203, 320addcld 9138 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) )  e.  CC )
322182, 203, 182, 319divdird 9859 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( ( A  /  N )  x.  t )  +  1 )  /  ( ( A  /  N )  x.  t ) )  =  ( ( ( ( A  /  N
)  x.  t )  /  ( ( A  /  N )  x.  t ) )  +  ( 1  /  (
( A  /  N
)  x.  t ) ) ) )
323182, 319dividd 9819 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( A  /  N )  x.  t
)  /  ( ( A  /  N )  x.  t ) )  =  1 )
324323oveq1d 6125 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( ( A  /  N )  x.  t )  /  (
( A  /  N
)  x.  t ) )  +  ( 1  /  ( ( A  /  N )  x.  t ) ) )  =  ( 1  +  ( 1  /  (
( A  /  N
)  x.  t ) ) ) )
325322, 324eqtrd 2474 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( ( A  /  N )  x.  t )  +  1 )  /  ( ( A  /  N )  x.  t ) )  =  ( 1  +  ( 1  /  (
( A  /  N
)  x.  t ) ) ) )
326204, 182, 205, 319divne0d 9837 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( ( A  /  N )  x.  t )  +  1 )  /  ( ( A  /  N )  x.  t ) )  =/=  0 )
327325, 326eqnetrrd 2627 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) )  =/=  0 )
328321, 327absrpcld 12281 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( 1  +  ( 1  /  (
( A  /  N
)  x.  t ) ) ) )  e.  RR+ )
3295a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  1  e.  RR )
330 0le1 9582 . . . . . . . . . . . . . 14  |-  0  <_  1
331330a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  0  <_  1 )
332311rpred 10679 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  -  R
)  /  R )  e.  RR )
333320negcld 9429 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  -u (
1  /  ( ( A  /  N )  x.  t ) )  e.  CC )
334333abscld 12269 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  -u ( 1  / 
( ( A  /  N )  x.  t
) ) )  e.  RR )
335334, 329resubcld 9496 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( abs `  -u (
1  /  ( ( A  /  N )  x.  t ) ) )  -  1 )  e.  RR )
336321abscld 12269 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( 1  +  ( 1  /  (
( A  /  N
)  x.  t ) ) ) )  e.  RR )
337246adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  R  e.  CC )
338310rpne0d 10684 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  R  =/=  0 )
339176, 337, 337, 338divsubdird 9860 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  -  R
)  /  R )  =  ( ( N  /  R )  -  ( R  /  R
) ) )
340337, 338dividd 9819 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( R  /  R )  =  1 )
341340oveq2d 6126 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  /  R
)  -  ( R  /  R ) )  =  ( ( N  /  R )  - 
1 ) )
342339, 341eqtrd 2474 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  -  R
)  /  R )  =  ( ( N  /  R )  - 
1 ) )
343285, 310rerpdivcld 10706 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  /  R )  e.  RR )
344337, 176, 338, 177recdivd 9838 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( R  /  N ) )  =  ( N  /  R ) )
345180, 93sylan2 462 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( A  /  N )  x.  t ) )  <_ 
( R  /  N
) )
346182, 319absrpcld 12281 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( A  /  N )  x.  t ) )  e.  RR+ )
34764adantr 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  N  e.  RR+ )
348310, 347rpdivcld 10696 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( R  /  N )  e.  RR+ )
349346, 348lerecd 10698 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( abs `  (
( A  /  N
)  x.  t ) )  <_  ( R  /  N )  <->  ( 1  /  ( R  /  N ) )  <_ 
( 1  /  ( abs `  ( ( A  /  N )  x.  t ) ) ) ) )
350345, 349mpbid 203 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( R  /  N ) )  <_  ( 1  / 
( abs `  (
( A  /  N
)  x.  t ) ) ) )
351344, 350eqbrtrrd 4259 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  /  R )  <_ 
( 1  /  ( abs `  ( ( A  /  N )  x.  t ) ) ) )
352320absnegd 12282 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  -u ( 1  / 
( ( A  /  N )  x.  t
) ) )  =  ( abs `  (
1  /  ( ( A  /  N )  x.  t ) ) ) )
353203, 182, 319absdivd 12288 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( 1  / 
( ( A  /  N )  x.  t
) ) )  =  ( ( abs `  1
)  /  ( abs `  ( ( A  /  N )  x.  t
) ) ) )
354 abs1 12133 . . . . . . . . . . . . . . . . . . . 20  |-  ( abs `  1 )  =  1
355354oveq1i 6120 . . . . . . . . . . . . . . . . . . 19  |-  ( ( abs `  1 )  /  ( abs `  (
( A  /  N
)  x.  t ) ) )  =  ( 1  /  ( abs `  ( ( A  /  N )  x.  t
) ) )
356353, 355syl6eq 2490 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( 1  / 
( ( A  /  N )  x.  t
) ) )  =  ( 1  /  ( abs `  ( ( A  /  N )  x.  t ) ) ) )
357352, 356eqtrd 2474 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  -u ( 1  / 
( ( A  /  N )  x.  t
) ) )  =  ( 1  /  ( abs `  ( ( A  /  N )  x.  t ) ) ) )
358351, 357breqtrrd 4263 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  /  R )  <_ 
( abs `  -u (
1  /  ( ( A  /  N )  x.  t ) ) ) )
359343, 334, 329, 358lesub1dd 9673 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  /  R
)  -  1 )  <_  ( ( abs `  -u ( 1  / 
( ( A  /  N )  x.  t
) ) )  - 
1 ) )
360342, 359eqbrtrd 4257 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  -  R
)  /  R )  <_  ( ( abs `  -u ( 1  / 
( ( A  /  N )  x.  t
) ) )  - 
1 ) )
361354oveq2i 6121 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  -u (
1  /  ( ( A  /  N )  x.  t ) ) )  -  ( abs `  1 ) )  =  ( ( abs `  -u ( 1  / 
( ( A  /  N )  x.  t
) ) )  - 
1 )
362333, 203abs2difd 12290 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( abs `  -u (
1  /  ( ( A  /  N )  x.  t ) ) )  -  ( abs `  1 ) )  <_  ( abs `  ( -u ( 1  /  (
( A  /  N
)  x.  t ) )  -  1 ) ) )
363361, 362syl5eqbrr 4271 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( abs `  -u (
1  /  ( ( A  /  N )  x.  t ) ) )  -  1 )  <_  ( abs `  ( -u ( 1  /  (
( A  /  N
)  x.  t ) )  -  1 ) ) )
364203, 320addcomd 9299 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) )  =  ( ( 1  /  ( ( A  /  N )  x.  t ) )  +  1 ) )
365364negeqd 9331 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  -u (
1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) )  =  -u ( ( 1  /  ( ( A  /  N )  x.  t ) )  +  1 ) )
366320, 203negdi2d 9456 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  -u (
( 1  /  (
( A  /  N
)  x.  t ) )  +  1 )  =  ( -u (
1  /  ( ( A  /  N )  x.  t ) )  -  1 ) )
367365, 366eqtrd 2474 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  -u (
1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) )  =  ( -u (
1  /  ( ( A  /  N )  x.  t ) )  -  1 ) )
368367fveq2d 5761 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  -u ( 1  +  ( 1  /  (
( A  /  N
)  x.  t ) ) ) )  =  ( abs `  ( -u ( 1  /  (
( A  /  N
)  x.  t ) )  -  1 ) ) )
369321absnegd 12282 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  -u ( 1  +  ( 1  /  (
( A  /  N
)  x.  t ) ) ) )  =  ( abs `  (
1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )
370368, 369eqtr3d 2476 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( -u (
1  /  ( ( A  /  N )  x.  t ) )  -  1 ) )  =  ( abs `  (
1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )
371363, 370breqtrd 4261 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( abs `  -u (
1  /  ( ( A  /  N )  x.  t ) ) )  -  1 )  <_  ( abs `  (
1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )
372332, 335, 336, 360, 371letrd 9258 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  -  R
)  /  R )  <_  ( abs `  (
1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )
373311, 328, 329, 331, 372lediv2ad 10701 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( abs `  ( 1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )  <_ 
( 1  /  (
( N  -  R
)  /  R ) ) )
37420, 246subcld 9442 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  -  R
)  e.  CC )
375374adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  -  R )  e.  CC )
37653, 249gtned 9239 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  =/=  R )
37720, 246, 376subne0d 9451 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  -  R
)  =/=  0 )
378377adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  -  R )  =/=  0 )
379375, 337, 378, 338recdivd 9838 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( ( N  -  R )  /  R ) )  =  ( R  / 
( N  -  R
) ) )
380176, 337nncand 9447 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  -  ( N  -  R ) )  =  R )
381380oveq1d 6125 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  -  ( N  -  R )
)  /  ( N  -  R ) )  =  ( R  / 
( N  -  R
) ) )
382176, 375, 375, 378divsubdird 9860 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  -  ( N  -  R )
)  /  ( N  -  R ) )  =  ( ( N  /  ( N  -  R ) )  -  ( ( N  -  R )  /  ( N  -  R )
) ) )
383381, 382eqtr3d 2476 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( R  /  ( N  -  R ) )  =  ( ( N  / 
( N  -  R
) )  -  (
( N  -  R
)  /  ( N  -  R ) ) ) )
384375, 378dividd 9819 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  -  R
)  /  ( N  -  R ) )  =  1 )
385384oveq2d 6126 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  /  ( N  -  R )
)  -  ( ( N  -  R )  /  ( N  -  R ) ) )  =  ( ( N  /  ( N  -  R ) )  - 
1 ) )
386379, 383, 3853eqtrd 2478 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( ( N  -  R )  /  R ) )  =  ( ( N  /  ( N  -  R ) )  - 
1 ) )
387373, 386breqtrd 4261 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( abs `  ( 1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )  <_ 
( ( N  / 
( N  -  R
) )  -  1 ) )
388204, 203, 204, 205divsubdird 9860 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( ( ( A  /  N )  x.  t )  +  1 )  -  1 )  /  ( ( ( A  /  N
)  x.  t )  +  1 ) )  =  ( ( ( ( ( A  /  N )  x.  t
)  +  1 )  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  -  ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) )
389182, 203pncand 9443 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( ( A  /  N )  x.  t )  +  1 )  -  1 )  =  ( ( A  /  N )  x.  t ) )
390389oveq1d 6125 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( ( ( A  /  N )  x.  t )  +  1 )  -  1 )  /  ( ( ( A  /  N
)  x.  t )  +  1 ) )  =  ( ( ( A  /  N )  x.  t )  / 
( ( ( A  /  N )  x.  t )  +  1 ) ) )
391204, 205dividd 9819 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( ( A  /  N )  x.  t )  +  1 )  /  ( ( ( A  /  N
)  x.  t )  +  1 ) )  =  1 )
392391oveq1d 6125 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( ( ( A  /  N )  x.  t )  +  1 )  /  (
( ( A  /  N )  x.  t
)  +  1 ) )  -  ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) ) )  =  ( 1  -  ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) )
393388, 390, 3923eqtr3rd 2483 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  -  ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) ) )  =  ( ( ( A  /  N )  x.  t )  / 
( ( ( A  /  N )  x.  t )  +  1 ) ) )
394204, 182, 205, 319recdivd 9838 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( ( ( ( A  /  N )  x.  t
)  +  1 )  /  ( ( A  /  N )  x.  t ) ) )  =  ( ( ( A  /  N )  x.  t )  / 
( ( ( A  /  N )  x.  t )  +  1 ) ) )
395325oveq2d 6126 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( ( ( ( A  /  N )  x.  t
)  +  1 )  /  ( ( A  /  N )  x.  t ) ) )  =  ( 1  / 
( 1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )
396393, 394, 3953eqtr2d 2480 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  -  ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) ) )  =  ( 1  / 
( 1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )
397396fveq2d 5761 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( 1  -  ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) )  =  ( abs `  (
1  /  ( 1  +  ( 1  / 
( ( A  /  N )  x.  t
) ) ) ) ) )
398203, 321, 327absdivd 12288 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( 1  / 
( 1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )  =  ( ( abs `  1
)  /  ( abs `  ( 1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) ) )
399354oveq1i 6120 . . . . . . . . . . . . 13  |-  ( ( abs `  1 )  /  ( abs `  (
1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )  =  ( 1  /  ( abs `  ( 1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )
400398, 399syl6eq 2490 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( 1  / 
( 1  +  ( 1  /  ( ( A  /  N )  x.  t ) ) ) ) )  =  ( 1  /  ( abs `  ( 1  +  ( 1  /  (
( A  /  N
)  x.  t ) ) ) ) ) )
401397, 400eqtrd 2474 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( 1  -  ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) )  =  ( 1  /  ( abs `  ( 1  +  ( 1  /  (
( A  /  N
)  x.  t ) ) ) ) ) )
402374, 377reccld 9814 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  /  ( N  -  R )
)  e.  CC )
403402adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  ( N  -  R ) )  e.  CC )
404254recnd 9145 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  /  N
)  e.  CC )
405404adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  /  N )  e.  CC )
406176, 403, 405subdid 9520 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) )  =  ( ( N  x.  ( 1  / 
( N  -  R
) ) )  -  ( N  x.  (
1  /  N ) ) ) )
407176, 375, 378divrecd 9824 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  /  ( N  -  R ) )  =  ( N  x.  (
1  /  ( N  -  R ) ) ) )
408407eqcomd 2447 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  x.  ( 1  /  ( N  -  R ) ) )  =  ( N  / 
( N  -  R
) ) )
409176, 177recidd 9816 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  x.  ( 1  /  N ) )  =  1 )
410408, 409oveq12d 6128 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( N  x.  (
1  /  ( N  -  R ) ) )  -  ( N  x.  ( 1  /  N ) ) )  =  ( ( N  /  ( N  -  R ) )  - 
1 ) )
411406, 410eqtrd 2474 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( N  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) )  =  ( ( N  /  ( N  -  R ) )  - 
1 ) )
412387, 401, 4113brtr4d 4267 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( 1  -  ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) )  <_ 
( N  x.  (
( 1  /  ( N  -  R )
)  -  ( 1  /  N ) ) ) )
413293, 300, 295, 304, 306, 307, 308, 412lemul12ad 9984 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( abs `  A
)  x.  ( abs `  ( 1  -  (
1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) ) )  <_ 
( R  x.  ( N  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) ) ) )
414255recnd 9145 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  / 
( N  -  R
) )  -  (
1  /  N ) )  e.  CC )
415414adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( 1  /  ( N  -  R )
)  -  ( 1  /  N ) )  e.  CC )
416337, 176, 415mul12d 9306 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( R  x.  ( N  x.  ( ( 1  / 
( N  -  R
) )  -  (
1  /  N ) ) ) )  =  ( N  x.  ( R  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) ) ) )
417413, 416breqtrd 4261 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( abs `  A
)  x.  ( abs `  ( 1  -  (
1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) ) )  <_ 
( N  x.  ( R  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) ) ) )
418293, 295remulcld 9147 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( abs `  A
)  x.  ( abs `  ( 1  -  (
1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) ) )  e.  RR )
419256adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( R  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) )  e.  RR )
420418, 419, 347ledivmuld 10728 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( ( abs `  A )  x.  ( abs `  ( 1  -  ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) ) )  /  N )  <_ 
( R  x.  (
( 1  /  ( N  -  R )
)  -  ( 1  /  N ) ) )  <->  ( ( abs `  A )  x.  ( abs `  ( 1  -  ( 1  /  (
( ( A  /  N )  x.  t
)  +  1 ) ) ) ) )  <_  ( N  x.  ( R  x.  (
( 1  /  ( N  -  R )
)  -  ( 1  /  N ) ) ) ) ) )
421417, 420mpbird 225 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  (
( ( abs `  A
)  x.  ( abs `  ( 1  -  (
1  /  ( ( ( A  /  N
)  x.  t )  +  1 ) ) ) ) )  /  N )  <_  ( R  x.  ( (
1  /  ( N  -  R ) )  -  ( 1  /  N ) ) ) )
422299, 421eqbrtrd 4257 . . . . . 6  |-  ( (
ph  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N )  -  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) ) ) `
 t ) )  <_  ( R  x.  ( ( 1  / 
( N  -  R
) )  -  (
1  /  N ) ) ) )
423267, 273, 422chvar 1971 . . . . 5  |-  ( (
ph  /\  y  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( t  e.  ( 0 (,) 1 )  |->  ( ( A  /  N )  -  ( ( 1  /  ( ( ( A  /  N )  x.  t )  +  1 ) )  x.  ( A  /  N
) ) ) ) `
 y ) )  <_  ( R  x.  ( ( 1  / 
( N  -  R
) )  -  (
1  /  N ) ) ) )
424259, 423eqbrtrd 4257 . . . 4  |-  ( (
ph  /\  y  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( RR 
_D  ( t  e.  ( 0 [,] 1
)  |->  ( ( ( A  /  N )  x.  t