Metamath Proof Explorer

Theorem evthiccabs

Description: Extreme Value Theorem on y closed interval, for the absolute value of y continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses evthiccabs.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
evthiccabs.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
evthiccabs.aleb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
evthiccabs.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
Assertion evthiccabs ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ) )

Proof

Step Hyp Ref Expression
1 evthiccabs.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 evthiccabs.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 evthiccabs.aleb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 evthiccabs.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
5 ax-resscn ⊢ ℝ ⊆ ℂ
6 ssid ⊢ ℂ ⊆ ℂ
7 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
8 5 6 7 mp2an ⊢ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ )
9 8 4 sselid ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
10 abscncf ⊢ abs ∈ ( ℂ –cn→ ℝ )
11 10 a1i ⊢ ( 𝜑 → abs ∈ ( ℂ –cn→ ℝ ) )
12 9 11 cncfco ⊢ ( 𝜑 → ( abs ∘ 𝐹 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
13 1 2 3 12 evthicc ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑤 ) ) )
14 13 simpld ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) )
15 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
16 ffun ⊢ ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ → Fun 𝐹 )
17 4 15 16 3syl ⊢ ( 𝜑 → Fun 𝐹 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → Fun 𝐹 )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
20 fdm ⊢ ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ → dom 𝐹 = ( 𝐴 [,] 𝐵 ) )
21 4 15 20 3syl ⊢ ( 𝜑 → dom 𝐹 = ( 𝐴 [,] 𝐵 ) )
22 21 eqcomd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
24 19 23 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦 ∈ dom 𝐹 )
25 fvco ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
26 18 24 25 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
27 26 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
28 17 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → Fun 𝐹 )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
30 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
31 29 30 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ dom 𝐹 )
32 fvco ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
33 28 31 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
35 27 34 breq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
36 35 ralbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
37 36 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
38 14 37 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
39 13 simprd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑤 ) )
40 17 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → Fun 𝐹 )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
42 22 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
43 41 42 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑧 ∈ dom 𝐹 )
44 fvco ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
45 40 43 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
46 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
47 17 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → Fun 𝐹 )
48 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑤 ∈ ( 𝐴 [,] 𝐵 ) )
49 22 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
50 48 49 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑤 ∈ dom 𝐹 )
51 fvco ⊢ ( ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ) → ( ( abs ∘ 𝐹 ) ‘ 𝑤 ) = ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) )
52 47 50 51 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑤 ) = ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) )
53 52 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑤 ) = ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) )
54 46 53 breq12d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑤 ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
55 54 ralbidva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑤 ) ↔ ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
56 55 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑤 ) ↔ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
57 39 56 mpbid ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) )
58 38 57 jca ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ) )