Step | Hyp | Ref
| Expression |
1 | | qssre 11674 |
. . 3
⊢ ℚ
⊆ ℝ |
2 | | lhop2.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
3 | | lhop2.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | 3 | rexrd 9968 |
. . . 4
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
5 | | lhop2.l |
. . . 4
⊢ (𝜑 → 𝐴 < 𝐵) |
6 | | qbtwnxr 11905 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵)) |
7 | 2, 4, 5, 6 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵)) |
8 | | ssrexv 3630 |
. . 3
⊢ (ℚ
⊆ ℝ → (∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵) → ∃𝑎 ∈ ℝ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) |
9 | 1, 7, 8 | mpsyl 66 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ ℝ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵)) |
10 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ (𝑎(,)𝐵)) |
11 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 ∈ ℝ) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑎 ∈ ℝ) |
13 | 3 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝐵 ∈ ℝ) |
14 | | elioore 12076 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑎(,)𝐵) → 𝑧 ∈ ℝ) |
15 | 14 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℝ) |
16 | | iooneg 12163 |
. . . . . . 7
⊢ ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎))) |
17 | 12, 13, 15, 16 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎))) |
18 | 10, 17 | mpbid 221 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎)) |
19 | 18 | adantrr 749 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 ≠ -𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎)) |
20 | | lhop2.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
21 | 20 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
22 | | elioore 12076 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → 𝑥 ∈ ℝ) |
23 | 22 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℝ) |
24 | 23 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℂ) |
25 | 24 | negnegd 10262 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 = 𝑥) |
26 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ (-𝐵(,)-𝑎)) |
27 | 25, 26 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 ∈ (-𝐵(,)-𝑎)) |
28 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑎 ∈ ℝ) |
29 | 3 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐵 ∈ ℝ) |
30 | 23 | renegcld 10336 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ ℝ) |
31 | | iooneg 12163 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ -𝑥 ∈ ℝ) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎))) |
32 | 28, 29, 30, 31 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎))) |
33 | 27, 32 | mpbird 246 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝑎(,)𝐵)) |
34 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 ∈
ℝ*) |
35 | | simprrl 800 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 < 𝑎) |
36 | 11 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 ∈ ℝ*) |
37 | | xrltle 11858 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝑎 ∈
ℝ*) → (𝐴 < 𝑎 → 𝐴 ≤ 𝑎)) |
38 | 34, 36, 37 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴 < 𝑎 → 𝐴 ≤ 𝑎)) |
39 | 35, 38 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 ≤ 𝑎) |
40 | | iooss1 12081 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑎) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵)) |
41 | 34, 39, 40 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵)) |
42 | 41 | sselda 3568 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ -𝑥 ∈ (𝑎(,)𝐵)) → -𝑥 ∈ (𝐴(,)𝐵)) |
43 | 33, 42 | syldan 486 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝐴(,)𝐵)) |
44 | 21, 43 | ffvelrnd 6268 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℝ) |
45 | 44 | recnd 9947 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℂ) |
46 | | lhop2.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
47 | 46 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
48 | 47, 43 | ffvelrnd 6268 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℝ) |
49 | 48 | recnd 9947 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℂ) |
50 | | lhop2.gn0 |
. . . . . . 7
⊢ (𝜑 → ¬ 0 ∈ ran 𝐺) |
51 | 50 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran 𝐺) |
52 | 46 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
53 | | ax-resscn 9872 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
54 | | fss 5969 |
. . . . . . . . . . . 12
⊢ ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
55 | 52, 53, 54 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
56 | 55 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
57 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐺:(𝐴(,)𝐵)⟶ℂ → 𝐺 Fn (𝐴(,)𝐵)) |
58 | 56, 57 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺 Fn (𝐴(,)𝐵)) |
59 | | fnfvelrn 6264 |
. . . . . . . . 9
⊢ ((𝐺 Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘-𝑥) ∈ ran 𝐺) |
60 | 58, 43, 59 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ran 𝐺) |
61 | | eleq1 2676 |
. . . . . . . 8
⊢ ((𝐺‘-𝑥) = 0 → ((𝐺‘-𝑥) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺)) |
62 | 60, 61 | syl5ibcom 234 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐺‘-𝑥) = 0 → 0 ∈ ran 𝐺)) |
63 | 62 | necon3bd 2796 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran 𝐺 → (𝐺‘-𝑥) ≠ 0)) |
64 | 51, 63 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ≠ 0) |
65 | 45, 49, 64 | divcld 10680 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) ∈ ℂ) |
66 | | limcresi 23455 |
. . . . . 6
⊢ ((𝑧 ∈ ℝ ↦ -𝑧) limℂ 𝐵) ⊆ (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) limℂ 𝐵) |
67 | | ioossre 12106 |
. . . . . . . 8
⊢ (𝑎(,)𝐵) ⊆ ℝ |
68 | | resmpt 5369 |
. . . . . . . 8
⊢ ((𝑎(,)𝐵) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧)) |
69 | 67, 68 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) |
70 | 69 | oveq1i 6559 |
. . . . . 6
⊢ (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) limℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) limℂ 𝐵) |
71 | 66, 70 | sseqtri 3600 |
. . . . 5
⊢ ((𝑧 ∈ ℝ ↦ -𝑧) limℂ 𝐵) ⊆ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) limℂ 𝐵) |
72 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑧 ∈ ℝ ↦ -𝑧) = (𝑧 ∈ ℝ ↦ -𝑧) |
73 | 72 | negcncf 22529 |
. . . . . . 7
⊢ (ℝ
⊆ ℂ → (𝑧
∈ ℝ ↦ -𝑧)
∈ (ℝ–cn→ℂ)) |
74 | 53, 73 | mp1i 13 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ)) |
75 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ℝ) |
76 | | negeq 10152 |
. . . . . 6
⊢ (𝑧 = 𝐵 → -𝑧 = -𝐵) |
77 | 74, 75, 76 | cnmptlimc 23460 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ ℝ ↦ -𝑧) limℂ 𝐵)) |
78 | 71, 77 | sseldi 3566 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) limℂ 𝐵)) |
79 | 75 | renegcld 10336 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ℝ) |
80 | 11 | renegcld 10336 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝑎 ∈ ℝ) |
81 | 80 | rexrd 9968 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝑎 ∈ ℝ*) |
82 | | simprrr 801 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 < 𝐵) |
83 | 11, 75 | ltnegd 10484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎 < 𝐵 ↔ -𝐵 < -𝑎)) |
84 | 82, 83 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 < -𝑎) |
85 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) |
86 | 44, 85 | fmptd 6292 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ) |
87 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) |
88 | 48, 87 | fmptd 6292 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ) |
89 | | reelprrecn 9907 |
. . . . . . . . . . 11
⊢ ℝ
∈ {ℝ, ℂ} |
90 | 89 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ℝ ∈ {ℝ,
ℂ}) |
91 | | neg1cn 11001 |
. . . . . . . . . . 11
⊢ -1 ∈
ℂ |
92 | 91 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -1 ∈ ℂ) |
93 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
94 | 93 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℝ) |
95 | 94 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℂ) |
96 | | fvex 6113 |
. . . . . . . . . . 11
⊢ ((ℝ
D 𝐹)‘𝑦) ∈ V |
97 | 96 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ V) |
98 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 1 ∈ ℂ) |
99 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
100 | 99 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
101 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
102 | 90 | dvmptid 23526 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1)) |
103 | | ioossre 12106 |
. . . . . . . . . . . . 13
⊢ (-𝐵(,)-𝑎) ⊆ ℝ |
104 | 103 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ⊆ ℝ) |
105 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
106 | 105 | tgioo2 22414 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
107 | | iooretop 22379 |
. . . . . . . . . . . . 13
⊢ (-𝐵(,)-𝑎) ∈ (topGen‘ran
(,)) |
108 | 107 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ∈ (topGen‘ran
(,))) |
109 | 90, 100, 101, 102, 104, 106, 105, 108 | dvmptres 23532 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 1)) |
110 | 90, 24, 98, 109 | dvmptneg 23535 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -1)) |
111 | 93 | feqmptd 6159 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))) |
112 | 111 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)))) |
113 | | dvf 23477 |
. . . . . . . . . . . . 13
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
114 | | lhop2.if |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
115 | 114 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
116 | 115 | feq2d 5944 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)) |
117 | 113, 116 | mpbii 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
118 | 117 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦))) |
119 | 112, 118 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦))) |
120 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑥 → (𝐹‘𝑦) = (𝐹‘-𝑥)) |
121 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘-𝑥)) |
122 | 90, 90, 43, 92, 95, 97, 110, 119, 120, 121 | dvmptco 23541 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1))) |
123 | 117 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
124 | 123, 43 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐹)‘-𝑥) ∈ ℂ) |
125 | 124, 92 | mulcomd 9940 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = (-1 · ((ℝ D
𝐹)‘-𝑥))) |
126 | 124 | mulm1d 10361 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐹)‘-𝑥)) = -((ℝ D 𝐹)‘-𝑥)) |
127 | 125, 126 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = -((ℝ D 𝐹)‘-𝑥)) |
128 | 127 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))) |
129 | 122, 128 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))) |
130 | 129 | dmeqd 5248 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))) |
131 | | negex 10158 |
. . . . . . . 8
⊢
-((ℝ D 𝐹)‘-𝑥) ∈ V |
132 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) |
133 | 131, 132 | dmmpti 5936 |
. . . . . . 7
⊢ dom
(𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (-𝐵(,)-𝑎) |
134 | 130, 133 | syl6eq 2660 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (-𝐵(,)-𝑎)) |
135 | 52 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑦) ∈ ℝ) |
136 | 135 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑦) ∈ ℂ) |
137 | | fvex 6113 |
. . . . . . . . . . 11
⊢ ((ℝ
D 𝐺)‘𝑦) ∈ V |
138 | 137 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑦) ∈ V) |
139 | 52 | feqmptd 6159 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦))) |
140 | 139 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)))) |
141 | | dvf 23477 |
. . . . . . . . . . . . 13
⊢ (ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ |
142 | | lhop2.ig |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
143 | 142 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
144 | 143 | feq2d 5944 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)) |
145 | 141, 144 | mpbii 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ) |
146 | 145 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦))) |
147 | 140, 146 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦))) |
148 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑥 → (𝐺‘𝑦) = (𝐺‘-𝑥)) |
149 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑥 → ((ℝ D 𝐺)‘𝑦) = ((ℝ D 𝐺)‘-𝑥)) |
150 | 90, 90, 43, 92, 136, 138, 110, 147, 148, 149 | dvmptco 23541 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1))) |
151 | 145 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ) |
152 | 151, 43 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ℂ) |
153 | 152, 92 | mulcomd 9940 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = (-1 · ((ℝ D
𝐺)‘-𝑥))) |
154 | 152 | mulm1d 10361 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐺)‘-𝑥)) = -((ℝ D 𝐺)‘-𝑥)) |
155 | 153, 154 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = -((ℝ D 𝐺)‘-𝑥)) |
156 | 155 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))) |
157 | 150, 156 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))) |
158 | 157 | dmeqd 5248 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))) |
159 | | negex 10158 |
. . . . . . . 8
⊢
-((ℝ D 𝐺)‘-𝑥) ∈ V |
160 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) |
161 | 159, 160 | dmmpti 5936 |
. . . . . . 7
⊢ dom
(𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (-𝐵(,)-𝑎) |
162 | 158, 161 | syl6eq 2660 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (-𝐵(,)-𝑎)) |
163 | 43 | adantrr 749 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 ≠ 𝐵)) → -𝑥 ∈ (𝐴(,)𝐵)) |
164 | | limcresi 23455 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ↦ -𝑥) limℂ -𝐵) ⊆ (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) limℂ -𝐵) |
165 | | resmpt 5369 |
. . . . . . . . . . 11
⊢ ((-𝐵(,)-𝑎) ⊆ ℝ → ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)) |
166 | 103, 165 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) |
167 | 166 | oveq1i 6559 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) limℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) limℂ -𝐵) |
168 | 164, 167 | sseqtri 3600 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ↦ -𝑥) limℂ -𝐵) ⊆ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) limℂ -𝐵) |
169 | 75 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ℂ) |
170 | 169 | negnegd 10262 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → --𝐵 = 𝐵) |
171 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ ↦ -𝑥) = (𝑥 ∈ ℝ ↦ -𝑥) |
172 | 171 | negcncf 22529 |
. . . . . . . . . . 11
⊢ (ℝ
⊆ ℂ → (𝑥
∈ ℝ ↦ -𝑥)
∈ (ℝ–cn→ℂ)) |
173 | 53, 172 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ)) |
174 | | negeq 10152 |
. . . . . . . . . 10
⊢ (𝑥 = -𝐵 → -𝑥 = --𝐵) |
175 | 173, 79, 174 | cnmptlimc 23460 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → --𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) limℂ -𝐵)) |
176 | 170, 175 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) limℂ -𝐵)) |
177 | 168, 176 | sseldi 3566 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) limℂ -𝐵)) |
178 | | lhop2.f0 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐵)) |
179 | 178 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ (𝐹 limℂ 𝐵)) |
180 | 111 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐹 limℂ 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)) limℂ 𝐵)) |
181 | 179, 180 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)) limℂ 𝐵)) |
182 | | eliooord 12104 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → (-𝐵 < 𝑥 ∧ 𝑥 < -𝑎)) |
183 | 182 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝐵 < 𝑥 ∧ 𝑥 < -𝑎)) |
184 | 183 | simpld 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝐵 < 𝑥) |
185 | 29, 23, 184 | ltnegcon1d 10486 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 < 𝐵) |
186 | 30, 185 | ltned 10052 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ≠ 𝐵) |
187 | 186 | neneqd 2787 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ -𝑥 = 𝐵) |
188 | 187 | pm2.21d 117 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐹‘-𝑥) = 0)) |
189 | 188 | impr 647 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐹‘-𝑥) = 0) |
190 | 163, 95, 177, 181, 120, 189 | limcco 23463 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) limℂ -𝐵)) |
191 | | lhop2.g0 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝐵)) |
192 | 191 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ (𝐺 limℂ 𝐵)) |
193 | 139 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐺 limℂ 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)) limℂ 𝐵)) |
194 | 192, 193 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)) limℂ 𝐵)) |
195 | 187 | pm2.21d 117 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐺‘-𝑥) = 0)) |
196 | 195 | impr 647 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐺‘-𝑥) = 0) |
197 | 163, 136,
177, 194, 148, 196 | limcco 23463 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) limℂ -𝐵)) |
198 | 60, 87 | fmptd 6292 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ran 𝐺) |
199 | | frn 5966 |
. . . . . . . 8
⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ran 𝐺 → ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) ⊆ ran 𝐺) |
200 | 198, 199 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) ⊆ ran 𝐺) |
201 | 50 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran 𝐺) |
202 | 200, 201 | ssneldd 3571 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) |
203 | | lhop2.gd0 |
. . . . . . . 8
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐺)) |
204 | 203 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D
𝐺)) |
205 | 157 | rneqd 5274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))) |
206 | 205 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) ↔ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))) |
207 | 160, 159 | elrnmpti 5297 |
. . . . . . . . 9
⊢ (0 ∈
ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) ↔ ∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥)) |
208 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ (0 =
-((ℝ D 𝐺)‘-𝑥) ↔ -((ℝ D 𝐺)‘-𝑥) = 0) |
209 | 152 | negeq0d 10263 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 ↔ -((ℝ D 𝐺)‘-𝑥) = 0)) |
210 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ ((ℝ
D 𝐺):(𝐴(,)𝐵)⟶ℂ → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
211 | 151, 210 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
212 | | fnfvelrn 6264 |
. . . . . . . . . . . . . 14
⊢
(((ℝ D 𝐺) Fn
(𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺)) |
213 | 211, 43, 212 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺)) |
214 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢
(((ℝ D 𝐺)‘-𝑥) = 0 → (((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺))) |
215 | 213, 214 | syl5ibcom 234 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
216 | 209, 215 | sylbird 249 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
217 | 208, 216 | syl5bi 231 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺))) |
218 | 217 | rexlimdva 3013 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺))) |
219 | 207, 218 | syl5bi 231 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) → 0 ∈ ran (ℝ D 𝐺))) |
220 | 206, 219 | sylbid 229 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) → 0 ∈ ran (ℝ D 𝐺))) |
221 | 204, 220 | mtod 188 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D
(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))) |
222 | 117 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ ℂ) |
223 | 145 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ℂ) |
224 | 203 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran (ℝ D
𝐺)) |
225 | 145, 210 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
226 | | fnfvelrn 6264 |
. . . . . . . . . . . . 13
⊢
(((ℝ D 𝐺) Fn
(𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺)) |
227 | 225, 226 | sylan 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺)) |
228 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢
(((ℝ D 𝐺)‘𝑧) = 0 → (((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺))) |
229 | 227, 228 | syl5ibcom 234 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐺)‘𝑧) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
230 | 229 | necon3bd 2796 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran (ℝ D
𝐺) → ((ℝ D 𝐺)‘𝑧) ≠ 0)) |
231 | 224, 230 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ≠ 0) |
232 | 222, 223,
231 | divcld 10680 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) ∈ ℂ) |
233 | | lhop2.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵)) |
234 | 233 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵)) |
235 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = -𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘-𝑥)) |
236 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = -𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘-𝑥)) |
237 | 235, 236 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑧 = -𝑥 → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) |
238 | 187 | pm2.21d 117 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶)) |
239 | 238 | impr 647 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶) |
240 | 163, 232,
177, 234, 237, 239 | limcco 23463 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) limℂ -𝐵)) |
241 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥ℝ |
242 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥
D |
243 | | nfmpt1 4675 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) |
244 | 241, 242,
243 | nfov 6575 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) |
245 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑦 |
246 | 244, 245 | nffv 6110 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) |
247 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥
/ |
248 | | nfmpt1 4675 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) |
249 | 241, 242,
248 | nfov 6575 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) |
250 | 249, 245 | nffv 6110 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦) |
251 | 246, 247,
250 | nfov 6575 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)) |
252 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) |
253 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥)) |
254 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) |
255 | 253, 254 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)) = (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))) |
256 | 251, 252,
255 | cbvmpt 4677 |
. . . . . . . . 9
⊢ (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))) |
257 | 129 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥)) |
258 | 132 | fvmpt2 6200 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐹)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥)) |
259 | 131, 258 | mpan2 703 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥)) |
260 | 257, 259 | sylan9eq 2664 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = -((ℝ D 𝐹)‘-𝑥)) |
261 | 157 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥)) |
262 | 160 | fvmpt2 6200 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐺)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥)) |
263 | 159, 262 | mpan2 703 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥)) |
264 | 261, 263 | sylan9eq 2664 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = -((ℝ D 𝐺)‘-𝑥)) |
265 | 260, 264 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥))) |
266 | 203 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran (ℝ D 𝐺)) |
267 | 215 | necon3bd 2796 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran (ℝ D
𝐺) → ((ℝ D 𝐺)‘-𝑥) ≠ 0)) |
268 | 266, 267 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ≠ 0) |
269 | 124, 152,
268 | div2negd 10695 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) |
270 | 265, 269 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) |
271 | 270 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))) |
272 | 256, 271 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))) |
273 | 272 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) limℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) limℂ -𝐵)) |
274 | 240, 273 | eleqtrrd 2691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) limℂ -𝐵)) |
275 | 79, 81, 84, 86, 88, 134, 162, 190, 197, 202, 221, 274 | lhop1 23581 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) limℂ -𝐵)) |
276 | | nffvmpt1 6111 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) |
277 | | nffvmpt1 6111 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦) |
278 | 276, 247,
277 | nfov 6575 |
. . . . . . . 8
⊢
Ⅎ𝑥(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)) |
279 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑦(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)) |
280 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥)) |
281 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)) |
282 | 280, 281 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)) = (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))) |
283 | 278, 279,
282 | cbvmpt 4677 |
. . . . . . 7
⊢ (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))) |
284 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐹‘-𝑥) ∈ V |
285 | 85 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐹‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥)) |
286 | 26, 284, 285 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥)) |
287 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐺‘-𝑥) ∈ V |
288 | 87 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐺‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥)) |
289 | 26, 287, 288 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥)) |
290 | 286, 289 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)) = ((𝐹‘-𝑥) / (𝐺‘-𝑥))) |
291 | 290 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥)))) |
292 | 283, 291 | syl5eq 2656 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥)))) |
293 | 292 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) limℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) limℂ -𝐵)) |
294 | 275, 293 | eleqtrd 2690 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) limℂ -𝐵)) |
295 | | negeq 10152 |
. . . . . 6
⊢ (𝑥 = -𝑧 → -𝑥 = --𝑧) |
296 | 295 | fveq2d 6107 |
. . . . 5
⊢ (𝑥 = -𝑧 → (𝐹‘-𝑥) = (𝐹‘--𝑧)) |
297 | 295 | fveq2d 6107 |
. . . . 5
⊢ (𝑥 = -𝑧 → (𝐺‘-𝑥) = (𝐺‘--𝑧)) |
298 | 296, 297 | oveq12d 6567 |
. . . 4
⊢ (𝑥 = -𝑧 → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) = ((𝐹‘--𝑧) / (𝐺‘--𝑧))) |
299 | 79 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 ∈ ℝ) |
300 | | eliooord 12104 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑎(,)𝐵) → (𝑎 < 𝑧 ∧ 𝑧 < 𝐵)) |
301 | 300 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑎 < 𝑧 ∧ 𝑧 < 𝐵)) |
302 | 301 | simprd 478 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 < 𝐵) |
303 | 15, 13 | ltnegd 10484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 < 𝐵 ↔ -𝐵 < -𝑧)) |
304 | 302, 303 | mpbid 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 < -𝑧) |
305 | 299, 304 | gtned 10051 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ≠ -𝐵) |
306 | 305 | neneqd 2787 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ¬ -𝑧 = -𝐵) |
307 | 306 | pm2.21d 117 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (-𝑧 = -𝐵 → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶)) |
308 | 307 | impr 647 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 = -𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶) |
309 | 19, 65, 78, 294, 298, 308 | limcco 23463 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) limℂ 𝐵)) |
310 | 15 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℂ) |
311 | 310 | negnegd 10262 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → --𝑧 = 𝑧) |
312 | 311 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐹‘--𝑧) = (𝐹‘𝑧)) |
313 | 311 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐺‘--𝑧) = (𝐺‘𝑧)) |
314 | 312, 313 | oveq12d 6567 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = ((𝐹‘𝑧) / (𝐺‘𝑧))) |
315 | 314 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧)))) |
316 | 315 | oveq1d 6564 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) limℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
317 | 41 | resmptd 5371 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧)))) |
318 | 317 | oveq1d 6564 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) limℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
319 | | fss 5969 |
. . . . . . . . 9
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
320 | 93, 53, 319 | sylancl 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
321 | 320 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑧) ∈ ℂ) |
322 | 55 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ℂ) |
323 | 50 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran 𝐺) |
324 | 55, 57 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺 Fn (𝐴(,)𝐵)) |
325 | | fnfvelrn 6264 |
. . . . . . . . . . 11
⊢ ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ran 𝐺) |
326 | 324, 325 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ran 𝐺) |
327 | | eleq1 2676 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑧) = 0 → ((𝐺‘𝑧) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺)) |
328 | 326, 327 | syl5ibcom 234 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐺‘𝑧) = 0 → 0 ∈ ran 𝐺)) |
329 | 328 | necon3bd 2796 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran 𝐺 → (𝐺‘𝑧) ≠ 0)) |
330 | 323, 329 | mpd 15 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ≠ 0) |
331 | 321, 322,
330 | divcld 10680 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑧) / (𝐺‘𝑧)) ∈ ℂ) |
332 | | eqid 2610 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) |
333 | 331, 332 | fmptd 6292 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))):(𝐴(,)𝐵)⟶ℂ) |
334 | | ioossre 12106 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ ℝ |
335 | 334, 53 | sstri 3577 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℂ |
336 | 335 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℂ) |
337 | | eqid 2610 |
. . . . 5
⊢
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((TopOpen‘ℂfld)
↾t ((𝐴(,)𝐵) ∪ {𝐵})) |
338 | | ssun2 3739 |
. . . . . . 7
⊢ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵}) |
339 | | snssg 4268 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵}))) |
340 | 75, 339 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵}))) |
341 | 338, 340 | mpbiri 247 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵})) |
342 | 105 | cnfldtopon 22396 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
343 | 334 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℝ) |
344 | 75 | snssd 4281 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → {𝐵} ⊆ ℝ) |
345 | 343, 344 | unssd 3751 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ) |
346 | 345, 53 | syl6ss 3580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ) |
347 | | resttopon 20775 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵}))) |
348 | 342, 346,
347 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵}))) |
349 | | topontop 20541 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})) →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top) |
350 | 348, 349 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top) |
351 | | indi 3832 |
. . . . . . . . . 10
⊢ ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵})) |
352 | | pnfxr 9971 |
. . . . . . . . . . . . . 14
⊢ +∞
∈ ℝ* |
353 | 352 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → +∞ ∈
ℝ*) |
354 | 4 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈
ℝ*) |
355 | | iooin 12080 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
→ ((𝑎(,)+∞)
∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵))) |
356 | 36, 353, 34, 354, 355 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵))) |
357 | | xrltnle 9984 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ*
∧ 𝑎 ∈
ℝ*) → (𝐴 < 𝑎 ↔ ¬ 𝑎 ≤ 𝐴)) |
358 | 34, 36, 357 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴 < 𝑎 ↔ ¬ 𝑎 ≤ 𝐴)) |
359 | 35, 358 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 𝑎 ≤ 𝐴) |
360 | 359 | iffalsed 4047 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝑎) |
361 | | ltpnf 11830 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℝ → 𝐵 < +∞) |
362 | 75, 361 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 < +∞) |
363 | | xrltnle 9984 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝐵 < +∞ ↔ ¬ +∞ ≤
𝐵)) |
364 | 354, 352,
363 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 < +∞ ↔ ¬ +∞ ≤
𝐵)) |
365 | 362, 364 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ +∞ ≤ 𝐵) |
366 | 365 | iffalsed 4047 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → if(+∞ ≤ 𝐵, +∞, 𝐵) = 𝐵) |
367 | 360, 366 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)) = (𝑎(,)𝐵)) |
368 | 356, 367 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (𝑎(,)𝐵)) |
369 | | elioopnf 12138 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℝ*
→ (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵))) |
370 | 36, 369 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵))) |
371 | 75, 82, 370 | mpbir2and 959 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ (𝑎(,)+∞)) |
372 | 371 | snssd 4281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → {𝐵} ⊆ (𝑎(,)+∞)) |
373 | | sseqin2 3779 |
. . . . . . . . . . . 12
⊢ ({𝐵} ⊆ (𝑎(,)+∞) ↔ ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵}) |
374 | 372, 373 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵}) |
375 | 368, 374 | uneq12d 3730 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵})) |
376 | 351, 375 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵})) |
377 | | retop 22375 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) ∈ Top |
378 | 377 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (topGen‘ran (,)) ∈
Top) |
379 | | reex 9906 |
. . . . . . . . . . . 12
⊢ ℝ
∈ V |
380 | 379 | ssex 4730 |
. . . . . . . . . . 11
⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V) |
381 | 345, 380 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V) |
382 | | iooretop 22379 |
. . . . . . . . . . 11
⊢ (𝑎(,)+∞) ∈
(topGen‘ran (,)) |
383 | 382 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎(,)+∞) ∈ (topGen‘ran
(,))) |
384 | | elrestr 15912 |
. . . . . . . . . 10
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V ∧ (𝑎(,)+∞) ∈ (topGen‘ran (,)))
→ ((𝑎(,)+∞)
∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,))
↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
385 | 378, 381,
383, 384 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,))
↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
386 | 376, 385 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((topGen‘ran (,))
↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
387 | | eqid 2610 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
388 | 105, 387 | rerest 22415 |
. . . . . . . . 9
⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,))
↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
389 | 345, 388 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,))
↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
390 | 386, 389 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
391 | | isopn3i 20696 |
. . . . . . 7
⊢
((((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top ∧ ((𝑎(,)𝐵) ∪ {𝐵}) ∈
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))) →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵})) |
392 | 350, 390,
391 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵})) |
393 | 341, 392 | eleqtrrd 2691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵}))) |
394 | 333, 41, 336, 105, 337, 393 | limcres 23456 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) limℂ 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
395 | 316, 318,
394 | 3eqtr2d 2650 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) limℂ 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
396 | 309, 395 | eleqtrd 2690 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
397 | 9, 396 | rexlimddv 3017 |
1
⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |