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