Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
evthicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
evthicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
evthicc.4 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
Assertion evthicc ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 evthicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 evthicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 evthicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 evthicc.4 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
5 eqid ⊢ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) )
6 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
7 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) )
8 6 7 icccmp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Comp )
9 1 2 8 syl2anc ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Comp )
10 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
11 1 2 10 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
12 ax-resscn ⊢ ℝ ⊆ ℂ
13 11 12 sstrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
14 eqid ⊢ ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) = ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) )
15 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
16 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) )
17 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
18 15 17 tgioo ⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
19 14 15 16 18 cncfmet ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) = ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) Cn ( topGen ‘ ran (,) ) ) )
20 13 12 19 sylancl ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) = ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) Cn ( topGen ‘ ran (,) ) ) )
21 6 16 resubmet ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
22 11 21 syl ⊢ ( 𝜑 → ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
23 22 oveq1d ⊢ ( 𝜑 → ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) ) Cn ( topGen ‘ ran (,) ) ) = ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( topGen ‘ ran (,) ) ) )
24 20 23 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) = ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( topGen ‘ ran (,) ) ) )
25 4 24 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( topGen ‘ ran (,) ) ) )
26 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
27 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
28 27 restuni ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → ( 𝐴 [,] 𝐵 ) = ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
29 26 11 28 sylancr ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
30 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
31 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
32 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
33 30 31 3 32 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
34 33 ne0d ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ≠ ∅ )
35 29 34 eqnetrrd ⊢ ( 𝜑 → ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ≠ ∅ )
36 5 6 9 25 35 evth ⊢ ( 𝜑 → ∃ 𝑥 ∈ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∀ 𝑦 ∈ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) )
37 29 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
38 29 37 rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∀ 𝑦 ∈ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
39 36 38 mpbird ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) )
40 5 6 9 25 35 evth2 ⊢ ( 𝜑 → ∃ 𝑧 ∈ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∀ 𝑤 ∈ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) )
41 29 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑤 ∈ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )
42 29 41 rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) ↔ ∃ 𝑧 ∈ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∀ 𝑤 ∈ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )
43 40 42 mpbird ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) )
44 39 43 jca ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )