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	$⊢ A = coeff (F)$
	ftalem.2	$⊢ N = \deg (F)$
	ftalem.3	$⊢ φ \to F \in Poly (S)$
	ftalem.4	$⊢ φ \to N \in ℕ$
	ftalem3.5	$⊢ D = \{y \in ℂ \| \|y\| \leq R\}$
	ftalem3.6	$⊢ J = TopOpen (ℂ_{fld})$
	ftalem3.7	$⊢ φ \to R \in ℝ^{+}$
	ftalem3.8	$⊢ φ \to \forall x \in ℂ (R < \|x\| \to \|F (0)\| < \|F (x)\|)$
Assertion	ftalem3	$⊢ φ \to \exists z \in ℂ \forall x \in ℂ \|F (z)\| \leq \|F (x)\|$

Proof

Step	Hyp	Ref	Expression
1		ftalem.1	$⊢ A = coeff (F)$
2		ftalem.2	$⊢ N = \deg (F)$
3		ftalem.3	$⊢ φ \to F \in Poly (S)$
4		ftalem.4	$⊢ φ \to N \in ℕ$
5		ftalem3.5	$⊢ D = \{y \in ℂ \| \|y\| \leq R\}$
6		ftalem3.6	$⊢ J = TopOpen (ℂ_{fld})$
7		ftalem3.7	$⊢ φ \to R \in ℝ^{+}$
8		ftalem3.8	$⊢ φ \to \forall x \in ℂ (R < \|x\| \to \|F (0)\| < \|F (x)\|)$
9	5	ssrab3	$⊢ D \subseteq ℂ$
10	6	cnfldtopon	$⊢ J \in TopOn (ℂ)$
11		resttopon	$⊢ (J \in TopOn (ℂ) \land D \subseteq ℂ) \to J ↾_{𝑡} D \in TopOn (D)$
12	10 9 11	mp2an	$⊢ J ↾_{𝑡} D \in TopOn (D)$
13	12	toponunii	$⊢ D = ⋃ (J ↾_{𝑡} D)$
14		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
15		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
16	15	a1i	$⊢ φ \to abs \circ - \in ∞Met (ℂ)$
17		0cn	$⊢ 0 \in ℂ$
18	17	a1i	$⊢ φ \to 0 \in ℂ$
19	7	rpxrd	$⊢ φ \to R \in ℝ^{*}$
20	6	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
21		eqid	$⊢ abs \circ - = abs \circ -$
22	21	cnmetdval	$⊢ (0 \in ℂ \land y \in ℂ) \to 0 (abs \circ -) y = \|0 - y\|$
23	17 22	mpan	$⊢ y \in ℂ \to 0 (abs \circ -) y = \|0 - y\|$
24		df-neg	$⊢ - y = 0 - y$
25	24	fveq2i	$⊢ \|- y\| = \|0 - y\|$
26		absneg	$⊢ y \in ℂ \to \|- y\| = \|y\|$
27	25 26	syl5eqr	$⊢ y \in ℂ \to \|0 - y\| = \|y\|$
28	23 27	eqtrd	$⊢ y \in ℂ \to 0 (abs \circ -) y = \|y\|$
29	28	breq1d	$⊢ y \in ℂ \to (0 (abs \circ -) y \leq R \leftrightarrow \|y\| \leq R)$
30	29	rabbiia	$⊢ \{y \in ℂ \| 0 (abs \circ -) y \leq R\} = \{y \in ℂ \| \|y\| \leq R\}$
31	5 30	eqtr4i	$⊢ D = \{y \in ℂ \| 0 (abs \circ -) y \leq R\}$
32	20 31	blcld	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land R \in ℝ^{*}) \to D \in Clsd (J)$
33	16 18 19 32	syl3anc	$⊢ φ \to D \in Clsd (J)$
34	7	rpred	$⊢ φ \to R \in ℝ$
35		fveq2	$⊢ y = x \to \|y\| = \|x\|$
36	35	breq1d	$⊢ y = x \to (\|y\| \leq R \leftrightarrow \|x\| \leq R)$
37	36 5	elrab2	$⊢ x \in D \leftrightarrow (x \in ℂ \land \|x\| \leq R)$
38	37	simprbi	$⊢ x \in D \to \|x\| \leq R$
39	38	rgen	$⊢ \forall x \in D \|x\| \leq R$
40		brralrspcev	$⊢ (R \in ℝ \land \forall x \in D \|x\| \leq R) \to \exists s \in ℝ \forall x \in D \|x\| \leq s$
41	34 39 40	sylancl	$⊢ φ \to \exists s \in ℝ \forall x \in D \|x\| \leq s$
42		eqid	$⊢ J ↾_{𝑡} D = J ↾_{𝑡} D$
43	6 42	cnheibor	$⊢ D \subseteq ℂ \to (J ↾_{𝑡} D \in Comp \leftrightarrow (D \in Clsd (J) \land \exists s \in ℝ \forall x \in D \|x\| \leq s))$
44	9 43	ax-mp	$⊢ J ↾_{𝑡} D \in Comp \leftrightarrow (D \in Clsd (J) \land \exists s \in ℝ \forall x \in D \|x\| \leq s)$
45	33 41 44	sylanbrc	$⊢ φ \to J ↾_{𝑡} D \in Comp$
46		plycn	$⊢ F \in Poly (S) \to F : ℂ \underset{cn}{⟶} ℂ$
47	3 46	syl	$⊢ φ \to F : ℂ \underset{cn}{⟶} ℂ$
48		abscncf	$⊢ abs : ℂ \underset{cn}{⟶} ℝ$
49	48	a1i	$⊢ φ \to abs : ℂ \underset{cn}{⟶} ℝ$
50	47 49	cncfco	$⊢ φ \to (abs \circ F) : ℂ \underset{cn}{⟶} ℝ$
51		ssid	$⊢ ℂ \subseteq ℂ$
52		ax-resscn	$⊢ ℝ \subseteq ℂ$
53	10	toponrestid	$⊢ J = J ↾_{𝑡} ℂ$
54	6	tgioo2	$⊢ topGen (ran (.)) = J ↾_{𝑡} ℝ$
55	6 53 54	cncfcn	$⊢ (ℂ \subseteq ℂ \land ℝ \subseteq ℂ) \to ℂ \underset{cn}{⟶} ℝ = J Cn topGen (ran (.))$
56	51 52 55	mp2an	$⊢ ℂ \underset{cn}{⟶} ℝ = J Cn topGen (ran (.))$
57	50 56	eleqtrdi	$⊢ φ \to abs \circ F \in (J Cn topGen (ran (.)))$
58	10	toponunii	$⊢ ℂ = ⋃ J$
59	58	cnrest	$⊢ (abs \circ F \in (J Cn topGen (ran (.))) \land D \subseteq ℂ) \to {(abs \circ F) ↾}_{D} \in ((J ↾_{𝑡} D) Cn topGen (ran (.)))$
60	57 9 59	sylancl	$⊢ φ \to {(abs \circ F) ↾}_{D} \in ((J ↾_{𝑡} D) Cn topGen (ran (.)))$
61	7	rpge0d	$⊢ φ \to 0 \leq R$
62		fveq2	$⊢ y = 0 \to \|y\| = \|0\|$
63		abs0	$⊢ \|0\| = 0$
64	62 63	eqtrdi	$⊢ y = 0 \to \|y\| = 0$
65	64	breq1d	$⊢ y = 0 \to (\|y\| \leq R \leftrightarrow 0 \leq R)$
66	65 5	elrab2	$⊢ 0 \in D \leftrightarrow (0 \in ℂ \land 0 \leq R)$
67	18 61 66	sylanbrc	$⊢ φ \to 0 \in D$
68	67	ne0d	$⊢ φ \to D \neq \emptyset$
69	13 14 45 60 68	evth2	$⊢ φ \to \exists z \in D \forall x \in D ({(abs \circ F) ↾}_{D}) (z) \leq ({(abs \circ F) ↾}_{D}) (x)$
70		fvres	$⊢ z \in D \to ({(abs \circ F) ↾}_{D}) (z) = (abs \circ F) (z)$
71	70	ad2antlr	$⊢ ((φ \land z \in D) \land x \in D) \to ({(abs \circ F) ↾}_{D}) (z) = (abs \circ F) (z)$
72		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
73	3 72	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
74	73	ad2antrr	$⊢ ((φ \land z \in D) \land x \in D) \to F : ℂ ⟶ ℂ$
75		simplr	$⊢ ((φ \land z \in D) \land x \in D) \to z \in D$
76	9 75	sseldi	$⊢ ((φ \land z \in D) \land x \in D) \to z \in ℂ$
77		fvco3	$⊢ (F : ℂ ⟶ ℂ \land z \in ℂ) \to (abs \circ F) (z) = \|F (z)\|$
78	74 76 77	syl2anc	$⊢ ((φ \land z \in D) \land x \in D) \to (abs \circ F) (z) = \|F (z)\|$
79	71 78	eqtrd	$⊢ ((φ \land z \in D) \land x \in D) \to ({(abs \circ F) ↾}_{D}) (z) = \|F (z)\|$
80		fvres	$⊢ x \in D \to ({(abs \circ F) ↾}_{D}) (x) = (abs \circ F) (x)$
81	80	adantl	$⊢ ((φ \land z \in D) \land x \in D) \to ({(abs \circ F) ↾}_{D}) (x) = (abs \circ F) (x)$
82		simpr	$⊢ ((φ \land z \in D) \land x \in D) \to x \in D$
83	9 82	sseldi	$⊢ ((φ \land z \in D) \land x \in D) \to x \in ℂ$
84		fvco3	$⊢ (F : ℂ ⟶ ℂ \land x \in ℂ) \to (abs \circ F) (x) = \|F (x)\|$
85	74 83 84	syl2anc	$⊢ ((φ \land z \in D) \land x \in D) \to (abs \circ F) (x) = \|F (x)\|$
86	81 85	eqtrd	$⊢ ((φ \land z \in D) \land x \in D) \to ({(abs \circ F) ↾}_{D}) (x) = \|F (x)\|$
87	79 86	breq12d	$⊢ ((φ \land z \in D) \land x \in D) \to (({(abs \circ F) ↾}_{D}) (z) \leq ({(abs \circ F) ↾}_{D}) (x) \leftrightarrow \|F (z)\| \leq \|F (x)\|)$
88	87	ralbidva	$⊢ (φ \land z \in D) \to (\forall x \in D ({(abs \circ F) ↾}_{D}) (z) \leq ({(abs \circ F) ↾}_{D}) (x) \leftrightarrow \forall x \in D \|F (z)\| \leq \|F (x)\|)$
89	88	rexbidva	$⊢ φ \to (\exists z \in D \forall x \in D ({(abs \circ F) ↾}_{D}) (z) \leq ({(abs \circ F) ↾}_{D}) (x) \leftrightarrow \exists z \in D \forall x \in D \|F (z)\| \leq \|F (x)\|)$
90	69 89	mpbid	$⊢ φ \to \exists z \in D \forall x \in D \|F (z)\| \leq \|F (x)\|$
91		ssrexv	$⊢ D \subseteq ℂ \to (\exists z \in D \forall x \in D \|F (z)\| \leq \|F (x)\| \to \exists z \in ℂ \forall x \in D \|F (z)\| \leq \|F (x)\|)$
92	9 90 91	mpsyl	$⊢ φ \to \exists z \in ℂ \forall x \in D \|F (z)\| \leq \|F (x)\|$
93	67	adantr	$⊢ (φ \land z \in ℂ) \to 0 \in D$
94		2fveq3	$⊢ x = 0 \to \|F (x)\| = \|F (0)\|$
95	94	breq2d	$⊢ x = 0 \to (\|F (z)\| \leq \|F (x)\| \leftrightarrow \|F (z)\| \leq \|F (0)\|)$
96	95	rspcv	$⊢ 0 \in D \to (\forall x \in D \|F (z)\| \leq \|F (x)\| \to \|F (z)\| \leq \|F (0)\|)$
97	93 96	syl	$⊢ (φ \land z \in ℂ) \to (\forall x \in D \|F (z)\| \leq \|F (x)\| \to \|F (z)\| \leq \|F (0)\|)$
98	73	ad2antrr	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to F : ℂ ⟶ ℂ$
99		ffvelrn	$⊢ (F : ℂ ⟶ ℂ \land 0 \in ℂ) \to F (0) \in ℂ$
100	98 17 99	sylancl	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to F (0) \in ℂ$
101	100	abscld	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to \|F (0)\| \in ℝ$
102		simpr	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to x \in (ℂ ∖ D)$
103	102	eldifad	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to x \in ℂ$
104	98 103	ffvelrnd	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to F (x) \in ℂ$
105	104	abscld	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to \|F (x)\| \in ℝ$
106	8	ad2antrr	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to \forall x \in ℂ (R < \|x\| \to \|F (0)\| < \|F (x)\|)$
107	102	eldifbd	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to \neg x \in D$
108	37	baib	$⊢ x \in ℂ \to (x \in D \leftrightarrow \|x\| \leq R)$
109	103 108	syl	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to (x \in D \leftrightarrow \|x\| \leq R)$
110	107 109	mtbid	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to \neg \|x\| \leq R$
111	34	ad2antrr	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to R \in ℝ$
112	103	abscld	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to \|x\| \in ℝ$
113	111 112	ltnled	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to (R < \|x\| \leftrightarrow \neg \|x\| \leq R)$
114	110 113	mpbird	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to R < \|x\|$
115		rsp	$⊢ \forall x \in ℂ (R < \|x\| \to \|F (0)\| < \|F (x)\|) \to (x \in ℂ \to (R < \|x\| \to \|F (0)\| < \|F (x)\|))$
116	106 103 114 115	syl3c	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to \|F (0)\| < \|F (x)\|$
117	101 105 116	ltled	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to \|F (0)\| \leq \|F (x)\|$
118		simplr	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to z \in ℂ$
119	98 118	ffvelrnd	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to F (z) \in ℂ$
120	119	abscld	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to \|F (z)\| \in ℝ$
121		letr	$⊢ (\|F (z)\| \in ℝ \land \|F (0)\| \in ℝ \land \|F (x)\| \in ℝ) \to ((\|F (z)\| \leq \|F (0)\| \land \|F (0)\| \leq \|F (x)\|) \to \|F (z)\| \leq \|F (x)\|)$
122	120 101 105 121	syl3anc	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to ((\|F (z)\| \leq \|F (0)\| \land \|F (0)\| \leq \|F (x)\|) \to \|F (z)\| \leq \|F (x)\|)$
123	117 122	mpan2d	$⊢ ((φ \land z \in ℂ) \land x \in (ℂ ∖ D)) \to (\|F (z)\| \leq \|F (0)\| \to \|F (z)\| \leq \|F (x)\|)$
124	123	ralrimdva	$⊢ (φ \land z \in ℂ) \to (\|F (z)\| \leq \|F (0)\| \to \forall x \in (ℂ ∖ D) \|F (z)\| \leq \|F (x)\|)$
125	97 124	syld	$⊢ (φ \land z \in ℂ) \to (\forall x \in D \|F (z)\| \leq \|F (x)\| \to \forall x \in (ℂ ∖ D) \|F (z)\| \leq \|F (x)\|)$
126	125	ancld	$⊢ (φ \land z \in ℂ) \to (\forall x \in D \|F (z)\| \leq \|F (x)\| \to (\forall x \in D \|F (z)\| \leq \|F (x)\| \land \forall x \in (ℂ ∖ D) \|F (z)\| \leq \|F (x)\|))$
127		ralunb	$⊢ \forall x \in (D \cup (ℂ ∖ D)) \|F (z)\| \leq \|F (x)\| \leftrightarrow (\forall x \in D \|F (z)\| \leq \|F (x)\| \land \forall x \in (ℂ ∖ D) \|F (z)\| \leq \|F (x)\|)$
128		undif2	$⊢ D \cup (ℂ ∖ D) = D \cup ℂ$
129		ssequn1	$⊢ D \subseteq ℂ \leftrightarrow D \cup ℂ = ℂ$
130	9 129	mpbi	$⊢ D \cup ℂ = ℂ$
131	128 130	eqtri	$⊢ D \cup (ℂ ∖ D) = ℂ$
132	131	raleqi	$⊢ \forall x \in (D \cup (ℂ ∖ D)) \|F (z)\| \leq \|F (x)\| \leftrightarrow \forall x \in ℂ \|F (z)\| \leq \|F (x)\|$
133	127 132	bitr3i	$⊢ (\forall x \in D \|F (z)\| \leq \|F (x)\| \land \forall x \in (ℂ ∖ D) \|F (z)\| \leq \|F (x)\|) \leftrightarrow \forall x \in ℂ \|F (z)\| \leq \|F (x)\|$
134	126 133	syl6ib	$⊢ (φ \land z \in ℂ) \to (\forall x \in D \|F (z)\| \leq \|F (x)\| \to \forall x \in ℂ \|F (z)\| \leq \|F (x)\|)$
135	134	reximdva	$⊢ φ \to (\exists z \in ℂ \forall x \in D \|F (z)\| \leq \|F (x)\| \to \exists z \in ℂ \forall x \in ℂ \|F (z)\| \leq \|F (x)\|)$
136	92 135	mpd	$⊢ φ \to \exists z \in ℂ \forall x \in ℂ \|F (z)\| \leq \|F (x)\|$

Metamath Proof Explorer

Theorem ftalem3

Proof