Step | Hyp | Ref
| Expression |
1 | | limcresiooub.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
ℝ*) |
2 | | limcresiooub.cled |
. . . . . 6
⊢ (𝜑 → 𝐷 ≤ 𝐵) |
3 | | iooss1 12415 |
. . . . . 6
⊢ ((𝐷 ∈ ℝ*
∧ 𝐷 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐷(,)𝐶)) |
4 | 1, 2, 3 | syl2anc 565 |
. . . . 5
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐷(,)𝐶)) |
5 | 4 | resabs1d 5569 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶)) = (𝐹 ↾ (𝐵(,)𝐶))) |
6 | 5 | eqcomd 2777 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐵(,)𝐶)) = ((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶))) |
7 | 6 | oveq1d 6808 |
. 2
⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐶) = (((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶)) limℂ 𝐶)) |
8 | | limcresiooub.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
9 | | fresin 6213 |
. . . 4
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐷(,)𝐶)):(𝐴 ∩ (𝐷(,)𝐶))⟶ℂ) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐷(,)𝐶)):(𝐴 ∩ (𝐷(,)𝐶))⟶ℂ) |
11 | | limcresiooub.bcss |
. . . 4
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴) |
12 | 11, 4 | ssind 3985 |
. . 3
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐴 ∩ (𝐷(,)𝐶))) |
13 | | inss2 3982 |
. . . . 5
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ⊆ (𝐷(,)𝐶) |
14 | | ioosscn 40237 |
. . . . 5
⊢ (𝐷(,)𝐶) ⊆ ℂ |
15 | 13, 14 | sstri 3761 |
. . . 4
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℂ |
16 | 15 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℂ) |
17 | | eqid 2771 |
. . 3
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
18 | | eqid 2771 |
. . 3
⊢
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
19 | | limcresiooub.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
20 | | limcresiooub.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
21 | 20 | rexrd 10291 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
22 | | limcresiooub.bltc |
. . . . 5
⊢ (𝜑 → 𝐵 < 𝐶) |
23 | | ubioc1 12432 |
. . . . 5
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
< 𝐶) → 𝐶 ∈ (𝐵(,]𝐶)) |
24 | 19, 21, 22, 23 | syl3anc 1476 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐵(,]𝐶)) |
25 | | snunioo2 40252 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
< 𝐶) → ((𝐵(,)𝐶) ∪ {𝐶}) = (𝐵(,]𝐶)) |
26 | 19, 21, 22, 25 | syl3anc 1476 |
. . . . . 6
⊢ (𝜑 → ((𝐵(,)𝐶) ∪ {𝐶}) = (𝐵(,]𝐶)) |
27 | 26 | fveq2d 6336 |
. . . . 5
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘((𝐵(,)𝐶) ∪ {𝐶})) =
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘(𝐵(,]𝐶))) |
28 | 17 | cnfldtop 22807 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈ Top |
29 | | ovex 6823 |
. . . . . . . . . 10
⊢ (𝐷(,)𝐶) ∈ V |
30 | 29 | inex2 4934 |
. . . . . . . . 9
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ∈ V |
31 | | snex 5036 |
. . . . . . . . 9
⊢ {𝐶} ∈ V |
32 | 30, 31 | unex 7103 |
. . . . . . . 8
⊢ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V |
33 | | resttop 21185 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V) →
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top) |
34 | 28, 32, 33 | mp2an 664 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top |
35 | 34 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top) |
36 | | pnfxr 10294 |
. . . . . . . . . . . . . 14
⊢ +∞
∈ ℝ* |
37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → +∞ ∈
ℝ*) |
38 | | xrleid 12188 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤ 𝐵) |
39 | 19, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ≤ 𝐵) |
40 | 20 | ltpnfd 12160 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 < +∞) |
41 | | iocssioo 12469 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ (𝐵 ≤ 𝐵 ∧ 𝐶 < +∞)) → (𝐵(,]𝐶) ⊆ (𝐵(,)+∞)) |
42 | 19, 37, 39, 40, 41 | syl22anc 1477 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ (𝐵(,)+∞)) |
43 | | simpr 471 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝑥 = 𝐶) |
44 | | snidg 4345 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐶 ∈ ℝ → 𝐶 ∈ {𝐶}) |
45 | | elun2 3932 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐶 ∈ {𝐶} → 𝐶 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
46 | 20, 44, 45 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐶 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
47 | 46 | adantr 466 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐶 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
48 | 43, 47 | eqeltrd 2850 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
49 | 48 | adantlr 686 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ 𝑥 = 𝐶) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
50 | | simpll 742 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝜑) |
51 | 19 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 ∈
ℝ*) |
52 | 51 | adantr 466 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐵 ∈
ℝ*) |
53 | 21 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐶 ∈
ℝ*) |
54 | 53 | adantr 466 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ∈
ℝ*) |
55 | | iocssre 12458 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈ ℝ)
→ (𝐵(,]𝐶) ⊆
ℝ) |
56 | 19, 20, 55 | syl2anc 565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ ℝ) |
57 | 56 | sselda 3752 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ℝ) |
58 | 57 | adantr 466 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ ℝ) |
59 | | simpr 471 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ (𝐵(,]𝐶)) |
60 | | iocgtlb 40245 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) |
61 | 51, 53, 59, 60 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) |
62 | 61 | adantr 466 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐵 < 𝑥) |
63 | 20 | ad2antrr 697 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ∈ ℝ) |
64 | | iocleub 40246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) |
65 | 51, 53, 59, 64 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) |
66 | 65 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ≤ 𝐶) |
67 | | neqne 2951 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑥 = 𝐶 → 𝑥 ≠ 𝐶) |
68 | 67 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ≠ 𝐶) |
69 | 68 | necomd 2998 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ≠ 𝑥) |
70 | 58, 63, 66, 69 | leneltd 10393 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 < 𝐶) |
71 | 52, 54, 58, 62, 70 | eliood 40241 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,)𝐶)) |
72 | 12 | sselda 3752 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶))) |
73 | | elun1 3931 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
75 | 50, 71, 74 | syl2anc 565 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
76 | 49, 75 | pm2.61dan 796 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
77 | 76 | ralrimiva 3115 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ (𝐵(,]𝐶)𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
78 | | dfss3 3741 |
. . . . . . . . . . . . 13
⊢ ((𝐵(,]𝐶) ⊆ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ↔ ∀𝑥 ∈ (𝐵(,]𝐶)𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
79 | 77, 78 | sylibr 224 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
80 | 42, 79 | ssind 3985 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
81 | 80 | sseld 3751 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝐵(,]𝐶) → 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))) |
82 | 24 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐶 ∈ (𝐵(,]𝐶)) |
83 | 43, 82 | eqeltrd 2850 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) |
84 | 83 | adantlr 686 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) |
85 | | ioossioc 40234 |
. . . . . . . . . . . . 13
⊢ (𝐵(,)𝐶) ⊆ (𝐵(,]𝐶) |
86 | 19 | ad2antrr 697 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐵 ∈
ℝ*) |
87 | 21 | ad2antrr 697 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ∈
ℝ*) |
88 | | elinel1 3950 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ (𝐵(,)+∞)) |
89 | 88 | elioored 40294 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ ℝ) |
90 | 89 | ad2antlr 698 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ ℝ) |
91 | 36 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → +∞ ∈
ℝ*) |
92 | 88 | ad2antlr 698 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,)+∞)) |
93 | | ioogtlb 40238 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑥 ∈ (𝐵(,)+∞)) → 𝐵 < 𝑥) |
94 | 86, 91, 92, 93 | syl3anc 1476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐵 < 𝑥) |
95 | 1 | ad2antrr 697 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐷 ∈
ℝ*) |
96 | | elinel2 3951 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
97 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑥 = 𝐶 → ¬ 𝑥 = 𝐶) |
98 | | velsn 4332 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝐶} ↔ 𝑥 = 𝐶) |
99 | 97, 98 | sylnibr 318 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑥 = 𝐶 → ¬ 𝑥 ∈ {𝐶}) |
100 | | elunnel2 39720 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∧ ¬ 𝑥 ∈ {𝐶}) → 𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶))) |
101 | 96, 99, 100 | syl2an 575 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶))) |
102 | 13, 101 | sseldi 3750 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐷(,)𝐶)) |
103 | 102 | adantll 685 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐷(,)𝐶)) |
104 | | iooltub 40255 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐷(,)𝐶)) → 𝑥 < 𝐶) |
105 | 95, 87, 103, 104 | syl3anc 1476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 < 𝐶) |
106 | 86, 87, 90, 94, 105 | eliood 40241 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,)𝐶)) |
107 | 85, 106 | sseldi 3750 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) |
108 | 84, 107 | pm2.61dan 796 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) → 𝑥 ∈ (𝐵(,]𝐶)) |
109 | 108 | ex 397 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ (𝐵(,]𝐶))) |
110 | 81, 109 | impbid 202 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐵(,]𝐶) ↔ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))) |
111 | 110 | eqrdv 2769 |
. . . . . . . 8
⊢ (𝜑 → (𝐵(,]𝐶) = ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
112 | | retop 22785 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) ∈ Top |
113 | 112 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (topGen‘ran (,))
∈ Top) |
114 | 32 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V) |
115 | | iooretop 22789 |
. . . . . . . . . 10
⊢ (𝐵(,)+∞) ∈
(topGen‘ran (,)) |
116 | 115 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵(,)+∞) ∈ (topGen‘ran
(,))) |
117 | | elrestr 16297 |
. . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V ∧ (𝐵(,)+∞) ∈ (topGen‘ran (,)))
→ ((𝐵(,)+∞)
∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
118 | 113, 114,
116, 117 | syl3anc 1476 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
119 | 111, 118 | eqeltrd 2850 |
. . . . . . 7
⊢ (𝜑 → (𝐵(,]𝐶) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
120 | 17 | tgioo2 22826 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
121 | 120 | oveq1i 6803 |
. . . . . . . 8
⊢
((topGen‘ran (,)) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) =
(((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
122 | 28 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) |
123 | | ioossre 12440 |
. . . . . . . . . . . 12
⊢ (𝐷(,)𝐶) ⊆ ℝ |
124 | 13, 123 | sstri 3761 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℝ |
125 | 124 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℝ) |
126 | 20 | snssd 4475 |
. . . . . . . . . 10
⊢ (𝜑 → {𝐶} ⊆ ℝ) |
127 | 125, 126 | unssd 3940 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ⊆ ℝ) |
128 | | reex 10229 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
129 | 128 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ∈
V) |
130 | | restabs 21190 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ⊆ ℝ ∧ ℝ ∈ V)
→ (((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
131 | 122, 127,
129, 130 | syl3anc 1476 |
. . . . . . . 8
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
132 | 121, 131 | syl5eq 2817 |
. . . . . . 7
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
133 | 119, 132 | eleqtrd 2852 |
. . . . . 6
⊢ (𝜑 → (𝐵(,]𝐶) ∈
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
134 | | isopn3i 21107 |
. . . . . 6
⊢
((((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top ∧ (𝐵(,]𝐶) ∈
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘(𝐵(,]𝐶)) = (𝐵(,]𝐶)) |
135 | 35, 133, 134 | syl2anc 565 |
. . . . 5
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘(𝐵(,]𝐶)) = (𝐵(,]𝐶)) |
136 | 27, 135 | eqtr2d 2806 |
. . . 4
⊢ (𝜑 → (𝐵(,]𝐶) =
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘((𝐵(,)𝐶) ∪ {𝐶}))) |
137 | 24, 136 | eleqtrd 2852 |
. . 3
⊢ (𝜑 → 𝐶 ∈
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘((𝐵(,)𝐶) ∪ {𝐶}))) |
138 | 10, 12, 16, 17, 18, 137 | limcres 23870 |
. 2
⊢ (𝜑 → (((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶)) limℂ 𝐶) = ((𝐹 ↾ (𝐷(,)𝐶)) limℂ 𝐶)) |
139 | 7, 138 | eqtrd 2805 |
1
⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐶) = ((𝐹 ↾ (𝐷(,)𝐶)) limℂ 𝐶)) |