Theorem ftalem1

Description: Lemma for fta : "growth lemma". There exists some r such that F is arbitrarily close in proportion to its dominant term. (Contributed by Mario Carneiro, 14-Sep-2014)

	Ref	Expression
Hypotheses	ftalem.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
	ftalem.2	⊢ 𝑁 = ( deg ‘ 𝐹 )
	ftalem.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
	ftalem.4	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	ftalem1.5	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	ftalem1.6	⊢ 𝑇 = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝐸 )
Assertion	ftalem1	⊢ ( 𝜑 → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ftalem.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2		ftalem.2	⊢ 𝑁 = ( deg ‘ 𝐹 )
3		ftalem.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4		ftalem.4	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5		ftalem1.5	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
6		ftalem1.6	⊢ 𝑇 = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝐸 )
7		fzfid	⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
8	1	coef3	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
9	3 8	syl	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
10		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
11		ffvelcdm	⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
12	9 10 11	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
13	12	abscld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
14	7 13	fsumrecl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
15	14 5	rerpdivcld	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝐸 ) ∈ ℝ )
16	6 15	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
17		1re	⊢ 1 ∈ ℝ
18		ifcl	⊢ ( ( 𝑇 ∈ ℝ ∧ 1 ∈ ℝ ) → if ( 1 ≤ 𝑇 , 𝑇 , 1 ) ∈ ℝ )
19	16 17 18	sylancl	⊢ ( 𝜑 → if ( 1 ≤ 𝑇 , 𝑇 , 1 ) ∈ ℝ )
20		fzfid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
21	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝐴 : ℕ0 ⟶ ℂ )
22	21 11	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
23		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
24		expcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
25	23 24	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
26	22 25	mulcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ ℂ )
27	10 26	sylan2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ ℂ )
28	20 27	fsumcl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ ℂ )
29	4	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
30	29	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑁 ∈ ℕ0 )
31	21 30	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐴 ‘ 𝑁 ) ∈ ℂ )
32	23 30	expcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝑥 ↑ 𝑁 ) ∈ ℂ )
33	31 32	mulcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ∈ ℂ )
34	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
35	1 2	coeid2	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) → ( 𝐹 ‘ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
36	34 23 35	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
37		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
38	30 37	eleqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
39		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
40	39 26	sylan2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ∈ ℂ )
41		fveq2	⊢ ( 𝑘 = 𝑁 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑁 ) )
42		oveq2	⊢ ( 𝑘 = 𝑁 → ( 𝑥 ↑ 𝑘 ) = ( 𝑥 ↑ 𝑁 ) )
43	41 42	oveq12d	⊢ ( 𝑘 = 𝑁 → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) )
44	38 40 43	fsumm1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) + ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) )
45	36 44	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) + ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) )
46	28 33 45	mvrraddd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
47	46	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) = ( abs ‘ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) )
48	28	abscld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ∈ ℝ )
49	27	abscld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ∈ ℝ )
50	20 49	fsumrecl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ∈ ℝ )
51	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝐸 ∈ ℝ+ )
52	51	rpred	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝐸 ∈ ℝ )
53	23	abscld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
54	53 30	reexpcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℝ )
55	52 54	remulcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ ℝ )
56	20 27	fsumabs	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) )
57	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
58	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑁 ∈ ℕ )
59		nnm1nn0	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
60	58 59	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝑁 − 1 ) ∈ ℕ0 )
61	53 60	reexpcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
62	57 61	remulcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ )
63	13	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
64	61	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
65	63 64	remulcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ )
66	22 25	absmuld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) ) )
67	10 66	sylan2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) ) )
68	10 25	sylan2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
69	68	abscld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) ∈ ℝ )
70	10 22	sylan2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
71	70	absge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 0 ≤ ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) )
72		absexp	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) = ( ( abs ‘ 𝑥 ) ↑ 𝑘 ) )
73	23 10 72	syl2an	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) = ( ( abs ‘ 𝑥 ) ↑ 𝑘 ) )
74	53	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
75	17	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
76	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → if ( 1 ≤ 𝑇 , 𝑇 , 1 ) ∈ ℝ )
77		max1	⊢ ( ( 1 ∈ ℝ ∧ 𝑇 ∈ ℝ ) → 1 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
78	17 16 77	sylancr	⊢ ( 𝜑 → 1 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
79	78	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 1 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
80		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) )
81	75 76 53 79 80	lelttrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 1 < ( abs ‘ 𝑥 ) )
82	75 53 81	ltled	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 1 ≤ ( abs ‘ 𝑥 ) )
83	82	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 1 ≤ ( abs ‘ 𝑥 ) )
84		elfzuz3	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑘 ) )
85	84	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑘 ) )
86	74 83 85	leexp2ad	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ 𝑘 ) ≤ ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
87	73 86	eqbrtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) ≤ ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
88	69 64 63 71 87	lemul2ad	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑥 ↑ 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
89	67 88	eqbrtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
90	20 49 65 89	fsumle	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
91	61	recnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
92	63	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
93	20 91 92	fsummulc1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
94	90 93	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) ≤ ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
95	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑇 ∈ ℝ )
96		max2	⊢ ( ( 1 ∈ ℝ ∧ 𝑇 ∈ ℝ ) → 𝑇 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
97	17 16 96	sylancr	⊢ ( 𝜑 → 𝑇 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
98	97	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑇 ≤ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) )
99	95 76 53 98 80	lelttrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝑇 < ( abs ‘ 𝑥 ) )
100	6 99	eqbrtrrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝐸 ) < ( abs ‘ 𝑥 ) )
101	57 53 51	ltdivmuld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝐸 ) < ( abs ‘ 𝑥 ) ↔ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) < ( 𝐸 · ( abs ‘ 𝑥 ) ) ) )
102	100 101	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) < ( 𝐸 · ( abs ‘ 𝑥 ) ) )
103	52 53	remulcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐸 · ( abs ‘ 𝑥 ) ) ∈ ℝ )
104	60	nn0zd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝑁 − 1 ) ∈ ℤ )
105		0red	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 0 ∈ ℝ )
106		0lt1	⊢ 0 < 1
107	106	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 0 < 1 )
108	105 75 53 107 81	lttrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 0 < ( abs ‘ 𝑥 ) )
109		expgt0	⊢ ( ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ 0 < ( abs ‘ 𝑥 ) ) → 0 < ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
110	53 104 108 109	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 0 < ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
111		ltmul1	⊢ ( ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ ∧ ( 𝐸 · ( abs ‘ 𝑥 ) ) ∈ ℝ ∧ ( ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ∈ ℝ ∧ 0 < ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) < ( 𝐸 · ( abs ‘ 𝑥 ) ) ↔ ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) < ( ( 𝐸 · ( abs ‘ 𝑥 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) )
112	57 103 61 110 111	syl112anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) < ( 𝐸 · ( abs ‘ 𝑥 ) ) ↔ ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) < ( ( 𝐸 · ( abs ‘ 𝑥 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) )
113	102 112	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) < ( ( 𝐸 · ( abs ‘ 𝑥 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
114	53	recnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℂ )
115		expm1t	⊢ ( ( ( abs ‘ 𝑥 ) ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) = ( ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) · ( abs ‘ 𝑥 ) ) )
116	114 58 115	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) = ( ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) · ( abs ‘ 𝑥 ) ) )
117	91 114	mulcomd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) · ( abs ‘ 𝑥 ) ) = ( ( abs ‘ 𝑥 ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
118	116 117	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) = ( ( abs ‘ 𝑥 ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
119	118	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) = ( 𝐸 · ( ( abs ‘ 𝑥 ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) )
120	52	recnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → 𝐸 ∈ ℂ )
121	120 114 91	mulassd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( ( 𝐸 · ( abs ‘ 𝑥 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) = ( 𝐸 · ( ( abs ‘ 𝑥 ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) ) )
122	119 121	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) = ( ( 𝐸 · ( abs ‘ 𝑥 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
123	113 122	breqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( ( abs ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) )
124	50 62 55 94 123	lelttrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) )
125	48 50 55 56 124	lelttrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) )
126	47 125	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) )
127	126	expr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) )
128	127	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) )
129		breq1	⊢ ( 𝑟 = if ( 1 ≤ 𝑇 , 𝑇 , 1 ) → ( 𝑟 < ( abs ‘ 𝑥 ) ↔ if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) ) )
130	129	rspceaimv	⊢ ( ( if ( 1 ≤ 𝑇 , 𝑇 , 1 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℂ ( if ( 1 ≤ 𝑇 , 𝑇 , 1 ) < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) )
131	19 128 130	syl2anc	⊢ ( 𝜑 → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ ℂ ( 𝑟 < ( abs ‘ 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( ( 𝐴 ‘ 𝑁 ) · ( 𝑥 ↑ 𝑁 ) ) ) ) < ( 𝐸 · ( ( abs ‘ 𝑥 ) ↑ 𝑁 ) ) ) )