Step | Hyp | Ref
| Expression |
1 | | limciccioolb.4 |
. 2
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
2 | | ioossicc 13021 |
. . 3
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
3 | 2 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
4 | | limciccioolb.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
5 | | limciccioolb.2 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
6 | 4, 5 | iccssred 13022 |
. . 3
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
7 | | ax-resscn 10786 |
. . 3
⊢ ℝ
⊆ ℂ |
8 | 6, 7 | sstrdi 3913 |
. 2
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
9 | | eqid 2737 |
. 2
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
10 | | eqid 2737 |
. 2
⊢
((TopOpen‘ℂfld) ↾t ((𝐴[,]𝐵) ∪ {𝐴})) = ((TopOpen‘ℂfld)
↾t ((𝐴[,]𝐵) ∪ {𝐴})) |
11 | | retop 23659 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (topGen‘ran (,))
∈ Top) |
13 | 5 | rexrd 10883 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
14 | | icossre 13016 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,)𝐵) ⊆
ℝ) |
15 | 4, 13, 14 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴[,)𝐵) ⊆ ℝ) |
16 | | difssd 4047 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ ∖ (𝐴[,]𝐵)) ⊆ ℝ) |
17 | 15, 16 | unssd 4100 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ) |
18 | | uniretop 23660 |
. . . . . . . . 9
⊢ ℝ =
∪ (topGen‘ran (,)) |
19 | 17, 18 | sseqtrdi 3951 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ∪
(topGen‘ran (,))) |
20 | | elioore 12965 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (-∞(,)𝐵) → 𝑥 ∈ ℝ) |
21 | 20 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ 𝐴 ≤ 𝑥) → 𝑥 ∈ ℝ) |
22 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ 𝐴 ≤ 𝑥) → 𝐴 ≤ 𝑥) |
23 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) → 𝑥 ∈ (-∞(,)𝐵)) |
24 | | mnfxr 10890 |
. . . . . . . . . . . . . . . . . . 19
⊢ -∞
∈ ℝ* |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) → -∞ ∈
ℝ*) |
26 | 13 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) → 𝐵 ∈
ℝ*) |
27 | | elioo2 12976 |
. . . . . . . . . . . . . . . . . 18
⊢
((-∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑥 ∈ (-∞(,)𝐵) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐵))) |
28 | 25, 26, 27 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) → (𝑥 ∈ (-∞(,)𝐵) ↔ (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐵))) |
29 | 23, 28 | mpbid 235 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) → (𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐵)) |
30 | 29 | simp3d 1146 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) → 𝑥 < 𝐵) |
31 | 30 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ 𝐴 ≤ 𝑥) → 𝑥 < 𝐵) |
32 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ 𝐴 ≤ 𝑥) → 𝐴 ∈ ℝ) |
33 | 13 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ 𝐴 ≤ 𝑥) → 𝐵 ∈
ℝ*) |
34 | | elico2 12999 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ (𝑥 ∈ (𝐴[,)𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵))) |
35 | 32, 33, 34 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ 𝐴 ≤ 𝑥) → (𝑥 ∈ (𝐴[,)𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵))) |
36 | 21, 22, 31, 35 | mpbir3and 1344 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ 𝐴 ≤ 𝑥) → 𝑥 ∈ (𝐴[,)𝐵)) |
37 | 36 | orcd 873 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ 𝐴 ≤ 𝑥) → (𝑥 ∈ (𝐴[,)𝐵) ∨ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)))) |
38 | 20 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ ¬ 𝐴 ≤ 𝑥) → 𝑥 ∈ ℝ) |
39 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ ¬ 𝐴 ≤ 𝑥) → ¬ 𝐴 ≤ 𝑥) |
40 | 39 | intnanrd 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ ¬ 𝐴 ≤ 𝑥) → ¬ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
41 | 4 | rexrd 10883 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
42 | 41 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ ¬ 𝐴 ≤ 𝑥) → 𝐴 ∈
ℝ*) |
43 | 13 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ ¬ 𝐴 ≤ 𝑥) → 𝐵 ∈
ℝ*) |
44 | 38 | rexrd 10883 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ ¬ 𝐴 ≤ 𝑥) → 𝑥 ∈ ℝ*) |
45 | | elicc4 13002 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ ℝ*) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
46 | 42, 43, 44, 45 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ ¬ 𝐴 ≤ 𝑥) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
47 | 40, 46 | mtbird 328 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ ¬ 𝐴 ≤ 𝑥) → ¬ 𝑥 ∈ (𝐴[,]𝐵)) |
48 | 38, 47 | eldifd 3877 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ ¬ 𝐴 ≤ 𝑥) → 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) |
49 | 48 | olcd 874 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) ∧ ¬ 𝐴 ≤ 𝑥) → (𝑥 ∈ (𝐴[,)𝐵) ∨ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)))) |
50 | 37, 49 | pm2.61dan 813 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) → (𝑥 ∈ (𝐴[,)𝐵) ∨ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)))) |
51 | | elun 4063 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ↔ (𝑥 ∈ (𝐴[,)𝐵) ∨ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)))) |
52 | 50, 51 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝐵)) → 𝑥 ∈ ((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) |
53 | 52 | ralrimiva 3105 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (-∞(,)𝐵)𝑥 ∈ ((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) |
54 | | dfss3 3888 |
. . . . . . . . 9
⊢
((-∞(,)𝐵)
⊆ ((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ↔ ∀𝑥 ∈ (-∞(,)𝐵)𝑥 ∈ ((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) |
55 | 53, 54 | sylibr 237 |
. . . . . . . 8
⊢ (𝜑 → (-∞(,)𝐵) ⊆ ((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) |
56 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ (topGen‘ran (,)) = ∪
(topGen‘ran (,)) |
57 | 56 | ntrss 21952 |
. . . . . . . 8
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ∪
(topGen‘ran (,)) ∧ (-∞(,)𝐵) ⊆ ((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) → ((int‘(topGen‘ran
(,)))‘(-∞(,)𝐵))
⊆ ((int‘(topGen‘ran (,)))‘((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) |
58 | 12, 19, 55, 57 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(-∞(,)𝐵)) ⊆ ((int‘(topGen‘ran
(,)))‘((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) |
59 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → -∞ ∈
ℝ*) |
60 | 4 | mnfltd 12716 |
. . . . . . . . 9
⊢ (𝜑 → -∞ < 𝐴) |
61 | | limciccioolb.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 < 𝐵) |
62 | 59, 13, 4, 60, 61 | eliood 42711 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ (-∞(,)𝐵)) |
63 | | iooretop 23663 |
. . . . . . . . . 10
⊢
(-∞(,)𝐵)
∈ (topGen‘ran (,)) |
64 | 63 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (-∞(,)𝐵) ∈ (topGen‘ran
(,))) |
65 | | isopn3i 21979 |
. . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ Top ∧ (-∞(,)𝐵) ∈ (topGen‘ran (,))) →
((int‘(topGen‘ran (,)))‘(-∞(,)𝐵)) = (-∞(,)𝐵)) |
66 | 12, 64, 65 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(-∞(,)𝐵)) = (-∞(,)𝐵)) |
67 | 62, 66 | eleqtrrd 2841 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ((int‘(topGen‘ran
(,)))‘(-∞(,)𝐵))) |
68 | 58, 67 | sseldd 3902 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ((int‘(topGen‘ran
(,)))‘((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) |
69 | 4 | leidd 11398 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐴) |
70 | 4, 5, 61 | ltled 10980 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
71 | 4, 5, 4, 69, 70 | eliccd 42717 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
72 | 68, 71 | elind 4108 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ (((int‘(topGen‘ran
(,)))‘((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) |
73 | | icossicc 13024 |
. . . . . . 7
⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) |
74 | 73 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵)) |
75 | | eqid 2737 |
. . . . . . 7
⊢
((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,))
↾t (𝐴[,]𝐵)) |
76 | 18, 75 | restntr 22079 |
. . . . . 6
⊢
(((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵)) → ((int‘((topGen‘ran
(,)) ↾t (𝐴[,]𝐵)))‘(𝐴[,)𝐵)) = (((int‘(topGen‘ran
(,)))‘((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) |
77 | 12, 6, 74, 76 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 →
((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴[,)𝐵)) = (((int‘(topGen‘ran
(,)))‘((𝐴[,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) |
78 | 72, 77 | eleqtrrd 2841 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ((int‘((topGen‘ran (,))
↾t (𝐴[,]𝐵)))‘(𝐴[,)𝐵))) |
79 | | eqid 2737 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
80 | 9, 79 | rerest 23701 |
. . . . . . . 8
⊢ ((𝐴[,]𝐵) ⊆ ℝ →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,))
↾t (𝐴[,]𝐵))) |
81 | 6, 80 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,))
↾t (𝐴[,]𝐵))) |
82 | 81 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → ((topGen‘ran (,))
↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵))) |
83 | 82 | fveq2d 6721 |
. . . . 5
⊢ (𝜑 →
(int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵))) =
(int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))) |
84 | 83 | fveq1d 6719 |
. . . 4
⊢ (𝜑 →
((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴[,)𝐵)) =
((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴[,)𝐵))) |
85 | 78, 84 | eleqtrd 2840 |
. . 3
⊢ (𝜑 → 𝐴 ∈
((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴[,)𝐵))) |
86 | 71 | snssd 4722 |
. . . . . . . 8
⊢ (𝜑 → {𝐴} ⊆ (𝐴[,]𝐵)) |
87 | | ssequn2 4097 |
. . . . . . . 8
⊢ ({𝐴} ⊆ (𝐴[,]𝐵) ↔ ((𝐴[,]𝐵) ∪ {𝐴}) = (𝐴[,]𝐵)) |
88 | 86, 87 | sylib 221 |
. . . . . . 7
⊢ (𝜑 → ((𝐴[,]𝐵) ∪ {𝐴}) = (𝐴[,]𝐵)) |
89 | 88 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) = ((𝐴[,]𝐵) ∪ {𝐴})) |
90 | 89 | oveq2d 7229 |
. . . . 5
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t ((𝐴[,]𝐵) ∪ {𝐴}))) |
91 | 90 | fveq2d 6721 |
. . . 4
⊢ (𝜑 →
(int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))) =
(int‘((TopOpen‘ℂfld) ↾t ((𝐴[,]𝐵) ∪ {𝐴})))) |
92 | | uncom 4067 |
. . . . 5
⊢ ((𝐴(,)𝐵) ∪ {𝐴}) = ({𝐴} ∪ (𝐴(,)𝐵)) |
93 | | snunioo 13066 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵)) |
94 | 41, 13, 61, 93 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵)) |
95 | 92, 94 | eqtr2id 2791 |
. . . 4
⊢ (𝜑 → (𝐴[,)𝐵) = ((𝐴(,)𝐵) ∪ {𝐴})) |
96 | 91, 95 | fveq12d 6724 |
. . 3
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴[,)𝐵)) =
((int‘((TopOpen‘ℂfld) ↾t ((𝐴[,]𝐵) ∪ {𝐴})))‘((𝐴(,)𝐵) ∪ {𝐴}))) |
97 | 85, 96 | eleqtrd 2840 |
. 2
⊢ (𝜑 → 𝐴 ∈
((int‘((TopOpen‘ℂfld) ↾t ((𝐴[,]𝐵) ∪ {𝐴})))‘((𝐴(,)𝐵) ∪ {𝐴}))) |
98 | 1, 3, 8, 9, 10, 97 | limcres 24783 |
1
⊢ (𝜑 → ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐴) = (𝐹 limℂ 𝐴)) |