Metamath Proof Explorer

Theorem lgamgulmlem2

Description: Lemma for lgamgulm . (Contributed by Mario Carneiro, 3-Jul-2017)

Ref Expression
Hypotheses 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 lgamgulmlem2 
|- ( ph -> ( abs ` ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) ) <_ ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) )

Proof

Step Hyp Ref Expression
1 lgamgulm.r 
 |-  ( ph -> R e. NN )
2 lgamgulm.u 
 |-  U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
3 lgamgulm.n 
 |-  ( ph -> N e. NN )
4 lgamgulm.a 
 |-  ( ph -> A e. U )
5 lgamgulm.l 
 |-  ( ph -> ( 2 x. R ) <_ N )
6 1elunit 
 |-  1 e. ( 0 [,] 1 )
7 0elunit 
 |-  0 e. ( 0 [,] 1 )
8 0red 
 |-  ( ph -> 0 e. RR )
9 1red 
 |-  ( ph -> 1 e. RR )
10 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
11 10 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
12 11 a1i 
 |-  ( ph -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
13 1 2 lgamgulmlem1 
 |-  ( ph -> U C_ ( CC \ ( ZZ \ NN ) ) )
14 13 4 sseldd 
 |-  ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
15 14 eldifad 
 |-  ( ph -> A e. CC )
16 3 nnred 
 |-  ( ph -> N e. RR )
17 16 recnd 
 |-  ( ph -> N e. CC )
18 3 nnne0d 
 |-  ( ph -> N =/= 0 )
19 15 17 18 divcld 
 |-  ( ph -> ( A / N ) e. CC )
20 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
21 ax-resscn 
 |-  RR C_ CC
22 20 21 sstri 
 |-  ( 0 [,] 1 ) C_ CC
23 22 a1i 
 |-  ( ph -> ( 0 [,] 1 ) C_ CC )
24 ssidd 
 |-  ( ph -> CC C_ CC )
25 cncfmptc 
 |-  ( ( ( A / N ) e. CC /\ ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( t e. ( 0 [,] 1 ) |-> ( A / N ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
26 19 23 24 25 syl3anc 
 |-  ( ph -> ( t e. ( 0 [,] 1 ) |-> ( A / N ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
27 cncfmptid 
 |-  ( ( ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( t e. ( 0 [,] 1 ) |-> t ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
28 22 24 27 sylancr 
 |-  ( ph -> ( t e. ( 0 [,] 1 ) |-> t ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
29 26 28 mulcncf 
 |-  ( ph -> ( t e. ( 0 [,] 1 ) |-> ( ( A / N ) x. t ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
30 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
31 30 logcn 
 |-  ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC )
32 31 a1i 
 |-  ( ph -> ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) )
33 cncff 
 |-  ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) -> ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) --> CC )
34 32 33 syl 
 |-  ( ph -> ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) --> CC )
35 19 adantr 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( A / N ) e. CC )
36 simpr 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> t e. ( 0 [,] 1 ) )
37 20 36 sselid 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> t e. RR )
38 37 recnd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> t e. CC )
39 35 38 mulcld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( A / N ) x. t ) e. CC )
40 1cnd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> 1 e. CC )
41 39 40 addcld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( ( A / N ) x. t ) + 1 ) e. CC )
42 rere 
 |-  ( ( ( ( A / N ) x. t ) + 1 ) e. RR -> ( Re ` ( ( ( A / N ) x. t ) + 1 ) ) = ( ( ( A / N ) x. t ) + 1 ) )
43 42 adantl 
 |-  ( ( ( ph /\ t e. ( 0 [,] 1 ) ) /\ ( ( ( A / N ) x. t ) + 1 ) e. RR ) -> ( Re ` ( ( ( A / N ) x. t ) + 1 ) ) = ( ( ( A / N ) x. t ) + 1 ) )
44 41 recld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( Re ` ( ( ( A / N ) x. t ) + 1 ) ) e. RR )
45 39 recld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( Re ` ( ( A / N ) x. t ) ) e. RR )
46 45 recnd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( Re ` ( ( A / N ) x. t ) ) e. CC )
47 46 abscld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( abs ` ( Re ` ( ( A / N ) x. t ) ) ) e. RR )
48 39 abscld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( abs ` ( ( A / N ) x. t ) ) e. RR )
49 1red 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> 1 e. RR )
50 absrele 
 |-  ( ( ( A / N ) x. t ) e. CC -> ( abs ` ( Re ` ( ( A / N ) x. t ) ) ) <_ ( abs ` ( ( A / N ) x. t ) ) )
51 39 50 syl 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( abs ` ( Re ` ( ( A / N ) x. t ) ) ) <_ ( abs ` ( ( A / N ) x. t ) ) )
52 49 rehalfcld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( 1 / 2 ) e. RR )
53 1 nnred 
 |-  ( ph -> R e. RR )
54 53 adantr 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> R e. RR )
55 3 adantr 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> N e. NN )
56 54 55 nndivred 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( R / N ) e. RR )
57 19 abscld 
 |-  ( ph -> ( abs ` ( A / N ) ) e. RR )
58 57 adantr 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( abs ` ( A / N ) ) e. RR )
59 35 absge0d 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> 0 <_ ( abs ` ( A / N ) ) )
60 elicc01 
 |-  ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
61 60 simp2bi 
 |-  ( t e. ( 0 [,] 1 ) -> 0 <_ t )
62 61 adantl 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> 0 <_ t )
63 15 17 18 absdivd 
 |-  ( ph -> ( abs ` ( A / N ) ) = ( ( abs ` A ) / ( abs ` N ) ) )
64 3 nnrpd 
 |-  ( ph -> N e. RR+ )
65 64 rpge0d 
 |-  ( ph -> 0 <_ N )
66 16 65 absidd 
 |-  ( ph -> ( abs ` N ) = N )
