ftalem3

Description: Lemma for fta . There exists a global minimum of the function abs o. F . The proof uses a circle of radius r where r is the value coming from ftalem1 ; since this is a compact set, the minimum on this disk is achieved, and this must then be the global minimum. (Contributed by Mario Carneiro, 14-Sep-2014)

	Ref	Expression
Hypotheses	ftalem.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
	ftalem.2	⊢ 𝑁 = ( deg ‘ 𝐹 )
	ftalem.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
	ftalem.4	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	ftalem3.5	⊢ 𝐷 = { 𝑦 ∈ ℂ ∣ ( abs ‘ 𝑦 ) ≤ 𝑅 }
	ftalem3.6	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
	ftalem3.7	⊢ ( 𝜑 → 𝑅 ∈ ℝ⁺ )
	ftalem3.8	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( 𝑅 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
Assertion	ftalem3	⊢ ( 𝜑 → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ftalem.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2		ftalem.2	⊢ 𝑁 = ( deg ‘ 𝐹 )
3		ftalem.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4		ftalem.4	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5		ftalem3.5	⊢ 𝐷 = { 𝑦 ∈ ℂ ∣ ( abs ‘ 𝑦 ) ≤ 𝑅 }
6		ftalem3.6	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
7		ftalem3.7	⊢ ( 𝜑 → 𝑅 ∈ ℝ⁺ )
8		ftalem3.8	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( 𝑅 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
9	5	ssrab3	⊢ 𝐷 ⊆ ℂ
10	6	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
11		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( 𝐽 ↾_t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
12	10 9 11	mp2an	⊢ ( 𝐽 ↾_t 𝐷 ) ∈ ( TopOn ‘ 𝐷 )
13	12	toponunii	⊢ 𝐷 = ∪ ( 𝐽 ↾_t 𝐷 )
14		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
15		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
16	15	a1i	⊢ ( 𝜑 → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
17		0cn	⊢ 0 ∈ ℂ
18	17	a1i	⊢ ( 𝜑 → 0 ∈ ℂ )
19	7	rpxrd	⊢ ( 𝜑 → 𝑅 ∈ ℝ^* )
20	6	cnfldtopn	⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
21		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
22	21	cnmetdval	⊢ ( ( 0 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 0 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 0 − 𝑦 ) ) )
23	17 22	mpan	⊢ ( 𝑦 ∈ ℂ → ( 0 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 0 − 𝑦 ) ) )
24		df-neg	⊢ - 𝑦 = ( 0 − 𝑦 )
25	24	fveq2i	⊢ ( abs ‘ - 𝑦 ) = ( abs ‘ ( 0 − 𝑦 ) )
26		absneg	⊢ ( 𝑦 ∈ ℂ → ( abs ‘ - 𝑦 ) = ( abs ‘ 𝑦 ) )
27	25 26	eqtr3id	⊢ ( 𝑦 ∈ ℂ → ( abs ‘ ( 0 − 𝑦 ) ) = ( abs ‘ 𝑦 ) )
28	23 27	eqtrd	⊢ ( 𝑦 ∈ ℂ → ( 0 ( abs ∘ − ) 𝑦 ) = ( abs ‘ 𝑦 ) )
29	28	breq1d	⊢ ( 𝑦 ∈ ℂ → ( ( 0 ( abs ∘ − ) 𝑦 ) ≤ 𝑅 ↔ ( abs ‘ 𝑦 ) ≤ 𝑅 ) )
30	29	rabbiia	⊢ { 𝑦 ∈ ℂ ∣ ( 0 ( abs ∘ − ) 𝑦 ) ≤ 𝑅 } = { 𝑦 ∈ ℂ ∣ ( abs ‘ 𝑦 ) ≤ 𝑅 }
31	5 30	eqtr4i	⊢ 𝐷 = { 𝑦 ∈ ℂ ∣ ( 0 ( abs ∘ − ) 𝑦 ) ≤ 𝑅 }
32	20 31	blcld	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑅 ∈ ℝ^* ) → 𝐷 ∈ ( Clsd ‘ 𝐽 ) )
33	16 18 19 32	syl3anc	⊢ ( 𝜑 → 𝐷 ∈ ( Clsd ‘ 𝐽 ) )
34	7	rpred	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
35		fveq2	⊢ ( 𝑦 = 𝑥 → ( abs ‘ 𝑦 ) = ( abs ‘ 𝑥 ) )
36	35	breq1d	⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ 𝑦 ) ≤ 𝑅 ↔ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
37	36 5	elrab2	⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
38	37	simprbi	⊢ ( 𝑥 ∈ 𝐷 → ( abs ‘ 𝑥 ) ≤ 𝑅 )
39	38	rgen	⊢ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑅
40		brralrspcev	⊢ ( ( 𝑅 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑅 ) → ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑠 )
41	34 39 40	sylancl	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑠 )
42		eqid	⊢ ( 𝐽 ↾_t 𝐷 ) = ( 𝐽 ↾_t 𝐷 )
43	6 42	cnheibor	⊢ ( 𝐷 ⊆ ℂ → ( ( 𝐽 ↾_t 𝐷 ) ∈ Comp ↔ ( 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑠 ) ) )
44	9 43	ax-mp	⊢ ( ( 𝐽 ↾_t 𝐷 ) ∈ Comp ↔ ( 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑥 ∈ 𝐷 ( abs ‘ 𝑥 ) ≤ 𝑠 ) )
45	33 41 44	sylanbrc	⊢ ( 𝜑 → ( 𝐽 ↾_t 𝐷 ) ∈ Comp )
46		plycn	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( ℂ –cn→ ℂ ) )
47	3 46	syl	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )
48		abscncf	⊢ abs ∈ ( ℂ –cn→ ℝ )
49	48	a1i	⊢ ( 𝜑 → abs ∈ ( ℂ –cn→ ℝ ) )
50	47 49	cncfco	⊢ ( 𝜑 → ( abs ∘ 𝐹 ) ∈ ( ℂ –cn→ ℝ ) )
51		ssid	⊢ ℂ ⊆ ℂ
52		ax-resscn	⊢ ℝ ⊆ ℂ
53	10	toponrestid	⊢ 𝐽 = ( 𝐽 ↾_t ℂ )
54	6	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( 𝐽 ↾_t ℝ )
55	6 53 54	cncfcn	⊢ ( ( ℂ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) = ( 𝐽 Cn ( topGen ‘ ran (,) ) ) )
56	51 52 55	mp2an	⊢ ( ℂ –cn→ ℝ ) = ( 𝐽 Cn ( topGen ‘ ran (,) ) )
57	50 56	eleqtrdi	⊢ ( 𝜑 → ( abs ∘ 𝐹 ) ∈ ( 𝐽 Cn ( topGen ‘ ran (,) ) ) )
58	10	toponunii	⊢ ℂ = ∪ 𝐽
59	58	cnrest	⊢ ( ( ( abs ∘ 𝐹 ) ∈ ( 𝐽 Cn ( topGen ‘ ran (,) ) ) ∧ 𝐷 ⊆ ℂ ) → ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ∈ ( ( 𝐽 ↾_t 𝐷 ) Cn ( topGen ‘ ran (,) ) ) )
60	57 9 59	sylancl	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ∈ ( ( 𝐽 ↾_t 𝐷 ) Cn ( topGen ‘ ran (,) ) ) )
61	7	rpge0d	⊢ ( 𝜑 → 0 ≤ 𝑅 )
62		fveq2	⊢ ( 𝑦 = 0 → ( abs ‘ 𝑦 ) = ( abs ‘ 0 ) )
63		abs0	⊢ ( abs ‘ 0 ) = 0
64	62 63	eqtrdi	⊢ ( 𝑦 = 0 → ( abs ‘ 𝑦 ) = 0 )
65	64	breq1d	⊢ ( 𝑦 = 0 → ( ( abs ‘ 𝑦 ) ≤ 𝑅 ↔ 0 ≤ 𝑅 ) )
66	65 5	elrab2	⊢ ( 0 ∈ 𝐷 ↔ ( 0 ∈ ℂ ∧ 0 ≤ 𝑅 ) )
67	18 61 66	sylanbrc	⊢ ( 𝜑 → 0 ∈ 𝐷 )
68	67	ne0d	⊢ ( 𝜑 → 𝐷 ≠ ∅ )
69	13 14 45 60 68	evth2	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) ≤ ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) )
70		fvres	⊢ ( 𝑧 ∈ 𝐷 → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) = ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) )
71	70	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) = ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) )
72		plyf	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
73	3 72	syl	⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
74	73	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝐹 : ℂ ⟶ ℂ )
75		simplr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑧 ∈ 𝐷 )
76	9 75	sselid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑧 ∈ ℂ )
77		fvco3	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
78	74 76 77	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
79	71 78	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
80		fvres	⊢ ( 𝑥 ∈ 𝐷 → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) = ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) )
81	80	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) = ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) )
82		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
83	9 82	sselid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ℂ )
84		fvco3	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
85	74 83 84	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
86	81 85	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
87	79 86	breq12d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) ≤ ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
88	87	ralbidva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐷 ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) ≤ ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
89	88	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑧 ) ≤ ( ( ( abs ∘ 𝐹 ) ↾ 𝐷 ) ‘ 𝑥 ) ↔ ∃ 𝑧 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
90	69 89	mpbid	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
91		ssrexv	⊢ ( 𝐷 ⊆ ℂ → ( ∃ 𝑧 ∈ 𝐷 ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
92	9 90 91	mpsyl	⊢ ( 𝜑 → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
93	67	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 0 ∈ 𝐷 )
94		2fveq3	⊢ ( 𝑥 = 0 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ 0 ) ) )
95	94	breq2d	⊢ ( 𝑥 = 0 → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ) )
96	95	rspcv	⊢ ( 0 ∈ 𝐷 → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ) )
97	93 96	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ) )
98	73	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝐹 : ℂ ⟶ ℂ )
99		ffvelcdm	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ 0 ∈ ℂ ) → ( 𝐹 ‘ 0 ) ∈ ℂ )
100	98 17 99	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( 𝐹 ‘ 0 ) ∈ ℂ )
101	100	abscld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) ∈ ℝ )
102		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑥 ∈ ( ℂ ∖ 𝐷 ) )
103	102	eldifad	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑥 ∈ ℂ )
104	98 103	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
105	104	abscld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
106	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ∀ 𝑥 ∈ ℂ ( 𝑅 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
107	102	eldifbd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ¬ 𝑥 ∈ 𝐷 )
108	37	baib	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ∈ 𝐷 ↔ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
109	103 108	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( 𝑥 ∈ 𝐷 ↔ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
110	107 109	mtbid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ¬ ( abs ‘ 𝑥 ) ≤ 𝑅 )
111	34	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑅 ∈ ℝ )
112	103	abscld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
113	111 112	ltnled	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( 𝑅 < ( abs ‘ 𝑥 ) ↔ ¬ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
114	110 113	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑅 < ( abs ‘ 𝑥 ) )
115		rsp	⊢ ( ∀ 𝑥 ∈ ℂ ( 𝑅 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℂ → ( 𝑅 < ( abs ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
116	106 103 114 115	syl3c	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
117	101 105 116	ltled	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ ( 𝐹 ‘ 0 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
118		simplr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑧 ∈ ℂ )
119	98 118	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
120	119	abscld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
121		letr	⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 0 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 0 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
122	120 101 105 121	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 0 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
123	117 122	mpan2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
124	123	ralrimdva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 0 ) ) → ∀ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
125	97 124	syld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
126	125	ancld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
127		ralunb	⊢ ( ∀ 𝑥 ∈ ( 𝐷 ∪ ( ℂ ∖ 𝐷 ) ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
128		undif2	⊢ ( 𝐷 ∪ ( ℂ ∖ 𝐷 ) ) = ( 𝐷 ∪ ℂ )
129		ssequn1	⊢ ( 𝐷 ⊆ ℂ ↔ ( 𝐷 ∪ ℂ ) = ℂ )
130	9 129	mpbi	⊢ ( 𝐷 ∪ ℂ ) = ℂ
131	128 130	eqtri	⊢ ( 𝐷 ∪ ( ℂ ∖ 𝐷 ) ) = ℂ
132	131	raleqi	⊢ ( ∀ 𝑥 ∈ ( 𝐷 ∪ ( ℂ ∖ 𝐷 ) ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
133	127 132	bitr3i	⊢ ( ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( ℂ ∖ 𝐷 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
134	126 133	imbitrdi	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
135	134	reximdva	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ 𝐷 ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
136	92 135	mpd	⊢ ( 𝜑 → ∃ 𝑧 ∈ ℂ ∀ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )

Metamath Proof Explorer

Theorem ftalem3

Proof