Metamath Proof Explorer

Theorem ftalem2

Description: Lemma for fta . There exists some r such that F has magnitude greater than F ( 0 ) outside the closed ball B(0,r). (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses ftalem.1 
|- A = ( coeff ` F )
ftalem.2 
|- N = ( deg ` F )
ftalem.3 
|- ( ph -> F e. ( Poly ` S ) )
ftalem.4 
|- ( ph -> N e. NN )
ftalem2.5 
|- U = if ( if ( 1 <_ s , s , 1 ) <_ T , T , if ( 1 <_ s , s , 1 ) )
ftalem2.6 
|- T = ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( A ` N ) ) / 2 ) )
Assertion ftalem2 
|- ( ph -> E. r e. RR+ A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 ftalem.1 
 |-  A = ( coeff ` F )
2 ftalem.2 
 |-  N = ( deg ` F )
3 ftalem.3 
 |-  ( ph -> F e. ( Poly ` S ) )
4 ftalem.4 
 |-  ( ph -> N e. NN )
5 ftalem2.5 
 |-  U = if ( if ( 1 <_ s , s , 1 ) <_ T , T , if ( 1 <_ s , s , 1 ) )
6 ftalem2.6 
 |-  T = ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( A ` N ) ) / 2 ) )
7 1 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
8 3 7 syl 
 |-  ( ph -> A : NN0 --> CC )
9 4 nnnn0d 
 |-  ( ph -> N e. NN0 )
10 8 9 ffvelrnd 
 |-  ( ph -> ( A ` N ) e. CC )
11 4 nnne0d 
 |-  ( ph -> N =/= 0 )
12 2 1 dgreq0 
 |-  ( F e. ( Poly ` S ) -> ( F = 0p <-> ( A ` N ) = 0 ) )
13 fveq2 
 |-  ( F = 0p -> ( deg ` F ) = ( deg ` 0p ) )
14 dgr0 
 |-  ( deg ` 0p ) = 0
15 13 14 eqtrdi 
 |-  ( F = 0p -> ( deg ` F ) = 0 )
16 2 15 eqtrid 
 |-  ( F = 0p -> N = 0 )
17 12 16 syl6bir 
 |-  ( F e. ( Poly ` S ) -> ( ( A ` N ) = 0 -> N = 0 ) )
18 3 17 syl 
 |-  ( ph -> ( ( A ` N ) = 0 -> N = 0 ) )
19 18 necon3d 
 |-  ( ph -> ( N =/= 0 -> ( A ` N ) =/= 0 ) )
20 11 19 mpd 
 |-  ( ph -> ( A ` N ) =/= 0 )
21 10 20 absrpcld 
 |-  ( ph -> ( abs ` ( A ` N ) ) e. RR+ )
22 21 rphalfcld 
 |-  ( ph -> ( ( abs ` ( A ` N ) ) / 2 ) e. RR+ )
23 2fveq3 
 |-  ( n = k -> ( abs ` ( A ` n ) ) = ( abs ` ( A ` k ) ) )
24 23 cbvsumv 
 |-  sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` n ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) )
25 24 oveq1i 
 |-  ( sum_ n e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` n ) ) / ( ( abs ` ( A ` N ) ) / 2 ) ) = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) / ( ( abs ` ( A ` N ) ) / 2 ) )
26 1 2 3 4 22 25 ftalem1 
 |-  ( ph -> E. s e. RR A. x e. CC ( s < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) ) )
27 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
28 3 27 syl 
 |-  ( ph -> F : CC --> CC )
29 0cn 
 |-  0 e. CC
30 ffvelrn 
 |-  ( ( F : CC --> CC /\ 0 e. CC ) -> ( F ` 0 ) e. CC )
31 28 29 30 sylancl 
 |-  ( ph -> ( F ` 0 ) e. CC )
32 31 abscld 
 |-  ( ph -> ( abs ` ( F ` 0 ) ) e. RR )
33 32 22 rerpdivcld 
 |-  ( ph -> ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( A ` N ) ) / 2 ) ) e. RR )
34 6 33 eqeltrid 
 |-  ( ph -> T e. RR )
35 34 adantr 
 |-  ( ( ph /\ s e. RR ) -> T e. RR )
36 simpr 
 |-  ( ( ph /\ s e. RR ) -> s e. RR )
37 1re 
 |-  1 e. RR
38 ifcl 
 |-  ( ( s e. RR /\ 1 e. RR ) -> if ( 1 <_ s , s , 1 ) e. RR )
39 36 37 38 sylancl 
 |-  ( ( ph /\ s e. RR ) -> if ( 1 <_ s , s , 1 ) e. RR )
40 35 39 ifcld 
 |-  ( ( ph /\ s e. RR ) -> if ( if ( 1 <_ s , s , 1 ) <_ T , T , if ( 1 <_ s , s , 1 ) ) e. RR )
41 5 40 eqeltrid 
 |-  ( ( ph /\ s e. RR ) -> U e. RR )
42 0red 
 |-  ( ( ph /\ s e. RR ) -> 0 e. RR )
43 1red 
 |-  ( ( ph /\ s e. RR ) -> 1 e. RR )
44 0lt1 
 |-  0 < 1
45 44 a1i 
 |-  ( ( ph /\ s e. RR ) -> 0 < 1 )
46 max1 
 |-  ( ( 1 e. RR /\ s e. RR ) -> 1 <_ if ( 1 <_ s , s , 1 ) )
47 37 36 46 sylancr 
 |-  ( ( ph /\ s e. RR ) -> 1 <_ if ( 1 <_ s , s , 1 ) )
48 max1 
 |-  ( ( if ( 1 <_ s , s , 1 ) e. RR /\ T e. RR ) -> if ( 1 <_ s , s , 1 ) <_ if ( if ( 1 <_ s , s , 1 ) <_ T , T , if ( 1 <_ s , s , 1 ) ) )
49 39 35 48 syl2anc 
 |-  ( ( ph /\ s e. RR ) -> if ( 1 <_ s , s , 1 ) <_ if ( if ( 1 <_ s , s , 1 ) <_ T , T , if ( 1 <_ s , s , 1 ) ) )
50 49 5 breqtrrdi 
 |-  ( ( ph /\ s e. RR ) -> if ( 1 <_ s , s , 1 ) <_ U )
51 43 39 41 47 50 letrd 
 |-  ( ( ph /\ s e. RR ) -> 1 <_ U )
52 42 43 41 45 51 ltletrd 
 |-  ( ( ph /\ s e. RR ) -> 0 < U )
53 41 52 elrpd 
 |-  ( ( ph /\ s e. RR ) -> U e. RR+ )
54 max2 
 |-  ( ( 1 e. RR /\ s e. RR ) -> s <_ if ( 1 <_ s , s , 1 ) )
55 37 36 54 sylancr 
 |-  ( ( ph /\ s e. RR ) -> s <_ if ( 1 <_ s , s , 1 ) )
56 36 39 41 55 50 letrd 
 |-  ( ( ph /\ s e. RR ) -> s <_ U )
57 56 adantr 
 |-  ( ( ( ph /\ s e. RR ) /\ x e. CC ) -> s <_ U )
58 abscl 
 |-  ( x e. CC -> ( abs ` x ) e. RR )
59 lelttr 
 |-  ( ( s e. RR /\ U e. RR /\ ( abs ` x ) e. RR ) -> ( ( s <_ U /\ U < ( abs ` x ) ) -> s < ( abs ` x ) ) )
60 36 41 58 59 syl2an3an 
 |-  ( ( ( ph /\ s e. RR ) /\ x e. CC ) -> ( ( s <_ U /\ U < ( abs ` x ) ) -> s < ( abs ` x ) ) )
61 57 60 mpand 
 |-  ( ( ( ph /\ s e. RR ) /\ x e. CC ) -> ( U < ( abs ` x ) -> s < ( abs ` x ) ) )
62 61 imim1d 
 |-  ( ( ( ph /\ s e. RR ) /\ x e. CC ) -> ( ( s < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) ) -> ( U < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) ) ) )
63 28 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> F : CC --> CC )
64 simprl 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> x e. CC )
65 63 64 ffvelrnd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( F ` x ) e. CC )
66 10 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( A ` N ) e. CC )
67 9 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> N e. NN0 )
68 64 67 expcld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( x ^ N ) e. CC )
69 66 68 mulcld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( A ` N ) x. ( x ^ N ) ) e. CC )
70 65 69 subcld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) e. CC )
71 70 abscld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) e. RR )
72 69 abscld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) e. RR )
73 72 rehalfcld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) e. RR )
74 71 73 72 ltsub2d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) <-> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) ) )
75 66 68 absmuld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) = ( ( abs ` ( A ` N ) ) x. ( abs ` ( x ^ N ) ) ) )
76 64 67 absexpd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( x ^ N ) ) = ( ( abs ` x ) ^ N ) )
77 76 oveq2d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( A ` N ) ) x. ( abs ` ( x ^ N ) ) ) = ( ( abs ` ( A ` N ) ) x. ( ( abs ` x ) ^ N ) ) )
78 75 77 eqtrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) = ( ( abs ` ( A ` N ) ) x. ( ( abs ` x ) ^ N ) ) )
79 78 oveq1d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) = ( ( ( abs ` ( A ` N ) ) x. ( ( abs ` x ) ^ N ) ) / 2 ) )
80 66 abscld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( A ` N ) ) e. RR )
81 80 recnd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( A ` N ) ) e. CC )
82 58 ad2antrl 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` x ) e. RR )
83 82 67 reexpcld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` x ) ^ N ) e. RR )
84 83 recnd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` x ) ^ N ) e. CC )
85 2cnd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> 2 e. CC )
86 2ne0 
 |-  2 =/= 0