67 66 oveq2d 
 |-  ( ph -> ( ( abs ` A ) / ( abs ` N ) ) = ( ( abs ` A ) / N ) )
68 63 67 eqtr2d 
 |-  ( ph -> ( ( abs ` A ) / N ) = ( abs ` ( A / N ) ) )
69 15 abscld 
 |-  ( ph -> ( abs ` A ) e. RR )
70 fveq2 
 |-  ( x = A -> ( abs ` x ) = ( abs ` A ) )
71 70 breq1d 
 |-  ( x = A -> ( ( abs ` x ) <_ R <-> ( abs ` A ) <_ R ) )
72 fvoveq1 
 |-  ( x = A -> ( abs ` ( x + k ) ) = ( abs ` ( A + k ) ) )
73 72 breq2d 
 |-  ( x = A -> ( ( 1 / R ) <_ ( abs ` ( x + k ) ) <-> ( 1 / R ) <_ ( abs ` ( A + k ) ) ) )
74 73 ralbidv 
 |-  ( x = A -> ( A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) <-> A. k e. NN0 ( 1 / R ) <_ ( abs ` ( A + k ) ) ) )
75 71 74 anbi12d 
 |-  ( 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 ) ) ) ) )
76 75 2 elrab2 
 |-  ( A e. U <-> ( A e. CC /\ ( ( abs ` A ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( A + k ) ) ) ) )
77 76 simprbi 
 |-  ( A e. U -> ( ( abs ` A ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( A + k ) ) ) )
78 4 77 syl 
 |-  ( ph -> ( ( abs ` A ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( A + k ) ) ) )
79 78 simpld 
 |-  ( ph -> ( abs ` A ) <_ R )
80 69 53 64 79 lediv1dd 
 |-  ( ph -> ( ( abs ` A ) / N ) <_ ( R / N ) )
81 68 80 eqbrtrrd 
 |-  ( ph -> ( abs ` ( A / N ) ) <_ ( R / N ) )
82 81 adantr 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( abs ` ( A / N ) ) <_ ( R / N ) )
83 60 simp3bi 
 |-  ( t e. ( 0 [,] 1 ) -> t <_ 1 )
84 83 adantl 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> t <_ 1 )
85 58 56 37 49 59 62 82 84 lemul12ad 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( abs ` ( A / N ) ) x. t ) <_ ( ( R / N ) x. 1 ) )
86 35 38 absmuld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( abs ` ( ( A / N ) x. t ) ) = ( ( abs ` ( A / N ) ) x. ( abs ` t ) ) )
87 37 62 absidd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( abs ` t ) = t )
88 87 oveq2d 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( abs ` ( A / N ) ) x. ( abs ` t ) ) = ( ( abs ` ( A / N ) ) x. t ) )
89 86 88 eqtr2d 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( abs ` ( A / N ) ) x. t ) = ( abs ` ( ( A / N ) x. t ) ) )
90 56 recnd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( R / N ) e. CC )
91 90 mulid1d 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( R / N ) x. 1 ) = ( R / N ) )
92 85 89 91 3brtr3d 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( abs ` ( ( A / N ) x. t ) ) <_ ( R / N ) )
93 2rp 
 |-  2 e. RR+
94 93 a1i 
 |-  ( ph -> 2 e. RR+ )
95 53 16 94 lemuldiv2d 
 |-  ( ph -> ( ( 2 x. R ) <_ N <-> R <_ ( N / 2 ) ) )
96 5 95 mpbid 
 |-  ( ph -> R <_ ( N / 2 ) )
97 2cnd 
 |-  ( ph -> 2 e. CC )
98 2ne0 
 |-  2 =/= 0
99 98 a1i 
 |-  ( ph -> 2 =/= 0 )
100 17 97 99 divrecd 
 |-  ( ph -> ( N / 2 ) = ( N x. ( 1 / 2 ) ) )
101 96 100 breqtrd 
 |-  ( ph -> R <_ ( N x. ( 1 / 2 ) ) )
102 9 rehalfcld 
 |-  ( ph -> ( 1 / 2 ) e. RR )
103 53 102 64 ledivmuld 
 |-  ( ph -> ( ( R / N ) <_ ( 1 / 2 ) <-> R <_ ( N x. ( 1 / 2 ) ) ) )
104 101 103 mpbird 
 |-  ( ph -> ( R / N ) <_ ( 1 / 2 ) )
105 104 adantr 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( R / N ) <_ ( 1 / 2 ) )
106 48 56 52 92 105 letrd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( abs ` ( ( A / N ) x. t ) ) <_ ( 1 / 2 ) )
107 halflt1 
 |-  ( 1 / 2 ) < 1
108 107 a1i 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( 1 / 2 ) < 1 )
109 48 52 49 106 108 lelttrd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( abs ` ( ( A / N ) x. t ) ) < 1 )
110 47 48 49 51 109 lelttrd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( abs ` ( Re ` ( ( A / N ) x. t ) ) ) < 1 )
111 45 49 absltd 
 |-  ( ( 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 ) ) )
112 110 111 mpbid 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( -u 1 < ( Re ` ( ( A / N ) x. t ) ) /\ ( Re ` ( ( A / N ) x. t ) ) < 1 ) )
113 112 simpld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> -u 1 < ( Re ` ( ( A / N ) x. t ) ) )
114 49 renegcld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> -u 1 e. RR )
115 114 45 posdifd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( -u 1 < ( Re ` ( ( A / N ) x. t ) ) <-> 0 < ( ( Re ` ( ( A / N ) x. t ) ) - -u 1 ) ) )
116 113 115 mpbid 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> 0 < ( ( Re ` ( ( A / N ) x. t ) ) - -u 1 ) )
117 46 40 subnegd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( Re ` ( ( A / N ) x. t ) ) - -u 1 ) = ( ( Re ` ( ( A / N ) x. t ) ) + 1 ) )
118 116 117 breqtrd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> 0 < ( ( Re ` ( ( A / N ) x. t ) ) + 1 ) )
119 39 40 readdd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( Re ` ( ( ( A / N ) x. t ) + 1 ) ) = ( ( Re ` ( ( A / N ) x. t ) ) + ( Re ` 1 ) ) )
120 re1 
 |-  ( Re ` 1 ) = 1
