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

Theorem lhop1 23676
 Description: L'Hôpital's Rule for limits from the right. 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
lhop1.a (𝜑𝐴 ∈ ℝ)
lhop1.b (𝜑𝐵 ∈ ℝ*)
lhop1.l (𝜑𝐴 < 𝐵)
lhop1.f (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
lhop1.g (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
lhop1.if (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
lhop1.ig (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
lhop1.f0 (𝜑 → 0 ∈ (𝐹 lim 𝐴))
lhop1.g0 (𝜑 → 0 ∈ (𝐺 lim 𝐴))
lhop1.gn0 (𝜑 → ¬ 0 ∈ ran 𝐺)
lhop1.gd0 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
lhop1.c (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴))
Assertion
Ref Expression
lhop1 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐴))
Distinct variable groups:   𝑧,𝐵   𝜑,𝑧   𝑧,𝐴   𝑧,𝐶   𝑧,𝐹   𝑧,𝐺

Proof of Theorem lhop1
Dummy variables 𝑒 𝑑 𝑟 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lhop1.c . 2 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴))
2 simpr 477 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
32rphalfcld 11828 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
4 breq2 4622 . . . . . . . . . 10 (𝑒 = (𝑥 / 2) → ((abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < 𝑒 ↔ (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)))
54imbi2d 330 . . . . . . . . 9 (𝑒 = (𝑥 / 2) → (((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < 𝑒) ↔ ((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2))))
65rexralbidv 3056 . . . . . . . 8 (𝑒 = (𝑥 / 2) → (∃𝑑 ∈ ℝ+𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2))))
76rspcv 3296 . . . . . . 7 ((𝑥 / 2) ∈ ℝ+ → (∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < 𝑒) → ∃𝑑 ∈ ℝ+𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2))))
83, 7syl 17 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < 𝑒) → ∃𝑑 ∈ ℝ+𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2))))
9 rabid 3111 . . . . . . . . . . . . . 14 (𝑣 ∈ {𝑣 ∈ (𝐴(,)𝐵) ∣ (abs‘(𝑣𝐴)) < 𝑑} ↔ (𝑣 ∈ (𝐴(,)𝐵) ∧ (abs‘(𝑣𝐴)) < 𝑑))
10 eliooord 12172 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑣𝑣 < 𝐵))
1110adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → (𝐴 < 𝑣𝑣 < 𝐵))
1211simprd 479 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → 𝑣 < 𝐵)
1312biantrurd 529 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → (𝑣 < (𝑑 + 𝐴) ↔ (𝑣 < 𝐵𝑣 < (𝑑 + 𝐴))))
14 ioossre 12174 . . . . . . . . . . . . . . . . . . . . 21 (𝐴(,)𝐵) ⊆ ℝ
15 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → 𝑣 ∈ (𝐴(,)𝐵))
1614, 15sseldi 3586 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → 𝑣 ∈ ℝ)
17 lhop1.a . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ ℝ)
1817ad3antrrr 765 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
19 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝑑 ∈ ℝ+)
2019rpred 11816 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝑑 ∈ ℝ)
2120adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → 𝑑 ∈ ℝ)
2216, 18, 21ltsubaddd 10568 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → ((𝑣𝐴) < 𝑑𝑣 < (𝑑 + 𝐴)))
2316rexrd 10034 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → 𝑣 ∈ ℝ*)
24 lhop1.b . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℝ*)
2524ad3antrrr 765 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ*)
2617ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐴 ∈ ℝ)
2720, 26readdcld 10014 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝑑 + 𝐴) ∈ ℝ)
2827rexrd 10034 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝑑 + 𝐴) ∈ ℝ*)
2928adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → (𝑑 + 𝐴) ∈ ℝ*)
30 xrltmin 11955 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑑 + 𝐴) ∈ ℝ*) → (𝑣 < if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ↔ (𝑣 < 𝐵𝑣 < (𝑑 + 𝐴))))
3123, 25, 29, 30syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → (𝑣 < if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ↔ (𝑣 < 𝐵𝑣 < (𝑑 + 𝐴))))
3213, 22, 313bitr4rd 301 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → (𝑣 < if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ↔ (𝑣𝐴) < 𝑑))
3318rexrd 10034 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ*)
3425, 29ifcld 4108 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∈ ℝ*)
3511simpld 475 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑣)
36 elioo5 12170 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ* ∧ if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∈ ℝ*𝑣 ∈ ℝ*) → (𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))) ↔ (𝐴 < 𝑣𝑣 < if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))))
3736baibd 947 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ ℝ* ∧ if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∈ ℝ*𝑣 ∈ ℝ*) ∧ 𝐴 < 𝑣) → (𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))) ↔ 𝑣 < if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))
3833, 34, 23, 35, 37syl31anc 1326 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → (𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))) ↔ 𝑣 < if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))
3918, 16, 35ltled 10130 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → 𝐴𝑣)
4018, 16, 39abssubge0d 14099 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → (abs‘(𝑣𝐴)) = (𝑣𝐴))
4140breq1d 4628 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑣𝐴)) < 𝑑 ↔ (𝑣𝐴) < 𝑑))
4232, 38, 413bitr4d 300 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → (𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))) ↔ (abs‘(𝑣𝐴)) < 𝑑))
4342rabbi2dva 3804 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → ((𝐴(,)𝐵) ∩ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) = {𝑣 ∈ (𝐴(,)𝐵) ∣ (abs‘(𝑣𝐴)) < 𝑑})
4424ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → 𝐵 ∈ ℝ*)
45 xrmin1 11950 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ ℝ* ∧ (𝑑 + 𝐴) ∈ ℝ*) → if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ≤ 𝐵)
4644, 28, 45syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ≤ 𝐵)
47 iooss2 12150 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ ℝ* ∧ if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ≤ 𝐵) → (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))) ⊆ (𝐴(,)𝐵))
4844, 46, 47syl2anc 692 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))) ⊆ (𝐴(,)𝐵))
49 sseqin2 3800 . . . . . . . . . . . . . . . . 17 ((𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))) ⊆ (𝐴(,)𝐵) ↔ ((𝐴(,)𝐵) ∩ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) = (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))
5048, 49sylib 208 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → ((𝐴(,)𝐵) ∩ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) = (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))
5143, 50eqtr3d 2662 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → {𝑣 ∈ (𝐴(,)𝐵) ∣ (abs‘(𝑣𝐴)) < 𝑑} = (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))
5251eleq2d 2689 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝑣 ∈ {𝑣 ∈ (𝐴(,)𝐵) ∣ (abs‘(𝑣𝐴)) < 𝑑} ↔ 𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))))
539, 52syl5bbr 274 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → ((𝑣 ∈ (𝐴(,)𝐵) ∧ (abs‘(𝑣𝐴)) < 𝑑) ↔ 𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))))
54 lbioo 12145 . . . . . . . . . . . . . . . . . . . . . 22 ¬ 𝐴 ∈ (𝐴(,)𝐵)
55 eleq1 2692 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝐴 → (𝑦 ∈ (𝐴(,)𝐵) ↔ 𝐴 ∈ (𝐴(,)𝐵)))
5654, 55mtbiri 317 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝐴 → ¬ 𝑦 ∈ (𝐴(,)𝐵))
5756necon2ai 2825 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴(,)𝐵) → 𝑦𝐴)
5857biantrurd 529 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝐴(,)𝐵) → ((abs‘(𝑦𝐴)) < 𝑑 ↔ (𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑)))
5958bicomd 213 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (𝐴(,)𝐵) → ((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) ↔ (abs‘(𝑦𝐴)) < 𝑑))
60 fveq2 6150 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘𝑦))
61 fveq2 6150 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘𝑦))
6260, 61oveq12d 6623 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) = (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)))
63 eqid 2626 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))
64 ovex 6633 . . . . . . . . . . . . . . . . . . . . . 22 (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) ∈ V
6562, 63, 64fvmpt3i 6245 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝐴(,)𝐵) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) = (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)))
6665oveq1d 6620 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴(,)𝐵) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶) = ((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶))
6766fveq2d 6154 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝐴(,)𝐵) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) = (abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)))
6867breq1d 4628 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (𝐴(,)𝐵) → ((abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2) ↔ (abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2)))
6959, 68imbi12d 334 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴(,)𝐵) → (((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) ↔ ((abs‘(𝑦𝐴)) < 𝑑 → (abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))))
7069ralbiia 2978 . . . . . . . . . . . . . . . 16 (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) ↔ ∀𝑦 ∈ (𝐴(,)𝐵)((abs‘(𝑦𝐴)) < 𝑑 → (abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2)))
71 oveq1 6612 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑦 → (𝑣𝐴) = (𝑦𝐴))
7271fveq2d 6154 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑦 → (abs‘(𝑣𝐴)) = (abs‘(𝑦𝐴)))
7372breq1d 4628 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑦 → ((abs‘(𝑣𝐴)) < 𝑑 ↔ (abs‘(𝑦𝐴)) < 𝑑))
7473ralrab 3355 . . . . . . . . . . . . . . . 16 (∀𝑦 ∈ {𝑣 ∈ (𝐴(,)𝐵) ∣ (abs‘(𝑣𝐴)) < 𝑑} (abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2) ↔ ∀𝑦 ∈ (𝐴(,)𝐵)((abs‘(𝑦𝐴)) < 𝑑 → (abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2)))
7570, 74bitr4i 267 . . . . . . . . . . . . . . 15 (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) ↔ ∀𝑦 ∈ {𝑣 ∈ (𝐴(,)𝐵) ∣ (abs‘(𝑣𝐴)) < 𝑑} (abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))
7651adantrr 752 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))) → {𝑣 ∈ (𝐴(,)𝐵) ∣ (abs‘(𝑣𝐴)) < 𝑑} = (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))
7776raleqdv 3138 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))) → (∀𝑦 ∈ {𝑣 ∈ (𝐴(,)𝐵) ∣ (abs‘(𝑣𝐴)) < 𝑑} (abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2) ↔ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2)))
7817ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝐴 ∈ ℝ)
7924ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝐵 ∈ ℝ*)
80 lhop1.l . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 < 𝐵)
8180ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝐴 < 𝐵)
82 lhop1.f . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
8382ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
84 lhop1.g . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
8584ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
86 lhop1.if . . . . . . . . . . . . . . . . . . . 20 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
8786ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
88 lhop1.ig . . . . . . . . . . . . . . . . . . . 20 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
8988ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
90 lhop1.f0 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ∈ (𝐹 lim 𝐴))
9190ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 0 ∈ (𝐹 lim 𝐴))
92 lhop1.g0 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ∈ (𝐺 lim 𝐴))
9392ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 0 ∈ (𝐺 lim 𝐴))
94 lhop1.gn0 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ 0 ∈ ran 𝐺)
9594ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → ¬ 0 ∈ ran 𝐺)
96 lhop1.gd0 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐺))
9796ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → ¬ 0 ∈ ran (ℝ D 𝐺))
981ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴))
993adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → (𝑥 / 2) ∈ ℝ+)
10078rexrd 10034 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝐴 ∈ ℝ*)
101 simprll 801 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝑑 ∈ ℝ+)
102101rpred 11816 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝑑 ∈ ℝ)
103102, 78readdcld 10014 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → (𝑑 + 𝐴) ∈ ℝ)
104 iocssre 12192 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ* ∧ (𝑑 + 𝐴) ∈ ℝ) → (𝐴(,](𝑑 + 𝐴)) ⊆ ℝ)
105100, 103, 104syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → (𝐴(,](𝑑 + 𝐴)) ⊆ ℝ)
10679adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) ∧ 𝐵 ≤ (𝑑 + 𝐴)) → 𝐵 ∈ ℝ*)
107102adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) ∧ ¬ 𝐵 ≤ (𝑑 + 𝐴)) → 𝑑 ∈ ℝ)
10878adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) ∧ ¬ 𝐵 ≤ (𝑑 + 𝐴)) → 𝐴 ∈ ℝ)
109107, 108readdcld 10014 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) ∧ ¬ 𝐵 ≤ (𝑑 + 𝐴)) → (𝑑 + 𝐴) ∈ ℝ)
110109rexrd 10034 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) ∧ ¬ 𝐵 ≤ (𝑑 + 𝐴)) → (𝑑 + 𝐴) ∈ ℝ*)
111106, 110ifclda 4097 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∈ ℝ*)
11278, 101ltaddrp2d 11850 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝐴 < (𝑑 + 𝐴))
113103rexrd 10034 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → (𝑑 + 𝐴) ∈ ℝ*)
114 xrltmin 11955 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑑 + 𝐴) ∈ ℝ*) → (𝐴 < if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ↔ (𝐴 < 𝐵𝐴 < (𝑑 + 𝐴))))
115100, 79, 113, 114syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → (𝐴 < if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ↔ (𝐴 < 𝐵𝐴 < (𝑑 + 𝐴))))
11681, 112, 115mpbir2and 956 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝐴 < if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))
117 xrmin2 11951 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵 ∈ ℝ* ∧ (𝑑 + 𝐴) ∈ ℝ*) → if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ≤ (𝑑 + 𝐴))
11879, 113, 117syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ≤ (𝑑 + 𝐴))
119 elioc1 12156 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ* ∧ (𝑑 + 𝐴) ∈ ℝ*) → (if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∈ (𝐴(,](𝑑 + 𝐴)) ↔ (if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∈ ℝ*𝐴 < if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∧ if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ≤ (𝑑 + 𝐴))))
120100, 113, 119syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → (if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∈ (𝐴(,](𝑑 + 𝐴)) ↔ (if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∈ ℝ*𝐴 < if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∧ if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ≤ (𝑑 + 𝐴))))
121111, 116, 118, 120mpbir3and 1243 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∈ (𝐴(,](𝑑 + 𝐴)))
122105, 121sseldd 3589 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ∈ ℝ)
12379, 113, 45syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)) ≤ 𝐵)
124 simprlr 802 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → 𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))
125 simprr 795 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))
126 eqid 2626 . . . . . . . . . . . . . . . . . . 19 (𝐴 + (𝑟 / 2)) = (𝐴 + (𝑟 / 2))
12778, 79, 81, 83, 85, 87, 89, 91, 93, 95, 97, 98, 99, 122, 123, 124, 125, 126lhop1lem 23675 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)) < (2 · (𝑥 / 2)))
1282rpcnd 11818 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
129 2cnd 11038 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ+) → 2 ∈ ℂ)
130 2ne0 11058 . . . . . . . . . . . . . . . . . . . . 21 2 ≠ 0
131130a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ+) → 2 ≠ 0)
132128, 129, 131divcan2d 10748 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → (2 · (𝑥 / 2)) = 𝑥)
133132adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → (2 · (𝑥 / 2)) = 𝑥)
134127, 133breqtrd 4644 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ ((𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))) ∧ ∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2))) → (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)) < 𝑥)
135134expr 642 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))) → (∀𝑦 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴)))(abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2) → (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)) < 𝑥))
13677, 135sylbid 230 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))) → (∀𝑦 ∈ {𝑣 ∈ (𝐴(,)𝐵) ∣ (abs‘(𝑣𝐴)) < 𝑑} (abs‘((((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)) − 𝐶)) < (𝑥 / 2) → (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)) < 𝑥))
13775, 136syl5bi 232 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))))) → (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)) < 𝑥))
138137expr 642 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (𝑣 ∈ (𝐴(,)if(𝐵 ≤ (𝑑 + 𝐴), 𝐵, (𝑑 + 𝐴))) → (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)) < 𝑥)))
13953, 138sylbid 230 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → ((𝑣 ∈ (𝐴(,)𝐵) ∧ (abs‘(𝑣𝐴)) < 𝑑) → (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)) < 𝑥)))
140139expdimp 453 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑣𝐴)) < 𝑑 → (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)) < 𝑥)))
141 fveq2 6150 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑣 → (𝐹𝑧) = (𝐹𝑣))
142 fveq2 6150 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑣 → (𝐺𝑧) = (𝐺𝑣))
143141, 142oveq12d 6623 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑣 → ((𝐹𝑧) / (𝐺𝑧)) = ((𝐹𝑣) / (𝐺𝑣)))
144 eqid 2626 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))
145 ovex 6633 . . . . . . . . . . . . . . . . 17 ((𝐹𝑧) / (𝐺𝑧)) ∈ V
146143, 144, 145fvmpt3i 6245 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (𝐴(,)𝐵) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) = ((𝐹𝑣) / (𝐺𝑣)))
147146oveq1d 6620 . . . . . . . . . . . . . . 15 (𝑣 ∈ (𝐴(,)𝐵) → (((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶) = (((𝐹𝑣) / (𝐺𝑣)) − 𝐶))
148147fveq2d 6154 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝐴(,)𝐵) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) = (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)))
149148breq1d 4628 . . . . . . . . . . . . 13 (𝑣 ∈ (𝐴(,)𝐵) → ((abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥 ↔ (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)) < 𝑥))
150149imbi2d 330 . . . . . . . . . . . 12 (𝑣 ∈ (𝐴(,)𝐵) → ((∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥) ↔ (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)) < 𝑥)))
151150adantl 482 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → ((∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥) ↔ (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → (abs‘(((𝐹𝑣) / (𝐺𝑣)) − 𝐶)) < 𝑥)))
152140, 151sylibrd 249 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑣𝐴)) < 𝑑 → (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥)))
153152adantld 483 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → ((𝑣𝐴 ∧ (abs‘(𝑣𝐴)) < 𝑑) → (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥)))
154153com23 86 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) ∧ 𝑣 ∈ (𝐴(,)𝐵)) → (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → ((𝑣𝐴 ∧ (abs‘(𝑣𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥)))
155154ralrimdva 2968 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (∀𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → ∀𝑣 ∈ (𝐴(,)𝐵)((𝑣𝐴 ∧ (abs‘(𝑣𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥)))
156155reximdva 3016 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (∃𝑑 ∈ ℝ+𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < (𝑥 / 2)) → ∃𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)𝐵)((𝑣𝐴 ∧ (abs‘(𝑣𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥)))
1578, 156syld 47 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < 𝑒) → ∃𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)𝐵)((𝑣𝐴 ∧ (abs‘(𝑣𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥)))
158157ralrimdva 2968 . . . 4 (𝜑 → (∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < 𝑒) → ∀𝑥 ∈ ℝ+𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)𝐵)((𝑣𝐴 ∧ (abs‘(𝑣𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥)))
159158anim2d 588 . . 3 (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < 𝑒)) → (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)𝐵)((𝑣𝐴 ∧ (abs‘(𝑣𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥))))
160 dvf 23572 . . . . . . . 8 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
16186feq2d 5990 . . . . . . . 8 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
162160, 161mpbii 223 . . . . . . 7 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
163162ffvelrnda 6316 . . . . . 6 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ ℂ)
164 dvf 23572 . . . . . . . 8 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
16588feq2d 5990 . . . . . . . 8 (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
166164, 165mpbii 223 . . . . . . 7 (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
167166ffvelrnda 6316 . . . . . 6 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ℂ)
16896adantr 481 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran (ℝ D 𝐺))
169 ffn 6004 . . . . . . . . . . 11 ((ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
170166, 169syl 17 . . . . . . . . . 10 (𝜑 → (ℝ D 𝐺) Fn (𝐴(,)𝐵))
171 fnfvelrn 6313 . . . . . . . . . 10 (((ℝ D 𝐺) Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
172170, 171sylan 488 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺))
173 eleq1 2692 . . . . . . . . 9 (((ℝ D 𝐺)‘𝑧) = 0 → (((ℝ D 𝐺)‘𝑧) ∈ ran (ℝ D 𝐺) ↔ 0 ∈ ran (ℝ D 𝐺)))
174172, 173syl5ibcom 235 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐺)‘𝑧) = 0 → 0 ∈ ran (ℝ D 𝐺)))
175174necon3bd 2810 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran (ℝ D 𝐺) → ((ℝ D 𝐺)‘𝑧) ≠ 0))
176168, 175mpd 15 . . . . . 6 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ≠ 0)
177163, 167, 176divcld 10746 . . . . 5 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)) ∈ ℂ)
178177, 63fmptd 6341 . . . 4 (𝜑 → (𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))):(𝐴(,)𝐵)⟶ℂ)
179 ax-resscn 9938 . . . . . 6 ℝ ⊆ ℂ
18014, 179sstri 3597 . . . . 5 (𝐴(,)𝐵) ⊆ ℂ
181180a1i 11 . . . 4 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
18217recnd 10013 . . . 4 (𝜑𝐴 ∈ ℂ)
183178, 181, 182ellimc3 23544 . . 3 (𝜑 → (𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴) ↔ (𝐶 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦 ∈ (𝐴(,)𝐵)((𝑦𝐴 ∧ (abs‘(𝑦𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧)))‘𝑦) − 𝐶)) < 𝑒))))
18482ffvelrnda 6316 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℝ)
185184recnd 10013 . . . . . 6 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℂ)
18684ffvelrnda 6316 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℝ)
187186recnd 10013 . . . . . 6 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℂ)
18894adantr 481 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran 𝐺)
189 ffn 6004 . . . . . . . . . . 11 (𝐺:(𝐴(,)𝐵)⟶ℝ → 𝐺 Fn (𝐴(,)𝐵))
19084, 189syl 17 . . . . . . . . . 10 (𝜑𝐺 Fn (𝐴(,)𝐵))
191 fnfvelrn 6313 . . . . . . . . . 10 ((𝐺 Fn (𝐴(,)𝐵) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ran 𝐺)
192190, 191sylan 488 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ran 𝐺)
193 eleq1 2692 . . . . . . . . 9 ((𝐺𝑧) = 0 → ((𝐺𝑧) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺))
194192, 193syl5ibcom 235 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((𝐺𝑧) = 0 → 0 ∈ ran 𝐺))
195194necon3bd 2810 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (¬ 0 ∈ ran 𝐺 → (𝐺𝑧) ≠ 0))
196188, 195mpd 15 . . . . . 6 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ≠ 0)
197185, 187, 196divcld 10746 . . . . 5 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((𝐹𝑧) / (𝐺𝑧)) ∈ ℂ)
198197, 144fmptd 6341 . . . 4 (𝜑 → (𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))):(𝐴(,)𝐵)⟶ℂ)
199198, 181, 182ellimc3 23544 . . 3 (𝜑 → (𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐴) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑑 ∈ ℝ+𝑣 ∈ (𝐴(,)𝐵)((𝑣𝐴 ∧ (abs‘(𝑣𝐴)) < 𝑑) → (abs‘(((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧)))‘𝑣) − 𝐶)) < 𝑥))))
200159, 183, 1993imtr4d 283 . 2 (𝜑 → (𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑧) / ((ℝ D 𝐺)‘𝑧))) lim 𝐴) → 𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐴)))
2011, 200mpd 15 1 (𝜑𝐶 ∈ ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑧) / (𝐺𝑧))) lim 𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1992   ≠ wne 2796  ∀wral 2912  ∃wrex 2913  {crab 2916   ∩ cin 3559   ⊆ wss 3560  ifcif 4063   class class class wbr 4618   ↦ cmpt 4678  dom cdm 5079  ran crn 5080   Fn wfn 5845  ⟶wf 5846  ‘cfv 5850  (class class class)co 6605  ℂcc 9879  ℝcr 9880  0cc0 9881   + caddc 9884   · cmul 9886  ℝ*cxr 10018   < clt 10019   ≤ cle 10020   − cmin 10211   / cdiv 10629  2c2 11015  ℝ+crp 11776  (,)cioo 12114  (,]cioc 12115  abscabs 13903   limℂ climc 23527   D cdv 23528 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-inf2 8483  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958  ax-pre-sup 9959  ax-addf 9960  ax-mulf 9961 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-isom 5859  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-of 6851  df-om 7014  df-1st 7116  df-2nd 7117  df-supp 7242  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-2o 7507  df-oadd 7510  df-er 7688  df-map 7805  df-pm 7806  df-ixp 7854  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-fsupp 8221  df-fi 8262  df-sup 8293  df-inf 8294  df-oi 8360  df-card 8710  df-cda 8935  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-nn 10966  df-2 11024  df-3 11025  df-4 11026  df-5 11027  df-6 11028  df-7 11029  df-8 11030  df-9 11031  df-n0 11238  df-z 11323  df-dec 11438  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12118  df-ioc 12119  df-ico 12120  df-icc 12121  df-fz 12266  df-fzo 12404  df-seq 12739  df-exp 12798  df-hash 13055  df-cj 13768  df-re 13769  df-im 13770  df-sqrt 13904  df-abs 13905  df-struct 15778  df-ndx 15779  df-slot 15780  df-base 15781  df-sets 15782  df-ress 15783  df-plusg 15870  df-mulr 15871  df-starv 15872  df-sca 15873  df-vsca 15874  df-ip 15875  df-tset 15876  df-ple 15877  df-ds 15880  df-unif 15881  df-hom 15882  df-cco 15883  df-rest 15999  df-topn 16000  df-0g 16018  df-gsum 16019  df-topgen 16020  df-pt 16021  df-prds 16024  df-xrs 16078  df-qtop 16083  df-imas 16084  df-xps 16086  df-mre 16162  df-mrc 16163  df-acs 16165  df-mgm 17158  df-sgrp 17200  df-mnd 17211  df-submnd 17252  df-mulg 17457  df-cntz 17666  df-cmn 18111  df-psmet 19652  df-xmet 19653  df-met 19654  df-bl 19655  df-mopn 19656  df-fbas 19657  df-fg 19658  df-cnfld 19661  df-top 20616  df-bases 20617  df-topon 20618  df-topsp 20619  df-cld 20728  df-ntr 20729  df-cls 20730  df-nei 20807  df-lp 20845  df-perf 20846  df-cn 20936  df-cnp 20937  df-haus 21024  df-cmp 21095  df-tx 21270  df-hmeo 21463  df-fil 21555  df-fm 21647  df-flim 21648  df-flf 21649  df-xms 22030  df-ms 22031  df-tms 22032  df-cncf 22584  df-limc 23531  df-dv 23532 This theorem is referenced by:  lhop2  23677  lhop  23678  fourierdlem61  39678
 Copyright terms: Public domain W3C validator