87 86 a1i 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> 2 =/= 0 )
88 81 84 85 87 div23d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( abs ` ( A ` N ) ) x. ( ( abs ` x ) ^ N ) ) / 2 ) = ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) )
89 79 88 eqtrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) = ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) )
90 89 breq2d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) <-> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) ) )
91 72 recnd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) e. CC )
92 91 2halvesd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) + ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) ) = ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) )
93 92 oveq1d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) + ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) ) - ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) ) = ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) ) )
94 73 recnd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) e. CC )
95 94 94 pncand 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) + ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) ) - ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) ) = ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) )
96 93 95 eqtr3d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) ) = ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) )
97 96 breq1d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) <-> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) ) )
98 74 90 97 3bitr3d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) <-> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) ) )
99 69 65 subcld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( A ` N ) x. ( x ^ N ) ) - ( F ` x ) ) e. CC )
100 69 99 abs2difd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( ( A ` N ) x. ( x ^ N ) ) - ( F ` x ) ) ) ) <_ ( abs ` ( ( ( A ` N ) x. ( x ^ N ) ) - ( ( ( A ` N ) x. ( x ^ N ) ) - ( F ` x ) ) ) ) )
101 69 65 abssubd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( ( ( A ` N ) x. ( x ^ N ) ) - ( F ` x ) ) ) = ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) )
102 101 oveq2d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( ( A ` N ) x. ( x ^ N ) ) - ( F ` x ) ) ) ) = ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) )
103 69 65 nncand 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( A ` N ) x. ( x ^ N ) ) - ( ( ( A ` N ) x. ( x ^ N ) ) - ( F ` x ) ) ) = ( F ` x ) )
104 103 fveq2d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( ( ( A ` N ) x. ( x ^ N ) ) - ( ( ( A ` N ) x. ( x ^ N ) ) - ( F ` x ) ) ) ) = ( abs ` ( F ` x ) ) )
105 100 102 104 3brtr3d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) <_ ( abs ` ( F ` x ) ) )
106 72 71 resubcld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) e. RR )
107 65 abscld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( F ` x ) ) e. RR )
108 ltletr 
 |-  ( ( ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) e. RR /\ ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) e. RR /\ ( abs ` ( F ` x ) ) e. RR ) -> ( ( ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) /\ ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) <_ ( abs ` ( F ` x ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( abs ` ( F ` x ) ) ) )
109 73 106 107 108 syl3anc 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) /\ ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) <_ ( abs ` ( F ` x ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( abs ` ( F ` x ) ) ) )
110 105 109 mpan2d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) - ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( abs ` ( F ` x ) ) ) )
111 98 110 sylbid 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) -> ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( abs ` ( F ` x ) ) ) )
112 32 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( F ` 0 ) ) e. RR )
113 22 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( A ` N ) ) / 2 ) e. RR+ )
114 113 rpred 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( A ` N ) ) / 2 ) e. RR )
115 114 82 remulcld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( abs ` x ) ) e. RR )
116 89 73 eqeltrrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) e. RR )
117 35 adantr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> T e. RR )
118 41 adantr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> U e. RR )
119 max2 
 |-  ( ( if ( 1 <_ s , s , 1 ) e. RR /\ T e. RR ) -> T <_ if ( if ( 1 <_ s , s , 1 ) <_ T , T , if ( 1 <_ s , s , 1 ) ) )
120 39 35 119 syl2anc 
 |-  ( ( ph /\ s e. RR ) -> T <_ if ( if ( 1 <_ s , s , 1 ) <_ T , T , if ( 1 <_ s , s , 1 ) ) )
121 120 5 breqtrrdi 
 |-  ( ( ph /\ s e. RR ) -> T <_ U )
122 121 adantr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> T <_ U )
123 simprr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> U < ( abs ` x ) )
124 117 118 82 122 123 lelttrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> T < ( abs ` x ) )
125 6 124 eqbrtrrid 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( A ` N ) ) / 2 ) ) < ( abs ` x ) )
126 112 82 113 ltdivmuld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( A ` N ) ) / 2 ) ) < ( abs ` x ) <-> ( abs ` ( F ` 0 ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( abs ` x ) ) ) )
127 125 126 mpbid 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( F ` 0 ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( abs ` x ) ) )
128 82 recnd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` x ) e. CC )
129 128 exp1d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` x ) ^ 1 ) = ( abs ` x ) )
130 1red 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> 1 e. RR )
131 51 adantr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> 1 <_ U )
132 130 118 82 131 123 lelttrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> 1 < ( abs ` x ) )
133 130 82 132 ltled 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> 1 <_ ( abs ` x ) )
134 4 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> N e. NN )
135 nnuz 
 |-  NN = ( ZZ>= ` 1 )
