evthicc

Description: Specialization of the Extreme Value Theorem to a closed interval of RR . (Contributed by Mario Carneiro, 12-Aug-2014)

	Ref	Expression
Hypotheses	evthicc.1	$⊢ φ \to A \in ℝ$
	evthicc.2	$⊢ φ \to B \in ℝ$
	evthicc.3	$⊢ φ \to A \leq B$
	evthicc.4	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
Assertion	evthicc	$⊢ φ \to (\exists x \in [A, B] \forall y \in [A, B] F (y) \leq F (x) \land \exists z \in [A, B] \forall w \in [A, B] F (z) \leq F (w))$

Proof

Step	Hyp	Ref	Expression
1		evthicc.1	$⊢ φ \to A \in ℝ$
2		evthicc.2	$⊢ φ \to B \in ℝ$
3		evthicc.3	$⊢ φ \to A \leq B$
4		evthicc.4	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
5		eqid	$⊢ ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) = ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B])$
6		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
7		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [A, B] = topGen (ran (.)) ↾_{𝑡} [A, B]$
8	6 7	icccmp	$⊢ (A \in ℝ \land B \in ℝ) \to topGen (ran (.)) ↾_{𝑡} [A, B] \in Comp$
9	1 2 8	syl2anc	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [A, B] \in Comp$
10		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
11	1 2 10	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
12		ax-resscn	$⊢ ℝ \subseteq ℂ$
13	11 12	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
14		eqid	$⊢ {(abs \circ -) ↾}_{([A, B] \times [A, B])} = {(abs \circ -) ↾}_{([A, B] \times [A, B])}$
15		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
16		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{([A, B] \times [A, B])}) = MetOpen ({(abs \circ -) ↾}_{([A, B] \times [A, B])})$
17		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
18	15 17	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
19	14 15 16 18	cncfmet	$⊢ ([A, B] \subseteq ℂ \land ℝ \subseteq ℂ) \to [A, B] \underset{cn}{⟶} ℝ = MetOpen ({(abs \circ -) ↾}_{([A, B] \times [A, B])}) Cn topGen (ran (.))$
20	13 12 19	sylancl	$⊢ φ \to [A, B] \underset{cn}{⟶} ℝ = MetOpen ({(abs \circ -) ↾}_{([A, B] \times [A, B])}) Cn topGen (ran (.))$
21	6 16	resubmet	$⊢ [A, B] \subseteq ℝ \to MetOpen ({(abs \circ -) ↾}_{([A, B] \times [A, B])}) = topGen (ran (.)) ↾_{𝑡} [A, B]$
22	11 21	syl	$⊢ φ \to MetOpen ({(abs \circ -) ↾}_{([A, B] \times [A, B])}) = topGen (ran (.)) ↾_{𝑡} [A, B]$
23	22	oveq1d	$⊢ φ \to MetOpen ({(abs \circ -) ↾}_{([A, B] \times [A, B])}) Cn topGen (ran (.)) = (topGen (ran (.)) ↾_{𝑡} [A, B]) Cn topGen (ran (.))$
24	20 23	eqtrd	$⊢ φ \to [A, B] \underset{cn}{⟶} ℝ = (topGen (ran (.)) ↾_{𝑡} [A, B]) Cn topGen (ran (.))$
25	4 24	eleqtrd	$⊢ φ \to F \in ((topGen (ran (.)) ↾_{𝑡} [A, B]) Cn topGen (ran (.)))$
26		retop	$⊢ topGen (ran (.)) \in Top$
27		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
28	27	restuni	$⊢ (topGen (ran (.)) \in Top \land [A, B] \subseteq ℝ) \to [A, B] = ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B])$
29	26 11 28	sylancr	$⊢ φ \to [A, B] = ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B])$
30	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
31	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
32		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
33	30 31 3 32	syl3anc	$⊢ φ \to A \in [A, B]$
34	33	ne0d	$⊢ φ \to [A, B] \neq \emptyset$
35	29 34	eqnetrrd	$⊢ φ \to ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) \neq \emptyset$
36	5 6 9 25 35	evth	$⊢ φ \to \exists x \in ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) \forall y \in ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) F (y) \leq F (x)$
37	29	raleqdv	$⊢ φ \to (\forall y \in [A, B] F (y) \leq F (x) \leftrightarrow \forall y \in ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) F (y) \leq F (x))$
38	29 37	rexeqbidv	$⊢ φ \to (\exists x \in [A, B] \forall y \in [A, B] F (y) \leq F (x) \leftrightarrow \exists x \in ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) \forall y \in ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) F (y) \leq F (x))$
39	36 38	mpbird	$⊢ φ \to \exists x \in [A, B] \forall y \in [A, B] F (y) \leq F (x)$
40	5 6 9 25 35	evth2	$⊢ φ \to \exists z \in ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) \forall w \in ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) F (z) \leq F (w)$
41	29	raleqdv	$⊢ φ \to (\forall w \in [A, B] F (z) \leq F (w) \leftrightarrow \forall w \in ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) F (z) \leq F (w))$
42	29 41	rexeqbidv	$⊢ φ \to (\exists z \in [A, B] \forall w \in [A, B] F (z) \leq F (w) \leftrightarrow \exists z \in ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) \forall w \in ⋃ (topGen (ran (.)) ↾_{𝑡} [A, B]) F (z) \leq F (w))$
43	40 42	mpbird	$⊢ φ \to \exists z \in [A, B] \forall w \in [A, B] F (z) \leq F (w)$
44	39 43	jca	$⊢ φ \to (\exists x \in [A, B] \forall y \in [A, B] F (y) \leq F (x) \land \exists z \in [A, B] \forall w \in [A, B] F (z) \leq F (w))$

Metamath Proof Explorer

Theorem evthicc

Proof