Metamath Proof Explorer

Theorem aalioulem3

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 15-Nov-2014)

Ref Expression
Hypotheses aalioulem2.a 
|- N = ( deg ` F )
aalioulem2.b 
|- ( ph -> F e. ( Poly ` ZZ ) )
aalioulem2.c 
|- ( ph -> N e. NN )
aalioulem2.d 
|- ( ph -> A e. RR )
aalioulem3.e 
|- ( ph -> ( F ` A ) = 0 )
Assertion aalioulem3 
|- ( ph -> E. x e. RR+ A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( x x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )

Proof

Step Hyp Ref Expression
1 aalioulem2.a 
 |-  N = ( deg ` F )
2 aalioulem2.b 
 |-  ( ph -> F e. ( Poly ` ZZ ) )
3 aalioulem2.c 
 |-  ( ph -> N e. NN )
4 aalioulem2.d 
 |-  ( ph -> A e. RR )
5 aalioulem3.e 
 |-  ( ph -> ( F ` A ) = 0 )
6 1re 
 |-  1 e. RR
7 resubcl 
 |-  ( ( A e. RR /\ 1 e. RR ) -> ( A - 1 ) e. RR )
8 4 6 7 sylancl 
 |-  ( ph -> ( A - 1 ) e. RR )
9 peano2re 
 |-  ( A e. RR -> ( A + 1 ) e. RR )
10 4 9 syl 
 |-  ( ph -> ( A + 1 ) e. RR )
11 reelprrecn 
 |-  RR e. { RR , CC }
12 ssid 
 |-  CC C_ CC
13 fncpn 
 |-  ( CC C_ CC -> ( C^n ` CC ) Fn NN0 )
14 12 13 ax-mp 
 |-  ( C^n ` CC ) Fn NN0
15 1nn0 
 |-  1 e. NN0
16 fnfvelrn 
 |-  ( ( ( C^n ` CC ) Fn NN0 /\ 1 e. NN0 ) -> ( ( C^n ` CC ) ` 1 ) e. ran ( C^n ` CC ) )
17 14 15 16 mp2an 
 |-  ( ( C^n ` CC ) ` 1 ) e. ran ( C^n ` CC )
18 intss1 
 |-  ( ( ( C^n ` CC ) ` 1 ) e. ran ( C^n ` CC ) -> |^| ran ( C^n ` CC ) C_ ( ( C^n ` CC ) ` 1 ) )
19 17 18 ax-mp 
 |-  |^| ran ( C^n ` CC ) C_ ( ( C^n ` CC ) ` 1 )
20 plycpn 
 |-  ( F e. ( Poly ` ZZ ) -> F e. |^| ran ( C^n ` CC ) )
21 2 20 syl 
 |-  ( ph -> F e. |^| ran ( C^n ` CC ) )
22 19 21 sseldi 
 |-  ( ph -> F e. ( ( C^n ` CC ) ` 1 ) )
23 cpnres 
 |-  ( ( RR e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` 1 ) ) -> ( F |` RR ) e. ( ( C^n ` RR ) ` 1 ) )
24 11 22 23 sylancr 
 |-  ( ph -> ( F |` RR ) e. ( ( C^n ` RR ) ` 1 ) )
25 df-ima 
 |-  ( F " RR ) = ran ( F |` RR )
26 zssre 
 |-  ZZ C_ RR
27 ax-resscn 
 |-  RR C_ CC
28 plyss 
 |-  ( ( ZZ C_ RR /\ RR C_ CC ) -> ( Poly ` ZZ ) C_ ( Poly ` RR ) )
29 26 27 28 mp2an 
 |-  ( Poly ` ZZ ) C_ ( Poly ` RR )
30 29 2 sseldi 
 |-  ( ph -> F e. ( Poly ` RR ) )
31 plyreres 
 |-  ( F e. ( Poly ` RR ) -> ( F |` RR ) : RR --> RR )
32 30 31 syl 
 |-  ( ph -> ( F |` RR ) : RR --> RR )
33 32 frnd 
 |-  ( ph -> ran ( F |` RR ) C_ RR )
34 25 33 eqsstrid 
 |-  ( ph -> ( F " RR ) C_ RR )
35 iccssre 
 |-  ( ( ( A - 1 ) e. RR /\ ( A + 1 ) e. RR ) -> ( ( A - 1 ) [,] ( A + 1 ) ) C_ RR )
36 8 10 35 syl2anc 
 |-  ( ph -> ( ( A - 1 ) [,] ( A + 1 ) ) C_ RR )
37 36 27 sstrdi 
 |-  ( ph -> ( ( A - 1 ) [,] ( A + 1 ) ) C_ CC )
38 plyf 
 |-  ( F e. ( Poly ` ZZ ) -> F : CC --> CC )
39 2 38 syl 
 |-  ( ph -> F : CC --> CC )
40 39 fdmd 
 |-  ( ph -> dom F = CC )
41 37 40 sseqtrrd 
 |-  ( ph -> ( ( A - 1 ) [,] ( A + 1 ) ) C_ dom F )
42 8 10 24 34 41 c1lip3 
 |-  ( ph -> E. a e. RR A. b e. ( ( A - 1 ) [,] ( A + 1 ) ) A. c e. ( ( A - 1 ) [,] ( A + 1 ) ) ( abs ` ( ( F ` c ) - ( F ` b ) ) ) <_ ( a x. ( abs ` ( c - b ) ) ) )
