| Step | Hyp | Ref
| Expression |
| 1 | | limcresiooub.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
ℝ*) |
| 2 | | limcresiooub.cled |
. . . . . 6
⊢ (𝜑 → 𝐷 ≤ 𝐵) |
| 3 | | iooss1 13422 |
. . . . . 6
⊢ ((𝐷 ∈ ℝ*
∧ 𝐷 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐷(,)𝐶)) |
| 4 | 1, 2, 3 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐷(,)𝐶)) |
| 5 | 4 | resabs1d 6026 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶)) = (𝐹 ↾ (𝐵(,)𝐶))) |
| 6 | 5 | eqcomd 2743 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐵(,)𝐶)) = ((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶))) |
| 7 | 6 | oveq1d 7446 |
. 2
⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐶) = (((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶)) limℂ 𝐶)) |
| 8 | | limcresiooub.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
| 9 | | fresin 6777 |
. . . 4
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐷(,)𝐶)):(𝐴 ∩ (𝐷(,)𝐶))⟶ℂ) |
| 10 | 8, 9 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐷(,)𝐶)):(𝐴 ∩ (𝐷(,)𝐶))⟶ℂ) |
| 11 | | limcresiooub.bcss |
. . . 4
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴) |
| 12 | 11, 4 | ssind 4241 |
. . 3
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐴 ∩ (𝐷(,)𝐶))) |
| 13 | | inss2 4238 |
. . . . 5
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ⊆ (𝐷(,)𝐶) |
| 14 | | ioosscn 13449 |
. . . . 5
⊢ (𝐷(,)𝐶) ⊆ ℂ |
| 15 | 13, 14 | sstri 3993 |
. . . 4
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℂ |
| 16 | 15 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℂ) |
| 17 | | eqid 2737 |
. . 3
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 18 | | eqid 2737 |
. . 3
⊢
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 19 | | limcresiooub.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 20 | | limcresiooub.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 21 | 20 | rexrd 11311 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
| 22 | | limcresiooub.bltc |
. . . . 5
⊢ (𝜑 → 𝐵 < 𝐶) |
| 23 | | ubioc1 13440 |
. . . . 5
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
< 𝐶) → 𝐶 ∈ (𝐵(,]𝐶)) |
| 24 | 19, 21, 22, 23 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐵(,]𝐶)) |
| 25 | | ioounsn 13517 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
< 𝐶) → ((𝐵(,)𝐶) ∪ {𝐶}) = (𝐵(,]𝐶)) |
| 26 | 19, 21, 22, 25 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → ((𝐵(,)𝐶) ∪ {𝐶}) = (𝐵(,]𝐶)) |
| 27 | 26 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘((𝐵(,)𝐶) ∪ {𝐶})) =
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘(𝐵(,]𝐶))) |
| 28 | 17 | cnfldtop 24804 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈ Top |
| 29 | | ovex 7464 |
. . . . . . . . . 10
⊢ (𝐷(,)𝐶) ∈ V |
| 30 | 29 | inex2 5318 |
. . . . . . . . 9
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ∈ V |
| 31 | | snex 5436 |
. . . . . . . . 9
⊢ {𝐶} ∈ V |
| 32 | 30, 31 | unex 7764 |
. . . . . . . 8
⊢ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V |
| 33 | | resttop 23168 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V) →
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top) |
| 34 | 28, 32, 33 | mp2an 692 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top |
| 35 | 34 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top) |
| 36 | | pnfxr 11315 |
. . . . . . . . . . . . . 14
⊢ +∞
∈ ℝ* |
| 37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → +∞ ∈
ℝ*) |
| 38 | 19 | xrleidd 13194 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ≤ 𝐵) |
| 39 | 20 | ltpnfd 13163 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 < +∞) |
| 40 | | iocssioo 13479 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ (𝐵 ≤ 𝐵 ∧ 𝐶 < +∞)) → (𝐵(,]𝐶) ⊆ (𝐵(,)+∞)) |
| 41 | 19, 37, 38, 39, 40 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ (𝐵(,)+∞)) |
| 42 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝑥 = 𝐶) |
| 43 | | snidg 4660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐶 ∈ ℝ → 𝐶 ∈ {𝐶}) |
| 44 | | elun2 4183 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐶 ∈ {𝐶} → 𝐶 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 45 | 20, 43, 44 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐶 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐶 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 47 | 42, 46 | eqeltrd 2841 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 48 | 47 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ 𝑥 = 𝐶) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 49 | | simpll 767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝜑) |
| 50 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 ∈
ℝ*) |
| 51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐵 ∈
ℝ*) |
| 52 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐶 ∈
ℝ*) |
| 53 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ∈
ℝ*) |
| 54 | | iocssre 13467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈ ℝ)
→ (𝐵(,]𝐶) ⊆
ℝ) |
| 55 | 19, 20, 54 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ ℝ) |
| 56 | 55 | sselda 3983 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ℝ) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ ℝ) |
| 58 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ (𝐵(,]𝐶)) |
| 59 | | iocgtlb 45515 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) |
| 60 | 50, 52, 58, 59 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝐵 < 𝑥) |
| 61 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐵 < 𝑥) |
| 62 | 20 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ∈ ℝ) |
| 63 | | iocleub 45516 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) |
| 64 | 50, 52, 58, 63 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ≤ 𝐶) |
| 65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ≤ 𝐶) |
| 66 | | neqne 2948 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑥 = 𝐶 → 𝑥 ≠ 𝐶) |
| 67 | 66 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ≠ 𝐶) |
| 68 | 67 | necomd 2996 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ≠ 𝑥) |
| 69 | 57, 62, 65, 68 | leneltd 11415 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 < 𝐶) |
| 70 | 51, 53, 57, 61, 69 | eliood 45511 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,)𝐶)) |
| 71 | 12 | sselda 3983 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶))) |
| 72 | | elun1 4182 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 74 | 49, 70, 73 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 75 | 48, 74 | pm2.61dan 813 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,]𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 76 | 75 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ (𝐵(,]𝐶)𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 77 | | dfss3 3972 |
. . . . . . . . . . . . 13
⊢ ((𝐵(,]𝐶) ⊆ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ↔ ∀𝑥 ∈ (𝐵(,]𝐶)𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 78 | 76, 77 | sylibr 234 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 79 | 41, 78 | ssind 4241 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵(,]𝐶) ⊆ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
| 80 | 79 | sseld 3982 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝐵(,]𝐶) → 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))) |
| 81 | 24 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐶 ∈ (𝐵(,]𝐶)) |
| 82 | 42, 81 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) |
| 83 | 82 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) |
| 84 | | ioossioc 45505 |
. . . . . . . . . . . . 13
⊢ (𝐵(,)𝐶) ⊆ (𝐵(,]𝐶) |
| 85 | 19 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐵 ∈
ℝ*) |
| 86 | 21 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐶 ∈
ℝ*) |
| 87 | | elinel1 4201 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ (𝐵(,)+∞)) |
| 88 | 87 | elioored 45562 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ ℝ) |
| 89 | 88 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ ℝ) |
| 90 | 36 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → +∞ ∈
ℝ*) |
| 91 | 87 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,)+∞)) |
| 92 | | ioogtlb 45508 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑥 ∈ (𝐵(,)+∞)) → 𝐵 < 𝑥) |
| 93 | 85, 90, 91, 92 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐵 < 𝑥) |
| 94 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝐷 ∈
ℝ*) |
| 95 | | elinel2 4202 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 96 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑥 = 𝐶 → ¬ 𝑥 = 𝐶) |
| 97 | | velsn 4642 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝐶} ↔ 𝑥 = 𝐶) |
| 98 | 96, 97 | sylnibr 329 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑥 = 𝐶 → ¬ 𝑥 ∈ {𝐶}) |
| 99 | | elunnel2 4155 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∧ ¬ 𝑥 ∈ {𝐶}) → 𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶))) |
| 100 | 95, 98, 99 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐴 ∩ (𝐷(,)𝐶))) |
| 101 | 13, 100 | sselid 3981 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐷(,)𝐶)) |
| 102 | 101 | adantll 714 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐷(,)𝐶)) |
| 103 | | iooltub 45523 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐷(,)𝐶)) → 𝑥 < 𝐶) |
| 104 | 94, 86, 102, 103 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 < 𝐶) |
| 105 | 85, 86, 89, 93, 104 | eliood 45511 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,)𝐶)) |
| 106 | 84, 105 | sselid 3981 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) ∧ ¬ 𝑥 = 𝐶) → 𝑥 ∈ (𝐵(,]𝐶)) |
| 107 | 83, 106 | pm2.61dan 813 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) → 𝑥 ∈ (𝐵(,]𝐶)) |
| 108 | 107 | ex 412 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) → 𝑥 ∈ (𝐵(,]𝐶))) |
| 109 | 80, 108 | impbid 212 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐵(,]𝐶) ↔ 𝑥 ∈ ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))) |
| 110 | 109 | eqrdv 2735 |
. . . . . . . 8
⊢ (𝜑 → (𝐵(,]𝐶) = ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
| 111 | | retop 24782 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) ∈ Top |
| 112 | 111 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (topGen‘ran (,))
∈ Top) |
| 113 | 32 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V) |
| 114 | | iooretop 24786 |
. . . . . . . . . 10
⊢ (𝐵(,)+∞) ∈
(topGen‘ran (,)) |
| 115 | 114 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵(,)+∞) ∈ (topGen‘ran
(,))) |
| 116 | | elrestr 17473 |
. . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ∈ V ∧ (𝐵(,)+∞) ∈ (topGen‘ran (,)))
→ ((𝐵(,)+∞)
∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
| 117 | 112, 113,
115, 116 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵(,)+∞) ∩ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
| 118 | 110, 117 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝜑 → (𝐵(,]𝐶) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
| 119 | | tgioo4 24826 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 120 | 119 | oveq1i 7441 |
. . . . . . . 8
⊢
((topGen‘ran (,)) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) =
(((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) |
| 121 | 28 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) |
| 122 | | ioossre 13448 |
. . . . . . . . . . . 12
⊢ (𝐷(,)𝐶) ⊆ ℝ |
| 123 | 13, 122 | sstri 3993 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℝ |
| 124 | 123 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∩ (𝐷(,)𝐶)) ⊆ ℝ) |
| 125 | 20 | snssd 4809 |
. . . . . . . . . 10
⊢ (𝜑 → {𝐶} ⊆ ℝ) |
| 126 | 124, 125 | unssd 4192 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ⊆ ℝ) |
| 127 | | reex 11246 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
| 128 | 127 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ∈
V) |
| 129 | | restabs 23173 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}) ⊆ ℝ ∧ ℝ ∈ V)
→ (((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
| 130 | 121, 126,
128, 129 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
| 131 | 120, 130 | eqtrid 2789 |
. . . . . . 7
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
| 132 | 118, 131 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → (𝐵(,]𝐶) ∈
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) |
| 133 | | isopn3i 23090 |
. . . . . 6
⊢
((((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})) ∈ Top ∧ (𝐵(,]𝐶) ∈
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶}))) →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘(𝐵(,]𝐶)) = (𝐵(,]𝐶)) |
| 134 | 35, 132, 133 | syl2anc 584 |
. . . . 5
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘(𝐵(,]𝐶)) = (𝐵(,]𝐶)) |
| 135 | 27, 134 | eqtr2d 2778 |
. . . 4
⊢ (𝜑 → (𝐵(,]𝐶) =
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘((𝐵(,)𝐶) ∪ {𝐶}))) |
| 136 | 24, 135 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 𝐶 ∈
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐷(,)𝐶)) ∪ {𝐶})))‘((𝐵(,)𝐶) ∪ {𝐶}))) |
| 137 | 10, 12, 16, 17, 18, 136 | limcres 25921 |
. 2
⊢ (𝜑 → (((𝐹 ↾ (𝐷(,)𝐶)) ↾ (𝐵(,)𝐶)) limℂ 𝐶) = ((𝐹 ↾ (𝐷(,)𝐶)) limℂ 𝐶)) |
| 138 | 7, 137 | eqtrd 2777 |
1
⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐶) = ((𝐹 ↾ (𝐷(,)𝐶)) limℂ 𝐶)) |