121 120 oveq2i 
 |-  ( ( Re ` ( ( A / N ) x. t ) ) + ( Re ` 1 ) ) = ( ( Re ` ( ( A / N ) x. t ) ) + 1 )
122 119 121 eqtrdi 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( Re ` ( ( ( A / N ) x. t ) + 1 ) ) = ( ( Re ` ( ( A / N ) x. t ) ) + 1 ) )
123 118 122 breqtrrd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> 0 < ( Re ` ( ( ( A / N ) x. t ) + 1 ) ) )
124 44 123 elrpd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( Re ` ( ( ( A / N ) x. t ) + 1 ) ) e. RR+ )
125 124 adantr 
 |-  ( ( ( ph /\ t e. ( 0 [,] 1 ) ) /\ ( ( ( A / N ) x. t ) + 1 ) e. RR ) -> ( Re ` ( ( ( A / N ) x. t ) + 1 ) ) e. RR+ )
126 43 125 eqeltrrd 
 |-  ( ( ( ph /\ t e. ( 0 [,] 1 ) ) /\ ( ( ( A / N ) x. t ) + 1 ) e. RR ) -> ( ( ( A / N ) x. t ) + 1 ) e. RR+ )
127 126 ex 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( ( ( A / N ) x. t ) + 1 ) e. RR -> ( ( ( A / N ) x. t ) + 1 ) e. RR+ ) )
128 30 ellogdm 
 |-  ( ( ( ( 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+ ) ) )
129 41 127 128 sylanbrc 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( ( A / N ) x. t ) + 1 ) e. ( CC \ ( -oo (,] 0 ) ) )
130 34 129 cofmpt 
 |-  ( 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 ) ) ) )
131 129 fvresd 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` ( ( ( A / N ) x. t ) + 1 ) ) = ( log ` ( ( ( A / N ) x. t ) + 1 ) ) )
132 131 mpteq2dva 
 |-  ( ph -> ( t e. ( 0 [,] 1 ) |-> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` ( ( ( A / N ) x. t ) + 1 ) ) ) = ( t e. ( 0 [,] 1 ) |-> ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) )
133 130 132 eqtrd 
 |-  ( 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 ) ) ) )
134 129 fmpttd 
 |-  ( ph -> ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) + 1 ) ) : ( 0 [,] 1 ) --> ( CC \ ( -oo (,] 0 ) ) )
135 difss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ CC
136 10 addcn 
 |-  + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
137 136 a1i 
 |-  ( ph -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
138 1cnd 
 |-  ( ph -> 1 e. CC )
139 cncfmptc 
 |-  ( ( 1 e. CC /\ ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( t e. ( 0 [,] 1 ) |-> 1 ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
140 138 23 24 139 syl3anc 
 |-  ( ph -> ( t e. ( 0 [,] 1 ) |-> 1 ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
141 10 137 29 140 cncfmpt2f 
 |-  ( ph -> ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) + 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
142 cncffvrn 
 |-  ( ( ( 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 ) ) ) )
143 135 141 142 sylancr 
 |-  ( 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 ) ) ) )
144 134 143 mpbird 
 |-  ( ph -> ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) + 1 ) ) e. ( ( 0 [,] 1 ) -cn-> ( CC \ ( -oo (,] 0 ) ) ) )
145 144 32 cncfco 
 |-  ( ph -> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) o. ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) + 1 ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
146 133 145 eqeltrrd 
 |-  ( ph -> ( t e. ( 0 [,] 1 ) |-> ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
147 10 12 29 146 cncfmpt2f 
 |-  ( ph -> ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
148 21 a1i 
 |-  ( ph -> RR C_ CC )
149 20 a1i 
 |-  ( ph -> ( 0 [,] 1 ) C_ RR )
150 30 logdmn0 
 |-  ( ( ( ( A / N ) x. t ) + 1 ) e. ( CC \ ( -oo (,] 0 ) ) -> ( ( ( A / N ) x. t ) + 1 ) =/= 0 )
151 129 150 syl 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( ( A / N ) x. t ) + 1 ) =/= 0 )
152 41 151 logcld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( log ` ( ( ( A / N ) x. t ) + 1 ) ) e. CC )
153 39 152 subcld 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) e. CC )
154 10 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
155 0re 
 |-  0 e. RR
156 iccntr 
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] 1 ) ) = ( 0 (,) 1 ) )
157 155 9 156 sylancr 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] 1 ) ) = ( 0 (,) 1 ) )
158 148 149 153 154 10 157 dvmptntr 
 |-  ( 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 ) ) ) ) ) )
159 reelprrecn 
 |-  RR e. { RR , CC }
160 159 a1i 
 |-  ( ph -> RR e. { RR , CC } )
161 15 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> A e. CC )
162 17 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> N e. CC )
163 18 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> N =/= 0 )
164 161 162 163 divcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( A / N ) e. CC )
165 ioossicc 
 |-  ( 0 (,) 1 ) C_ ( 0 [,] 1 )
166 165 sseli 
 |-  ( t e. ( 0 (,) 1 ) -> t e. ( 0 [,] 1 ) )
167 166 38 sylan2 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> t e. CC )
168 164 167 mulcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( A / N ) x. t ) e. CC )
169 15 adantr 
 |-  ( ( ph /\ t e. RR ) -> A e. CC )
170 17 adantr 
 |-  ( ( ph /\ t e. RR ) -> N e. CC )
