This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑁 ) ∈ ℂ )
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 biimtrrdi ⊢ ( 𝐹 ∈ ( 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 ffvelcdm ⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ 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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑈 < ( 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 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )