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 ‘ 𝑆 ) → 𝐴 : ℕ₀ ⟶ ℂ )
8	3 7	syl	⊢ ( 𝜑 → 𝐴 : ℕ₀ ⟶ ℂ )
9	4	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
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 ‘ 𝑥 ) ) ) → 𝑁 ∈ ℕ₀ )
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 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem ftalem2

Proof