171 18 adantr 
 |-  ( ( ph /\ t e. RR ) -> N =/= 0 )
172 169 170 171 divcld 
 |-  ( ( ph /\ t e. RR ) -> ( A / N ) e. CC )
173 148 sselda 
 |-  ( ( ph /\ t e. RR ) -> t e. CC )
174 172 173 mulcld 
 |-  ( ( ph /\ t e. RR ) -> ( ( A / N ) x. t ) e. CC )
175 1cnd 
 |-  ( ( ph /\ t e. RR ) -> 1 e. CC )
176 160 dvmptid 
 |-  ( ph -> ( RR _D ( t e. RR |-> t ) ) = ( t e. RR |-> 1 ) )
177 160 173 175 176 19 dvmptcmul 
 |-  ( ph -> ( RR _D ( t e. RR |-> ( ( A / N ) x. t ) ) ) = ( t e. RR |-> ( ( A / N ) x. 1 ) ) )
178 19 mulid1d 
 |-  ( ph -> ( ( A / N ) x. 1 ) = ( A / N ) )
179 178 mpteq2dv 
 |-  ( ph -> ( t e. RR |-> ( ( A / N ) x. 1 ) ) = ( t e. RR |-> ( A / N ) ) )
180 177 179 eqtrd 
 |-  ( ph -> ( RR _D ( t e. RR |-> ( ( A / N ) x. t ) ) ) = ( t e. RR |-> ( A / N ) ) )
181 165 149 sstrid 
 |-  ( ph -> ( 0 (,) 1 ) C_ RR )
182 retop 
 |-  ( topGen ` ran (,) ) e. Top
183 iooretop 
 |-  ( 0 (,) 1 ) e. ( topGen ` ran (,) )
184 isopn3i 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( 0 (,) 1 ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 (,) 1 ) ) = ( 0 (,) 1 ) )
185 182 183 184 mp2an 
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 (,) 1 ) ) = ( 0 (,) 1 )
186 185 a1i 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 (,) 1 ) ) = ( 0 (,) 1 ) )
187 160 174 172 180 181 154 10 186 dvmptres2 
 |-  ( ph -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( ( A / N ) x. t ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( A / N ) ) )
188 166 152 sylan2 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( log ` ( ( ( A / N ) x. t ) + 1 ) ) e. CC )
189 1cnd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> 1 e. CC )
190 168 189 addcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( ( A / N ) x. t ) + 1 ) e. CC )
191 166 151 sylan2 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( ( A / N ) x. t ) + 1 ) =/= 0 )
192 190 191 reccld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) e. CC )
193 192 164 mulcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) x. ( A / N ) ) e. CC )
194 cnelprrecn 
 |-  CC e. { RR , CC }
195 194 a1i 
 |-  ( ph -> CC e. { RR , CC } )
196 166 129 sylan2 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( ( A / N ) x. t ) + 1 ) e. ( CC \ ( -oo (,] 0 ) ) )
197 eldifi 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) -> y e. CC )
198 197 adantl 
 |-  ( ( ph /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> y e. CC )
199 30 logdmn0 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) -> y =/= 0 )
200 199 adantl 
 |-  ( ( ph /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> y =/= 0 )
201 198 200 logcld 
 |-  ( ( ph /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> ( log ` y ) e. CC )
