Step | Hyp | Ref
| Expression |
1 | | limcresiooub.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
ℝ*) |
2 | | limcresiooub.cled |
. . . . . 6
⊢ (𝜑 → 𝐷 ≤ 𝐵) |
3 | | iooss1 12210 |
. . . . . 6
⊢ ((𝐷 ∈ ℝ*
∧ 𝐷 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐷(,)𝐶)) |
4 | 1, 2, 3 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐷(,)𝐶)) |
5 | 4 | resabs1d 5428 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶)) = (𝐹 ↾ (𝐵(,)𝐶))) |
6 | 5 | eqcomd 2628 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐵(,)𝐶)) = ((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶))) |
7 | 6 | oveq1d 6665 |
. 2
⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐶) = (((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶)) limℂ 𝐶)) |
8 | | limcresiooub.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
9 | | fresin 6073 |
. . . 4
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐷(,)𝐶)):(𝐴 ∩ (𝐷(,)𝐶))⟶ℂ) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐷(,)𝐶)):(𝐴 ∩ (𝐷(,)𝐶))⟶ℂ) |
11 | | limcresiooub.bcss |
. . . 4
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴) |
12 | 11, 4 | ssind 3837 |
. . 3
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐴 ∩ (𝐷(,)𝐶))) |
13 | | inss2 3834 |
. . . . 5
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ⊆ (𝐷(,)𝐶) |
14 | | ioosscn 39716 |
. . . . 5
⊢ (𝐷(,)𝐶) ⊆ ℂ |
15 | 13, 14 | sstri 3612 |
. . . 4
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℂ |
16 | 15 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℂ) |
17 | | eqid 2622 |
. . 3
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
18 | | eqid 2622 |
. . 3
⊢
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
19 | | limcresiooub.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
20 | | limcresiooub.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
21 | 20 | rexrd 10089 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
22 | | limcresiooub.bltc |
. . . . 5
⊢ (𝜑 → 𝐵 < 𝐶) |
23 | | ubioc1 12227 |
. . . . 5
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
< 𝐶) → 𝐶 ∈ (𝐵(,]𝐶)) |
24 | 19, 21, 22, 23 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐵(,]𝐶)) |
25 | | snunioo2 39731 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
< 𝐶) → ((𝐵(,)𝐶) ∪ {𝐶}) = (𝐵(,]𝐶)) |
26 | 19, 21, 22, 25 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → ((𝐵(,)𝐶) ∪ {𝐶}) = (𝐵(,]𝐶)) |
27 | 26 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘((𝐵(,)𝐶) ∪ {𝐶})) =
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘(𝐵(,]𝐶))) |
28 | 17 | cnfldtop 22587 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈ Top |
29 | | ovex 6678 |
. . . . . . . . . 10
⊢ (𝐷(,)𝐶) ∈ V |
30 | 29 | inex2 4800 |
. . . . . . . . 9
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ∈ V |
31 | | snex 4908 |
. . . . . . . . 9
⊢ {𝐶} ∈ V |
32 | 30, 31 | unex 6956 |
. . . . . . . 8
⊢ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V |
33 | | resttop 20964 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V) →
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top) |
34 | 28, 32, 33 | mp2an 708 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top |
35 | 34 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top) |
36 | | pnfxr 10092 |
. . . . . . . . . . . . . 14
⊢ +∞
∈ ℝ* |
37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → +∞ ∈
ℝ*) |
38 | | xrleid 11983 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤ 𝐵) |
39 | 19, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ≤ 𝐵) |
40 | 20 | ltpnfd 11955 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 < +∞) |
41 | | iocssioo 12263 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ (𝐵 ≤ 𝐵 ∧ 𝐶 < +∞)) → (𝐵(,]𝐶) ⊆ (𝐵(,)+∞)) |
42 | 19, 37, 39, 40, 41 | syl22anc 1327 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ (𝐵(,)+∞)) |
43 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝑥 = 𝐶) |
44 | | snidg 4206 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐶 ∈ ℝ → 𝐶 ∈ {𝐶}) |
45 | | elun2 3781 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐶 ∈ {𝐶} → 𝐶 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
46 | 20, 44, 45 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐶 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐶 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
48 | 43, 47 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
49 | 48 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ 𝑥 = 𝐶) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
50 | | simpll 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝜑) |
51 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 ∈
ℝ*) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐵 ∈
ℝ*) |
53 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐶 ∈
ℝ*) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ∈
ℝ*) |
55 | | iocssre 12253 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈ ℝ)
→ (𝐵(,]𝐶) ⊆
ℝ) |
56 | 19, 20, 55 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ ℝ) |
57 | 56 | sselda 3603 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ℝ) |
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ ℝ) |
59 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ (𝐵(,]𝐶)) |
60 | | iocgtlb 39724 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) |
61 | 51, 53, 59, 60 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐵 < 𝑥) |
63 | 20 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ∈ ℝ) |
64 | | iocleub 39725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) |
65 | 51, 53, 59, 64 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ≤ 𝐶) |
67 | | neqne 2802 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑥 = 𝐶 → 𝑥 ≠ 𝐶) |
68 | 67 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ≠ 𝐶) |
69 | 68 | necomd 2849 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ≠ 𝑥) |
70 | 58, 63, 66, 69 | leneltd 10191 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 < 𝐶) |
71 | 52, 54, 58, 62, 70 | eliood 39720 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,)𝐶)) |
72 | 12 | sselda 3603 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶))) |
73 | | elun1 3780 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
75 | 50, 71, 74 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
76 | 49, 75 | pm2.61dan 832 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
77 | 76 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ (𝐵(,]𝐶)𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
78 | | dfss3 3592 |
. . . . . . . . . . . . 13
⊢ ((𝐵(,]𝐶) ⊆ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ↔ ∀𝑥 ∈ (𝐵(,]𝐶)𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
79 | 77, 78 | sylibr 224 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
80 | 42, 79 | ssind 3837 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
81 | 80 | sseld 3602 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝐵(,]𝐶) → 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))) |
82 | 24 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐶 ∈ (𝐵(,]𝐶)) |
83 | 43, 82 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) |
84 | 83 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) |
85 | | ioossioc 39713 |
. . . . . . . . . . . . 13
⊢ (𝐵(,)𝐶) ⊆ (𝐵(,]𝐶) |
86 | 19 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐵 ∈
ℝ*) |
87 | 21 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ∈
ℝ*) |
88 | | elinel1 3799 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ (𝐵(,)+∞)) |
89 | 88 | elioored 39776 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ ℝ) |
90 | 89 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ ℝ) |
91 | 36 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → +∞ ∈
ℝ*) |
92 | 88 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,)+∞)) |
93 | | ioogtlb 39717 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑥 ∈ (𝐵(,)+∞)) → 𝐵 < 𝑥) |
94 | 86, 91, 92, 93 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐵 < 𝑥) |
95 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐷 ∈
ℝ*) |
96 | | elinel2 3800 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
97 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑥 = 𝐶 → ¬ 𝑥 = 𝐶) |
98 | | velsn 4193 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝐶} ↔ 𝑥 = 𝐶) |
99 | 97, 98 | sylnibr 319 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑥 = 𝐶 → ¬ 𝑥 ∈ {𝐶}) |
100 | | elunnel2 39198 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∧ ¬ 𝑥 ∈ {𝐶}) → 𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶))) |
101 | 96, 99, 100 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶))) |
102 | 13, 101 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐷(,)𝐶)) |
103 | 102 | adantll 750 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐷(,)𝐶)) |
104 | | iooltub 39735 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐷(,)𝐶)) → 𝑥 < 𝐶) |
105 | 95, 87, 103, 104 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 < 𝐶) |
106 | 86, 87, 90, 94, 105 | eliood 39720 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,)𝐶)) |
107 | 85, 106 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) |
108 | 84, 107 | pm2.61dan 832 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) → 𝑥 ∈ (𝐵(,]𝐶)) |
109 | 108 | ex 450 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ (𝐵(,]𝐶))) |
110 | 81, 109 | impbid 202 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐵(,]𝐶) ↔ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))) |
111 | 110 | eqrdv 2620 |
. . . . . . . 8
⊢ (𝜑 → (𝐵(,]𝐶) = ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
112 | | retop 22565 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) ∈ Top |
113 | 112 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (topGen‘ran (,))
∈ Top) |
114 | 32 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V) |
115 | | iooretop 22569 |
. . . . . . . . . 10
⊢ (𝐵(,)+∞) ∈
(topGen‘ran (,)) |
116 | 115 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵(,)+∞) ∈ (topGen‘ran
(,))) |
117 | | elrestr 16089 |
. . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V ∧ (𝐵(,)+∞) ∈ (topGen‘ran (,)))
→ ((𝐵(,)+∞)
∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
118 | 113, 114,
116, 117 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
119 | 111, 118 | eqeltrd 2701 |
. . . . . . 7
⊢ (𝜑 → (𝐵(,]𝐶) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
120 | 17 | tgioo2 22606 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
121 | 120 | oveq1i 6660 |
. . . . . . . 8
⊢
((topGen‘ran (,)) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) =
(((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
122 | 28 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) |
123 | | ioossre 12235 |
. . . . . . . . . . . 12
⊢ (𝐷(,)𝐶) ⊆ ℝ |
124 | 13, 123 | sstri 3612 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℝ |
125 | 124 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℝ) |
126 | 20 | snssd 4340 |
. . . . . . . . . 10
⊢ (𝜑 → {𝐶} ⊆ ℝ) |
127 | 125, 126 | unssd 3789 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ⊆ ℝ) |
128 | | reex 10027 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
129 | 128 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ∈
V) |
130 | | restabs 20969 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ⊆ ℝ ∧ ℝ ∈ V)
→ (((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
131 | 122, 127,
129, 130 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
132 | 121, 131 | syl5eq 2668 |
. . . . . . 7
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
133 | 119, 132 | eleqtrd 2703 |
. . . . . 6
⊢ (𝜑 → (𝐵(,]𝐶) ∈
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
134 | | isopn3i 20886 |
. . . . . 6
⊢
((((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top ∧ (𝐵(,]𝐶) ∈
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘(𝐵(,]𝐶)) = (𝐵(,]𝐶)) |
135 | 35, 133, 134 | syl2anc 693 |
. . . . 5
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘(𝐵(,]𝐶)) = (𝐵(,]𝐶)) |
136 | 27, 135 | eqtr2d 2657 |
. . . 4
⊢ (𝜑 → (𝐵(,]𝐶) =
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘((𝐵(,)𝐶) ∪ {𝐶}))) |
137 | 24, 136 | eleqtrd 2703 |
. . 3
⊢ (𝜑 → 𝐶 ∈
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘((𝐵(,)𝐶) ∪ {𝐶}))) |
138 | 10, 12, 16, 17, 18, 137 | limcres 23650 |
. 2
⊢ (𝜑 → (((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶)) limℂ 𝐶) = ((𝐹 ↾ (𝐷(,)𝐶)) limℂ 𝐶)) |
139 | 7, 138 | eqtrd 2656 |
1
⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐶) = ((𝐹 ↾ (𝐷(,)𝐶)) limℂ 𝐶)) |