43 simp2 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> r e. RR )
44 43 recnd 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> r e. CC )
45 4 adantr 
 |-  ( ( ph /\ a e. RR ) -> A e. RR )
46 45 3ad2ant1 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> A e. RR )
47 46 recnd 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> A e. CC )
48 44 47 abssubd 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( abs ` ( r - A ) ) = ( abs ` ( A - r ) ) )
49 simp3 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( abs ` ( A - r ) ) <_ 1 )
50 48 49 eqbrtrd 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( abs ` ( r - A ) ) <_ 1 )
51 1red 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> 1 e. RR )
52 elicc4abs 
 |-  ( ( A e. RR /\ 1 e. RR /\ r e. RR ) -> ( r e. ( ( A - 1 ) [,] ( A + 1 ) ) <-> ( abs ` ( r - A ) ) <_ 1 ) )
53 46 51 43 52 syl3anc 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( r e. ( ( A - 1 ) [,] ( A + 1 ) ) <-> ( abs ` ( r - A ) ) <_ 1 ) )
54 50 53 mpbird 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> r e. ( ( A - 1 ) [,] ( A + 1 ) ) )
55 4 recnd 
 |-  ( ph -> A e. CC )
56 55 subidd 
 |-  ( ph -> ( A - A ) = 0 )
57 56 fveq2d 
 |-  ( ph -> ( abs ` ( A - A ) ) = ( abs ` 0 ) )
58 abs0 
 |-  ( abs ` 0 ) = 0
59 0le1 
 |-  0 <_ 1
60 58 59 eqbrtri 
 |-  ( abs ` 0 ) <_ 1
61 57 60 eqbrtrdi 
 |-  ( ph -> ( abs ` ( A - A ) ) <_ 1 )
62 1red 
 |-  ( ph -> 1 e. RR )
63 elicc4abs 
 |-  ( ( A e. RR /\ 1 e. RR /\ A e. RR ) -> ( A e. ( ( A - 1 ) [,] ( A + 1 ) ) <-> ( abs ` ( A - A ) ) <_ 1 ) )
