Metamath Proof Explorer

Theorem cncfioobd

Description: A continuous function F on an open interval ( A (,) B ) with a finite right limit R in A and a finite left limit L in B is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfioobd.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
cncfioobd.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
cncfioobd.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
cncfioobd.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
cncfioobd.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 limℂ 𝐴 ) )
Assertion cncfioobd ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )

Proof

Step Hyp Ref Expression
1 cncfioobd.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 cncfioobd.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 cncfioobd.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
4 cncfioobd.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
5 cncfioobd.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 limℂ 𝐴 ) )
6 nfv ⊢ Ⅎ 𝑧 𝜑
7 eqid ⊢ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) )
8 6 7 1 2 3 4 5 cncfiooicc ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
9 cniccbdd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 )
10 1 2 8 9 syl3anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 )
11 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ ℝ )
12 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥
13 11 12 nfan ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ( 𝐴 (,) 𝐵 ) )
15 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
16 3 15 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
17 16 fdmd ⊢ ( 𝜑 → dom 𝐹 = ( 𝐴 (,) 𝐵 ) )
18 17 eqcomd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) = dom 𝐹 )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) = dom 𝐹 )
20 14 19 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ dom 𝐹 )
21 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → 𝐴 ∈ ℝ )
22 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → 𝐵 ∈ ℝ )
23 16 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → 𝑦 ∈ dom 𝐹 )
25 17 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → dom 𝐹 = ( 𝐴 (,) 𝐵 ) )
26 24 25 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → 𝑦 ∈ ( 𝐴 (,) 𝐵 ) )
27 21 22 23 7 26 cncfioobdlem ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
28 20 27 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
29 28 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) = ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) )
30 29 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) = ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) )
31 30 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) = ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) )
32 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 )
33 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
34 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ( 𝐴 (,) 𝐵 ) )
35 33 34 sseldi ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
36 rspa ⊢ ( ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 )
37 32 35 36 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 )
38 31 37 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
39 38 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) )
40 13 39 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
41 40 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) )
42 41 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑧 = 𝐴 , 𝑅 , if ( 𝑧 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ) ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) )
43 10 42 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )