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

Theorem lhop2 23997
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 12011 . . 3 ℚ ⊆ ℝ
2 lhop2.a . . . 4 (𝜑𝐴 ∈ ℝ*)
3 lhop2.b . . . . 5 (𝜑𝐵 ∈ ℝ)
43rexrd 10301 . . . 4 (𝜑𝐵 ∈ ℝ*)
5 lhop2.l . . . 4 (𝜑𝐴 < 𝐵)
6 qbtwnxr 12244 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → ∃𝑎 ∈ ℚ (𝐴 < 𝑎𝑎 < 𝐵))
72, 4, 5, 6syl3anc 1477 . . 3 (𝜑 → ∃𝑎 ∈ ℚ (𝐴 < 𝑎𝑎 < 𝐵))
8 ssrexv 3808 . . 3 (ℚ ⊆ ℝ → (∃𝑎 ∈ ℚ (𝐴 < 𝑎𝑎 < 𝐵) → ∃𝑎 ∈ ℝ (𝐴 < 𝑎𝑎 < 𝐵)))
91, 7, 8mpsyl 68 . 2 (𝜑 → ∃𝑎 ∈ ℝ (𝐴 < 𝑎𝑎 < 𝐵))
10 simpr 479 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ (𝑎(,)𝐵))
11 simprl 811 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝑎 ∈ ℝ)
1211adantr 472 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑎 ∈ ℝ)
133ad2antrr 764 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝐵 ∈ ℝ)
14 elioore 12418 . . . . . . . 8 (𝑧 ∈ (𝑎(,)𝐵) → 𝑧 ∈ ℝ)
1514adantl 473 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℝ)
16 iooneg 12505 . . . . . . 7 ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎)))
1712, 13, 15, 16syl3anc 1477 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 ∈ (𝑎(,)𝐵) ↔ -𝑧 ∈ (-𝐵(,)-𝑎)))
1810, 17mpbid 222 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎))
1918adantrr 755 . . . 4 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 ≠ -𝐵)) → -𝑧 ∈ (-𝐵(,)-𝑎))
20 lhop2.f . . . . . . . 8 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
2120ad2antrr 764 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
22 elioore 12418 . . . . . . . . . . . . 13 (𝑥 ∈ (-𝐵(,)-𝑎) → 𝑥 ∈ ℝ)
2322adantl 473 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℝ)
2423recnd 10280 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ ℂ)
2524negnegd 10595 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 = 𝑥)
26 simpr 479 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑥 ∈ (-𝐵(,)-𝑎))
2725, 26eqeltrd 2839 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → --𝑥 ∈ (-𝐵(,)-𝑎))
2811adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝑎 ∈ ℝ)
293ad2antrr 764 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐵 ∈ ℝ)
3023renegcld 10669 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ ℝ)
31 iooneg 12505 . . . . . . . . . 10 ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ -𝑥 ∈ ℝ) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎)))
3228, 29, 30, 31syl3anc 1477 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 ∈ (𝑎(,)𝐵) ↔ --𝑥 ∈ (-𝐵(,)-𝑎)))
3327, 32mpbird 247 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝑎(,)𝐵))
342adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐴 ∈ ℝ*)
35 simprrl 823 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐴 < 𝑎)
3611rexrd 10301 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝑎 ∈ ℝ*)
37 xrltle 12195 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ*𝑎 ∈ ℝ*) → (𝐴 < 𝑎𝐴𝑎))
3834, 36, 37syl2anc 696 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐴 < 𝑎𝐴𝑎))
3935, 38mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐴𝑎)
40 iooss1 12423 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐴𝑎) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵))
4134, 39, 40syl2anc 696 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑎(,)𝐵) ⊆ (𝐴(,)𝐵))
4241sselda 3744 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ -𝑥 ∈ (𝑎(,)𝐵)) → -𝑥 ∈ (𝐴(,)𝐵))
4333, 42syldan 488 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 ∈ (𝐴(,)𝐵))
4421, 43ffvelrnd 6524 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℝ)
4544recnd 10280 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐹‘-𝑥) ∈ ℂ)
46 lhop2.g . . . . . . . 8 (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
4746ad2antrr 764 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
4847, 43ffvelrnd 6524 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℝ)
4948recnd 10280 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ℂ)
50 lhop2.gn0 . . . . . . 7 (𝜑 → ¬ 0 ∈ ran 𝐺)
5150ad2antrr 764 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran 𝐺)
5246adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
53 ax-resscn 10205 . . . . . . . . . . . 12 ℝ ⊆ ℂ
54 fss 6217 . . . . . . . . . . . 12 ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
5552, 53, 54sylancl 697 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
5655adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
57 ffn 6206 . . . . . . . . . 10 (𝐺:(𝐴(,)𝐵)⟶ℂ → 𝐺 Fn (𝐴(,)𝐵))
5856, 57syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 𝐺 Fn (𝐴(,)𝐵))
59 fnfvelrn 6520 . . . . . . . . 9 ((𝐺 Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘-𝑥) ∈ ran 𝐺)
6058, 43, 59syl2anc 696 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ∈ ran 𝐺)
61 eleq1 2827 . . . . . . . 8 ((𝐺‘-𝑥) = 0 → ((𝐺‘-𝑥) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
6260, 61syl5ibcom 235 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐺‘-𝑥) = 0 → 0 ∈ ran 𝐺))
6362necon3bd 2946 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran 𝐺 → (𝐺‘-𝑥) ≠ 0))
6451, 63mpd 15 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (𝐺‘-𝑥) ≠ 0)
6545, 49, 64divcld 11013 . . . 4 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) ∈ ℂ)
66 limcresi 23868 . . . . . 6 ((𝑧 ∈ ℝ ↦ -𝑧) lim 𝐵) ⊆ (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) lim 𝐵)
67 ioossre 12448 . . . . . . . 8 (𝑎(,)𝐵) ⊆ ℝ
68 resmpt 5607 . . . . . . . 8 ((𝑎(,)𝐵) ⊆ ℝ → ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧))
6967, 68ax-mp 5 . . . . . . 7 ((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧)
7069oveq1i 6824 . . . . . 6 (((𝑧 ∈ ℝ ↦ -𝑧) ↾ (𝑎(,)𝐵)) lim 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim 𝐵)
7166, 70sseqtri 3778 . . . . 5 ((𝑧 ∈ ℝ ↦ -𝑧) lim 𝐵) ⊆ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim 𝐵)
72 eqid 2760 . . . . . . . 8 (𝑧 ∈ ℝ ↦ -𝑧) = (𝑧 ∈ ℝ ↦ -𝑧)
7372negcncf 22942 . . . . . . 7 (ℝ ⊆ ℂ → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ))
7453, 73mp1i 13 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑧 ∈ ℝ ↦ -𝑧) ∈ (ℝ–cn→ℂ))
753adantr 472 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ℝ)
76 negeq 10485 . . . . . 6 (𝑧 = 𝐵 → -𝑧 = -𝐵)
7774, 75, 76cnmptlimc 23873 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ ℝ ↦ -𝑧) lim 𝐵))
7871, 77sseldi 3742 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ -𝑧) lim 𝐵))
7975renegcld 10669 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 ∈ ℝ)
8011renegcld 10669 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝑎 ∈ ℝ)
8180rexrd 10301 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝑎 ∈ ℝ*)
82 simprrr 824 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝑎 < 𝐵)
8311, 75ltnegd 10817 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑎 < 𝐵 ↔ -𝐵 < -𝑎))
8482, 83mpbid 222 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → -𝐵 < -𝑎)
85 eqid 2760 . . . . . . 7 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))
8644, 85fmptd 6549 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ)
87 eqid 2760 . . . . . . 7 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))
8848, 87fmptd 6549 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ℝ)
89 reelprrecn 10240 . . . . . . . . . . 11 ℝ ∈ {ℝ, ℂ}
9089a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ℝ ∈ {ℝ, ℂ})
91 neg1cn 11336 . . . . . . . . . . 11 -1 ∈ ℂ
9291a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -1 ∈ ℂ)
9320adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
9493ffvelrnda 6523 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹𝑦) ∈ ℝ)
9594recnd 10280 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹𝑦) ∈ ℂ)
96 fvexd 6365 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ V)
97 1cnd 10268 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → 1 ∈ ℂ)
98 simpr 479 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
9998recnd 10280 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
100 1cnd 10268 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
10190dvmptid 23939 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
102 ioossre 12448 . . . . . . . . . . . . 13 (-𝐵(,)-𝑎) ⊆ ℝ
103102a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ⊆ ℝ)
104 eqid 2760 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
105104tgioo2 22827 . . . . . . . . . . . 12 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
106 iooretop 22790 . . . . . . . . . . . . 13 (-𝐵(,)-𝑎) ∈ (topGen‘ran (,))
107106a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (-𝐵(,)-𝑎) ∈ (topGen‘ran (,)))
10890, 99, 100, 101, 103, 105, 104, 107dvmptres 23945 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ 1))
10990, 24, 97, 108dvmptneg 23948 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -1))
11093feqmptd 6412 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦)))
111110oveq2d 6830 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦))))
112 dvf 23890 . . . . . . . . . . . . 13 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
113 lhop2.if . . . . . . . . . . . . . . 15 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
114113adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
115114feq2d 6192 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
116112, 115mpbii 223 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
117116feqmptd 6412 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐹) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
118111, 117eqtr3d 2796 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
119 fveq2 6353 . . . . . . . . . 10 (𝑦 = -𝑥 → (𝐹𝑦) = (𝐹‘-𝑥))
120 fveq2 6353 . . . . . . . . . 10 (𝑦 = -𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘-𝑥))
12190, 90, 43, 92, 95, 96, 109, 118, 119, 120dvmptco 23954 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)))
122116adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
123122, 43ffvelrnd 6524 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐹)‘-𝑥) ∈ ℂ)
124123, 92mulcomd 10273 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = (-1 · ((ℝ D 𝐹)‘-𝑥)))
125123mulm1d 10694 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐹)‘-𝑥)) = -((ℝ D 𝐹)‘-𝑥))
126124, 125eqtrd 2794 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐹)‘-𝑥) · -1) = -((ℝ D 𝐹)‘-𝑥))
127126mpteq2dva 4896 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
128121, 127eqtrd 2794 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
129128dmeqd 5481 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)))
130 negex 10491 . . . . . . . 8 -((ℝ D 𝐹)‘-𝑥) ∈ V
131 eqid 2760 . . . . . . . 8 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))
132130, 131dmmpti 6184 . . . . . . 7 dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥)) = (-𝐵(,)-𝑎)
133129, 132syl6eq 2810 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))) = (-𝐵(,)-𝑎))
13452ffvelrnda 6523 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺𝑦) ∈ ℝ)
135134recnd 10280 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺𝑦) ∈ ℂ)
136 fvexd 6365 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑦) ∈ V)
13752feqmptd 6412 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦)))
138137oveq2d 6830 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦))))
139 dvf 23890 . . . . . . . . . . . . 13 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
140 lhop2.ig . . . . . . . . . . . . . . 15 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
141140adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
142141feq2d 6192 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
143139, 142mpbii 223 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
144143feqmptd 6412 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦)))
145138, 144eqtr3d 2796 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑦)))
146 fveq2 6353 . . . . . . . . . 10 (𝑦 = -𝑥 → (𝐺𝑦) = (𝐺‘-𝑥))
147 fveq2 6353 . . . . . . . . . 10 (𝑦 = -𝑥 → ((ℝ D 𝐺)‘𝑦) = ((ℝ D 𝐺)‘-𝑥))
14890, 90, 43, 92, 135, 136, 109, 145, 146, 147dvmptco 23954 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)))
149143adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
150149, 43ffvelrnd 6524 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ℂ)
151150, 92mulcomd 10273 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = (-1 · ((ℝ D 𝐺)‘-𝑥)))
152150mulm1d 10694 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-1 · ((ℝ D 𝐺)‘-𝑥)) = -((ℝ D 𝐺)‘-𝑥))
153151, 152eqtrd 2794 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) · -1) = -((ℝ D 𝐺)‘-𝑥))
154153mpteq2dva 4896 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐺)‘-𝑥) · -1)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
155148, 154eqtrd 2794 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
156155dmeqd 5481 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
157 negex 10491 . . . . . . . 8 -((ℝ D 𝐺)‘-𝑥) ∈ V
158 eqid 2760 . . . . . . . 8 (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))
159157, 158dmmpti 6184 . . . . . . 7 dom (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) = (-𝐵(,)-𝑎)
160156, 159syl6eq 2810 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → dom (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = (-𝐵(,)-𝑎))
16143adantrr 755 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥𝐵)) → -𝑥 ∈ (𝐴(,)𝐵))
162 limcresi 23868 . . . . . . . . 9 ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵) ⊆ (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) lim -𝐵)
163 resmpt 5607 . . . . . . . . . . 11 ((-𝐵(,)-𝑎) ⊆ ℝ → ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥))
164102, 163ax-mp 5 . . . . . . . . . 10 ((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥)
165164oveq1i 6824 . . . . . . . . 9 (((𝑥 ∈ ℝ ↦ -𝑥) ↾ (-𝐵(,)-𝑎)) lim -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim -𝐵)
166162, 165sseqtri 3778 . . . . . . . 8 ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵) ⊆ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim -𝐵)
16775recnd 10280 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ℂ)
168167negnegd 10595 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → --𝐵 = 𝐵)
169 eqid 2760 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ -𝑥) = (𝑥 ∈ ℝ ↦ -𝑥)
170169negcncf 22942 . . . . . . . . . . 11 (ℝ ⊆ ℂ → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ))
17153, 170mp1i 13 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ ℝ ↦ -𝑥) ∈ (ℝ–cn→ℂ))
172 negeq 10485 . . . . . . . . . 10 (𝑥 = -𝐵 → -𝑥 = --𝐵)
173171, 79, 172cnmptlimc 23873 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → --𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵))
174168, 173eqeltrrd 2840 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ ℝ ↦ -𝑥) lim -𝐵))
175166, 174sseldi 3742 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -𝑥) lim -𝐵))
176 lhop2.f0 . . . . . . . . 9 (𝜑 → 0 ∈ (𝐹 lim 𝐵))
177176adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ (𝐹 lim 𝐵))
178110oveq1d 6829 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐹 lim 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦)) lim 𝐵))
179177, 178eleqtrd 2841 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦)) lim 𝐵))
180 eliooord 12446 . . . . . . . . . . . . . 14 (𝑥 ∈ (-𝐵(,)-𝑎) → (-𝐵 < 𝑥𝑥 < -𝑎))
181180adantl 473 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝐵 < 𝑥𝑥 < -𝑎))
182181simpld 477 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝐵 < 𝑥)
18329, 23, 182ltnegcon1d 10819 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥 < 𝐵)
18430, 183ltned 10385 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → -𝑥𝐵)
185184neneqd 2937 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ -𝑥 = 𝐵)
186185pm2.21d 118 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐹‘-𝑥) = 0))
187186impr 650 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐹‘-𝑥) = 0)
188161, 95, 175, 179, 119, 187limcco 23876 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)) lim -𝐵))
189 lhop2.g0 . . . . . . . . 9 (𝜑 → 0 ∈ (𝐺 lim 𝐵))
190189adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ (𝐺 lim 𝐵))
191137oveq1d 6829 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐺 lim 𝐵) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦)) lim 𝐵))
192190, 191eleqtrd 2841 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑦)) lim 𝐵))
193185pm2.21d 118 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (𝐺‘-𝑥) = 0))
194193impr 650 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (𝐺‘-𝑥) = 0)
195161, 135, 175, 192, 146, 194limcco 23876 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 0 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) lim -𝐵))
19660, 87fmptd 6549 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ran 𝐺)
197 frn 6214 . . . . . . . 8 ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)):(-𝐵(,)-𝑎)⟶ran 𝐺 → ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) ⊆ ran 𝐺)
198196, 197syl 17 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)) ⊆ ran 𝐺)
19950adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran 𝐺)
200198, 199ssneldd 3747 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))
201 lhop2.gd0 . . . . . . . 8 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
202201adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D 𝐺))
203155rneqd 5508 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) = ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)))
204203eleq2d 2825 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) ↔ 0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))))
205158, 157elrnmpti 5531 . . . . . . . . 9 (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) ↔ ∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥))
206 eqcom 2767 . . . . . . . . . . 11 (0 = -((ℝ D 𝐺)‘-𝑥) ↔ -((ℝ D 𝐺)‘-𝑥) = 0)
207150negeq0d 10596 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 ↔ -((ℝ D 𝐺)‘-𝑥) = 0))
208 ffn 6206 . . . . . . . . . . . . . . 15 ((ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
209149, 208syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
210 fnfvelrn 6520 . . . . . . . . . . . . . 14 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ -𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺))
211209, 43, 210syl2anc 696 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺))
212 eleq1 2827 . . . . . . . . . . . . 13 (((ℝ D 𝐺)‘-𝑥) = 0 → (((ℝ D 𝐺)‘-𝑥) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
213211, 212syl5ibcom 235 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺)))
214207, 213sylbird 250 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐺)‘-𝑥) = 0 → 0 ∈ ran (ℝ D 𝐺)))
215206, 214syl5bi 232 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺)))
216215rexlimdva 3169 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (∃𝑥 ∈ (-𝐵(,)-𝑎)0 = -((ℝ D 𝐺)‘-𝑥) → 0 ∈ ran (ℝ D 𝐺)))
217205, 216syl5bi 232 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (0 ∈ ran (𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥)) → 0 ∈ ran (ℝ D 𝐺)))
218204, 217sylbid 230 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))) → 0 ∈ ran (ℝ D 𝐺)))
219202, 218mtod 189 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 0 ∈ ran (ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))))
220116ffvelrnda 6523 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ ℂ)
221143ffvelrnda 6523 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ℂ)
222201ad2antrr 764 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran (ℝ D 𝐺))
223143, 208syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
224 fnfvelrn 6520 . . . . . . . . . . . . 13 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
225223, 224sylan 489 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
226 eleq1 2827 . . . . . . . . . . . 12 (((ℝ D 𝐺)‘𝑧) = 0 → (((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
227225, 226syl5ibcom 235 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐺)‘𝑧) = 0 → 0 ∈ ran (ℝ D 𝐺)))
228227necon3bd 2946 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘𝑧) ≠ 0))
229222, 228mpd 15 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ≠ 0)
230220, 221, 229divcld 11013 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) ∈ ℂ)
231 lhop2.c . . . . . . . . 9 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
232231adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐵))
233 fveq2 6353 . . . . . . . . 9 (𝑧 = -𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘-𝑥))
234 fveq2 6353 . . . . . . . . 9 (𝑧 = -𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘-𝑥))
235233, 234oveq12d 6832 . . . . . . . 8 (𝑧 = -𝑥 → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
236185pm2.21d 118 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-𝑥 = 𝐵 → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶))
237236impr 650 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑥 ∈ (-𝐵(,)-𝑎) ∧ -𝑥 = 𝐵)) → (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)) = 𝐶)
238161, 230, 175, 232, 235, 237limcco 23876 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) lim -𝐵))
239 nfcv 2902 . . . . . . . . . . . . 13 𝑥
240 nfcv 2902 . . . . . . . . . . . . 13 𝑥 D
241 nfmpt1 4899 . . . . . . . . . . . . 13 𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))
242239, 240, 241nfov 6840 . . . . . . . . . . . 12 𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))
243 nfcv 2902 . . . . . . . . . . . 12 𝑥𝑦
244242, 243nffv 6360 . . . . . . . . . . 11 𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦)
245 nfcv 2902 . . . . . . . . . . 11 𝑥 /
246 nfmpt1 4899 . . . . . . . . . . . . 13 𝑥(𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))
247239, 240, 246nfov 6840 . . . . . . . . . . . 12 𝑥(ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))
248247, 243nffv 6360 . . . . . . . . . . 11 𝑥((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)
249244, 245, 248nfov 6840 . . . . . . . . . 10 𝑥(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))
250 nfcv 2902 . . . . . . . . . 10 𝑦(((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))
251 fveq2 6353 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥))
252 fveq2 6353 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦) = ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))
253251, 252oveq12d 6832 . . . . . . . . . 10 (𝑦 = 𝑥 → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦)) = (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)))
254249, 250, 253cbvmpt 4901 . . . . . . . . 9 (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)))
255128fveq1d 6355 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥))
256131fvmpt2 6454 . . . . . . . . . . . . . 14 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐹)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
257130, 256mpan2 709 . . . . . . . . . . . . 13 (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐹)‘-𝑥))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
258255, 257sylan9eq 2814 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) = -((ℝ D 𝐹)‘-𝑥))
259155fveq1d 6355 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥))
260158fvmpt2 6454 . . . . . . . . . . . . . 14 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ -((ℝ D 𝐺)‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
261157, 260mpan2 709 . . . . . . . . . . . . 13 (𝑥 ∈ (-𝐵(,)-𝑎) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ -((ℝ D 𝐺)‘-𝑥))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
262259, 261sylan9eq 2814 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥) = -((ℝ D 𝐺)‘-𝑥))
263258, 262oveq12d 6832 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)))
264201ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ¬ 0 ∈ ran (ℝ D 𝐺))
265213necon3bd 2946 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘-𝑥) ≠ 0))
266264, 265mpd 15 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((ℝ D 𝐺)‘-𝑥) ≠ 0)
267123, 150, 266div2negd 11028 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (-((ℝ D 𝐹)‘-𝑥) / -((ℝ D 𝐺)‘-𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
268263, 267eqtrd 2794 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥)) = (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥)))
269268mpteq2dva 4896 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑥) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))))
270254, 269syl5eq 2806 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))))
271270oveq1d 6829 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) lim -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D 𝐹)‘-𝑥) / ((ℝ D 𝐺)‘-𝑥))) lim -𝐵))
272238, 271eleqtrrd 2842 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥)))‘𝑦) / ((ℝ D (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥)))‘𝑦))) lim -𝐵))
27379, 81, 84, 86, 88, 133, 160, 188, 195, 200, 219, 272lhop1 23996 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) lim -𝐵))
274 nffvmpt1 6361 . . . . . . . . 9 𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦)
275 nffvmpt1 6361 . . . . . . . . 9 𝑥((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)
276274, 245, 275nfov 6840 . . . . . . . 8 𝑥(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))
277 nfcv 2902 . . . . . . . 8 𝑦(((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))
278 fveq2 6353 . . . . . . . . 9 (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥))
279 fveq2 6353 . . . . . . . . 9 (𝑦 = 𝑥 → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))
280278, 279oveq12d 6832 . . . . . . . 8 (𝑦 = 𝑥 → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦)) = (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)))
281276, 277, 280cbvmpt 4901 . . . . . . 7 (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)))
282 fvex 6363 . . . . . . . . . 10 (𝐹‘-𝑥) ∈ V
28385fvmpt2 6454 . . . . . . . . . 10 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐹‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥))
28426, 282, 283sylancl 697 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) = (𝐹‘-𝑥))
285 fvex 6363 . . . . . . . . . 10 (𝐺‘-𝑥) ∈ V
28687fvmpt2 6454 . . . . . . . . . 10 ((𝑥 ∈ (-𝐵(,)-𝑎) ∧ (𝐺‘-𝑥) ∈ V) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥))
28726, 285, 286sylancl 697 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥) = (𝐺‘-𝑥))
288284, 287oveq12d 6832 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑥 ∈ (-𝐵(,)-𝑎)) → (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥)) = ((𝐹‘-𝑥) / (𝐺‘-𝑥)))
289288mpteq2dva 4896 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑥 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑥) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑥))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))))
290281, 289syl5eq 2806 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) = (𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))))
291290oveq1d 6829 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑦 ∈ (-𝐵(,)-𝑎) ↦ (((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐹‘-𝑥))‘𝑦) / ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ (𝐺‘-𝑥))‘𝑦))) lim -𝐵) = ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) lim -𝐵))
292273, 291eleqtrd 2841 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑥 ∈ (-𝐵(,)-𝑎) ↦ ((𝐹‘-𝑥) / (𝐺‘-𝑥))) lim -𝐵))
293 negeq 10485 . . . . . 6 (𝑥 = -𝑧 → -𝑥 = --𝑧)
294293fveq2d 6357 . . . . 5 (𝑥 = -𝑧 → (𝐹‘-𝑥) = (𝐹‘--𝑧))
295293fveq2d 6357 . . . . 5 (𝑥 = -𝑧 → (𝐺‘-𝑥) = (𝐺‘--𝑧))
296294, 295oveq12d 6832 . . . 4 (𝑥 = -𝑧 → ((𝐹‘-𝑥) / (𝐺‘-𝑥)) = ((𝐹‘--𝑧) / (𝐺‘--𝑧)))
29779adantr 472 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 ∈ ℝ)
298 eliooord 12446 . . . . . . . . . . 11 (𝑧 ∈ (𝑎(,)𝐵) → (𝑎 < 𝑧𝑧 < 𝐵))
299298adantl 473 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑎 < 𝑧𝑧 < 𝐵))
300299simprd 482 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 < 𝐵)
30115, 13ltnegd 10817 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝑧 < 𝐵 ↔ -𝐵 < -𝑧))
302300, 301mpbid 222 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝐵 < -𝑧)
303297, 302gtned 10384 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → -𝑧 ≠ -𝐵)
304303neneqd 2937 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ¬ -𝑧 = -𝐵)
305304pm2.21d 118 . . . . 5 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (-𝑧 = -𝐵 → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶))
306305impr 650 . . . 4 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ (𝑧 ∈ (𝑎(,)𝐵) ∧ -𝑧 = -𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = 𝐶)
30719, 65, 78, 292, 296, 306limcco 23876 . . 3 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim 𝐵))
30815recnd 10280 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → 𝑧 ∈ ℂ)
309308negnegd 10595 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → --𝑧 = 𝑧)
310309fveq2d 6357 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐹‘--𝑧) = (𝐹𝑧))
311309fveq2d 6357 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → (𝐺‘--𝑧) = (𝐺𝑧))
312310, 311oveq12d 6832 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝑎(,)𝐵)) → ((𝐹‘--𝑧) / (𝐺‘--𝑧)) = ((𝐹𝑧) / (𝐺𝑧)))
313312mpteq2dva 4896 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))))
314313oveq1d 6829 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
31541resmptd 5610 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝑎(,)𝐵)) = (𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))))
316315oveq1d 6829 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝑎(,)𝐵)) lim 𝐵) = ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
317 fss 6217 . . . . . . . . 9 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
31893, 53, 317sylancl 697 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
319318ffvelrnda 6523 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℂ)
32055ffvelrnda 6523 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℂ)
32150ad2antrr 764 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran 𝐺)
32255, 57syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐺 Fn (𝐴(,)𝐵))
323 fnfvelrn 6520 . . . . . . . . . . 11 ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ran 𝐺)
324322, 323sylan 489 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ran 𝐺)
325 eleq1 2827 . . . . . . . . . 10 ((𝐺𝑧) = 0 → ((𝐺𝑧) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
326324, 325syl5ibcom 235 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐺𝑧) = 0 → 0 ∈ ran 𝐺))
327326necon3bd 2946 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran 𝐺 → (𝐺𝑧) ≠ 0))
328321, 327mpd 15 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ≠ 0)
329319, 320, 328divcld 11013 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
330 eqid 2760 . . . . . 6 (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))
331329, 330fmptd 6549 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))):(𝐴(,)𝐵)⟶ℂ)
332 ioossre 12448 . . . . . . 7 (𝐴(,)𝐵) ⊆ ℝ
333332, 53sstri 3753 . . . . . 6 (𝐴(,)𝐵) ⊆ ℂ
334333a1i 11 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℂ)
335 eqid 2760 . . . . 5 ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))
336 ssun2 3920 . . . . . . 7 {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})
337 snssg 4459 . . . . . . . 8 (𝐵 ∈ ℝ → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})))
33875, 337syl 17 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}) ↔ {𝐵} ⊆ ((𝑎(,)𝐵) ∪ {𝐵})))
339336, 338mpbiri 248 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((𝑎(,)𝐵) ∪ {𝐵}))
340104cnfldtopon 22807 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
341332a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐴(,)𝐵) ⊆ ℝ)
34275snssd 4485 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → {𝐵} ⊆ ℝ)
343341, 342unssd 3932 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ)
344343, 53syl6ss 3756 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ)
345 resttopon 21187 . . . . . . . . 9 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})))
346340, 344, 345sylancr 698 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})))
347 topontop 20940 . . . . . . . 8 (((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ (TopOn‘((𝐴(,)𝐵) ∪ {𝐵})) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top)
348346, 347syl 17 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top)
349 indi 4016 . . . . . . . . . 10 ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵}))
350 pnfxr 10304 . . . . . . . . . . . . . 14 +∞ ∈ ℝ*
351350a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → +∞ ∈ ℝ*)
3524adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ℝ*)
353 iooin 12422 . . . . . . . . . . . . 13 (((𝑎 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝐴 ∈ ℝ*𝐵 ∈ ℝ*)) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)))
35436, 351, 34, 352, 353syl22anc 1478 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (if(𝑎𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)))
355 xrltnle 10317 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ*𝑎 ∈ ℝ*) → (𝐴 < 𝑎 ↔ ¬ 𝑎𝐴))
35634, 36, 355syl2anc 696 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐴 < 𝑎 ↔ ¬ 𝑎𝐴))
35735, 356mpbid 222 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ 𝑎𝐴)
358357iffalsed 4241 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → if(𝑎𝐴, 𝐴, 𝑎) = 𝑎)
359 ltpnf 12167 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℝ → 𝐵 < +∞)
36075, 359syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 < +∞)
361 xrltnle 10317 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵))
362352, 350, 361sylancl 697 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵))
363360, 362mpbid 222 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ¬ +∞ ≤ 𝐵)
364363iffalsed 4241 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → if(+∞ ≤ 𝐵, +∞, 𝐵) = 𝐵)
365358, 364oveq12d 6832 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (if(𝑎𝐴, 𝐴, 𝑎)(,)if(+∞ ≤ 𝐵, +∞, 𝐵)) = (𝑎(,)𝐵))
366354, 365eqtrd 2794 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) = (𝑎(,)𝐵))
367 elioopnf 12480 . . . . . . . . . . . . . . 15 (𝑎 ∈ ℝ* → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵)))
36836, 367syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝐵 ∈ (𝑎(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝑎 < 𝐵)))
36975, 82, 368mpbir2and 995 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ (𝑎(,)+∞))
370369snssd 4485 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → {𝐵} ⊆ (𝑎(,)+∞))
371 sseqin2 3960 . . . . . . . . . . . 12 ({𝐵} ⊆ (𝑎(,)+∞) ↔ ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵})
372370, 371sylib 208 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ {𝐵}) = {𝐵})
373366, 372uneq12d 3911 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (((𝑎(,)+∞) ∩ (𝐴(,)𝐵)) ∪ ((𝑎(,)+∞) ∩ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
374349, 373syl5eq 2806 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
375 retop 22786 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
376375a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (topGen‘ran (,)) ∈ Top)
377 reex 10239 . . . . . . . . . . . 12 ℝ ∈ V
378377ssex 4954 . . . . . . . . . . 11 (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V)
379343, 378syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V)
380 iooretop 22790 . . . . . . . . . . 11 (𝑎(,)+∞) ∈ (topGen‘ran (,))
381380a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (𝑎(,)+∞) ∈ (topGen‘ran (,)))
382 elrestr 16311 . . . . . . . . . 10 (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ {𝐵}) ∈ V ∧ (𝑎(,)+∞) ∈ (topGen‘ran (,))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
383376, 379, 381, 382syl3anc 1477 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)+∞) ∩ ((𝐴(,)𝐵) ∪ {𝐵})) ∈ ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
384374, 383eqeltrrd 2840 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
385 eqid 2760 . . . . . . . . . 10 (topGen‘ran (,)) = (topGen‘ran (,))
386104, 385rerest 22828 . . . . . . . . 9 (((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
387343, 386syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) = ((topGen‘ran (,)) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
388384, 387eleqtrrd 2842 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))
389 isopn3i 21108 . . . . . . 7 ((((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})) ∈ Top ∧ ((𝑎(,)𝐵) ∪ {𝐵}) ∈ ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))) → ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
390348, 388, 389syl2anc 696 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})) = ((𝑎(,)𝐵) ∪ {𝐵}))
391339, 390eleqtrrd 2842 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵})))‘((𝑎(,)𝐵) ∪ {𝐵})))
392331, 41, 334, 104, 335, 391limcres 23869 . . . 4 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) ↾ (𝑎(,)𝐵)) lim 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
393314, 316, 3923eqtr2d 2800 . . 3 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → ((𝑧 ∈ (𝑎(,)𝐵) ↦ ((𝐹‘--𝑧) / (𝐺‘--𝑧))) lim 𝐵) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
394307, 393eleqtrd 2841 . 2 ((𝜑 ∧ (𝑎 ∈ ℝ ∧ (𝐴 < 𝑎𝑎 < 𝐵))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
3959, 394rexlimddv 3173 1 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1632  wcel 2139  wne 2932  wrex 3051  Vcvv 3340  cun 3713  cin 3714  wss 3715  ifcif 4230  {csn 4321  {cpr 4323   class class class wbr 4804  cmpt 4881  dom cdm 5266  ran crn 5267  cres 5268   Fn wfn 6044  wf 6045  cfv 6049  (class class class)co 6814  cc 10146  cr 10147  0cc0 10148  1c1 10149   · cmul 10153  +∞cpnf 10283  *cxr 10285   < clt 10286  cle 10287  -cneg 10479   / cdiv 10896  cq 12001  (,)cioo 12388  t crest 16303  TopOpenctopn 16304  topGenctg 16320  fldccnfld 19968  Topctop 20920  TopOnctopon 20937  intcnt 21043  cnccncf 22900   lim climc 23845   D cdv 23846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-inf2 8713  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226  ax-addf 10227  ax-mulf 10228
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-of 7063  df-om 7232  df-1st 7334  df-2nd 7335  df-supp 7465  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-2o 7731  df-oadd 7734  df-er 7913  df-map 8027  df-pm 8028  df-ixp 8077  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-fsupp 8443  df-fi 8484  df-sup 8515  df-inf 8516  df-oi 8582  df-card 8975  df-cda 9202  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-4 11293  df-5 11294  df-6 11295  df-7 11296  df-8 11297  df-9 11298  df-n0 11505  df-z 11590  df-dec 11706  df-uz 11900  df-q 12002  df-rp 12046  df-xneg 12159  df-xadd 12160  df-xmul 12161  df-ioo 12392  df-ioc 12393  df-ico 12394  df-icc 12395  df-fz 12540  df-fzo 12680  df-seq 13016  df-exp 13075  df-hash 13332  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-struct 16081  df-ndx 16082  df-slot 16083  df-base 16085  df-sets 16086  df-ress 16087  df-plusg 16176  df-mulr 16177  df-starv 16178  df-sca 16179  df-vsca 16180  df-ip 16181  df-tset 16182  df-ple 16183  df-ds 16186  df-unif 16187  df-hom 16188  df-cco 16189  df-rest 16305  df-topn 16306  df-0g 16324  df-gsum 16325  df-topgen 16326  df-pt 16327  df-prds 16330  df-xrs 16384  df-qtop 16389  df-imas 16390  df-xps 16392  df-mre 16468  df-mrc 16469  df-acs 16471  df-mgm 17463  df-sgrp 17505  df-mnd 17516  df-submnd 17557  df-mulg 17762  df-cntz 17970  df-cmn 18415  df-psmet 19960  df-xmet 19961  df-met 19962  df-bl 19963  df-mopn 19964  df-fbas 19965  df-fg 19966  df-cnfld 19969  df-top 20921  df-topon 20938  df-topsp 20959  df-bases 20972  df-cld 21045  df-ntr 21046  df-cls 21047  df-nei 21124  df-lp 21162  df-perf 21163  df-cn 21253  df-cnp 21254  df-haus 21341  df-cmp 21412  df-tx 21587  df-hmeo 21780  df-fil 21871  df-fm 21963  df-flim 21964  df-flf 21965  df-xms 22346  df-ms 22347  df-tms 22348  df-cncf 22902  df-limc 23849  df-dv 23850
This theorem is referenced by:  lhop  23998  fourierdlem60  40904
  Copyright terms: Public domain W3C validator