136 134 135 eleqtrdi 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> N e. ( ZZ>= ` 1 ) )
137 82 133 136 leexp2ad 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` x ) ^ 1 ) <_ ( ( abs ` x ) ^ N ) )
138 129 137 eqbrtrrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` x ) <_ ( ( abs ` x ) ^ N ) )
139 82 83 113 lemul2d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` x ) <_ ( ( abs ` x ) ^ N ) <-> ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( abs ` x ) ) <_ ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) ) )
140 138 139 mpbid 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( abs ` x ) ) <_ ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) )
141 112 115 116 127 140 ltletrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( F ` 0 ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) )
142 141 89 breqtrrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( abs ` ( F ` 0 ) ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) )
143 lttr 
 |-  ( ( ( abs ` ( F ` 0 ) ) e. RR /\ ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) e. RR /\ ( abs ` ( F ` x ) ) e. RR ) -> ( ( ( abs ` ( F ` 0 ) ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) /\ ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( abs ` ( F ` x ) ) ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
144 112 73 107 143 syl3anc 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( abs ` ( F ` 0 ) ) < ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) /\ ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( abs ` ( F ` x ) ) ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
145 142 144 mpand 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( ( abs ` ( ( A ` N ) x. ( x ^ N ) ) ) / 2 ) < ( abs ` ( F ` x ) ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
146 111 145 syld 
 |-  ( ( ( ph /\ s e. RR ) /\ ( x e. CC /\ U < ( abs ` x ) ) ) -> ( ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
147 146 expr 
 |-  ( ( ( ph /\ s e. RR ) /\ x e. CC ) -> ( U < ( abs ` x ) -> ( ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) ) )
148 147 a2d 
 |-  ( ( ( ph /\ s e. RR ) /\ x e. CC ) -> ( ( U < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) ) -> ( U < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) ) )
149 62 148 syld 
 |-  ( ( ( ph /\ s e. RR ) /\ x e. CC ) -> ( ( s < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) ) -> ( U < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) ) )
150 149 ralimdva 
 |-  ( ( ph /\ s e. RR ) -> ( A. x e. CC ( s < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) ) -> A. x e. CC ( U < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) ) )
151 breq1 
 |-  ( r = U -> ( r < ( abs ` x ) <-> U < ( abs ` x ) ) )
152 151 rspceaimv 
 |-  ( ( U e. RR+ /\ A. x e. CC ( U < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) ) -> E. r e. RR+ A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
153 53 150 152 syl6an 
 |-  ( ( ph /\ s e. RR ) -> ( A. x e. CC ( s < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) ) -> E. r e. RR+ A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) ) )
154 153 rexlimdva 
 |-  ( ph -> ( E. s e. RR A. x e. CC ( s < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( ( ( abs ` ( A ` N ) ) / 2 ) x. ( ( abs ` x ) ^ N ) ) ) -> E. r e. RR+ A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) ) )
155 26 154 mpd 
 |-  ( ph -> E. r e. RR+ A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )