| Step | Hyp | Ref
| Expression |
| 1 | | qssre 13001 |
. . 3
⊢ ℚ
⊆ ℝ |
| 2 | | lhop2.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 3 | | lhop2.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 4 | 3 | rexrd 11311 |
. . . 4
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 5 | | lhop2.l |
. . . 4
⊢ (𝜑 → 𝐴 < 𝐵) |
| 6 | | qbtwnxr 13242 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵)) |
| 7 | 2, 4, 5, 6 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵)) |
| 8 | | ssrexv 4053 |
. . 3
⊢ (ℚ
⊆ ℝ → (∃𝑎 ∈ ℚ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵) → ∃𝑎 ∈ ℝ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) |
| 9 | 1, 7, 8 | mpsyl 68 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ ℝ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵)) |
| 10 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ (𝑎(,)𝐵)) |
| 11 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 ∈ ℝ) |
| 12 | 11 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑎 ∈ ℝ) |
| 13 | 3 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝐵 ∈ ℝ) |
| 14 | | elioore 13417 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑎(,)𝐵) → 𝑧 ∈ ℝ) |
| 15 | 14 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℝ) |
| 16 | | iooneg 13511 |
. . . . . . 7
⊢ ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎))) |
| 17 | 12, 13, 15, 16 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎))) |
| 18 | 10, 17 | mpbid 232 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎)) |
| 19 | 18 | adantrr 717 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 ≠ -𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎)) |
| 20 | | lhop2.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 21 | 20 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 22 | | elioore 13417 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → 𝑥 ∈ ℝ) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℝ) |
| 24 | 23 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℂ) |
| 25 | 24 | negnegd 11611 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 = 𝑥) |
| 26 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ (-𝐵(,)-𝑎)) |
| 27 | 25, 26 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 ∈ (-𝐵(,)-𝑎)) |
| 28 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑎 ∈ ℝ) |
| 29 | 3 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐵 ∈ ℝ) |
| 30 | 23 | renegcld 11690 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ ℝ) |
| 31 | | iooneg 13511 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ -𝑥 ∈ ℝ) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎))) |
| 32 | 28, 29, 30, 31 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎))) |
| 33 | 27, 32 | mpbird 257 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝑎(,)𝐵)) |
| 34 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 ∈
ℝ*) |
| 35 | 11 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 ∈ ℝ*) |
| 36 | | simprrl 781 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 < 𝑎) |
| 37 | 34, 35, 36 | xrltled 13192 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐴 ≤ 𝑎) |
| 38 | | iooss1 13422 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑎) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵)) |
| 39 | 34, 37, 38 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵)) |
| 40 | 39 | sselda 3983 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ -𝑥 ∈ (𝑎(,)𝐵)) → -𝑥 ∈ (𝐴(,)𝐵)) |
| 41 | 33, 40 | syldan 591 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝐴(,)𝐵)) |
| 42 | 21, 41 | ffvelcdmd 7105 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℝ) |
| 43 | 42 | recnd 11289 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℂ) |
| 44 | | lhop2.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
| 45 | 44 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
| 46 | 45, 41 | ffvelcdmd 7105 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℝ) |
| 47 | 46 | recnd 11289 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℂ) |
| 48 | | lhop2.gn0 |
. . . . . . 7
⊢ (𝜑 → ¬ 0 ∈ ran 𝐺) |
| 49 | 48 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran 𝐺) |
| 50 | 44 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
| 51 | | ax-resscn 11212 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
| 52 | | fss 6752 |
. . . . . . . . . . . 12
⊢ ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
| 53 | 50, 51, 52 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
| 54 | 53 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
| 55 | 54 | ffnd 6737 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺 Fn (𝐴(,)𝐵)) |
| 56 | | fnfvelrn 7100 |
. . . . . . . . 9
⊢ ((𝐺 Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘-𝑥) ∈ ran 𝐺) |
| 57 | 55, 41, 56 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ran 𝐺) |
| 58 | | eleq1 2829 |
. . . . . . . 8
⊢ ((𝐺‘-𝑥) = 0 → ((𝐺‘-𝑥) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺)) |
| 59 | 57, 58 | syl5ibcom 245 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐺‘-𝑥) = 0 → 0 ∈ ran 𝐺)) |
| 60 | 59 | necon3bd 2954 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran 𝐺 → (𝐺‘-𝑥) ≠ 0)) |
| 61 | 49, 60 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ≠ 0) |
| 62 | 43, 47, 61 | divcld 12043 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) ∈ ℂ) |
| 63 | | limcresi 25920 |
. . . . . 6
⊢ ((𝑧 ∈ ℝ ↦ -𝑧) limℂ 𝐵) ⊆ (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) limℂ 𝐵) |
| 64 | | ioossre 13448 |
. . . . . . . 8
⊢ (𝑎(,)𝐵) ⊆ ℝ |
| 65 | | resmpt 6055 |
. . . . . . . 8
⊢ ((𝑎(,)𝐵) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧)) |
| 66 | 64, 65 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) |
| 67 | 66 | oveq1i 7441 |
. . . . . 6
⊢ (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) limℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) limℂ 𝐵) |
| 68 | 63, 67 | sseqtri 4032 |
. . . . 5
⊢ ((𝑧 ∈ ℝ ↦ -𝑧) limℂ 𝐵) ⊆ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) limℂ 𝐵) |
| 69 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑧 ∈ ℝ ↦ -𝑧) = (𝑧 ∈ ℝ ↦ -𝑧) |
| 70 | 69 | negcncf 24948 |
. . . . . . 7
⊢ (ℝ
⊆ ℂ → (𝑧
∈ ℝ ↦ -𝑧)
∈ (ℝ–cn→ℂ)) |
| 71 | 51, 70 | mp1i 13 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ)) |
| 72 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ℝ) |
| 73 | | negeq 11500 |
. . . . . 6
⊢ (𝑧 = 𝐵 → -𝑧 = -𝐵) |
| 74 | 71, 72, 73 | cnmptlimc 25925 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ ℝ ↦ -𝑧) limℂ 𝐵)) |
| 75 | 68, 74 | sselid 3981 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) limℂ 𝐵)) |
| 76 | 72 | renegcld 11690 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 ∈ ℝ) |
| 77 | 11 | renegcld 11690 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝑎 ∈ ℝ) |
| 78 | 77 | rexrd 11311 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝑎 ∈ ℝ*) |
| 79 | | simprrr 782 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝑎 < 𝐵) |
| 80 | 11, 72 | ltnegd 11841 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎 < 𝐵 ↔ -𝐵 < -𝑎)) |
| 81 | 79, 80 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → -𝐵 < -𝑎) |
| 82 | 42 | fmpttd 7135 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ) |
| 83 | 46 | fmpttd 7135 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ) |
| 84 | | reelprrecn 11247 |
. . . . . . . . . . 11
⊢ ℝ
∈ {ℝ, ℂ} |
| 85 | 84 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ℝ ∈ {ℝ,
ℂ}) |
| 86 | | neg1cn 12380 |
. . . . . . . . . . 11
⊢ -1 ∈
ℂ |
| 87 | 86 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -1 ∈ ℂ) |
| 88 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 89 | 88 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℝ) |
| 90 | 89 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℂ) |
| 91 | | fvexd 6921 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ V) |
| 92 | | 1cnd 11256 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 1 ∈ ℂ) |
| 93 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
| 94 | 93 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
| 95 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
| 96 | 85 | dvmptid 25995 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1)) |
| 97 | | ioossre 13448 |
. . . . . . . . . . . . 13
⊢ (-𝐵(,)-𝑎) ⊆ ℝ |
| 98 | 97 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ⊆ ℝ) |
| 99 | | tgioo4 24826 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 100 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 101 | | iooretop 24786 |
. . . . . . . . . . . . 13
⊢ (-𝐵(,)-𝑎) ∈ (topGen‘ran
(,)) |
| 102 | 101 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ∈ (topGen‘ran
(,))) |
| 103 | 85, 94, 95, 96, 98, 99, 100, 102 | dvmptres 26001 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 1)) |
| 104 | 85, 24, 92, 103 | dvmptneg 26004 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -1)) |
| 105 | 88 | feqmptd 6977 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))) |
| 106 | 105 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)))) |
| 107 | | dvf 25942 |
. . . . . . . . . . . . 13
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
| 108 | | lhop2.if |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
| 109 | 108 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
| 110 | 109 | feq2d 6722 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)) |
| 111 | 107, 110 | mpbii 233 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
| 112 | 111 | feqmptd 6977 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐹) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦))) |
| 113 | 106, 112 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦))) |
| 114 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑥 → (𝐹‘𝑦) = (𝐹‘-𝑥)) |
| 115 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘-𝑥)) |
| 116 | 85, 85, 41, 87, 90, 91, 104, 113, 114, 115 | dvmptco 26010 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1))) |
| 117 | 111 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
| 118 | 117, 41 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐹)‘-𝑥) ∈ ℂ) |
| 119 | 118, 87 | mulcomd 11282 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = (-1 · ((ℝ D
𝐹)‘-𝑥))) |
| 120 | 118 | mulm1d 11715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐹)‘-𝑥)) = -((ℝ D 𝐹)‘-𝑥)) |
| 121 | 119, 120 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = -((ℝ D 𝐹)‘-𝑥)) |
| 122 | 121 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))) |
| 123 | 116, 122 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))) |
| 124 | 123 | dmeqd 5916 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))) |
| 125 | | negex 11506 |
. . . . . . . 8
⊢
-((ℝ D 𝐹)‘-𝑥) ∈ V |
| 126 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) |
| 127 | 125, 126 | dmmpti 6712 |
. . . . . . 7
⊢ dom
(𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (-𝐵(,)-𝑎) |
| 128 | 124, 127 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (-𝐵(,)-𝑎)) |
| 129 | 50 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑦) ∈ ℝ) |
| 130 | 129 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑦) ∈ ℂ) |
| 131 | | fvexd 6921 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑦) ∈ V) |
| 132 | 50 | feqmptd 6977 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦))) |
| 133 | 132 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)))) |
| 134 | | dvf 25942 |
. . . . . . . . . . . . 13
⊢ (ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ |
| 135 | | lhop2.ig |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
| 136 | 135 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
| 137 | 136 | feq2d 6722 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)) |
| 138 | 134, 137 | mpbii 233 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ) |
| 139 | 138 | feqmptd 6977 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦))) |
| 140 | 133, 139 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦))) |
| 141 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑥 → (𝐺‘𝑦) = (𝐺‘-𝑥)) |
| 142 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑥 → ((ℝ D 𝐺)‘𝑦) = ((ℝ D 𝐺)‘-𝑥)) |
| 143 | 85, 85, 41, 87, 130, 131, 104, 140, 141, 142 | dvmptco 26010 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1))) |
| 144 | 138 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ) |
| 145 | 144, 41 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ℂ) |
| 146 | 145, 87 | mulcomd 11282 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = (-1 · ((ℝ D
𝐺)‘-𝑥))) |
| 147 | 145 | mulm1d 11715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐺)‘-𝑥)) = -((ℝ D 𝐺)‘-𝑥)) |
| 148 | 146, 147 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = -((ℝ D 𝐺)‘-𝑥)) |
| 149 | 148 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))) |
| 150 | 143, 149 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))) |
| 151 | 150 | dmeqd 5916 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))) |
| 152 | | negex 11506 |
. . . . . . . 8
⊢
-((ℝ D 𝐺)‘-𝑥) ∈ V |
| 153 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) |
| 154 | 152, 153 | dmmpti 6712 |
. . . . . . 7
⊢ dom
(𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (-𝐵(,)-𝑎) |
| 155 | 151, 154 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (-𝐵(,)-𝑎)) |
| 156 | 41 | adantrr 717 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 ≠ 𝐵)) → -𝑥 ∈ (𝐴(,)𝐵)) |
| 157 | | limcresi 25920 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ↦ -𝑥) limℂ -𝐵) ⊆ (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) limℂ -𝐵) |
| 158 | | resmpt 6055 |
. . . . . . . . . . 11
⊢ ((-𝐵(,)-𝑎) ⊆ ℝ → ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)) |
| 159 | 97, 158 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) |
| 160 | 159 | oveq1i 7441 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) limℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) limℂ -𝐵) |
| 161 | 157, 160 | sseqtri 4032 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ↦ -𝑥) limℂ -𝐵) ⊆ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) limℂ -𝐵) |
| 162 | 72 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ℂ) |
| 163 | 162 | negnegd 11611 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → --𝐵 = 𝐵) |
| 164 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ ↦ -𝑥) = (𝑥 ∈ ℝ ↦ -𝑥) |
| 165 | 164 | negcncf 24948 |
. . . . . . . . . . 11
⊢ (ℝ
⊆ ℂ → (𝑥
∈ ℝ ↦ -𝑥)
∈ (ℝ–cn→ℂ)) |
| 166 | 51, 165 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ)) |
| 167 | | negeq 11500 |
. . . . . . . . . 10
⊢ (𝑥 = -𝐵 → -𝑥 = --𝐵) |
| 168 | 166, 76, 167 | cnmptlimc 25925 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → --𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) limℂ -𝐵)) |
| 169 | 163, 168 | eqeltrrd 2842 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) limℂ -𝐵)) |
| 170 | 161, 169 | sselid 3981 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) limℂ -𝐵)) |
| 171 | | lhop2.f0 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐵)) |
| 172 | 171 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ (𝐹 limℂ 𝐵)) |
| 173 | 105 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐹 limℂ 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)) limℂ 𝐵)) |
| 174 | 172, 173 | eleqtrd 2843 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)) limℂ 𝐵)) |
| 175 | | eliooord 13446 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → (-𝐵 < 𝑥 ∧ 𝑥 < -𝑎)) |
| 176 | 175 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝐵 < 𝑥 ∧ 𝑥 < -𝑎)) |
| 177 | 176 | simpld 494 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝐵 < 𝑥) |
| 178 | 29, 23, 177 | ltnegcon1d 11843 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 < 𝐵) |
| 179 | 30, 178 | ltned 11397 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ≠ 𝐵) |
| 180 | 179 | neneqd 2945 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ -𝑥 = 𝐵) |
| 181 | 180 | pm2.21d 121 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐹‘-𝑥) = 0)) |
| 182 | 181 | impr 454 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐹‘-𝑥) = 0) |
| 183 | 156, 90, 170, 174, 114, 182 | limcco 25928 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) limℂ -𝐵)) |
| 184 | | lhop2.g0 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝐵)) |
| 185 | 184 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ (𝐺 limℂ 𝐵)) |
| 186 | 132 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐺 limℂ 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)) limℂ 𝐵)) |
| 187 | 185, 186 | eleqtrd 2843 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑦)) limℂ 𝐵)) |
| 188 | 180 | pm2.21d 121 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐺‘-𝑥) = 0)) |
| 189 | 188 | impr 454 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐺‘-𝑥) = 0) |
| 190 | 156, 130,
170, 187, 141, 189 | limcco 25928 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) limℂ -𝐵)) |
| 191 | 57 | fmpttd 7135 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ran 𝐺) |
| 192 | 191 | frnd 6744 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) ⊆ ran 𝐺) |
| 193 | 48 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran 𝐺) |
| 194 | 192, 193 | ssneldd 3986 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) |
| 195 | | lhop2.gd0 |
. . . . . . . 8
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐺)) |
| 196 | 195 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D
𝐺)) |
| 197 | 150 | rneqd 5949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))) |
| 198 | 197 | eleq2d 2827 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) ↔ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))) |
| 199 | 153, 152 | elrnmpti 5973 |
. . . . . . . . 9
⊢ (0 ∈
ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) ↔ ∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥)) |
| 200 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (0 =
-((ℝ D 𝐺)‘-𝑥) ↔ -((ℝ D 𝐺)‘-𝑥) = 0) |
| 201 | 145 | negeq0d 11612 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 ↔ -((ℝ D 𝐺)‘-𝑥) = 0)) |
| 202 | 144 | ffnd 6737 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
| 203 | | fnfvelrn 7100 |
. . . . . . . . . . . . . 14
⊢
(((ℝ D 𝐺) Fn
(𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺)) |
| 204 | 202, 41, 203 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺)) |
| 205 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢
(((ℝ D 𝐺)‘-𝑥) = 0 → (((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺))) |
| 206 | 204, 205 | syl5ibcom 245 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
| 207 | 201, 206 | sylbird 260 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
| 208 | 200, 207 | biimtrid 242 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺))) |
| 209 | 208 | rexlimdva 3155 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺))) |
| 210 | 199, 209 | biimtrid 242 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) → 0 ∈ ran (ℝ D 𝐺))) |
| 211 | 198, 210 | sylbid 240 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) → 0 ∈ ran (ℝ D 𝐺))) |
| 212 | 196, 211 | mtod 198 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D
(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))) |
| 213 | 111 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ ℂ) |
| 214 | 138 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ℂ) |
| 215 | 195 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran (ℝ D
𝐺)) |
| 216 | 138 | ffnd 6737 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (ℝ D 𝐺) Fn (𝐴(,)𝐵)) |
| 217 | | fnfvelrn 7100 |
. . . . . . . . . . . . 13
⊢
(((ℝ D 𝐺) Fn
(𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺)) |
| 218 | 216, 217 | sylan 580 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺)) |
| 219 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢
(((ℝ D 𝐺)‘𝑧) = 0 → (((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺))) |
| 220 | 218, 219 | syl5ibcom 245 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐺)‘𝑧) = 0 → 0 ∈ ran (ℝ D 𝐺))) |
| 221 | 220 | necon3bd 2954 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran (ℝ D
𝐺) → ((ℝ D 𝐺)‘𝑧) ≠ 0)) |
| 222 | 215, 221 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ≠ 0) |
| 223 | 213, 214,
222 | divcld 12043 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) ∈ ℂ) |
| 224 | | lhop2.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵)) |
| 225 | 224 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) limℂ 𝐵)) |
| 226 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑧 = -𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘-𝑥)) |
| 227 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑧 = -𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘-𝑥)) |
| 228 | 226, 227 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑧 = -𝑥 → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) |
| 229 | 180 | pm2.21d 121 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶)) |
| 230 | 229 | impr 454 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶) |
| 231 | 156, 223,
170, 225, 228, 230 | limcco 25928 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) limℂ -𝐵)) |
| 232 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥ℝ |
| 233 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥
D |
| 234 | | nfmpt1 5250 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) |
| 235 | 232, 233,
234 | nfov 7461 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) |
| 236 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑦 |
| 237 | 235, 236 | nffv 6916 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) |
| 238 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥
/ |
| 239 | | nfmpt1 5250 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) |
| 240 | 232, 233,
239 | nfov 7461 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) |
| 241 | 240, 236 | nffv 6916 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦) |
| 242 | 237, 238,
241 | nfov 7461 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)) |
| 243 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) |
| 244 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥)) |
| 245 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) |
| 246 | 244, 245 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)) = (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))) |
| 247 | 242, 243,
246 | cbvmpt 5253 |
. . . . . . . . 9
⊢ (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))) |
| 248 | 123 | fveq1d 6908 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥)) |
| 249 | 126 | fvmpt2 7027 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐹)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥)) |
| 250 | 125, 249 | mpan2 691 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥)) |
| 251 | 248, 250 | sylan9eq 2797 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = -((ℝ D 𝐹)‘-𝑥)) |
| 252 | 150 | fveq1d 6908 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥)) |
| 253 | 153 | fvmpt2 7027 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐺)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥)) |
| 254 | 152, 253 | mpan2 691 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥)) |
| 255 | 252, 254 | sylan9eq 2797 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = -((ℝ D 𝐺)‘-𝑥)) |
| 256 | 251, 255 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥))) |
| 257 | 195 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran (ℝ D 𝐺)) |
| 258 | 206 | necon3bd 2954 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran (ℝ D
𝐺) → ((ℝ D 𝐺)‘-𝑥) ≠ 0)) |
| 259 | 257, 258 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ≠ 0) |
| 260 | 118, 145,
259 | div2negd 12058 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) |
| 261 | 256, 260 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) |
| 262 | 261 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))) |
| 263 | 247, 262 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))) |
| 264 | 263 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) limℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) limℂ -𝐵)) |
| 265 | 231, 264 | eleqtrrd 2844 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) limℂ -𝐵)) |
| 266 | 76, 78, 81, 82, 83, 128, 155, 183, 190, 194, 212, 265 | lhop1 26053 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) limℂ -𝐵)) |
| 267 | | nffvmpt1 6917 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) |
| 268 | | nffvmpt1 6917 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦) |
| 269 | 267, 238,
268 | nfov 7461 |
. . . . . . . 8
⊢
Ⅎ𝑥(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)) |
| 270 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑦(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)) |
| 271 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥)) |
| 272 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)) |
| 273 | 271, 272 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)) = (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))) |
| 274 | 269, 270,
273 | cbvmpt 5253 |
. . . . . . 7
⊢ (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))) |
| 275 | | fvex 6919 |
. . . . . . . . . 10
⊢ (𝐹‘-𝑥) ∈ V |
| 276 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) |
| 277 | 276 | fvmpt2 7027 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐹‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥)) |
| 278 | 26, 275, 277 | sylancl 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥)) |
| 279 | | fvex 6919 |
. . . . . . . . . 10
⊢ (𝐺‘-𝑥) ∈ V |
| 280 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) |
| 281 | 280 | fvmpt2 7027 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐺‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥)) |
| 282 | 26, 279, 281 | sylancl 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥)) |
| 283 | 278, 282 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)) = ((𝐹‘-𝑥) / (𝐺‘-𝑥))) |
| 284 | 283 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥)))) |
| 285 | 274, 284 | eqtrid 2789 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥)))) |
| 286 | 285 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) limℂ -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) limℂ -𝐵)) |
| 287 | 266, 286 | eleqtrd 2843 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) limℂ -𝐵)) |
| 288 | | negeq 11500 |
. . . . . 6
⊢ (𝑥 = -𝑧 → -𝑥 = --𝑧) |
| 289 | 288 | fveq2d 6910 |
. . . . 5
⊢ (𝑥 = -𝑧 → (𝐹‘-𝑥) = (𝐹‘--𝑧)) |
| 290 | 288 | fveq2d 6910 |
. . . . 5
⊢ (𝑥 = -𝑧 → (𝐺‘-𝑥) = (𝐺‘--𝑧)) |
| 291 | 289, 290 | oveq12d 7449 |
. . . 4
⊢ (𝑥 = -𝑧 → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) = ((𝐹‘--𝑧) / (𝐺‘--𝑧))) |
| 292 | 76 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 ∈ ℝ) |
| 293 | | eliooord 13446 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑎(,)𝐵) → (𝑎 < 𝑧 ∧ 𝑧 < 𝐵)) |
| 294 | 293 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑎 < 𝑧 ∧ 𝑧 < 𝐵)) |
| 295 | 294 | simprd 495 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 < 𝐵) |
| 296 | 15, 13 | ltnegd 11841 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 < 𝐵 ↔ -𝐵 < -𝑧)) |
| 297 | 295, 296 | mpbid 232 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 < -𝑧) |
| 298 | 292, 297 | gtned 11396 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ≠ -𝐵) |
| 299 | 298 | neneqd 2945 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ¬ -𝑧 = -𝐵) |
| 300 | 299 | pm2.21d 121 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (-𝑧 = -𝐵 → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶)) |
| 301 | 300 | impr 454 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 = -𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶) |
| 302 | 19, 62, 75, 287, 291, 301 | limcco 25928 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) limℂ 𝐵)) |
| 303 | 15 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℂ) |
| 304 | 303 | negnegd 11611 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → --𝑧 = 𝑧) |
| 305 | 304 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐹‘--𝑧) = (𝐹‘𝑧)) |
| 306 | 304 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐺‘--𝑧) = (𝐺‘𝑧)) |
| 307 | 305, 306 | oveq12d 7449 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = ((𝐹‘𝑧) / (𝐺‘𝑧))) |
| 308 | 307 | mpteq2dva 5242 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧)))) |
| 309 | 308 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) limℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
| 310 | 39 | resmptd 6058 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧)))) |
| 311 | 310 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) limℂ 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
| 312 | | fss 6752 |
. . . . . . . . 9
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
| 313 | 88, 51, 312 | sylancl 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
| 314 | 313 | ffvelcdmda 7104 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑧) ∈ ℂ) |
| 315 | 53 | ffvelcdmda 7104 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ℂ) |
| 316 | 48 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran 𝐺) |
| 317 | 50 | ffnd 6737 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐺 Fn (𝐴(,)𝐵)) |
| 318 | | fnfvelrn 7100 |
. . . . . . . . . . 11
⊢ ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ran 𝐺) |
| 319 | 317, 318 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ran 𝐺) |
| 320 | | eleq1 2829 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑧) = 0 → ((𝐺‘𝑧) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺)) |
| 321 | 319, 320 | syl5ibcom 245 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐺‘𝑧) = 0 → 0 ∈ ran 𝐺)) |
| 322 | 321 | necon3bd 2954 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran 𝐺 → (𝐺‘𝑧) ≠ 0)) |
| 323 | 316, 322 | mpd 15 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ≠ 0) |
| 324 | 314, 315,
323 | divcld 12043 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑧) / (𝐺‘𝑧)) ∈ ℂ) |
| 325 | 324 | fmpttd 7135 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))):(𝐴(,)𝐵)⟶ℂ) |
| 326 | | ioossre 13448 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 327 | 326, 51 | sstri 3993 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℂ |
| 328 | 327 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℂ) |
| 329 | | eqid 2737 |
. . . . 5
⊢
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((TopOpen‘ℂfld)
↾t ((𝐴(,)𝐵) ∪ {𝐵})) |
| 330 | | ssun2 4179 |
. . . . . . 7
⊢ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵}) |
| 331 | | snssg 4783 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵}))) |
| 332 | 72, 331 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵}))) |
| 333 | 330, 332 | mpbiri 258 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵})) |
| 334 | 100 | cnfldtopon 24803 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 335 | 326 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℝ) |
| 336 | 72 | snssd 4809 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → {𝐵} ⊆ ℝ) |
| 337 | 335, 336 | unssd 4192 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ) |
| 338 | 337, 51 | sstrdi 3996 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ) |
| 339 | | resttopon 23169 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵}))) |
| 340 | 334, 338,
339 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵}))) |
| 341 | | topontop 22919 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})) →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top) |
| 342 | 340, 341 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top) |
| 343 | | indi 4284 |
. . . . . . . . . 10
⊢ ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵})) |
| 344 | | pnfxr 11315 |
. . . . . . . . . . . . . 14
⊢ +∞
∈ ℝ* |
| 345 | 344 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → +∞ ∈
ℝ*) |
| 346 | 4 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈
ℝ*) |
| 347 | | iooin 13421 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
→ ((𝑎(,)+∞)
∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵))) |
| 348 | 35, 345, 34, 346, 347 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵))) |
| 349 | | xrltnle 11328 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ*
∧ 𝑎 ∈
ℝ*) → (𝐴 < 𝑎 ↔ ¬ 𝑎 ≤ 𝐴)) |
| 350 | 34, 35, 349 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐴 < 𝑎 ↔ ¬ 𝑎 ≤ 𝐴)) |
| 351 | 36, 350 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ 𝑎 ≤ 𝐴) |
| 352 | 351 | iffalsed 4536 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → if(𝑎 ≤ 𝐴, 𝐴, 𝑎) = 𝑎) |
| 353 | 72 | ltpnfd 13163 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 < +∞) |
| 354 | | xrltnle 11328 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝐵 < +∞ ↔ ¬ +∞ ≤
𝐵)) |
| 355 | 346, 344,
354 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 < +∞ ↔ ¬ +∞ ≤
𝐵)) |
| 356 | 353, 355 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ¬ +∞ ≤ 𝐵) |
| 357 | 356 | iffalsed 4536 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → if(+∞ ≤ 𝐵, +∞, 𝐵) = 𝐵) |
| 358 | 352, 357 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (if(𝑎 ≤ 𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)) = (𝑎(,)𝐵)) |
| 359 | 348, 358 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (𝑎(,)𝐵)) |
| 360 | | elioopnf 13483 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℝ*
→ (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵))) |
| 361 | 35, 360 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵))) |
| 362 | 72, 79, 361 | mpbir2and 713 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈ (𝑎(,)+∞)) |
| 363 | 362 | snssd 4809 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → {𝐵} ⊆ (𝑎(,)+∞)) |
| 364 | | sseqin2 4223 |
. . . . . . . . . . . 12
⊢ ({𝐵} ⊆ (𝑎(,)+∞) ↔ ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵}) |
| 365 | 363, 364 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵}) |
| 366 | 359, 365 | uneq12d 4169 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵})) |
| 367 | 343, 366 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵})) |
| 368 | | retop 24782 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) ∈ Top |
| 369 | | reex 11246 |
. . . . . . . . . . . 12
⊢ ℝ
∈ V |
| 370 | 369 | ssex 5321 |
. . . . . . . . . . 11
⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V) |
| 371 | 337, 370 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V) |
| 372 | | iooretop 24786 |
. . . . . . . . . . 11
⊢ (𝑎(,)+∞) ∈
(topGen‘ran (,)) |
| 373 | 372 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (𝑎(,)+∞) ∈ (topGen‘ran
(,))) |
| 374 | | elrestr 17473 |
. . . . . . . . . 10
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V ∧ (𝑎(,)+∞) ∈ (topGen‘ran (,)))
→ ((𝑎(,)+∞)
∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,))
↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
| 375 | 368, 371,
373, 374 | mp3an2i 1468 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,))
↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
| 376 | 367, 375 | eqeltrrd 2842 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((topGen‘ran (,))
↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
| 377 | | eqid 2737 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 378 | 100, 377 | rerest 24825 |
. . . . . . . . 9
⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,))
↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
| 379 | 337, 378 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) →
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,))
↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
| 380 | 376, 379 | eleqtrrd 2844 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))) |
| 381 | | isopn3i 23090 |
. . . . . . 7
⊢
((((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top ∧ ((𝑎(,)𝐵) ∪ {𝐵}) ∈
((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))) →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵})) |
| 382 | 342, 380,
381 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵})) |
| 383 | 333, 382 | eleqtrrd 2844 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵}))) |
| 384 | 325, 39, 328, 100, 329, 383 | limcres 25921 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) ↾ (𝑎(,)𝐵)) limℂ 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
| 385 | 309, 311,
384 | 3eqtr2d 2783 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) limℂ 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
| 386 | 302, 385 | eleqtrd 2843 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎 ∧ 𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |
| 387 | 9, 386 | rexlimddv 3161 |
1
⊢ (𝜑 → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑧) / (𝐺‘𝑧))) limℂ 𝐵)) |