202 198 200 reccld 
 |-  ( ( ph /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> ( 1 / y ) e. CC )
203 174 175 addcld 
 |-  ( ( ph /\ t e. RR ) -> ( ( ( A / N ) x. t ) + 1 ) e. CC )
204 0cnd 
 |-  ( ( ph /\ t e. RR ) -> 0 e. CC )
205 160 138 dvmptc 
 |-  ( ph -> ( RR _D ( t e. RR |-> 1 ) ) = ( t e. RR |-> 0 ) )
206 160 174 172 180 175 204 205 dvmptadd 
 |-  ( ph -> ( RR _D ( t e. RR |-> ( ( ( A / N ) x. t ) + 1 ) ) ) = ( t e. RR |-> ( ( A / N ) + 0 ) ) )
207 19 addid1d 
 |-  ( ph -> ( ( A / N ) + 0 ) = ( A / N ) )
208 207 mpteq2dv 
 |-  ( ph -> ( t e. RR |-> ( ( A / N ) + 0 ) ) = ( t e. RR |-> ( A / N ) ) )
209 206 208 eqtrd 
 |-  ( ph -> ( RR _D ( t e. RR |-> ( ( ( A / N ) x. t ) + 1 ) ) ) = ( t e. RR |-> ( A / N ) ) )
210 160 203 172 209 181 154 10 186 dvmptres2 
 |-  ( ph -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( ( ( A / N ) x. t ) + 1 ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( A / N ) ) )
211 34 feqmptd 
 |-  ( ph -> ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` y ) ) )
212 fvres 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) -> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` y ) = ( log ` y ) )
213 212 mpteq2ia 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) ` y ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) )
214 211 213 eqtr2di 
 |-  ( ph -> ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) ) = ( log |` ( CC \ ( -oo (,] 0 ) ) ) )
215 214 oveq2d 
 |-  ( ph -> ( CC _D ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) ) ) = ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) )
216 30 dvlog 
 |-  ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / y ) )
217 215 216 eqtrdi 
 |-  ( ph -> ( CC _D ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / y ) ) )
218 fveq2 
 |-  ( y = ( ( ( A / N ) x. t ) + 1 ) -> ( log ` y ) = ( log ` ( ( ( A / N ) x. t ) + 1 ) ) )
219 oveq2 
 |-  ( y = ( ( ( A / N ) x. t ) + 1 ) -> ( 1 / y ) = ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) )
220 160 195 196 164 201 202 210 217 218 219 dvmptco 
 |-  ( 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 ) ) ) )
221 160 168 164 187 188 193 220 dvmptsub 
 |-  ( 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 ) ) ) ) )
222 158 221 eqtrd 
 |-  ( 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 ) ) ) ) )
223 222 dmeqd 
 |-  ( 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 ) ) ) ) )
224 ovex 
 |-  ( ( A / N ) - ( ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) x. ( A / N ) ) ) e. _V
225 eqid 
 |-  ( 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 ) ) ) )
226 224 225 dmmpti 
 |-  dom ( t e. ( 0 (,) 1 ) |-> ( ( A / N ) - ( ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) x. ( A / N ) ) ) ) = ( 0 (,) 1 )
227 223 226 eqtrdi 
 |-  ( ph -> dom ( RR _D ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ) = ( 0 (,) 1 ) )
228 2re 
 |-  2 e. RR
229 228 a1i 
 |-  ( ph -> 2 e. RR )
230 229 53 remulcld 
 |-  ( ph -> ( 2 x. R ) e. RR )
231 1 nnrpd 
 |-  ( ph -> R e. RR+ )
232 53 231 ltaddrpd 
 |-  ( ph -> R < ( R + R ) )
233 53 recnd 
 |-  ( ph -> R e. CC )
234 233 2timesd 
 |-  ( ph -> ( 2 x. R ) = ( R + R ) )
235 232 234 breqtrrd 
 |-  ( ph -> R < ( 2 x. R ) )
236 53 230 16 235 5 ltletrd 
 |-  ( ph -> R < N )
237 difrp 
 |-  ( ( R e. RR /\ N e. RR ) -> ( R < N <-> ( N - R ) e. RR+ ) )
238 53 16 237 syl2anc 
 |-  ( ph -> ( R < N <-> ( N - R ) e. RR+ ) )
239 236 238 mpbid 
 |-  ( ph -> ( N - R ) e. RR+ )
240 239 rprecred 
 |-  ( ph -> ( 1 / ( N - R ) ) e. RR )
241 3 nnrecred 
 |-  ( ph -> ( 1 / N ) e. RR )
242 240 241 resubcld 
 |-  ( ph -> ( ( 1 / ( N - R ) ) - ( 1 / N ) ) e. RR )
243 53 242 remulcld 
 |-  ( ph -> ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) e. RR )
244 222 fveq1d 
 |-  ( 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 ) )
245 244 fveq2d 
 |-  ( 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 ) ) )
246 245 adantr 
 |-  ( ( 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 ) ) )
247 nfv 
 |-  F/ t ( ph /\ y e. ( 0 (,) 1 ) )
248 nfcv 
 |-  F/_ t abs
249 nffvmpt1 
 |-  F/_ t ( ( t e. ( 0 (,) 1 ) |-> ( ( A / N ) - ( ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) x. ( A / N ) ) ) ) ` y )
250 248 249 nffv 
 |-  F/_ t ( abs ` ( ( t e. ( 0 (,) 1 ) |-> ( ( A / N ) - ( ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) x. ( A / N ) ) ) ) ` y ) )
251 nfcv 
 |-  F/_ t <_
252 nfcv 
 |-  F/_ t ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) )
253 250 251 252 nfbr 
 |-  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 ) ) )
254 247 253 nfim 
 |-  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 ) ) ) )
255 eleq1w 
 |-  ( t = y -> ( t e. ( 0 (,) 1 ) <-> y e. ( 0 (,) 1 ) ) )
256 255 anbi2d 
 |-  ( t = y -> ( ( ph /\ t e. ( 0 (,) 1 ) ) <-> ( ph /\ y e. ( 0 (,) 1 ) ) ) )
257 2fveq3 
 |-  ( 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 ) ) )
258 257 breq1d 
 |-  ( 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 ) ) ) ) )
259 256 258 imbi12d 
 |-  ( 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 ) ) ) ) ) )
260 simpr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> t e. ( 0 (,) 1 ) )
261 225 fvmpt2 
 |-  ( ( 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 ) ) ) )
262 260 224 261 sylancl 
 |-  ( ( 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 ) ) ) )
263 262 fveq2d 
 |-  ( ( 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 ) ) ) ) )
264 164 189 192 subdid 
 |-  ( ( 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 ) ) ) ) )
265 164 mulid1d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( A / N ) x. 1 ) = ( A / N ) )
266 164 192 mulcomd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( A / N ) x. ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) = ( ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) x. ( A / N ) ) )
267 265 266 oveq12d 
 |-  ( ( 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 ) ) ) )
268 264 267 eqtr2d 
 |-  ( ( 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 ) ) ) ) )
269 268 fveq2d 
 |-  ( ( 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 ) ) ) ) ) )
270 161 162 163 absdivd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( A / N ) ) = ( ( abs ` A ) / ( abs ` N ) ) )
271 16 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> N e. RR )
272 65 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> 0 <_ N )
273 271 272 absidd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` N ) = N )
274 273 oveq2d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( abs ` A ) / ( abs ` N ) ) = ( ( abs ` A ) / N ) )
275 270 274 eqtrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( A / N ) ) = ( ( abs ` A ) / N ) )
276 275 oveq1d 
 |-  ( ( 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 ) ) ) ) ) )
277 189 192 subcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 - ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) e. CC )
278 164 277 absmuld 
 |-  ( ( 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 ) ) ) ) ) )
279 69 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` A ) e. RR )
280 279 recnd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` A ) e. CC )
281 277 abscld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( 1 - ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) ) e. RR )
282 281 recnd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( 1 - ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) ) e. CC )
283 280 282 162 163 div23d 
 |-  ( ( 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 ) ) ) ) ) )
284 276 278 283 3eqtr4d 
 |-  ( ( 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 ) )
285 263 269 284 3eqtrd 
 |-  ( ( 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 ) )
286 53 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> R e. RR )
287 240 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( N - R ) ) e. RR )
288 241 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / N ) e. RR )
289 287 288 resubcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( 1 / ( N - R ) ) - ( 1 / N ) ) e. RR )
290 271 289 remulcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) e. RR )
291 15 absge0d 
 |-  ( ph -> 0 <_ ( abs ` A ) )
292 291 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> 0 <_ ( abs ` A ) )
293 277 absge0d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> 0 <_ ( abs ` ( 1 - ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) ) )
294 79 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` A ) <_ R )
295 239 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N - R ) e. RR+ )
296 231 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> R e. RR+ )
297 295 296 rpdivcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N - R ) / R ) e. RR+ )
298 14 dmgmn0 
 |-  ( ph -> A =/= 0 )
299 298 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> A =/= 0 )
300 161 162 299 163 divne0d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( A / N ) =/= 0 )
301 eliooord 
 |-  ( t e. ( 0 (,) 1 ) -> ( 0 < t /\ t < 1 ) )
302 301 adantl 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 0 < t /\ t < 1 ) )
303 302 simpld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> 0 < t )
304 303 gt0ne0d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> t =/= 0 )
305 164 167 300 304 mulne0d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( A / N ) x. t ) =/= 0 )
306 168 305 reccld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( ( A / N ) x. t ) ) e. CC )
307 189 306 addcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) e. CC )
308 168 189 168 305 divdird 
 |-  ( ( 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 ) ) ) )
309 168 305 dividd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( ( A / N ) x. t ) / ( ( A / N ) x. t ) ) = 1 )
310 309 oveq1d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( ( ( A / N ) x. t ) / ( ( A / N ) x. t ) ) + ( 1 / ( ( A / N ) x. t ) ) ) = ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) )
311 308 310 eqtrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( ( ( A / N ) x. t ) + 1 ) / ( ( A / N ) x. t ) ) = ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) )
312 190 168 191 305 divne0d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( ( ( A / N ) x. t ) + 1 ) / ( ( A / N ) x. t ) ) =/= 0 )
313 311 312 eqnetrrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) =/= 0 )
314 307 313 absrpcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) e. RR+ )
315 1red 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> 1 e. RR )
316 0le1 
 |-  0 <_ 1
317 316 a1i 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> 0 <_ 1 )
318 297 rpred 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N - R ) / R ) e. RR )
319 306 negcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> -u ( 1 / ( ( A / N ) x. t ) ) e. CC )
320 319 abscld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) e. RR )
321 320 315 resubcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) - 1 ) e. RR )
322 307 abscld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) e. RR )
323 233 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> R e. CC )
324 296 rpne0d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> R =/= 0 )
325 162 323 323 324 divsubdird 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N - R ) / R ) = ( ( N / R ) - ( R / R ) ) )
326 323 324 dividd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( R / R ) = 1 )
327 326 oveq2d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N / R ) - ( R / R ) ) = ( ( N / R ) - 1 ) )
328 325 327 eqtrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N - R ) / R ) = ( ( N / R ) - 1 ) )
329 271 296 rerpdivcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N / R ) e. RR )
330 323 162 324 163 recdivd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( R / N ) ) = ( N / R ) )
331 166 92 sylan2 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( ( A / N ) x. t ) ) <_ ( R / N ) )
332 168 305 absrpcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( ( A / N ) x. t ) ) e. RR+ )
333 64 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> N e. RR+ )
334 296 333 rpdivcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( R / N ) e. RR+ )
335 332 334 lerecd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( abs ` ( ( A / N ) x. t ) ) <_ ( R / N ) <-> ( 1 / ( R / N ) ) <_ ( 1 / ( abs ` ( ( A / N ) x. t ) ) ) ) )
336 331 335 mpbid 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( R / N ) ) <_ ( 1 / ( abs ` ( ( A / N ) x. t ) ) ) )
337 330 336 eqbrtrrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N / R ) <_ ( 1 / ( abs ` ( ( A / N ) x. t ) ) ) )
338 306 absnegd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) = ( abs ` ( 1 / ( ( A / N ) x. t ) ) ) )
339 189 168 305 absdivd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( 1 / ( ( A / N ) x. t ) ) ) = ( ( abs ` 1 ) / ( abs ` ( ( A / N ) x. t ) ) ) )
340 abs1 
 |-  ( abs ` 1 ) = 1
341 340 oveq1i 
 |-  ( ( abs ` 1 ) / ( abs ` ( ( A / N ) x. t ) ) ) = ( 1 / ( abs ` ( ( A / N ) x. t ) ) )
342 339 341 eqtrdi 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( 1 / ( ( A / N ) x. t ) ) ) = ( 1 / ( abs ` ( ( A / N ) x. t ) ) ) )
343 338 342 eqtrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) = ( 1 / ( abs ` ( ( A / N ) x. t ) ) ) )
344 337 343 breqtrrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N / R ) <_ ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) )
345 329 320 315 344 lesub1dd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N / R ) - 1 ) <_ ( ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) - 1 ) )
346 328 345 eqbrtrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N - R ) / R ) <_ ( ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) - 1 ) )
347 340 oveq2i 
 |-  ( ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) - ( abs ` 1 ) ) = ( ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) - 1 )
348 319 189 abs2difd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) - ( abs ` 1 ) ) <_ ( abs ` ( -u ( 1 / ( ( A / N ) x. t ) ) - 1 ) ) )
349 347 348 eqbrtrrid 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) - 1 ) <_ ( abs ` ( -u ( 1 / ( ( A / N ) x. t ) ) - 1 ) ) )
350 189 306 addcomd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) = ( ( 1 / ( ( A / N ) x. t ) ) + 1 ) )
351 350 negeqd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> -u ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) = -u ( ( 1 / ( ( A / N ) x. t ) ) + 1 ) )
352 306 189 negdi2d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> -u ( ( 1 / ( ( A / N ) x. t ) ) + 1 ) = ( -u ( 1 / ( ( A / N ) x. t ) ) - 1 ) )
353 351 352 eqtrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> -u ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) = ( -u ( 1 / ( ( A / N ) x. t ) ) - 1 ) )
354 353 fveq2d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` -u ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) = ( abs ` ( -u ( 1 / ( ( A / N ) x. t ) ) - 1 ) ) )
355 307 absnegd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` -u ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) = ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) )
356 354 355 eqtr3d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( -u ( 1 / ( ( A / N ) x. t ) ) - 1 ) ) = ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) )
357 349 356 breqtrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( abs ` -u ( 1 / ( ( A / N ) x. t ) ) ) - 1 ) <_ ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) )
358 318 321 322 346 357 letrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N - R ) / R ) <_ ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) )
359 297 314 315 317 358 lediv2ad 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) ) <_ ( 1 / ( ( N - R ) / R ) ) )
360 17 233 subcld 
 |-  ( ph -> ( N - R ) e. CC )
361 360 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N - R ) e. CC )
362 53 236 gtned 
 |-  ( ph -> N =/= R )
363 17 233 362 subne0d 
 |-  ( ph -> ( N - R ) =/= 0 )
364 363 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N - R ) =/= 0 )
365 361 323 364 324 recdivd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( ( N - R ) / R ) ) = ( R / ( N - R ) ) )
366 162 323 nncand 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N - ( N - R ) ) = R )
367 366 oveq1d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N - ( N - R ) ) / ( N - R ) ) = ( R / ( N - R ) ) )
368 162 361 361 364 divsubdird 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N - ( N - R ) ) / ( N - R ) ) = ( ( N / ( N - R ) ) - ( ( N - R ) / ( N - R ) ) ) )
369 367 368 eqtr3d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( R / ( N - R ) ) = ( ( N / ( N - R ) ) - ( ( N - R ) / ( N - R ) ) ) )
370 361 364 dividd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N - R ) / ( N - R ) ) = 1 )
371 370 oveq2d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N / ( N - R ) ) - ( ( N - R ) / ( N - R ) ) ) = ( ( N / ( N - R ) ) - 1 ) )
372 365 369 371 3eqtrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( ( N - R ) / R ) ) = ( ( N / ( N - R ) ) - 1 ) )
373 359 372 breqtrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) ) <_ ( ( N / ( N - R ) ) - 1 ) )
374 190 189 190 191 divsubdird 
 |-  ( ( 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 ) ) ) )
375 168 189 pncand 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( ( ( A / N ) x. t ) + 1 ) - 1 ) = ( ( A / N ) x. t ) )
376 375 oveq1d 
 |-  ( ( 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 ) ) )
377 190 191 dividd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( ( ( A / N ) x. t ) + 1 ) / ( ( ( A / N ) x. t ) + 1 ) ) = 1 )
378 377 oveq1d 
 |-  ( ( 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 ) ) ) )
379 374 376 378 3eqtr3rd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 - ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) = ( ( ( A / N ) x. t ) / ( ( ( A / N ) x. t ) + 1 ) ) )
380 190 168 191 305 recdivd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( ( ( ( A / N ) x. t ) + 1 ) / ( ( A / N ) x. t ) ) ) = ( ( ( A / N ) x. t ) / ( ( ( A / N ) x. t ) + 1 ) ) )
381 311 oveq2d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( ( ( ( A / N ) x. t ) + 1 ) / ( ( A / N ) x. t ) ) ) = ( 1 / ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) )
382 379 380 381 3eqtr2d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 - ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) = ( 1 / ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) )
383 382 fveq2d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( 1 - ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) ) = ( abs ` ( 1 / ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) ) )
384 189 307 313 absdivd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( 1 / ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) ) = ( ( abs ` 1 ) / ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) ) )
385 340 oveq1i 
 |-  ( ( abs ` 1 ) / ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) ) = ( 1 / ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) )
386 384 385 eqtrdi 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( 1 / ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) ) = ( 1 / ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) ) )
387 383 386 eqtrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( 1 - ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) ) = ( 1 / ( abs ` ( 1 + ( 1 / ( ( A / N ) x. t ) ) ) ) ) )
388 360 363 reccld 
 |-  ( ph -> ( 1 / ( N - R ) ) e. CC )
389 388 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / ( N - R ) ) e. CC )
390 241 recnd 
 |-  ( ph -> ( 1 / N ) e. CC )
391 390 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 / N ) e. CC )
392 162 389 391 subdid 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) = ( ( N x. ( 1 / ( N - R ) ) ) - ( N x. ( 1 / N ) ) ) )
393 162 361 364 divrecd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N / ( N - R ) ) = ( N x. ( 1 / ( N - R ) ) ) )
394 393 eqcomd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N x. ( 1 / ( N - R ) ) ) = ( N / ( N - R ) ) )
395 162 163 recidd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N x. ( 1 / N ) ) = 1 )
396 394 395 oveq12d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( N x. ( 1 / ( N - R ) ) ) - ( N x. ( 1 / N ) ) ) = ( ( N / ( N - R ) ) - 1 ) )
397 392 396 eqtrd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) = ( ( N / ( N - R ) ) - 1 ) )
398 373 387 397 3brtr4d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( 1 - ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) ) <_ ( N x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) )
399 279 286 281 290 292 293 294 398 lemul12ad 
 |-  ( ( 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 ) ) ) ) )
400 242 recnd 
 |-  ( ph -> ( ( 1 / ( N - R ) ) - ( 1 / N ) ) e. CC )
401 400 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( 1 / ( N - R ) ) - ( 1 / N ) ) e. CC )
402 323 162 401 mul12d 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( R x. ( N x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) ) = ( N x. ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) ) )
403 399 402 breqtrd 
 |-  ( ( 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 ) ) ) ) )
