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 𝐴 = ( coeff ‘ 𝐹 )
ftalem.2 𝑁 = ( deg ‘ 𝐹 )
ftalem.3 ( 𝜑𝐹 ∈ ( Poly ‘ 𝑆 ) )
ftalem.4 ( 𝜑𝑁 ∈ ℕ )
ftalem2.5 𝑈 = if ( if ( 1 ≤ 𝑠 , 𝑠 , 1 ) ≤ 𝑇 , 𝑇 , if ( 1 ≤ 𝑠 , 𝑠 , 1 ) )
ftalem2.6 𝑇 = ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( ( abs ‘ ( 𝐴𝑁 ) ) / 2 ) )
Assertion ftalem2 ( 𝜑 → ∃ 𝑟 ∈ ℝ+𝑥 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹𝑥 ) ) ) )

Proof

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