Metamath Proof Explorer

Theorem ioccncflimc

Description: Limit at the upper bound of a continuous function defined on a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ioccncflimc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
ioccncflimc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ioccncflimc.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
ioccncflimc.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,] 𝐵 ) –cn→ ℂ ) )
Assertion ioccncflimc ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ioccncflimc.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 ioccncflimc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ioccncflimc.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 ioccncflimc.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,] 𝐵 ) –cn→ ℂ ) )
5 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
6 2 leidd ⊢ ( 𝜑 → 𝐵 ≤ 𝐵 )
7 1 5 5 3 6 eliocd ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 (,] 𝐵 ) )
8 4 7 cnlimci ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) )
9 cncfrss ⊢ ( 𝐹 ∈ ( ( 𝐴 (,] 𝐵 ) –cn→ ℂ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℂ )
10 4 9 syl ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℂ )
11 ssid ⊢ ℂ ⊆ ℂ
12 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
13 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) )
14 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
15 12 13 14 cncfcn ⊢ ( ( ( 𝐴 (,] 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 (,] 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) )
16 10 11 15 sylancl ⊢ ( 𝜑 → ( ( 𝐴 (,] 𝐵 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) )
17 4 16 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) )
18 12 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
19 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 (,] 𝐵 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,] 𝐵 ) ) )
20 18 10 19 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,] 𝐵 ) ) )
21 12 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
22 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
23 22 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
24 21 23 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
25 24 cnfldtopon ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ∈ ( TopOn ‘ ℂ )
26 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 (,] 𝐵 ) ) ∧ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ∈ ( TopOn ‘ ℂ ) ) → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) ↔ ( 𝐹 : ( 𝐴 (,] 𝐵 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 (,] 𝐵 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) ‘ 𝑥 ) ) ) )
27 20 25 26 sylancl ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) ↔ ( 𝐹 : ( 𝐴 (,] 𝐵 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 (,] 𝐵 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) ‘ 𝑥 ) ) ) )
28 17 27 mpbid ⊢ ( 𝜑 → ( 𝐹 : ( 𝐴 (,] 𝐵 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 (,] 𝐵 ) 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) ) ‘ 𝑥 ) ) )
29 28 simpld ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,] 𝐵 ) ⟶ ℂ )
30 ioossioc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,] 𝐵 )
31 30 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,] 𝐵 ) )
32 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,] 𝐵 ) ∪ { 𝐵 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,] 𝐵 ) ∪ { 𝐵 } ) )
33 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
34 22 ntrtop ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℂ ) = ℂ )
35 21 34 ax-mp ⊢ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℂ ) = ℂ
36 undif ⊢ ( ( 𝐴 (,] 𝐵 ) ⊆ ℂ ↔ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℂ ∖ ( 𝐴 (,] 𝐵 ) ) ) = ℂ )
37 10 36 sylib ⊢ ( 𝜑 → ( ( 𝐴 (,] 𝐵 ) ∪ ( ℂ ∖ ( 𝐴 (,] 𝐵 ) ) ) = ℂ )
38 37 eqcomd ⊢ ( 𝜑 → ℂ = ( ( 𝐴 (,] 𝐵 ) ∪ ( ℂ ∖ ( 𝐴 (,] 𝐵 ) ) ) )
39 38 fveq2d ⊢ ( 𝜑 → ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ℂ ) = ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℂ ∖ ( 𝐴 (,] 𝐵 ) ) ) ) )
40 35 39 eqtr3id ⊢ ( 𝜑 → ℂ = ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℂ ∖ ( 𝐴 (,] 𝐵 ) ) ) ) )
41 33 40 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℂ ∖ ( 𝐴 (,] 𝐵 ) ) ) ) )
42 41 7 elind ⊢ ( 𝜑 → 𝐵 ∈ ( ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℂ ∖ ( 𝐴 (,] 𝐵 ) ) ) ) ∩ ( 𝐴 (,] 𝐵 ) ) )
43 21 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
44 ssid ⊢ ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 (,] 𝐵 )
45 44 a1i ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 (,] 𝐵 ) )
46 22 13 restntr ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐴 (,] 𝐵 ) ⊆ ℂ ∧ ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 (,] 𝐵 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) ) ‘ ( 𝐴 (,] 𝐵 ) ) = ( ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℂ ∖ ( 𝐴 (,] 𝐵 ) ) ) ) ∩ ( 𝐴 (,] 𝐵 ) ) )
47 43 10 45 46 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) ) ‘ ( 𝐴 (,] 𝐵 ) ) = ( ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℂ ∖ ( 𝐴 (,] 𝐵 ) ) ) ) ∩ ( 𝐴 (,] 𝐵 ) ) )
48 42 47 eleqtrrd ⊢ ( 𝜑 → 𝐵 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) ) ‘ ( 𝐴 (,] 𝐵 ) ) )
49 7 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ ( 𝐴 (,] 𝐵 ) )
50 ssequn2 ⊢ ( { 𝐵 } ⊆ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐴 (,] 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
51 49 50 sylib ⊢ ( 𝜑 → ( ( 𝐴 (,] 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
52 51 eqcomd ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) = ( ( 𝐴 (,] 𝐵 ) ∪ { 𝐵 } ) )
53 52 oveq2d ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,] 𝐵 ) ∪ { 𝐵 } ) ) )
54 53 fveq2d ⊢ ( 𝜑 → ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) ) = ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,] 𝐵 ) ∪ { 𝐵 } ) ) ) )
55 ioounsn ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
56 1 5 3 55 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
57 56 eqcomd ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) )
58 54 57 fveq12d ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 (,] 𝐵 ) ) ) ‘ ( 𝐴 (,] 𝐵 ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,] 𝐵 ) ∪ { 𝐵 } ) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) )
59 48 58 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,] 𝐵 ) ∪ { 𝐵 } ) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) )
60 29 31 10 12 32 59 limcres ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) = ( 𝐹 limℂ 𝐵 ) )
61 8 60 eleqtrrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) )