Metamath Proof Explorer

Theorem cniccbdd

Description: A continuous function on a closed interval is bounded. (Contributed by Mario Carneiro, 7-Sep-2014)

Ref Expression
Assertion cniccbdd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 ral0 ⊢ ∀ 𝑦 ∈ ∅ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 0
3 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐴 ∈ ℝ )
4 3 rexrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐴 ∈ ℝ* )
5 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐵 ∈ ℝ )
6 5 rexrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐵 ∈ ℝ* )
7 icc0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
8 4 6 7 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
9 8 biimpar ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝐵 < 𝐴 ) → ( 𝐴 [,] 𝐵 ) = ∅ )
10 9 raleqdv ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝐵 < 𝐴 ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 0 ↔ ∀ 𝑦 ∈ ∅ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 0 ) )
11 2 10 mpbiri ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝐵 < 𝐴 ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 0 )
12 brralrspcev ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 0 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
13 1 11 12 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝐵 < 𝐴 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
14 3 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ )
15 5 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
16 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
17 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
18 abscncf ⊢ abs ∈ ( ℂ –cn→ ℝ )
19 18 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → abs ∈ ( ℂ –cn→ ℝ ) )
20 17 19 cncfco ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( abs ∘ 𝐹 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
21 20 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝐴 ≤ 𝐵 ) → ( abs ∘ 𝐹 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
22 14 15 16 21 evthicc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝐴 ≤ 𝐵 ) → ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ) )
23 22 simpld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝐴 ≤ 𝐵 ) → ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) )
24 cncff ⊢ ( ( abs ∘ 𝐹 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → ( abs ∘ 𝐹 ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
25 20 24 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( abs ∘ 𝐹 ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
26 25 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ∈ ℝ )
27 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
28 17 27 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
29 28 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
30 fvco3 ⊢ ( ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
31 29 30 sylan ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
32 31 breq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ) )
33 32 ralbidva ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ↔ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ) )
34 33 biimpd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ) )
35 brralrspcev ⊢ ( ( ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
36 26 34 35 syl6an ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) )
37 36 rexlimdva ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) )
38 37 imp ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑧 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
39 23 38 syldan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) ∧ 𝐴 ≤ 𝐵 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
40 13 39 5 3 ltlecasei ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )