| Step | Hyp | Ref
| Expression |
| 1 | | limcicciooub.4 |
. 2
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
| 2 | | ioossicc 13473 |
. . 3
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
| 4 | | limcicciooub.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 5 | | limcicciooub.2 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 6 | 4, 5 | iccssred 13474 |
. . 3
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
| 7 | | ax-resscn 11212 |
. . 3
⊢ ℝ
⊆ ℂ |
| 8 | 6, 7 | sstrdi 3996 |
. 2
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
| 9 | | eqid 2737 |
. 2
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 10 | | eqid 2737 |
. 2
⊢
((TopOpen‘ℂfld) ↾t ((𝐴[,]𝐵) ∪ {𝐵})) = ((TopOpen‘ℂfld)
↾t ((𝐴[,]𝐵) ∪ {𝐵})) |
| 11 | | retop 24782 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
| 12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (topGen‘ran (,))
∈ Top) |
| 13 | 4 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 14 | | iocssre 13467 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴(,]𝐵) ⊆
ℝ) |
| 15 | 13, 5, 14 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ) |
| 16 | | difssd 4137 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ ∖ (𝐴[,]𝐵)) ⊆ ℝ) |
| 17 | 15, 16 | unssd 4192 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ) |
| 18 | | uniretop 24783 |
. . . . . . . . 9
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 19 | 17, 18 | sseqtrdi 4024 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ∪
(topGen‘ran (,))) |
| 20 | | elioore 13417 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐴(,)+∞) → 𝑥 ∈ ℝ) |
| 21 | 20 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ 𝑥 ≤ 𝐵) → 𝑥 ∈ ℝ) |
| 22 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ 𝑥 ≤ 𝐵) → 𝑥 ∈ (𝐴(,)+∞)) |
| 23 | 13 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ 𝑥 ≤ 𝐵) → 𝐴 ∈
ℝ*) |
| 24 | | pnfxr 11315 |
. . . . . . . . . . . . . . . . 17
⊢ +∞
∈ ℝ* |
| 25 | | elioo2 13428 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞))) |
| 26 | 23, 24, 25 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ 𝑥 ≤ 𝐵) → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞))) |
| 27 | 22, 26 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ 𝑥 ≤ 𝐵) → (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞)) |
| 28 | 27 | simp2d 1144 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ 𝑥 ≤ 𝐵) → 𝐴 < 𝑥) |
| 29 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ 𝑥 ≤ 𝐵) → 𝑥 ≤ 𝐵) |
| 30 | 5 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ 𝑥 ≤ 𝐵) → 𝐵 ∈ ℝ) |
| 31 | | elioc2 13450 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝑥 ∈ (𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) |
| 32 | 23, 30, 31 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ 𝑥 ≤ 𝐵) → (𝑥 ∈ (𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) |
| 33 | 21, 28, 29, 32 | mpbir3and 1343 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ 𝑥 ≤ 𝐵) → 𝑥 ∈ (𝐴(,]𝐵)) |
| 34 | 33 | orcd 874 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ 𝑥 ≤ 𝐵) → (𝑥 ∈ (𝐴(,]𝐵) ∨ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)))) |
| 35 | 20 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ ¬ 𝑥 ≤ 𝐵) → 𝑥 ∈ ℝ) |
| 36 | | 3mix3 1333 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 ≤ 𝐵 → (¬ 𝑥 ∈ ℝ ∨ ¬ 𝐴 ≤ 𝑥 ∨ ¬ 𝑥 ≤ 𝐵)) |
| 37 | | 3ianor 1107 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝑥 ∈ ℝ ∧
𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵) ↔ (¬ 𝑥 ∈ ℝ ∨ ¬ 𝐴 ≤ 𝑥 ∨ ¬ 𝑥 ≤ 𝐵)) |
| 38 | 36, 37 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 ≤ 𝐵 → ¬ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
| 39 | 38 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ ¬ 𝑥 ≤ 𝐵) → ¬ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
| 40 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ ¬ 𝑥 ≤ 𝐵) → 𝐴 ∈ ℝ) |
| 41 | 5 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ ¬ 𝑥 ≤ 𝐵) → 𝐵 ∈ ℝ) |
| 42 | | elicc2 13452 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
| 43 | 40, 41, 42 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ ¬ 𝑥 ≤ 𝐵) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
| 44 | 39, 43 | mtbird 325 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ ¬ 𝑥 ≤ 𝐵) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) |
| 45 | 35, 44 | eldifd 3962 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ ¬ 𝑥 ≤ 𝐵) → 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) |
| 46 | 45 | olcd 875 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) ∧ ¬ 𝑥 ≤ 𝐵) → (𝑥 ∈ (𝐴(,]𝐵) ∨ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)))) |
| 47 | 34, 46 | pm2.61dan 813 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) → (𝑥 ∈ (𝐴(,]𝐵) ∨ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)))) |
| 48 | | elun 4153 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ↔ (𝑥 ∈ (𝐴(,]𝐵) ∨ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)))) |
| 49 | 47, 48 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)+∞)) → 𝑥 ∈ ((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) |
| 50 | 49 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)+∞)𝑥 ∈ ((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) |
| 51 | | dfss3 3972 |
. . . . . . . . 9
⊢ ((𝐴(,)+∞) ⊆ ((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ↔ ∀𝑥 ∈ (𝐴(,)+∞)𝑥 ∈ ((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) |
| 52 | 50, 51 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)+∞) ⊆ ((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) |
| 53 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ (topGen‘ran (,)) = ∪
(topGen‘ran (,)) |
| 54 | 53 | ntrss 23063 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ∪
(topGen‘ran (,)) ∧ (𝐴(,)+∞) ⊆ ((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) → ((int‘(topGen‘ran
(,)))‘(𝐴(,)+∞))
⊆ ((int‘(topGen‘ran (,)))‘((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) |
| 55 | 12, 19, 52, 54 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴(,)+∞)) ⊆
((int‘(topGen‘ran (,)))‘((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) |
| 56 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → +∞ ∈
ℝ*) |
| 57 | | limcicciooub.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 < 𝐵) |
| 58 | 5 | ltpnfd 13163 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 < +∞) |
| 59 | 13, 56, 5, 57, 58 | eliood 45511 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (𝐴(,)+∞)) |
| 60 | | iooretop 24786 |
. . . . . . . . 9
⊢ (𝐴(,)+∞) ∈
(topGen‘ran (,)) |
| 61 | | isopn3i 23090 |
. . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ Top ∧ (𝐴(,)+∞) ∈ (topGen‘ran (,)))
→ ((int‘(topGen‘ran (,)))‘(𝐴(,)+∞)) = (𝐴(,)+∞)) |
| 62 | 12, 60, 61 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴(,)+∞)) = (𝐴(,)+∞)) |
| 63 | 59, 62 | eleqtrrd 2844 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ((int‘(topGen‘ran
(,)))‘(𝐴(,)+∞))) |
| 64 | 55, 63 | sseldd 3984 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ((int‘(topGen‘ran
(,)))‘((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) |
| 65 | 5 | rexrd 11311 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 66 | 4, 5, 57 | ltled 11409 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 67 | | ubicc2 13505 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
| 68 | 13, 65, 66, 67 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
| 69 | 64, 68 | elind 4200 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (((int‘(topGen‘ran
(,)))‘((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) |
| 70 | | iocssicc 13477 |
. . . . . . 7
⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵) |
| 71 | 70 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)) |
| 72 | | eqid 2737 |
. . . . . . 7
⊢
((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,))
↾t (𝐴[,]𝐵)) |
| 73 | 18, 72 | restntr 23190 |
. . . . . 6
⊢
(((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)) → ((int‘((topGen‘ran
(,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,]𝐵)) = (((int‘(topGen‘ran
(,)))‘((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) |
| 74 | 12, 6, 71, 73 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 →
((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,]𝐵)) = (((int‘(topGen‘ran
(,)))‘((𝐴(,]𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) |
| 75 | 69, 74 | eleqtrrd 2844 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ((int‘((topGen‘ran (,))
↾t (𝐴[,]𝐵)))‘(𝐴(,]𝐵))) |
| 76 | | eqid 2737 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 77 | 9, 76 | rerest 24825 |
. . . . . . . 8
⊢ ((𝐴[,]𝐵) ⊆ ℝ →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,))
↾t (𝐴[,]𝐵))) |
| 78 | 6, 77 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,))
↾t (𝐴[,]𝐵))) |
| 79 | 78 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → ((topGen‘ran (,))
↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵))) |
| 80 | 79 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 →
(int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵))) =
(int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))) |
| 81 | 80 | fveq1d 6908 |
. . . 4
⊢ (𝜑 →
((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,]𝐵)) =
((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,]𝐵))) |
| 82 | 75, 81 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,]𝐵))) |
| 83 | 68 | snssd 4809 |
. . . . . . . 8
⊢ (𝜑 → {𝐵} ⊆ (𝐴[,]𝐵)) |
| 84 | | ssequn2 4189 |
. . . . . . . 8
⊢ ({𝐵} ⊆ (𝐴[,]𝐵) ↔ ((𝐴[,]𝐵) ∪ {𝐵}) = (𝐴[,]𝐵)) |
| 85 | 83, 84 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → ((𝐴[,]𝐵) ∪ {𝐵}) = (𝐴[,]𝐵)) |
| 86 | 85 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) = ((𝐴[,]𝐵) ∪ {𝐵})) |
| 87 | 86 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t ((𝐴[,]𝐵) ∪ {𝐵}))) |
| 88 | 87 | fveq2d 6910 |
. . . 4
⊢ (𝜑 →
(int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))) =
(int‘((TopOpen‘ℂfld) ↾t ((𝐴[,]𝐵) ∪ {𝐵})))) |
| 89 | | ioounsn 13517 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵)) |
| 90 | 13, 65, 57, 89 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵)) |
| 91 | 90 | eqcomd 2743 |
. . . 4
⊢ (𝜑 → (𝐴(,]𝐵) = ((𝐴(,)𝐵) ∪ {𝐵})) |
| 92 | 88, 91 | fveq12d 6913 |
. . 3
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,]𝐵)) =
((int‘((TopOpen‘ℂfld) ↾t ((𝐴[,]𝐵) ∪ {𝐵})))‘((𝐴(,)𝐵) ∪ {𝐵}))) |
| 93 | 82, 92 | eleqtrd 2843 |
. 2
⊢ (𝜑 → 𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t ((𝐴[,]𝐵) ∪ {𝐵})))‘((𝐴(,)𝐵) ∪ {𝐵}))) |
| 94 | 1, 3, 8, 9, 10, 93 | limcres 25921 |
1
⊢ (𝜑 → ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵) = (𝐹 limℂ 𝐵)) |