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

Theorem lhop2 24618
 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 12346 . . 3 ℚ ⊆ ℝ
2 lhop2.a . . . 4 (𝜑𝐴 ∈ ℝ*)
3 lhop2.b . . . . 5 (𝜑𝐵 ∈ ℝ)
43rexrd 10680 . . . 4 (𝜑𝐵 ∈ ℝ*)
5 lhop2.l . . . 4 (𝜑𝐴 < 𝐵)
6 qbtwnxr 12581 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → ∃𝑎 ∈ ℚ (𝐴 < 𝑎𝑎 < 𝐵))
72, 4, 5, 6syl3anc 1368 . . 3 (𝜑 → ∃𝑎 ∈ ℚ (𝐴 < 𝑎𝑎 < 𝐵))
8 ssrexv 3982 . . 3 (ℚ ⊆ ℝ → (∃𝑎 ∈ ℚ (𝐴 < 𝑎𝑎 < 𝐵) → ∃𝑎 ∈ ℝ (𝐴 < 𝑎𝑎 < 𝐵)))
91, 7, 8mpsyl 68 . 2 (𝜑 → ∃𝑎 ∈ ℝ (𝐴 < 𝑎𝑎 < 𝐵))
10 simpr 488 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ (𝑎(,)𝐵))
11 simprl 770 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝑎 ∈ ℝ)
1211adantr 484 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑎 ∈ ℝ)
133ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝐵 ∈ ℝ)
14 elioore 12756 . . . . . . . 8 (𝑧 ∈ (𝑎(,)𝐵) → 𝑧 ∈ ℝ)
1514adantl 485 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℝ)
16 iooneg 12849 . . . . . . 7 ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎)))
1712, 13, 15, 16syl3anc 1368 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎)))
1810, 17mpbid 235 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎))
1918adantrr 716 . . . 4 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 ≠ -𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎))
20 lhop2.f . . . . . . . 8 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
2120ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
22 elioore 12756 . . . . . . . . . . . . 13 (𝑥 ∈ (-𝐵(,)-𝑎) → 𝑥 ∈ ℝ)
2322adantl 485 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℝ)
2423recnd 10658 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℂ)
2524negnegd 10977 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 = 𝑥)
26 simpr 488 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ (-𝐵(,)-𝑎))
2725, 26eqeltrd 2890 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 ∈ (-𝐵(,)-𝑎))
2811adantr 484 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑎 ∈ ℝ)
293ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐵 ∈ ℝ)
3023renegcld 11056 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ ℝ)
31 iooneg 12849 . . . . . . . . . 10 ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ -𝑥 ∈ ℝ) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎)))
3228, 29, 30, 31syl3anc 1368 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎)))
3327, 32mpbird 260 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝑎(,)𝐵))
342adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐴 ∈ ℝ*)
3511rexrd 10680 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝑎 ∈ ℝ*)
36 simprrl 780 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐴 < 𝑎)
3734, 35, 36xrltled 12531 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐴𝑎)
38 iooss1 12761 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐴𝑎) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵))
3934, 37, 38syl2anc 587 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵))
4039sselda 3915 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ -𝑥 ∈ (𝑎(,)𝐵)) → -𝑥 ∈ (𝐴(,)𝐵))
4133, 40syldan 594 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝐴(,)𝐵))
4221, 41ffvelrnd 6829 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℝ)
4342recnd 10658 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℂ)
44 lhop2.g . . . . . . . 8 (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
4544ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
4645, 41ffvelrnd 6829 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℝ)
4746recnd 10658 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℂ)
48 lhop2.gn0 . . . . . . 7 (𝜑 → ¬ 0 ∈ ran 𝐺)
4948ad2antrr 725 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran 𝐺)
5044adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
51 ax-resscn 10583 . . . . . . . . . . . 12 ℝ ⊆ ℂ
52 fss 6501 . . . . . . . . . . . 12 ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
5350, 51, 52sylancl 589 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
5453adantr 484 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
5554ffnd 6488 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺 Fn (𝐴(,)𝐵))
56 fnfvelrn 6825 . . . . . . . . 9 ((𝐺 Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘-𝑥) ∈ ran 𝐺)
5755, 41, 56syl2anc 587 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ran 𝐺)
58 eleq1 2877 . . . . . . . 8 ((𝐺‘-𝑥) = 0 → ((𝐺‘-𝑥) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
5957, 58syl5ibcom 248 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐺‘-𝑥) = 0 → 0 ∈ ran 𝐺))
6059necon3bd 3001 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran 𝐺 → (𝐺‘-𝑥) ≠ 0))
6149, 60mpd 15 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ≠ 0)
6243, 47, 61divcld 11405 . . . 4 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) ∈ ℂ)
63 limcresi 24488 . . . . . 6 ((𝑧 ∈ ℝ ↦ -𝑧) lim 𝐵) ⊆ (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) lim 𝐵)
64 ioossre 12786 . . . . . . . 8 (𝑎(,)𝐵) ⊆ ℝ
65 resmpt 5872 . . . . . . . 8 ((𝑎(,)𝐵) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧))
6664, 65ax-mp 5 . . . . . . 7 ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧)
6766oveq1i 7145 . . . . . 6 (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) lim 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim 𝐵)
6863, 67sseqtri 3951 . . . . 5 ((𝑧 ∈ ℝ ↦ -𝑧) lim 𝐵) ⊆ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim 𝐵)
69 eqid 2798 . . . . . . . 8 (𝑧 ∈ ℝ ↦ -𝑧) = (𝑧 ∈ ℝ ↦ -𝑧)
7069negcncf 23527 . . . . . . 7 (ℝ ⊆ ℂ → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ))
7151, 70mp1i 13 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ))
723adantr 484 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ℝ)
73 negeq 10867 . . . . . 6 (𝑧 = 𝐵 → -𝑧 = -𝐵)
7471, 72, 73cnmptlimc 24493 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ ℝ ↦ -𝑧) lim 𝐵))
7568, 74sseldi 3913 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim 𝐵))
7672renegcld 11056 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 ∈ ℝ)
7711renegcld 11056 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝑎 ∈ ℝ)
7877rexrd 10680 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝑎 ∈ ℝ*)
79 simprrr 781 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝑎 < 𝐵)
8011, 72ltnegd 11207 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑎 < 𝐵 ↔ -𝐵 < -𝑎))
8179, 80mpbid 235 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 < -𝑎)
8242fmpttd 6856 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ)
8346fmpttd 6856 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ)
84 reelprrecn 10618 . . . . . . . . . . 11 ℝ ∈ {ℝ, ℂ}
8584a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ℝ ∈ {ℝ, ℂ})
86 neg1cn 11739 . . . . . . . . . . 11 -1 ∈ ℂ
8786a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -1 ∈ ℂ)
8820adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
8988ffvelrnda 6828 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹𝑦) ∈ ℝ)
9089recnd 10658 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹𝑦) ∈ ℂ)
91 fvexd 6660 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ V)
92 1cnd 10625 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 1 ∈ ℂ)
93 simpr 488 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
9493recnd 10658 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
95 1cnd 10625 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
9685dvmptid 24560 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
97 ioossre 12786 . . . . . . . . . . . . 13 (-𝐵(,)-𝑎) ⊆ ℝ
9897a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ⊆ ℝ)
99 eqid 2798 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
10099tgioo2 23408 . . . . . . . . . . . 12 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
101 iooretop 23371 . . . . . . . . . . . . 13 (-𝐵(,)-𝑎) ∈ (topGen‘ran (,))
102101a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ∈ (topGen‘ran (,)))
10385, 94, 95, 96, 98, 100, 99, 102dvmptres 24566 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 1))
10485, 24, 92, 103dvmptneg 24569 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -1))
10588feqmptd 6708 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦)))
106105oveq2d 7151 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦))))
107 dvf 24510 . . . . . . . . . . . . 13 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
108 lhop2.if . . . . . . . . . . . . . . 15 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
109108adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
110109feq2d 6473 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
111107, 110mpbii 236 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
112111feqmptd 6708 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐹) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
113106, 112eqtr3d 2835 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
114 fveq2 6645 . . . . . . . . . 10 (𝑦 = -𝑥 → (𝐹𝑦) = (𝐹‘-𝑥))
115 fveq2 6645 . . . . . . . . . 10 (𝑦 = -𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘-𝑥))
11685, 85, 41, 87, 90, 91, 104, 113, 114, 115dvmptco 24575 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)))
117111adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
118117, 41ffvelrnd 6829 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐹)‘-𝑥) ∈ ℂ)
119118, 87mulcomd 10651 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = (-1 · ((ℝ D 𝐹)‘-𝑥)))
120118mulm1d 11081 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐹)‘-𝑥)) = -((ℝ D 𝐹)‘-𝑥))
121119, 120eqtrd 2833 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = -((ℝ D 𝐹)‘-𝑥))
122121mpteq2dva 5125 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
123116, 122eqtrd 2833 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
124123dmeqd 5738 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
125 negex 10873 . . . . . . . 8 -((ℝ D 𝐹)‘-𝑥) ∈ V
126 eqid 2798 . . . . . . . 8 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))
127125, 126dmmpti 6464 . . . . . . 7 dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (-𝐵(,)-𝑎)
128124, 127eqtrdi 2849 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (-𝐵(,)-𝑎))
12950ffvelrnda 6828 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺𝑦) ∈ ℝ)
130129recnd 10658 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺𝑦) ∈ ℂ)
131 fvexd 6660 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑦) ∈ V)
13250feqmptd 6708 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦)))
133132oveq2d 7151 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦))))
134 dvf 24510 . . . . . . . . . . . . 13 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
135 lhop2.ig . . . . . . . . . . . . . . 15 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
136135adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
137136feq2d 6473 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
138134, 137mpbii 236 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
139138feqmptd 6708 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦)))
140133, 139eqtr3d 2835 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦)))
141 fveq2 6645 . . . . . . . . . 10 (𝑦 = -𝑥 → (𝐺𝑦) = (𝐺‘-𝑥))
142 fveq2 6645 . . . . . . . . . 10 (𝑦 = -𝑥 → ((ℝ D 𝐺)‘𝑦) = ((ℝ D 𝐺)‘-𝑥))
14385, 85, 41, 87, 130, 131, 104, 140, 141, 142dvmptco 24575 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)))
144138adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
145144, 41ffvelrnd 6829 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ℂ)
146145, 87mulcomd 10651 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = (-1 · ((ℝ D 𝐺)‘-𝑥)))
147145mulm1d 11081 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐺)‘-𝑥)) = -((ℝ D 𝐺)‘-𝑥))
148146, 147eqtrd 2833 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = -((ℝ D 𝐺)‘-𝑥))
149148mpteq2dva 5125 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
150143, 149eqtrd 2833 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
151150dmeqd 5738 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
152 negex 10873 . . . . . . . 8 -((ℝ D 𝐺)‘-𝑥) ∈ V
153 eqid 2798 . . . . . . . 8 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))
154152, 153dmmpti 6464 . . . . . . 7 dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (-𝐵(,)-𝑎)
155151, 154eqtrdi 2849 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (-𝐵(,)-𝑎))
15641adantrr 716 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥𝐵)) → -𝑥 ∈ (𝐴(,)𝐵))
157 limcresi 24488 . . . . . . . . 9 ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵) ⊆ (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) lim -𝐵)
158 resmpt 5872 . . . . . . . . . . 11 ((-𝐵(,)-𝑎) ⊆ ℝ → ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥))
15997, 158ax-mp 5 . . . . . . . . . 10 ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)
160159oveq1i 7145 . . . . . . . . 9 (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) lim -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim -𝐵)
161157, 160sseqtri 3951 . . . . . . . 8 ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵) ⊆ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim -𝐵)
16272recnd 10658 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ℂ)
163162negnegd 10977 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → --𝐵 = 𝐵)
164 eqid 2798 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ -𝑥) = (𝑥 ∈ ℝ ↦ -𝑥)
165164negcncf 23527 . . . . . . . . . . 11 (ℝ ⊆ ℂ → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ))
16651, 165mp1i 13 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ))
167 negeq 10867 . . . . . . . . . 10 (𝑥 = -𝐵 → -𝑥 = --𝐵)
168166, 76, 167cnmptlimc 24493 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → --𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵))
169163, 168eqeltrrd 2891 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵))
170161, 169sseldi 3913 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim -𝐵))
171 lhop2.f0 . . . . . . . . 9 (𝜑 → 0 ∈ (𝐹 lim 𝐵))
172171adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ (𝐹 lim 𝐵))
173105oveq1d 7150 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐹 lim 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦)) lim 𝐵))
174172, 173eleqtrd 2892 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦)) lim 𝐵))
175 eliooord 12784 . . . . . . . . . . . . . 14 (𝑥 ∈ (-𝐵(,)-𝑎) → (-𝐵 < 𝑥𝑥 < -𝑎))
176175adantl 485 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝐵 < 𝑥𝑥 < -𝑎))
177176simpld 498 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝐵 < 𝑥)
17829, 23, 177ltnegcon1d 11209 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 < 𝐵)
17930, 178ltned 10765 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥𝐵)
180179neneqd 2992 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ -𝑥 = 𝐵)
181180pm2.21d 121 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐹‘-𝑥) = 0))
182181impr 458 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐹‘-𝑥) = 0)
183156, 90, 170, 174, 114, 182limcco 24496 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) lim -𝐵))
184 lhop2.g0 . . . . . . . . 9 (𝜑 → 0 ∈ (𝐺 lim 𝐵))
185184adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ (𝐺 lim 𝐵))
186132oveq1d 7150 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐺 lim 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦)) lim 𝐵))
187185, 186eleqtrd 2892 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦)) lim 𝐵))
188180pm2.21d 121 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐺‘-𝑥) = 0))
189188impr 458 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐺‘-𝑥) = 0)
190156, 130, 170, 187, 141, 189limcco 24496 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) lim -𝐵))
19157fmpttd 6856 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ran 𝐺)
192191frnd 6494 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) ⊆ ran 𝐺)
19348adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran 𝐺)
194192, 193ssneldd 3918 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))
195 lhop2.gd0 . . . . . . . 8 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
196195adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D 𝐺))
197150rneqd 5772 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
198197eleq2d 2875 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) ↔ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))))
199153, 152elrnmpti 5796 . . . . . . . . 9 (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) ↔ ∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥))
200 eqcom 2805 . . . . . . . . . . 11 (0 = -((ℝ D 𝐺)‘-𝑥) ↔ -((ℝ D 𝐺)‘-𝑥) = 0)
201145negeq0d 10978 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 ↔ -((ℝ D 𝐺)‘-𝑥) = 0))
202144ffnd 6488 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
203 fnfvelrn 6825 . . . . . . . . . . . . . 14 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺))
204202, 41, 203syl2anc 587 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺))
205 eleq1 2877 . . . . . . . . . . . . 13 (((ℝ D 𝐺)‘-𝑥) = 0 → (((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
206204, 205syl5ibcom 248 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺)))
207201, 206sylbird 263 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺)))
208200, 207syl5bi 245 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺)))
209208rexlimdva 3243 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺)))
210199, 209syl5bi 245 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) → 0 ∈ ran (ℝ D 𝐺)))
211198, 210sylbid 243 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) → 0 ∈ ran (ℝ D 𝐺)))
212196, 211mtod 201 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))))
213111ffvelrnda 6828 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ ℂ)
214138ffvelrnda 6828 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ℂ)
215195ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran (ℝ D 𝐺))
216138ffnd 6488 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
217 fnfvelrn 6825 . . . . . . . . . . . . 13 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
218216, 217sylan 583 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
219 eleq1 2877 . . . . . . . . . . . 12 (((ℝ D 𝐺)‘𝑧) = 0 → (((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
220218, 219syl5ibcom 248 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐺)‘𝑧) = 0 → 0 ∈ ran (ℝ D 𝐺)))
221220necon3bd 3001 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘𝑧) ≠ 0))
222215, 221mpd 15 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ≠ 0)
223213, 214, 222divcld 11405 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) ∈ ℂ)
224 lhop2.c . . . . . . . . 9 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
225224adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
226 fveq2 6645 . . . . . . . . 9 (𝑧 = -𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘-𝑥))
227 fveq2 6645 . . . . . . . . 9 (𝑧 = -𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘-𝑥))
228226, 227oveq12d 7153 . . . . . . . 8 (𝑧 = -𝑥 → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
229180pm2.21d 121 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶))
230229impr 458 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶)
231156, 223, 170, 225, 228, 230limcco 24496 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) lim -𝐵))
232 nfcv 2955 . . . . . . . . . . . . 13 𝑥
233 nfcv 2955 . . . . . . . . . . . . 13 𝑥 D
234 nfmpt1 5128 . . . . . . . . . . . . 13 𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))
235232, 233, 234nfov 7165 . . . . . . . . . . . 12 𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))
236 nfcv 2955 . . . . . . . . . . . 12 𝑥𝑦
237235, 236nffv 6655 . . . . . . . . . . 11 𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦)
238 nfcv 2955 . . . . . . . . . . 11 𝑥 /
239 nfmpt1 5128 . . . . . . . . . . . . 13 𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))
240232, 233, 239nfov 7165 . . . . . . . . . . . 12 𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))
241240, 236nffv 6655 . . . . . . . . . . 11 𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)
242237, 238, 241nfov 7165 . . . . . . . . . 10 𝑥(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))
243 nfcv 2955 . . . . . . . . . 10 𝑦(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))
244 fveq2 6645 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥))
245 fveq2 6645 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))
246244, 245oveq12d 7153 . . . . . . . . . 10 (𝑦 = 𝑥 → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)) = (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)))
247242, 243, 246cbvmpt 5131 . . . . . . . . 9 (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)))
248123fveq1d 6647 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥))
249126fvmpt2 6756 . . . . . . . . . . . . . 14 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐹)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
250125, 249mpan2 690 . . . . . . . . . . . . 13 (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
251248, 250sylan9eq 2853 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
252150fveq1d 6647 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥))
253153fvmpt2 6756 . . . . . . . . . . . . . 14 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐺)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
254152, 253mpan2 690 . . . . . . . . . . . . 13 (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
255252, 254sylan9eq 2853 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
256251, 255oveq12d 7153 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)))
257195ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran (ℝ D 𝐺))
258206necon3bd 3001 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘-𝑥) ≠ 0))
259257, 258mpd 15 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ≠ 0)
260118, 145, 259div2negd 11420 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
261256, 260eqtrd 2833 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
262261mpteq2dva 5125 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))))
263247, 262syl5eq 2845 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))))
264263oveq1d 7150 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) lim -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) lim -𝐵))
265231, 264eleqtrrd 2893 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) lim -𝐵))
26676, 78, 81, 82, 83, 128, 155, 183, 190, 194, 212, 265lhop1 24617 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) lim -𝐵))
267 nffvmpt1 6656 . . . . . . . . 9 𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦)
268 nffvmpt1 6656 . . . . . . . . 9 𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)
269267, 238, 268nfov 7165 . . . . . . . 8 𝑥(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))
270 nfcv 2955 . . . . . . . 8 𝑦(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))
271 fveq2 6645 . . . . . . . . 9 (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥))
272 fveq2 6645 . . . . . . . . 9 (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))
273271, 272oveq12d 7153 . . . . . . . 8 (𝑦 = 𝑥 → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)) = (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)))
274269, 270, 273cbvmpt 5131 . . . . . . 7 (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)))
275 fvex 6658 . . . . . . . . . 10 (𝐹‘-𝑥) ∈ V
276 eqid 2798 . . . . . . . . . . 11 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))
277276fvmpt2 6756 . . . . . . . . . 10 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐹‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥))
27826, 275, 277sylancl 589 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥))
279 fvex 6658 . . . . . . . . . 10 (𝐺‘-𝑥) ∈ V
280 eqid 2798 . . . . . . . . . . 11 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))
281280fvmpt2 6756 . . . . . . . . . 10 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐺‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥))
28226, 279, 281sylancl 589 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥))
283278, 282oveq12d 7153 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)) = ((𝐹‘-𝑥) / (𝐺‘-𝑥)))
284283mpteq2dva 5125 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))))
285274, 284syl5eq 2845 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))))
286285oveq1d 7150 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) lim -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) lim -𝐵))
287266, 286eleqtrd 2892 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) lim -𝐵))
288 negeq 10867 . . . . . 6 (𝑥 = -𝑧 → -𝑥 = --𝑧)
289288fveq2d 6649 . . . . 5 (𝑥 = -𝑧 → (𝐹‘-𝑥) = (𝐹‘--𝑧))
290288fveq2d 6649 . . . . 5 (𝑥 = -𝑧 → (𝐺‘-𝑥) = (𝐺‘--𝑧))
291289, 290oveq12d 7153 . . . 4 (𝑥 = -𝑧 → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) = ((𝐹‘--𝑧) / (𝐺‘--𝑧)))
29276adantr 484 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 ∈ ℝ)
293 eliooord 12784 . . . . . . . . . . 11 (𝑧 ∈ (𝑎(,)𝐵) → (𝑎 < 𝑧𝑧 < 𝐵))
294293adantl 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑎 < 𝑧𝑧 < 𝐵))
295294simprd 499 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 < 𝐵)
29615, 13ltnegd 11207 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 < 𝐵 ↔ -𝐵 < -𝑧))
297295, 296mpbid 235 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 < -𝑧)
298292, 297gtned 10764 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ≠ -𝐵)
299298neneqd 2992 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ¬ -𝑧 = -𝐵)
300299pm2.21d 121 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (-𝑧 = -𝐵 → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶))
301300impr 458 . . . 4 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 = -𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶)
30219, 62, 75, 287, 291, 301limcco 24496 . . 3 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim 𝐵))
30315recnd 10658 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℂ)
304303negnegd 10977 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → --𝑧 = 𝑧)
305304fveq2d 6649 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐹‘--𝑧) = (𝐹𝑧))
306304fveq2d 6649 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐺‘--𝑧) = (𝐺𝑧))
307305, 306oveq12d 7153 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = ((𝐹𝑧) / (𝐺𝑧)))
308307mpteq2dva 5125 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))))
309308oveq1d 7150 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
31039resmptd 5875 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))))
311310oveq1d 7150 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝑎(,)𝐵)) lim 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
312 fss 6501 . . . . . . . . 9 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
31388, 51, 312sylancl 589 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
314313ffvelrnda 6828 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℂ)
31553ffvelrnda 6828 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℂ)
31648ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran 𝐺)
31750ffnd 6488 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺 Fn (𝐴(,)𝐵))
318 fnfvelrn 6825 . . . . . . . . . . 11 ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ran 𝐺)
319317, 318sylan 583 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ran 𝐺)
320 eleq1 2877 . . . . . . . . . 10 ((𝐺𝑧) = 0 → ((𝐺𝑧) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
321319, 320syl5ibcom 248 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐺𝑧) = 0 → 0 ∈ ran 𝐺))
322321necon3bd 3001 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran 𝐺 → (𝐺𝑧) ≠ 0))
323316, 322mpd 15 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ≠ 0)
324314, 315, 323divcld 11405 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
325324fmpttd 6856 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))):(𝐴(,)𝐵)⟶ℂ)
326 ioossre 12786 . . . . . . 7 (𝐴(,)𝐵) ⊆ ℝ
327326, 51sstri 3924 . . . . . 6 (𝐴(,)𝐵) ⊆ ℂ
328327a1i 11 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℂ)
329 eqid 2798 . . . . 5 ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))
330 ssun2 4100 . . . . . . 7 {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})
331 snssg 4678 . . . . . . . 8 (𝐵 ∈ ℝ → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})))
33272, 331syl 17 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})))
333330, 332mpbiri 261 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}))
33499cnfldtopon 23388 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
335326a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℝ)
33672snssd 4702 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → {𝐵} ⊆ ℝ)
337335, 336unssd 4113 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ)
338337, 51sstrdi 3927 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ)
339 resttopon 21766 . . . . . . . . 9 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})))
340334, 338, 339sylancr 590 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})))
341 topontop 21518 . . . . . . . 8 (((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top)
342340, 341syl 17 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top)
343 indi 4200 . . . . . . . . . 10 ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵}))
344 pnfxr 10684 . . . . . . . . . . . . . 14 +∞ ∈ ℝ*
345344a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → +∞ ∈ ℝ*)
3464adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ℝ*)
347 iooin 12760 . . . . . . . . . . . . 13 (((𝑎 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝐴 ∈ ℝ*𝐵 ∈ ℝ*)) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)))
34835, 345, 34, 346, 347syl22anc 837 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)))
349 xrltnle 10697 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ*𝑎 ∈ ℝ*) → (𝐴 < 𝑎 ↔ ¬ 𝑎𝐴))
35034, 35, 349syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐴 < 𝑎 ↔ ¬ 𝑎𝐴))
35136, 350mpbid 235 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 𝑎𝐴)
352351iffalsed 4436 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → if(𝑎𝐴, 𝐴, 𝑎) = 𝑎)
35372ltpnfd 12504 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 < +∞)
354 xrltnle 10697 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵))
355346, 344, 354sylancl 589 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵))
356353, 355mpbid 235 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ +∞ ≤ 𝐵)
357356iffalsed 4436 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → if(+∞ ≤ 𝐵, +∞, 𝐵) = 𝐵)
358352, 357oveq12d 7153 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (if(𝑎𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)) = (𝑎(,)𝐵))
359348, 358eqtrd 2833 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (𝑎(,)𝐵))
360 elioopnf 12821 . . . . . . . . . . . . . . 15 (𝑎 ∈ ℝ* → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵)))
36135, 360syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵)))
36272, 79, 361mpbir2and 712 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ (𝑎(,)+∞))
363362snssd 4702 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → {𝐵} ⊆ (𝑎(,)+∞))
364 sseqin2 4142 . . . . . . . . . . . 12 ({𝐵} ⊆ (𝑎(,)+∞) ↔ ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵})
365363, 364sylib 221 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵})
366359, 365uneq12d 4091 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
367343, 366syl5eq 2845 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
368 retop 23367 . . . . . . . . . 10 (topGen‘ran (,)) ∈ Top
369 reex 10617 . . . . . . . . . . . 12 ℝ ∈ V
370369ssex 5189 . . . . . . . . . . 11 (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V)
371337, 370syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V)
372 iooretop 23371 . . . . . . . . . . 11 (𝑎(,)+∞) ∈ (topGen‘ran (,))
373372a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑎(,)+∞) ∈ (topGen‘ran (,)))
374 elrestr 16694 . . . . . . . . . 10 (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V ∧ (𝑎(,)+∞) ∈ (topGen‘ran (,))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
375368, 371, 373, 374mp3an2i 1463 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
376367, 375eqeltrrd 2891 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
377 eqid 2798 . . . . . . . . . 10 (topGen‘ran (,)) = (topGen‘ran (,))
37899, 377rerest 23409 . . . . . . . . 9 (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
379337, 378syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
380376, 379eleqtrrd 2893 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
381 isopn3i 21687 . . . . . . 7 ((((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top ∧ ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))) → ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
382342, 380, 381syl2anc 587 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
383333, 382eleqtrrd 2893 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})))
384325, 39, 328, 99, 329, 383limcres 24489 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝑎(,)𝐵)) lim 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
385309, 311, 3843eqtr2d 2839 . . 3 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
386302, 385eleqtrd 2892 . 2 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
3879, 386rexlimddv 3250 1 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∃wrex 3107  Vcvv 3441   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ifcif 4425  {csn 4525  {cpr 4527   class class class wbr 5030   ↦ cmpt 5110  dom cdm 5519  ran crn 5520   ↾ cres 5521   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  ℂcc 10524  ℝcr 10525  0cc0 10526  1c1 10527   · cmul 10531  +∞cpnf 10661  ℝ*cxr 10663   < clt 10664   ≤ cle 10665  -cneg 10860   / cdiv 11286  ℚcq 12336  (,)cioo 12726   ↾t crest 16686  TopOpenctopn 16687  topGenctg 16703  ℂfldccnfld 20091  Topctop 21498  TopOnctopon 21515  intcnt 21622  –cn→ccncf 23481   limℂ climc 24465   D cdv 24466 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-om 7561  df-1st 7671  df-2nd 7672  df-supp 7814  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-map 8391  df-pm 8392  df-ixp 8445  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-fi 8859  df-sup 8890  df-inf 8891  df-oi 8958  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-seq 13365  df-exp 13426  df-hash 13687  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-mulg 18217  df-cntz 18439  df-cmn 18900  df-psmet 20083  df-xmet 20084  df-met 20085  df-bl 20086  df-mopn 20087  df-fbas 20088  df-fg 20089  df-cnfld 20092  df-top 21499  df-topon 21516  df-topsp 21538  df-bases 21551  df-cld 21624  df-ntr 21625  df-cls 21626  df-nei 21703  df-lp 21741  df-perf 21742  df-cn 21832  df-cnp 21833  df-haus 21920  df-cmp 21992  df-tx 22167  df-hmeo 22360  df-fil 22451  df-fm 22543  df-flim 22544  df-flf 22545  df-xms 22927  df-ms 22928  df-tms 22929  df-cncf 23483  df-limc 24469  df-dv 24470 This theorem is referenced by:  lhop  24619  fourierdlem60  42803
 Copyright terms: Public domain W3C validator