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 syl5eq
 |-  ( 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 ) ) ) )