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ℂ 𝐴 ) )