MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lhop2 Structured version   Visualization version   GIF version

Theorem lhop2 25935
Description: L'Hôpital's Rule for limits from the left. If 𝐹 and 𝐺 are differentiable real functions on (𝐴, 𝐵), and 𝐹 and 𝐺 both approach 0 at 𝐵, and 𝐺(𝑥) and 𝐺' (𝑥) are not zero on (𝐴, 𝐵), and the limit of 𝐹' (𝑥) / 𝐺' (𝑥) at 𝐵 is 𝐶, then the limit 𝐹(𝑥) / 𝐺(𝑥) at 𝐵 also exists and equals 𝐶. (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypotheses
Ref Expression
lhop2.a (𝜑𝐴 ∈ ℝ*)
lhop2.b (𝜑𝐵 ∈ ℝ)
lhop2.l (𝜑𝐴 < 𝐵)
lhop2.f (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
lhop2.g (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
lhop2.if (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
lhop2.ig (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
lhop2.f0 (𝜑 → 0 ∈ (𝐹 lim 𝐵))
lhop2.g0 (𝜑 → 0 ∈ (𝐺 lim 𝐵))
lhop2.gn0 (𝜑 → ¬ 0 ∈ ran 𝐺)
lhop2.gd0 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
lhop2.c (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
Assertion
Ref Expression
lhop2 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
Distinct variable groups:   𝑧,𝐴   𝑧,𝐵   𝑧,𝐶   𝜑,𝑧   𝑧,𝐹   𝑧,𝐺

Proof of Theorem lhop2
Dummy variables 𝑥 𝑎 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qssre 12965 . . 3 ℚ ⊆ ℝ
2 lhop2.a . . . 4 (𝜑𝐴 ∈ ℝ*)
3 lhop2.b . . . . 5 (𝜑𝐵 ∈ ℝ)
43rexrd 11286 . . . 4 (𝜑𝐵 ∈ ℝ*)
5 lhop2.l . . . 4 (𝜑𝐴 < 𝐵)
6 qbtwnxr 13203 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → ∃𝑎 ∈ ℚ (𝐴 < 𝑎𝑎 < 𝐵))
72, 4, 5, 6syl3anc 1369 . . 3 (𝜑 → ∃𝑎 ∈ ℚ (𝐴 < 𝑎𝑎 < 𝐵))
8 ssrexv 4047 . . 3 (ℚ ⊆ ℝ → (∃𝑎 ∈ ℚ (𝐴 < 𝑎𝑎 < 𝐵) → ∃𝑎 ∈ ℝ (𝐴 < 𝑎𝑎 < 𝐵)))
91, 7, 8mpsyl 68 . 2 (𝜑 → ∃𝑎 ∈ ℝ (𝐴 < 𝑎𝑎 < 𝐵))
10 simpr 484 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ (𝑎(,)𝐵))
11 simprl 770 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝑎 ∈ ℝ)
1211adantr 480 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑎 ∈ ℝ)
133ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝐵 ∈ ℝ)
14 elioore 13378 . . . . . . . 8 (𝑧 ∈ (𝑎(,)𝐵) → 𝑧 ∈ ℝ)
1514adantl 481 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℝ)
16 iooneg 13472 . . . . . . 7 ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎)))
1712, 13, 15, 16syl3anc 1369 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎)))
1810, 17mpbid 231 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎))
1918adantrr 716 . . . 4 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 ≠ -𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎))
20 lhop2.f . . . . . . . 8 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
2120ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
22 elioore 13378 . . . . . . . . . . . . 13 (𝑥 ∈ (-𝐵(,)-𝑎) → 𝑥 ∈ ℝ)
2322adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℝ)
2423recnd 11264 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℂ)
2524negnegd 11584 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 = 𝑥)
26 simpr 484 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ (-𝐵(,)-𝑎))
2725, 26eqeltrd 2828 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 ∈ (-𝐵(,)-𝑎))
2811adantr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑎 ∈ ℝ)
293ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐵 ∈ ℝ)
3023renegcld 11663 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ ℝ)
31 iooneg 13472 . . . . . . . . . 10 ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ -𝑥 ∈ ℝ) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎)))
3228, 29, 30, 31syl3anc 1369 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎)))
3327, 32mpbird 257 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝑎(,)𝐵))
342adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐴 ∈ ℝ*)
3511rexrd 11286 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝑎 ∈ ℝ*)
36 simprrl 780 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐴 < 𝑎)
3734, 35, 36xrltled 13153 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐴𝑎)
38 iooss1 13383 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐴𝑎) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵))
3934, 37, 38syl2anc 583 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵))
4039sselda 3978 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ -𝑥 ∈ (𝑎(,)𝐵)) → -𝑥 ∈ (𝐴(,)𝐵))
4133, 40syldan 590 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝐴(,)𝐵))
4221, 41ffvelcdmd 7089 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℝ)
4342recnd 11264 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℂ)
44 lhop2.g . . . . . . . 8 (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
4544ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
4645, 41ffvelcdmd 7089 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℝ)
4746recnd 11264 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℂ)
48 lhop2.gn0 . . . . . . 7 (𝜑 → ¬ 0 ∈ ran 𝐺)
4948ad2antrr 725 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran 𝐺)
5044adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
51 ax-resscn 11187 . . . . . . . . . . . 12 ℝ ⊆ ℂ
52 fss 6733 . . . . . . . . . . . 12 ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
5350, 51, 52sylancl 585 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
5453adantr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
5554ffnd 6717 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺 Fn (𝐴(,)𝐵))
56 fnfvelrn 7084 . . . . . . . . 9 ((𝐺 Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘-𝑥) ∈ ran 𝐺)
5755, 41, 56syl2anc 583 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ran 𝐺)
58 eleq1 2816 . . . . . . . 8 ((𝐺‘-𝑥) = 0 → ((𝐺‘-𝑥) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
5957, 58syl5ibcom 244 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐺‘-𝑥) = 0 → 0 ∈ ran 𝐺))
6059necon3bd 2949 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran 𝐺 → (𝐺‘-𝑥) ≠ 0))
6149, 60mpd 15 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ≠ 0)
6243, 47, 61divcld 12012 . . . 4 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) ∈ ℂ)
63 limcresi 25801 . . . . . 6 ((𝑧 ∈ ℝ ↦ -𝑧) lim 𝐵) ⊆ (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) lim 𝐵)
64 ioossre 13409 . . . . . . . 8 (𝑎(,)𝐵) ⊆ ℝ
65 resmpt 6035 . . . . . . . 8 ((𝑎(,)𝐵) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧))
6664, 65ax-mp 5 . . . . . . 7 ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧)
6766oveq1i 7424 . . . . . 6 (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) lim 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim 𝐵)
6863, 67sseqtri 4014 . . . . 5 ((𝑧 ∈ ℝ ↦ -𝑧) lim 𝐵) ⊆ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim 𝐵)
69 eqid 2727 . . . . . . . 8 (𝑧 ∈ ℝ ↦ -𝑧) = (𝑧 ∈ ℝ ↦ -𝑧)
7069negcncf 24829 . . . . . . 7 (ℝ ⊆ ℂ → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ))
7151, 70mp1i 13 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ))
723adantr 480 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ℝ)
73 negeq 11474 . . . . . 6 (𝑧 = 𝐵 → -𝑧 = -𝐵)
7471, 72, 73cnmptlimc 25806 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ ℝ ↦ -𝑧) lim 𝐵))
7568, 74sselid 3976 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim 𝐵))
7672renegcld 11663 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 ∈ ℝ)
7711renegcld 11663 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝑎 ∈ ℝ)
7877rexrd 11286 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝑎 ∈ ℝ*)
79 simprrr 781 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝑎 < 𝐵)
8011, 72ltnegd 11814 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑎 < 𝐵 ↔ -𝐵 < -𝑎))
8179, 80mpbid 231 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 < -𝑎)
8242fmpttd 7119 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ)
8346fmpttd 7119 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ)
84 reelprrecn 11222 . . . . . . . . . . 11 ℝ ∈ {ℝ, ℂ}
8584a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ℝ ∈ {ℝ, ℂ})
86 neg1cn 12348 . . . . . . . . . . 11 -1 ∈ ℂ
8786a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -1 ∈ ℂ)
8820adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
8988ffvelcdmda 7088 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹𝑦) ∈ ℝ)
9089recnd 11264 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹𝑦) ∈ ℂ)
91 fvexd 6906 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ V)
92 1cnd 11231 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 1 ∈ ℂ)
93 simpr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
9493recnd 11264 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
95 1cnd 11231 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
9685dvmptid 25876 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
97 ioossre 13409 . . . . . . . . . . . . 13 (-𝐵(,)-𝑎) ⊆ ℝ
9897a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ⊆ ℝ)
99 eqid 2727 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
10099tgioo2 24706 . . . . . . . . . . . 12 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
101 iooretop 24669 . . . . . . . . . . . . 13 (-𝐵(,)-𝑎) ∈ (topGen‘ran (,))
102101a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ∈ (topGen‘ran (,)))
10385, 94, 95, 96, 98, 100, 99, 102dvmptres 25882 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 1))
10485, 24, 92, 103dvmptneg 25885 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -1))
10588feqmptd 6961 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦)))
106105oveq2d 7430 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦))))
107 dvf 25823 . . . . . . . . . . . . 13 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
108 lhop2.if . . . . . . . . . . . . . . 15 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
109108adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
110109feq2d 6702 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
111107, 110mpbii 232 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
112111feqmptd 6961 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐹) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
113106, 112eqtr3d 2769 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
114 fveq2 6891 . . . . . . . . . 10 (𝑦 = -𝑥 → (𝐹𝑦) = (𝐹‘-𝑥))
115 fveq2 6891 . . . . . . . . . 10 (𝑦 = -𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘-𝑥))
11685, 85, 41, 87, 90, 91, 104, 113, 114, 115dvmptco 25891 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)))
117111adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
118117, 41ffvelcdmd 7089 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐹)‘-𝑥) ∈ ℂ)
119118, 87mulcomd 11257 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = (-1 · ((ℝ D 𝐹)‘-𝑥)))
120118mulm1d 11688 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐹)‘-𝑥)) = -((ℝ D 𝐹)‘-𝑥))
121119, 120eqtrd 2767 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = -((ℝ D 𝐹)‘-𝑥))
122121mpteq2dva 5242 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
123116, 122eqtrd 2767 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
124123dmeqd 5902 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
125 negex 11480 . . . . . . . 8 -((ℝ D 𝐹)‘-𝑥) ∈ V
126 eqid 2727 . . . . . . . 8 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))
127125, 126dmmpti 6693 . . . . . . 7 dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (-𝐵(,)-𝑎)
128124, 127eqtrdi 2783 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (-𝐵(,)-𝑎))
12950ffvelcdmda 7088 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺𝑦) ∈ ℝ)
130129recnd 11264 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺𝑦) ∈ ℂ)
131 fvexd 6906 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑦) ∈ V)
13250feqmptd 6961 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦)))
133132oveq2d 7430 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦))))
134 dvf 25823 . . . . . . . . . . . . 13 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
135 lhop2.ig . . . . . . . . . . . . . . 15 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
136135adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
137136feq2d 6702 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
138134, 137mpbii 232 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
139138feqmptd 6961 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦)))
140133, 139eqtr3d 2769 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦)))
141 fveq2 6891 . . . . . . . . . 10 (𝑦 = -𝑥 → (𝐺𝑦) = (𝐺‘-𝑥))
142 fveq2 6891 . . . . . . . . . 10 (𝑦 = -𝑥 → ((ℝ D 𝐺)‘𝑦) = ((ℝ D 𝐺)‘-𝑥))
14385, 85, 41, 87, 130, 131, 104, 140, 141, 142dvmptco 25891 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)))
144138adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
145144, 41ffvelcdmd 7089 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ℂ)
146145, 87mulcomd 11257 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = (-1 · ((ℝ D 𝐺)‘-𝑥)))
147145mulm1d 11688 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐺)‘-𝑥)) = -((ℝ D 𝐺)‘-𝑥))
148146, 147eqtrd 2767 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = -((ℝ D 𝐺)‘-𝑥))
149148mpteq2dva 5242 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
150143, 149eqtrd 2767 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
151150dmeqd 5902 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
152 negex 11480 . . . . . . . 8 -((ℝ D 𝐺)‘-𝑥) ∈ V
153 eqid 2727 . . . . . . . 8 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))
154152, 153dmmpti 6693 . . . . . . 7 dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (-𝐵(,)-𝑎)
155151, 154eqtrdi 2783 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (-𝐵(,)-𝑎))
15641adantrr 716 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥𝐵)) → -𝑥 ∈ (𝐴(,)𝐵))
157 limcresi 25801 . . . . . . . . 9 ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵) ⊆ (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) lim -𝐵)
158 resmpt 6035 . . . . . . . . . . 11 ((-𝐵(,)-𝑎) ⊆ ℝ → ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥))
15997, 158ax-mp 5 . . . . . . . . . 10 ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)
160159oveq1i 7424 . . . . . . . . 9 (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) lim -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim -𝐵)
161157, 160sseqtri 4014 . . . . . . . 8 ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵) ⊆ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim -𝐵)
16272recnd 11264 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ℂ)
163162negnegd 11584 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → --𝐵 = 𝐵)
164 eqid 2727 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ -𝑥) = (𝑥 ∈ ℝ ↦ -𝑥)
165164negcncf 24829 . . . . . . . . . . 11 (ℝ ⊆ ℂ → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ))
16651, 165mp1i 13 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ))
167 negeq 11474 . . . . . . . . . 10 (𝑥 = -𝐵 → -𝑥 = --𝐵)
168166, 76, 167cnmptlimc 25806 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → --𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵))
169163, 168eqeltrrd 2829 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵))
170161, 169sselid 3976 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim -𝐵))
171 lhop2.f0 . . . . . . . . 9 (𝜑 → 0 ∈ (𝐹 lim 𝐵))
172171adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ (𝐹 lim 𝐵))
173105oveq1d 7429 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐹 lim 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦)) lim 𝐵))
174172, 173eleqtrd 2830 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦)) lim 𝐵))
175 eliooord 13407 . . . . . . . . . . . . . 14 (𝑥 ∈ (-𝐵(,)-𝑎) → (-𝐵 < 𝑥𝑥 < -𝑎))
176175adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝐵 < 𝑥𝑥 < -𝑎))
177176simpld 494 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝐵 < 𝑥)
17829, 23, 177ltnegcon1d 11816 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 < 𝐵)
17930, 178ltned 11372 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥𝐵)
180179neneqd 2940 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ -𝑥 = 𝐵)
181180pm2.21d 121 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐹‘-𝑥) = 0))
182181impr 454 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐹‘-𝑥) = 0)
183156, 90, 170, 174, 114, 182limcco 25809 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) lim -𝐵))
184 lhop2.g0 . . . . . . . . 9 (𝜑 → 0 ∈ (𝐺 lim 𝐵))
185184adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ (𝐺 lim 𝐵))
186132oveq1d 7429 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐺 lim 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦)) lim 𝐵))
187185, 186eleqtrd 2830 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦)) lim 𝐵))
188180pm2.21d 121 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐺‘-𝑥) = 0))
189188impr 454 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐺‘-𝑥) = 0)
190156, 130, 170, 187, 141, 189limcco 25809 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) lim -𝐵))
19157fmpttd 7119 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ran 𝐺)
192191frnd 6724 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) ⊆ ran 𝐺)
19348adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran 𝐺)
194192, 193ssneldd 3981 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))
195 lhop2.gd0 . . . . . . . 8 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
196195adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D 𝐺))
197150rneqd 5934 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
198197eleq2d 2814 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) ↔ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))))
199153, 152elrnmpti 5956 . . . . . . . . 9 (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) ↔ ∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥))
200 eqcom 2734 . . . . . . . . . . 11 (0 = -((ℝ D 𝐺)‘-𝑥) ↔ -((ℝ D 𝐺)‘-𝑥) = 0)
201145negeq0d 11585 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 ↔ -((ℝ D 𝐺)‘-𝑥) = 0))
202144ffnd 6717 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
203 fnfvelrn 7084 . . . . . . . . . . . . . 14 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺))
204202, 41, 203syl2anc 583 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺))
205 eleq1 2816 . . . . . . . . . . . . 13 (((ℝ D 𝐺)‘-𝑥) = 0 → (((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
206204, 205syl5ibcom 244 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺)))
207201, 206sylbird 260 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺)))
208200, 207biimtrid 241 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺)))
209208rexlimdva 3150 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺)))
210199, 209biimtrid 241 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) → 0 ∈ ran (ℝ D 𝐺)))
211198, 210sylbid 239 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) → 0 ∈ ran (ℝ D 𝐺)))
212196, 211mtod 197 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))))
213111ffvelcdmda 7088 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ ℂ)
214138ffvelcdmda 7088 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ℂ)
215195ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran (ℝ D 𝐺))
216138ffnd 6717 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
217 fnfvelrn 7084 . . . . . . . . . . . . 13 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
218216, 217sylan 579 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
219 eleq1 2816 . . . . . . . . . . . 12 (((ℝ D 𝐺)‘𝑧) = 0 → (((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
220218, 219syl5ibcom 244 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐺)‘𝑧) = 0 → 0 ∈ ran (ℝ D 𝐺)))
221220necon3bd 2949 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘𝑧) ≠ 0))
222215, 221mpd 15 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ≠ 0)
223213, 214, 222divcld 12012 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) ∈ ℂ)
224 lhop2.c . . . . . . . . 9 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
225224adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
226 fveq2 6891 . . . . . . . . 9 (𝑧 = -𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘-𝑥))
227 fveq2 6891 . . . . . . . . 9 (𝑧 = -𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘-𝑥))
228226, 227oveq12d 7432 . . . . . . . 8 (𝑧 = -𝑥 → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
229180pm2.21d 121 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶))
230229impr 454 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶)
231156, 223, 170, 225, 228, 230limcco 25809 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) lim -𝐵))
232 nfcv 2898 . . . . . . . . . . . . 13 𝑥
233 nfcv 2898 . . . . . . . . . . . . 13 𝑥 D
234 nfmpt1 5250 . . . . . . . . . . . . 13 𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))
235232, 233, 234nfov 7444 . . . . . . . . . . . 12 𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))
236 nfcv 2898 . . . . . . . . . . . 12 𝑥𝑦
237235, 236nffv 6901 . . . . . . . . . . 11 𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦)
238 nfcv 2898 . . . . . . . . . . 11 𝑥 /
239 nfmpt1 5250 . . . . . . . . . . . . 13 𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))
240232, 233, 239nfov 7444 . . . . . . . . . . . 12 𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))
241240, 236nffv 6901 . . . . . . . . . . 11 𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)
242237, 238, 241nfov 7444 . . . . . . . . . 10 𝑥(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))
243 nfcv 2898 . . . . . . . . . 10 𝑦(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))
244 fveq2 6891 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥))
245 fveq2 6891 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))
246244, 245oveq12d 7432 . . . . . . . . . 10 (𝑦 = 𝑥 → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)) = (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)))
247242, 243, 246cbvmpt 5253 . . . . . . . . 9 (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)))
248123fveq1d 6893 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥))
249126fvmpt2 7010 . . . . . . . . . . . . . 14 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐹)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
250125, 249mpan2 690 . . . . . . . . . . . . 13 (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
251248, 250sylan9eq 2787 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
252150fveq1d 6893 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥))
253153fvmpt2 7010 . . . . . . . . . . . . . 14 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐺)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
254152, 253mpan2 690 . . . . . . . . . . . . 13 (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
255252, 254sylan9eq 2787 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
256251, 255oveq12d 7432 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)))
257195ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran (ℝ D 𝐺))
258206necon3bd 2949 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘-𝑥) ≠ 0))
259257, 258mpd 15 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ≠ 0)
260118, 145, 259div2negd 12027 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
261256, 260eqtrd 2767 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
262261mpteq2dva 5242 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))))
263247, 262eqtrid 2779 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))))
264263oveq1d 7429 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) lim -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) lim -𝐵))
265231, 264eleqtrrd 2831 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) lim -𝐵))
26676, 78, 81, 82, 83, 128, 155, 183, 190, 194, 212, 265lhop1 25934 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) lim -𝐵))
267 nffvmpt1 6902 . . . . . . . . 9 𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦)
268 nffvmpt1 6902 . . . . . . . . 9 𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)
269267, 238, 268nfov 7444 . . . . . . . 8 𝑥(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))
270 nfcv 2898 . . . . . . . 8 𝑦(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))
271 fveq2 6891 . . . . . . . . 9 (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥))
272 fveq2 6891 . . . . . . . . 9 (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))
273271, 272oveq12d 7432 . . . . . . . 8 (𝑦 = 𝑥 → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)) = (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)))
274269, 270, 273cbvmpt 5253 . . . . . . 7 (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)))
275 fvex 6904 . . . . . . . . . 10 (𝐹‘-𝑥) ∈ V
276 eqid 2727 . . . . . . . . . . 11 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))
277276fvmpt2 7010 . . . . . . . . . 10 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐹‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥))
27826, 275, 277sylancl 585 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥))
279 fvex 6904 . . . . . . . . . 10 (𝐺‘-𝑥) ∈ V
280 eqid 2727 . . . . . . . . . . 11 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))
281280fvmpt2 7010 . . . . . . . . . 10 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐺‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥))
28226, 279, 281sylancl 585 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥))
283278, 282oveq12d 7432 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)) = ((𝐹‘-𝑥) / (𝐺‘-𝑥)))
284283mpteq2dva 5242 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))))
285274, 284eqtrid 2779 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))))
286285oveq1d 7429 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) lim -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) lim -𝐵))
287266, 286eleqtrd 2830 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) lim -𝐵))
288 negeq 11474 . . . . . 6 (𝑥 = -𝑧 → -𝑥 = --𝑧)
289288fveq2d 6895 . . . . 5 (𝑥 = -𝑧 → (𝐹‘-𝑥) = (𝐹‘--𝑧))
290288fveq2d 6895 . . . . 5 (𝑥 = -𝑧 → (𝐺‘-𝑥) = (𝐺‘--𝑧))
291289, 290oveq12d 7432 . . . 4 (𝑥 = -𝑧 → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) = ((𝐹‘--𝑧) / (𝐺‘--𝑧)))
29276adantr 480 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 ∈ ℝ)
293 eliooord 13407 . . . . . . . . . . 11 (𝑧 ∈ (𝑎(,)𝐵) → (𝑎 < 𝑧𝑧 < 𝐵))
294293adantl 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑎 < 𝑧𝑧 < 𝐵))
295294simprd 495 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 < 𝐵)
29615, 13ltnegd 11814 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 < 𝐵 ↔ -𝐵 < -𝑧))
297295, 296mpbid 231 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 < -𝑧)
298292, 297gtned 11371 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ≠ -𝐵)
299298neneqd 2940 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ¬ -𝑧 = -𝐵)
300299pm2.21d 121 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (-𝑧 = -𝐵 → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶))
301300impr 454 . . . 4 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 = -𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶)
30219, 62, 75, 287, 291, 301limcco 25809 . . 3 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim 𝐵))
30315recnd 11264 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℂ)
304303negnegd 11584 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → --𝑧 = 𝑧)
305304fveq2d 6895 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐹‘--𝑧) = (𝐹𝑧))
306304fveq2d 6895 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐺‘--𝑧) = (𝐺𝑧))
307305, 306oveq12d 7432 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = ((𝐹𝑧) / (𝐺𝑧)))
308307mpteq2dva 5242 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))))
309308oveq1d 7429 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
31039resmptd 6038 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))))
311310oveq1d 7429 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝑎(,)𝐵)) lim 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
312 fss 6733 . . . . . . . . 9 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
31388, 51, 312sylancl 585 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
314313ffvelcdmda 7088 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℂ)
31553ffvelcdmda 7088 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℂ)
31648ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran 𝐺)
31750ffnd 6717 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺 Fn (𝐴(,)𝐵))
318 fnfvelrn 7084 . . . . . . . . . . 11 ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ran 𝐺)
319317, 318sylan 579 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ran 𝐺)
320 eleq1 2816 . . . . . . . . . 10 ((𝐺𝑧) = 0 → ((𝐺𝑧) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
321319, 320syl5ibcom 244 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐺𝑧) = 0 → 0 ∈ ran 𝐺))
322321necon3bd 2949 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran 𝐺 → (𝐺𝑧) ≠ 0))
323316, 322mpd 15 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ≠ 0)
324314, 315, 323divcld 12012 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
325324fmpttd 7119 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))):(𝐴(,)𝐵)⟶ℂ)
326 ioossre 13409 . . . . . . 7 (𝐴(,)𝐵) ⊆ ℝ
327326, 51sstri 3987 . . . . . 6 (𝐴(,)𝐵) ⊆ ℂ
328327a1i 11 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℂ)
329 eqid 2727 . . . . 5 ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))
330 ssun2 4169 . . . . . . 7 {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})
331 snssg 4783 . . . . . . . 8 (𝐵 ∈ ℝ → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})))
33272, 331syl 17 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})))
333330, 332mpbiri 258 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}))
33499cnfldtopon 24686 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
335326a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℝ)
33672snssd 4808 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → {𝐵} ⊆ ℝ)
337335, 336unssd 4182 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ)
338337, 51sstrdi 3990 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ)
339 resttopon 23052 . . . . . . . . 9 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})))
340334, 338, 339sylancr 586 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})))
341 topontop 22802 . . . . . . . 8 (((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top)
342340, 341syl 17 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top)
343 indi 4269 . . . . . . . . . 10 ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵}))
344 pnfxr 11290 . . . . . . . . . . . . . 14 +∞ ∈ ℝ*
345344a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → +∞ ∈ ℝ*)
3464adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ℝ*)
347 iooin 13382 . . . . . . . . . . . . 13 (((𝑎 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝐴 ∈ ℝ*𝐵 ∈ ℝ*)) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)))
34835, 345, 34, 346, 347syl22anc 838 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)))
349 xrltnle 11303 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ*𝑎 ∈ ℝ*) → (𝐴 < 𝑎 ↔ ¬ 𝑎𝐴))
35034, 35, 349syl2anc 583 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐴 < 𝑎 ↔ ¬ 𝑎𝐴))
35136, 350mpbid 231 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 𝑎𝐴)
352351iffalsed 4535 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → if(𝑎𝐴, 𝐴, 𝑎) = 𝑎)
35372ltpnfd 13125 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 < +∞)
354 xrltnle 11303 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵))
355346, 344, 354sylancl 585 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵))
356353, 355mpbid 231 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ +∞ ≤ 𝐵)
357356iffalsed 4535 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → if(+∞ ≤ 𝐵, +∞, 𝐵) = 𝐵)
358352, 357oveq12d 7432 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (if(𝑎𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)) = (𝑎(,)𝐵))
359348, 358eqtrd 2767 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (𝑎(,)𝐵))
360 elioopnf 13444 . . . . . . . . . . . . . . 15 (𝑎 ∈ ℝ* → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵)))
36135, 360syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵)))
36272, 79, 361mpbir2and 712 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ (𝑎(,)+∞))
363362snssd 4808 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → {𝐵} ⊆ (𝑎(,)+∞))
364 sseqin2 4211 . . . . . . . . . . . 12 ({𝐵} ⊆ (𝑎(,)+∞) ↔ ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵})
365363, 364sylib 217 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵})
366359, 365uneq12d 4160 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
367343, 366eqtrid 2779 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
368 retop 24665 . . . . . . . . . 10 (topGen‘ran (,)) ∈ Top
369 reex 11221 . . . . . . . . . . . 12 ℝ ∈ V
370369ssex 5315 . . . . . . . . . . 11 (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V)
371337, 370syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V)
372 iooretop 24669 . . . . . . . . . . 11 (𝑎(,)+∞) ∈ (topGen‘ran (,))
373372a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑎(,)+∞) ∈ (topGen‘ran (,)))
374 elrestr 17401 . . . . . . . . . 10 (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V ∧ (𝑎(,)+∞) ∈ (topGen‘ran (,))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
375368, 371, 373, 374mp3an2i 1463 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
376367, 375eqeltrrd 2829 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
377 eqid 2727 . . . . . . . . . 10 (topGen‘ran (,)) = (topGen‘ran (,))
37899, 377rerest 24707 . . . . . . . . 9 (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
379337, 378syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
380376, 379eleqtrrd 2831 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
381 isopn3i 22973 . . . . . . 7 ((((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top ∧ ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))) → ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
382342, 380, 381syl2anc 583 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
383333, 382eleqtrrd 2831 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})))
384325, 39, 328, 99, 329, 383limcres 25802 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝑎(,)𝐵)) lim 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
385309, 311, 3843eqtr2d 2773 . . 3 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
386302, 385eleqtrd 2830 . 2 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
3879, 386rexlimddv 3156 1 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395   = wceq 1534  wcel 2099  wne 2935  wrex 3065  Vcvv 3469  cun 3942  cin 3943  wss 3944  ifcif 4524  {csn 4624  {cpr 4626   class class class wbr 5142  cmpt 5225  dom cdm 5672  ran crn 5673  cres 5674   Fn wfn 6537  wf 6538  cfv 6542  (class class class)co 7414  cc 11128  cr 11129  0cc0 11130  1c1 11131   · cmul 11135  +∞cpnf 11267  *cxr 11269   < clt 11270  cle 11271  -cneg 11467   / cdiv 11893  cq 12954  (,)cioo 13348  t crest 17393  TopOpenctopn 17394  topGenctg 17410  fldccnfld 21266  Topctop 22782  TopOnctopon 22799  intcnt 22908  cnccncf 24783   lim climc 25778   D cdv 25779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-fi 9426  df-sup 9457  df-inf 9458  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-z 12581  df-dec 12700  df-uz 12845  df-q 12955  df-rp 12999  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ioo 13352  df-ioc 13353  df-ico 13354  df-icc 13355  df-fz 13509  df-fzo 13652  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-hom 17248  df-cco 17249  df-rest 17395  df-topn 17396  df-0g 17414  df-gsum 17415  df-topgen 17416  df-pt 17417  df-prds 17420  df-xrs 17475  df-qtop 17480  df-imas 17481  df-xps 17483  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-submnd 18732  df-mulg 19015  df-cntz 19259  df-cmn 19728  df-psmet 21258  df-xmet 21259  df-met 21260  df-bl 21261  df-mopn 21262  df-fbas 21263  df-fg 21264  df-cnfld 21267  df-top 22783  df-topon 22800  df-topsp 22822  df-bases 22836  df-cld 22910  df-ntr 22911  df-cls 22912  df-nei 22989  df-lp 23027  df-perf 23028  df-cn 23118  df-cnp 23119  df-haus 23206  df-cmp 23278  df-tx 23453  df-hmeo 23646  df-fil 23737  df-fm 23829  df-flim 23830  df-flf 23831  df-xms 24213  df-ms 24214  df-tms 24215  df-cncf 24785  df-limc 25782  df-dv 25783
This theorem is referenced by:  lhop  25936  fourierdlem60  45477
  Copyright terms: Public domain W3C validator