Metamath Proof Explorer


Theorem icocncflimc

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

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

Proof

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