404 279 281 remulcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( abs ` A ) x. ( abs ` ( 1 - ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) ) ) e. RR )
405 243 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) e. RR )
406 404 405 333 ledivmuld 
 |-  ( ( 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 ) ) ) ) ) )
407 403 406 mpbird 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( ( abs ` A ) x. ( abs ` ( 1 - ( 1 / ( ( ( A / N ) x. t ) + 1 ) ) ) ) ) / N ) <_ ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) )
408 285 407 eqbrtrd 
 |-  ( ( 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 ) ) ) )
409 254 259 408 chvarfv 
 |-  ( ( 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 ) ) ) )
410 246 409 eqbrtrd 
 |-  ( ( ph /\ y e. ( 0 (,) 1 ) ) -> ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ) ` y ) ) <_ ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) )
411 8 9 147 227 243 410 dvlip 
 |-  ( ( ph /\ ( 1 e. ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) ) ) -> ( abs ` ( ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 1 ) - ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 0 ) ) ) <_ ( ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) x. ( abs ` ( 1 - 0 ) ) ) )
412 6 7 411 mpanr12 
 |-  ( ph -> ( abs ` ( ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 1 ) - ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 0 ) ) ) <_ ( ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) x. ( abs ` ( 1 - 0 ) ) ) )
413 eqidd 
 |-  ( ph -> ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) = ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) )
414 oveq2 
 |-  ( t = 1 -> ( ( A / N ) x. t ) = ( ( A / N ) x. 1 ) )
415 414 178 sylan9eqr 
 |-  ( ( ph /\ t = 1 ) -> ( ( A / N ) x. t ) = ( A / N ) )
416 415 fvoveq1d 
 |-  ( ( ph /\ t = 1 ) -> ( log ` ( ( ( A / N ) x. t ) + 1 ) ) = ( log ` ( ( A / N ) + 1 ) ) )
417 415 416 oveq12d 
 |-  ( ( ph /\ t = 1 ) -> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) = ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) )
418 6 a1i 
 |-  ( ph -> 1 e. ( 0 [,] 1 ) )
419 ovexd 
 |-  ( ph -> ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) e. _V )
420 413 417 418 419 fvmptd 
 |-  ( ph -> ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 1 ) = ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) )
421 oveq2 
 |-  ( t = 0 -> ( ( A / N ) x. t ) = ( ( A / N ) x. 0 ) )
422 19 mul01d 
 |-  ( ph -> ( ( A / N ) x. 0 ) = 0 )
423 421 422 sylan9eqr 
 |-  ( ( ph /\ t = 0 ) -> ( ( A / N ) x. t ) = 0 )
424 423 oveq1d 
 |-  ( ( ph /\ t = 0 ) -> ( ( ( A / N ) x. t ) + 1 ) = ( 0 + 1 ) )
425 0p1e1 
 |-  ( 0 + 1 ) = 1
426 424 425 eqtrdi 
 |-  ( ( ph /\ t = 0 ) -> ( ( ( A / N ) x. t ) + 1 ) = 1 )
427 426 fveq2d 
 |-  ( ( ph /\ t = 0 ) -> ( log ` ( ( ( A / N ) x. t ) + 1 ) ) = ( log ` 1 ) )
428 log1 
 |-  ( log ` 1 ) = 0
429 427 428 eqtrdi 
 |-  ( ( ph /\ t = 0 ) -> ( log ` ( ( ( A / N ) x. t ) + 1 ) ) = 0 )
430 423 429 oveq12d 
 |-  ( ( ph /\ t = 0 ) -> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) = ( 0 - 0 ) )
431 0m0e0 
 |-  ( 0 - 0 ) = 0
432 430 431 eqtrdi 
 |-  ( ( ph /\ t = 0 ) -> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) = 0 )
433 7 a1i 
 |-  ( ph -> 0 e. ( 0 [,] 1 ) )
434 413 432 433 433 fvmptd 
 |-  ( ph -> ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 0 ) = 0 )
435 420 434 oveq12d 
 |-  ( ph -> ( ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 1 ) - ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 0 ) ) = ( ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) - 0 ) )
436 19 138 addcld 
 |-  ( ph -> ( ( A / N ) + 1 ) e. CC )
437 14 3 dmgmdivn0 
 |-  ( ph -> ( ( A / N ) + 1 ) =/= 0 )
438 436 437 logcld 
 |-  ( ph -> ( log ` ( ( A / N ) + 1 ) ) e. CC )
439 19 438 subcld 
 |-  ( ph -> ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) e. CC )
440 439 subid1d 
 |-  ( ph -> ( ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) - 0 ) = ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) )
441 435 440 eqtr2d 
 |-  ( ph -> ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) = ( ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 1 ) - ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 0 ) ) )
442 441 fveq2d 
 |-  ( ph -> ( abs ` ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) ) = ( abs ` ( ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 1 ) - ( ( t e. ( 0 [,] 1 ) |-> ( ( ( A / N ) x. t ) - ( log ` ( ( ( A / N ) x. t ) + 1 ) ) ) ) ` 0 ) ) ) )
443 1m0e1 
 |-  ( 1 - 0 ) = 1
444 443 fveq2i 
 |-  ( abs ` ( 1 - 0 ) ) = ( abs ` 1 )
445 444 340 eqtri 
 |-  ( abs ` ( 1 - 0 ) ) = 1
446 445 oveq2i 
 |-  ( ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) x. ( abs ` ( 1 - 0 ) ) ) = ( ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) x. 1 )
447 233 400 mulcld 
 |-  ( ph -> ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) e. CC )
448 447 mulid1d 
 |-  ( ph -> ( ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) x. 1 ) = ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) )
449 446 448 eqtr2id 
 |-  ( ph -> ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) = ( ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) x. ( abs ` ( 1 - 0 ) ) ) )
450 412 442 449 3brtr4d 
 |-  ( ph -> ( abs ` ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) ) <_ ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) )