64 4 62 4 63 syl3anc 
 |-  ( ph -> ( A e. ( ( A - 1 ) [,] ( A + 1 ) ) <-> ( abs ` ( A - A ) ) <_ 1 ) )
65 61 64 mpbird 
 |-  ( ph -> A e. ( ( A - 1 ) [,] ( A + 1 ) ) )
66 65 adantr 
 |-  ( ( ph /\ a e. RR ) -> A e. ( ( A - 1 ) [,] ( A + 1 ) ) )
67 66 3ad2ant1 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> A e. ( ( A - 1 ) [,] ( A + 1 ) ) )
68 fveq2 
 |-  ( b = r -> ( F ` b ) = ( F ` r ) )
69 68 oveq2d 
 |-  ( b = r -> ( ( F ` c ) - ( F ` b ) ) = ( ( F ` c ) - ( F ` r ) ) )
70 69 fveq2d 
 |-  ( b = r -> ( abs ` ( ( F ` c ) - ( F ` b ) ) ) = ( abs ` ( ( F ` c ) - ( F ` r ) ) ) )
71 oveq2 
 |-  ( b = r -> ( c - b ) = ( c - r ) )
72 71 fveq2d 
 |-  ( b = r -> ( abs ` ( c - b ) ) = ( abs ` ( c - r ) ) )
73 72 oveq2d 
 |-  ( b = r -> ( a x. ( abs ` ( c - b ) ) ) = ( a x. ( abs ` ( c - r ) ) ) )
74 70 73 breq12d 
 |-  ( b = r -> ( ( abs ` ( ( F ` c ) - ( F ` b ) ) ) <_ ( a x. ( abs ` ( c - b ) ) ) <-> ( abs ` ( ( F ` c ) - ( F ` r ) ) ) <_ ( a x. ( abs ` ( c - r ) ) ) ) )
75 fveq2 
 |-  ( c = A -> ( F ` c ) = ( F ` A ) )
76 75 fvoveq1d 
 |-  ( c = A -> ( abs ` ( ( F ` c ) - ( F ` r ) ) ) = ( abs ` ( ( F ` A ) - ( F ` r ) ) ) )
77 fvoveq1 
 |-  ( c = A -> ( abs ` ( c - r ) ) = ( abs ` ( A - r ) ) )
78 77 oveq2d 
 |-  ( c = A -> ( a x. ( abs ` ( c - r ) ) ) = ( a x. ( abs ` ( A - r ) ) ) )
79 76 78 breq12d 
 |-  ( c = A -> ( ( abs ` ( ( F ` c ) - ( F ` r ) ) ) <_ ( a x. ( abs ` ( c - r ) ) ) <-> ( abs ` ( ( F ` A ) - ( F ` r ) ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) )
80 74 79 rspc2v 
 |-  ( ( r e. ( ( A - 1 ) [,] ( A + 1 ) ) /\ A e. ( ( A - 1 ) [,] ( A + 1 ) ) ) -> ( A. b e. ( ( A - 1 ) [,] ( A + 1 ) ) A. c e. ( ( A - 1 ) [,] ( A + 1 ) ) ( abs ` ( ( F ` c ) - ( F ` b ) ) ) <_ ( a x. ( abs ` ( c - b ) ) ) -> ( abs ` ( ( F ` A ) - ( F ` r ) ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) )
81 54 67 80 syl2anc 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( A. b e. ( ( A - 1 ) [,] ( A + 1 ) ) A. c e. ( ( A - 1 ) [,] ( A + 1 ) ) ( abs ` ( ( F ` c ) - ( F ` b ) ) ) <_ ( a x. ( abs ` ( c - b ) ) ) -> ( abs ` ( ( F ` A ) - ( F ` r ) ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) )
82 simp1l 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ph )
83 82 5 syl 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( F ` A ) = 0 )
84 0cn 
 |-  0 e. CC
85 83 84 eqeltrdi 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( F ` A ) e. CC )
86 39 adantr 
 |-  ( ( ph /\ a e. RR ) -> F : CC --> CC )
87 86 3ad2ant1 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> F : CC --> CC )
88 87 44 ffvelrnd 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( F ` r ) e. CC )
89 85 88 abssubd 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( abs ` ( ( F ` A ) - ( F ` r ) ) ) = ( abs ` ( ( F ` r ) - ( F ` A ) ) ) )
90 83 oveq2d 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( ( F ` r ) - ( F ` A ) ) = ( ( F ` r ) - 0 ) )
91 88 subid1d 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( ( F ` r ) - 0 ) = ( F ` r ) )
92 90 91 eqtrd 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( ( F ` r ) - ( F ` A ) ) = ( F ` r ) )
93 92 fveq2d 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( abs ` ( ( F ` r ) - ( F ` A ) ) ) = ( abs ` ( F ` r ) ) )
94 89 93 eqtrd 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( abs ` ( ( F ` A ) - ( F ` r ) ) ) = ( abs ` ( F ` r ) ) )
95 94 breq1d 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( ( abs ` ( ( F ` A ) - ( F ` r ) ) ) <_ ( a x. ( abs ` ( A - r ) ) ) <-> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) )
96 81 95 sylibd 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR /\ ( abs ` ( A - r ) ) <_ 1 ) -> ( A. b e. ( ( A - 1 ) [,] ( A + 1 ) ) A. c e. ( ( A - 1 ) [,] ( A + 1 ) ) ( abs ` ( ( F ` c ) - ( F ` b ) ) ) <_ ( a x. ( abs ` ( c - b ) ) ) -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) )
97 96 3exp 
 |-  ( ( ph /\ a e. RR ) -> ( r e. RR -> ( ( abs ` ( A - r ) ) <_ 1 -> ( A. b e. ( ( A - 1 ) [,] ( A + 1 ) ) A. c e. ( ( A - 1 ) [,] ( A + 1 ) ) ( abs ` ( ( F ` c ) - ( F ` b ) ) ) <_ ( a x. ( abs ` ( c - b ) ) ) -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) ) )
98 97 com34 
 |-  ( ( ph /\ a e. RR ) -> ( r e. RR -> ( A. b e. ( ( A - 1 ) [,] ( A + 1 ) ) A. c e. ( ( A - 1 ) [,] ( A + 1 ) ) ( abs ` ( ( F ` c ) - ( F ` b ) ) ) <_ ( a x. ( abs ` ( c - b ) ) ) -> ( ( abs ` ( A - r ) ) <_ 1 -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) ) )
99 98 com23 
 |-  ( ( ph /\ a e. RR ) -> ( A. b e. ( ( A - 1 ) [,] ( A + 1 ) ) A. c e. ( ( A - 1 ) [,] ( A + 1 ) ) ( abs ` ( ( F ` c ) - ( F ` b ) ) ) <_ ( a x. ( abs ` ( c - b ) ) ) -> ( r e. RR -> ( ( abs ` ( A - r ) ) <_ 1 -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) ) )
100 99 ralrimdv 
 |-  ( ( ph /\ a e. RR ) -> ( A. b e. ( ( A - 1 ) [,] ( A + 1 ) ) A. c e. ( ( A - 1 ) [,] ( A + 1 ) ) ( abs ` ( ( F ` c ) - ( F ` b ) ) ) <_ ( a x. ( abs ` ( c - b ) ) ) -> A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) )
101 100 reximdva 
 |-  ( ph -> ( E. a e. RR A. b e. ( ( A - 1 ) [,] ( A + 1 ) ) A. c e. ( ( A - 1 ) [,] ( A + 1 ) ) ( abs ` ( ( F ` c ) - ( F ` b ) ) ) <_ ( a x. ( abs ` ( c - b ) ) ) -> E. a e. RR A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) )
102 42 101 mpd 
 |-  ( ph -> E. a e. RR A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) )
103 1rp 
 |-  1 e. RR+
104 103 a1i 
 |-  ( ( ( ph /\ a e. RR ) /\ a = 0 ) -> 1 e. RR+ )
105 recn 
 |-  ( a e. RR -> a e. CC )
106 105 adantl 
 |-  ( ( ph /\ a e. RR ) -> a e. CC )
107 neqne 
 |-  ( -. a = 0 -> a =/= 0 )
108 absrpcl 
 |-  ( ( a e. CC /\ a =/= 0 ) -> ( abs ` a ) e. RR+ )
109 106 107 108 syl2an 
 |-  ( ( ( ph /\ a e. RR ) /\ -. a = 0 ) -> ( abs ` a ) e. RR+ )
110 109 rpreccld 
 |-  ( ( ( ph /\ a e. RR ) /\ -. a = 0 ) -> ( 1 / ( abs ` a ) ) e. RR+ )
111 104 110 ifclda 
 |-  ( ( ph /\ a e. RR ) -> if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) e. RR+ )
112 eqid 
 |-  if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) )
113 eqif 
 |-  ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) <-> ( ( a = 0 /\ if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = 1 ) \/ ( -. a = 0 /\ if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = ( 1 / ( abs ` a ) ) ) ) )
114 112 113 mpbi 
 |-  ( ( a = 0 /\ if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = 1 ) \/ ( -. a = 0 /\ if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = ( 1 / ( abs ` a ) ) ) )
115 simplrr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) )
116 oveq1 
 |-  ( a = 0 -> ( a x. ( abs ` ( A - r ) ) ) = ( 0 x. ( abs ` ( A - r ) ) ) )
117 116 adantl 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( a x. ( abs ` ( A - r ) ) ) = ( 0 x. ( abs ` ( A - r ) ) ) )
118 4 ad2antrr 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> A e. RR )
119 simprl 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> r e. RR )
120 118 119 resubcld 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( A - r ) e. RR )
121 120 recnd 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( A - r ) e. CC )
122 121 abscld 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( abs ` ( A - r ) ) e. RR )
123 122 recnd 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( abs ` ( A - r ) ) e. CC )
124 123 adantr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( abs ` ( A - r ) ) e. CC )
125 124 mul02d 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( 0 x. ( abs ` ( A - r ) ) ) = 0 )
126 117 125 eqtrd 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( a x. ( abs ` ( A - r ) ) ) = 0 )
127 115 126 breqtrd 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( abs ` ( F ` r ) ) <_ 0 )
128 39 ad2antrr 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> F : CC --> CC )
129 119 recnd 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> r e. CC )
130 128 129 ffvelrnd 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( F ` r ) e. CC )
131 130 adantr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( F ` r ) e. CC )
132 131 absge0d 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> 0 <_ ( abs ` ( F ` r ) ) )
133 130 abscld 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( abs ` ( F ` r ) ) e. RR )
134 133 adantr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( abs ` ( F ` r ) ) e. RR )
135 0re 
 |-  0 e. RR
136 letri3 
 |-  ( ( ( abs ` ( F ` r ) ) e. RR /\ 0 e. RR ) -> ( ( abs ` ( F ` r ) ) = 0 <-> ( ( abs ` ( F ` r ) ) <_ 0 /\ 0 <_ ( abs ` ( F ` r ) ) ) ) )
137 134 135 136 sylancl 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( ( abs ` ( F ` r ) ) = 0 <-> ( ( abs ` ( F ` r ) ) <_ 0 /\ 0 <_ ( abs ` ( F ` r ) ) ) ) )
138 127 132 137 mpbir2and 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( abs ` ( F ` r ) ) = 0 )
139 138 oveq2d 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( 1 x. ( abs ` ( F ` r ) ) ) = ( 1 x. 0 ) )
140 ax-1cn 
 |-  1 e. CC
141 140 mul01i 
 |-  ( 1 x. 0 ) = 0
142 139 141 eqtrdi 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( 1 x. ( abs ` ( F ` r ) ) ) = 0 )
143 121 adantr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( A - r ) e. CC )
144 143 absge0d 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> 0 <_ ( abs ` ( A - r ) ) )
145 142 144 eqbrtrd 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( 1 x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) )
146 oveq1 
 |-  ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = 1 -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) = ( 1 x. ( abs ` ( F ` r ) ) ) )
147 146 breq1d 
 |-  ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = 1 -> ( ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) <-> ( 1 x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )
148 145 147 syl5ibrcom 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a = 0 ) -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = 1 -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )
149 148 expimpd 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( ( a = 0 /\ if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = 1 ) -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )
150 df-ne 
 |-  ( a =/= 0 <-> -. a = 0 )
151 133 adantr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> ( abs ` ( F ` r ) ) e. RR )
152 151 recnd 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> ( abs ` ( F ` r ) ) e. CC )
153 simpllr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> a e. RR )
154 153 recnd 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> a e. CC )
155 154 108 sylancom 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> ( abs ` a ) e. RR+ )
156 155 rpcnne0d 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> ( ( abs ` a ) e. CC /\ ( abs ` a ) =/= 0 ) )
157 divrec2 
 |-  ( ( ( abs ` ( F ` r ) ) e. CC /\ ( abs ` a ) e. CC /\ ( abs ` a ) =/= 0 ) -> ( ( abs ` ( F ` r ) ) / ( abs ` a ) ) = ( ( 1 / ( abs ` a ) ) x. ( abs ` ( F ` r ) ) ) )
158 157 3expb 
 |-  ( ( ( abs ` ( F ` r ) ) e. CC /\ ( ( abs ` a ) e. CC /\ ( abs ` a ) =/= 0 ) ) -> ( ( abs ` ( F ` r ) ) / ( abs ` a ) ) = ( ( 1 / ( abs ` a ) ) x. ( abs ` ( F ` r ) ) ) )
159 152 156 158 syl2anc 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> ( ( abs ` ( F ` r ) ) / ( abs ` a ) ) = ( ( 1 / ( abs ` a ) ) x. ( abs ` ( F ` r ) ) ) )
160 simplr 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> a e. RR )
161 160 122 remulcld 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( a x. ( abs ` ( A - r ) ) ) e. RR )
162 160 recnd 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> a e. CC )
163 162 abscld 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( abs ` a ) e. RR )
164 163 122 remulcld 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( ( abs ` a ) x. ( abs ` ( A - r ) ) ) e. RR )
165 simprr 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) )
166 121 absge0d 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> 0 <_ ( abs ` ( A - r ) ) )
167 leabs 
 |-  ( a e. RR -> a <_ ( abs ` a ) )
168 167 ad2antlr 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> a <_ ( abs ` a ) )
169 160 163 122 166 168 lemul1ad 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( a x. ( abs ` ( A - r ) ) ) <_ ( ( abs ` a ) x. ( abs ` ( A - r ) ) ) )
170 133 161 164 165 169 letrd 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( abs ` ( F ` r ) ) <_ ( ( abs ` a ) x. ( abs ` ( A - r ) ) ) )
171 170 adantr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> ( abs ` ( F ` r ) ) <_ ( ( abs ` a ) x. ( abs ` ( A - r ) ) ) )
172 122 adantr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> ( abs ` ( A - r ) ) e. RR )
173 151 172 155 ledivmuld 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> ( ( ( abs ` ( F ` r ) ) / ( abs ` a ) ) <_ ( abs ` ( A - r ) ) <-> ( abs ` ( F ` r ) ) <_ ( ( abs ` a ) x. ( abs ` ( A - r ) ) ) ) )
174 171 173 mpbird 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> ( ( abs ` ( F ` r ) ) / ( abs ` a ) ) <_ ( abs ` ( A - r ) ) )
175 159 174 eqbrtrrd 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ a =/= 0 ) -> ( ( 1 / ( abs ` a ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) )
176 150 175 sylan2br 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ -. a = 0 ) -> ( ( 1 / ( abs ` a ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) )
177 oveq1 
 |-  ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = ( 1 / ( abs ` a ) ) -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) = ( ( 1 / ( abs ` a ) ) x. ( abs ` ( F ` r ) ) ) )
178 177 breq1d 
 |-  ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = ( 1 / ( abs ` a ) ) -> ( ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) <-> ( ( 1 / ( abs ` a ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )
179 176 178 syl5ibrcom 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) /\ -. a = 0 ) -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = ( 1 / ( abs ` a ) ) -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )
180 179 expimpd 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( ( -. a = 0 /\ if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = ( 1 / ( abs ` a ) ) ) -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )
181 149 180 jaod 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( ( ( a = 0 /\ if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = 1 ) \/ ( -. a = 0 /\ if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) = ( 1 / ( abs ` a ) ) ) ) -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )
182 114 181 mpi 
 |-  ( ( ( ph /\ a e. RR ) /\ ( r e. RR /\ ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) ) -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) )
183 182 expr 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR ) -> ( ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )
184 183 imim2d 
 |-  ( ( ( ph /\ a e. RR ) /\ r e. RR ) -> ( ( ( abs ` ( A - r ) ) <_ 1 -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) -> ( ( abs ` ( A - r ) ) <_ 1 -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) ) )
185 184 ralimdva 
 |-  ( ( ph /\ a e. RR ) -> ( A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) -> A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) ) )
186 oveq1 
 |-  ( x = if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) -> ( x x. ( abs ` ( F ` r ) ) ) = ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) )
187 186 breq1d 
 |-  ( x = if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) -> ( ( x x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) <-> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )
188 187 imbi2d 
 |-  ( x = if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) -> ( ( ( abs ` ( A - r ) ) <_ 1 -> ( x x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) <-> ( ( abs ` ( A - r ) ) <_ 1 -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) ) )
189 188 ralbidv 
 |-  ( x = if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) -> ( A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( x x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) <-> A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) ) )
190 189 rspcev 
 |-  ( ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) e. RR+ /\ A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( if ( a = 0 , 1 , ( 1 / ( abs ` a ) ) ) x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) ) -> E. x e. RR+ A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( x x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )
191 111 185 190 syl6an 
 |-  ( ( ph /\ a e. RR ) -> ( A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) -> E. x e. RR+ A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( x x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) ) )
192 191 rexlimdva 
 |-  ( ph -> ( E. a e. RR A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( abs ` ( F ` r ) ) <_ ( a x. ( abs ` ( A - r ) ) ) ) -> E. x e. RR+ A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( x x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) ) )
193 102 192 mpd 
 |-  ( ph -> E. x e. RR+ A. r e. RR ( ( abs ` ( A - r ) ) <_ 1 -> ( x x. ( abs ` ( F ` r ) ) ) <_ ( abs ` ( A - r ) ) ) )