Metamath Proof Explorer

Theorem lhop1

Description: L'Hôpital's Rule for limits from the right. If F and G are differentiable real functions on ( A , B ) , and F and G both approach 0 at A , and G ( x ) and G ' ( x ) are not zero on ( A , B ) , and the limit of F ' ( x ) / G ' ( x ) at A is C , then the limit F ( x ) / G ( x ) at A also exists and equals C . (Contributed by Mario Carneiro, 29-Dec-2016)

Ref Expression
Hypotheses 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 lhop1 ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 lhop1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 lhop1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 lhop1.l ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 lhop1.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
5 lhop1.g ⊢ ( 𝜑 → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
6 lhop1.if ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
7 lhop1.ig ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
8 lhop1.f0 ⊢ ( 𝜑 → 0 ∈ ( 𝐹 limℂ 𝐴 ) )
9 lhop1.g0 ⊢ ( 𝜑 → 0 ∈ ( 𝐺 limℂ 𝐴 ) )
10 lhop1.gn0 ⊢ ( 𝜑 → ¬ 0 ∈ ran 𝐺 )
11 lhop1.gd0 ⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐺 ) )
12 lhop1.c ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐴 ) )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
14 13 rphalfcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ+ )
15 breq2 ⊢ ( 𝑒 = ( 𝑥 / 2 ) → ( ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < 𝑒 ↔ ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) )
16 15 imbi2d ⊢ ( 𝑒 = ( 𝑥 / 2 ) → ( ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < 𝑒 ) ↔ ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) )
17 16 rexralbidv ⊢ ( 𝑒 = ( 𝑥 / 2 ) → ( ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < 𝑒 ) ↔ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) )
18 17 rspcv ⊢ ( ( 𝑥 / 2 ) ∈ ℝ+ → ( ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < 𝑒 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) )
19 14 18 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < 𝑒 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) )
20 rabid ⊢ ( 𝑣 ∈ { 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∣ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 } ↔ ( 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) )
21 eliooord ⊢ ( 𝑣 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝑣 ∧ 𝑣 < 𝐵 ) )
22 21 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 < 𝑣 ∧ 𝑣 < 𝐵 ) )
23 22 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑣 < 𝐵 )
24 23 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑣 < ( 𝑑 + 𝐴 ) ↔ ( 𝑣 < 𝐵 ∧ 𝑣 < ( 𝑑 + 𝐴 ) ) ) )
25 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
26 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑣 ∈ ( 𝐴 (,) 𝐵 ) )
27 25 26 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑣 ∈ ℝ )
28 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
29 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → 𝑑 ∈ ℝ+ )
30 29 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → 𝑑 ∈ ℝ )
31 30 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑑 ∈ ℝ )
32 27 28 31 ltsubaddd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑣 − 𝐴 ) < 𝑑 ↔ 𝑣 < ( 𝑑 + 𝐴 ) ) )
33 27 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑣 ∈ ℝ* )
34 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
35 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
36 30 35 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → ( 𝑑 + 𝐴 ) ∈ ℝ )
37 36 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → ( 𝑑 + 𝐴 ) ∈ ℝ* )
38 37 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑑 + 𝐴 ) ∈ ℝ* )
39 xrltmin ⊢ ( ( 𝑣 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑑 + 𝐴 ) ∈ ℝ* ) → ( 𝑣 < if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ↔ ( 𝑣 < 𝐵 ∧ 𝑣 < ( 𝑑 + 𝐴 ) ) ) )
40 33 34 38 39 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑣 < if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ↔ ( 𝑣 < 𝐵 ∧ 𝑣 < ( 𝑑 + 𝐴 ) ) ) )
41 24 32 40 3bitr4rd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑣 < if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ↔ ( 𝑣 − 𝐴 ) < 𝑑 ) )
42 28 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
43 34 38 ifcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∈ ℝ* )
44 22 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑣 )
45 elioo5 ⊢ ( ( 𝐴 ∈ ℝ* ∧ if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∈ ℝ* ∧ 𝑣 ∈ ℝ* ) → ( 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ↔ ( 𝐴 < 𝑣 ∧ 𝑣 < if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) )
46 45 baibd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∈ ℝ* ∧ 𝑣 ∈ ℝ* ) ∧ 𝐴 < 𝑣 ) → ( 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ↔ 𝑣 < if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) )
47 42 43 33 44 46 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ↔ 𝑣 < if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) )
48 28 27 44 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ≤ 𝑣 )
49 28 27 48 abssubge0d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝑣 − 𝐴 ) ) = ( 𝑣 − 𝐴 ) )
50 49 breq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ↔ ( 𝑣 − 𝐴 ) < 𝑑 ) )
51 41 47 50 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ↔ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) )
52 51 rabbi2dva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) = { 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∣ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 } )
53 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → 𝐵 ∈ ℝ* )
54 xrmin1 ⊢ ( ( 𝐵 ∈ ℝ* ∧ ( 𝑑 + 𝐴 ) ∈ ℝ* ) → if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ≤ 𝐵 )
55 53 37 54 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ≤ 𝐵 )
56 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ≤ 𝐵 ) → ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ⊆ ( 𝐴 (,) 𝐵 ) )
57 53 55 56 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ⊆ ( 𝐴 (,) 𝐵 ) )
58 sseqin2 ⊢ ( ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ⊆ ( 𝐴 (,) 𝐵 ) ↔ ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) = ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) )
59 57 58 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) = ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) )
60 52 59 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → { 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∣ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 } = ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) )
61 60 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → ( 𝑣 ∈ { 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∣ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 } ↔ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) )
62 20 61 bitr3id ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → ( ( 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) ↔ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) )
63 lbioo ⊢ ¬ 𝐴 ∈ ( 𝐴 (,) 𝐵 )
64 eleq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↔ 𝐴 ∈ ( 𝐴 (,) 𝐵 ) ) )
65 63 64 mtbiri ⊢ ( 𝑦 = 𝐴 → ¬ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) )
66 65 necon2ai ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → 𝑦 ≠ 𝐴 )
67 66 biantrurd ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → ( ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ↔ ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) ) )
68 67 bicomd ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) ↔ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) )
69 fveq2 ⊢ ( 𝑧 = 𝑦 → ( ( ℝ D 𝐹 ) ‘ 𝑧 ) = ( ( ℝ D 𝐹 ) ‘ 𝑦 ) )
70 fveq2 ⊢ ( 𝑧 = 𝑦 → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) = ( ( ℝ D 𝐺 ) ‘ 𝑦 ) )
71 69 70 oveq12d ⊢ ( 𝑧 = 𝑦 → ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) )
72 eqid ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) )
73 ovex ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ∈ V
74 71 72 73 fvmpt3i ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) )
75 74 fvoveq1d ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) = ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) )
76 75 breq1d ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → ( ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ↔ ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) )
77 68 76 imbi12d ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → ( ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ↔ ( ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 → ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) )
78 77 ralbiia ⊢ ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ↔ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 → ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) )
79 fvoveq1 ⊢ ( 𝑣 = 𝑦 → ( abs ‘ ( 𝑣 − 𝐴 ) ) = ( abs ‘ ( 𝑦 − 𝐴 ) ) )
80 79 breq1d ⊢ ( 𝑣 = 𝑦 → ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ↔ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) )
81 80 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∣ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 } ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ↔ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 → ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) )
82 78 81 bitr4i ⊢ ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ↔ ∀ 𝑦 ∈ { 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∣ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 } ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) )
83 60 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ) → { 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∣ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 } = ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) )
84 83 raleqdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ) → ( ∀ 𝑦 ∈ { 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∣ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 } ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ↔ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) )
85 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝐴 ∈ ℝ )
86 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝐵 ∈ ℝ* )
87 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝐴 < 𝐵 )
88 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
89 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
90 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
91 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
92 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 0 ∈ ( 𝐹 limℂ 𝐴 ) )
93 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 0 ∈ ( 𝐺 limℂ 𝐴 ) )
94 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ¬ 0 ∈ ran 𝐺 )
95 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ¬ 0 ∈ ran ( ℝ D 𝐺 ) )
96 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐴 ) )
97 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ( 𝑥 / 2 ) ∈ ℝ+ )
98 85 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝐴 ∈ ℝ* )
99 simprll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝑑 ∈ ℝ+ )
100 99 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝑑 ∈ ℝ )
101 100 85 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ( 𝑑 + 𝐴 ) ∈ ℝ )
102 iocssre ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝑑 + 𝐴 ) ∈ ℝ ) → ( 𝐴 (,] ( 𝑑 + 𝐴 ) ) ⊆ ℝ )
103 98 101 102 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ( 𝐴 (,] ( 𝑑 + 𝐴 ) ) ⊆ ℝ )
104 86 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) ∧ 𝐵 ≤ ( 𝑑 + 𝐴 ) ) → 𝐵 ∈ ℝ* )
105 100 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) ∧ ¬ 𝐵 ≤ ( 𝑑 + 𝐴 ) ) → 𝑑 ∈ ℝ )
106 85 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) ∧ ¬ 𝐵 ≤ ( 𝑑 + 𝐴 ) ) → 𝐴 ∈ ℝ )
107 105 106 readdcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) ∧ ¬ 𝐵 ≤ ( 𝑑 + 𝐴 ) ) → ( 𝑑 + 𝐴 ) ∈ ℝ )
108 107 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) ∧ ¬ 𝐵 ≤ ( 𝑑 + 𝐴 ) ) → ( 𝑑 + 𝐴 ) ∈ ℝ* )
109 104 108 ifclda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∈ ℝ* )
110 85 99 ltaddrp2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝐴 < ( 𝑑 + 𝐴 ) )
111 101 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ( 𝑑 + 𝐴 ) ∈ ℝ* )
112 xrltmin ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑑 + 𝐴 ) ∈ ℝ* ) → ( 𝐴 < if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ↔ ( 𝐴 < 𝐵 ∧ 𝐴 < ( 𝑑 + 𝐴 ) ) ) )
113 98 86 111 112 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ( 𝐴 < if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ↔ ( 𝐴 < 𝐵 ∧ 𝐴 < ( 𝑑 + 𝐴 ) ) ) )
114 87 110 113 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝐴 < if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) )
115 xrmin2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ ( 𝑑 + 𝐴 ) ∈ ℝ* ) → if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ≤ ( 𝑑 + 𝐴 ) )
116 86 111 115 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ≤ ( 𝑑 + 𝐴 ) )
117 elioc1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝑑 + 𝐴 ) ∈ ℝ* ) → ( if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∈ ( 𝐴 (,] ( 𝑑 + 𝐴 ) ) ↔ ( if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∈ ℝ* ∧ 𝐴 < if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∧ if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ≤ ( 𝑑 + 𝐴 ) ) ) )
118 98 111 117 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ( if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∈ ( 𝐴 (,] ( 𝑑 + 𝐴 ) ) ↔ ( if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∈ ℝ* ∧ 𝐴 < if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∧ if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ≤ ( 𝑑 + 𝐴 ) ) ) )
119 109 114 116 118 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∈ ( 𝐴 (,] ( 𝑑 + 𝐴 ) ) )
120 103 119 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ∈ ℝ )
121 86 111 54 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ≤ 𝐵 )
122 simprlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) )
123 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) )
124 eqid ⊢ ( 𝐴 + ( 𝑟 / 2 ) ) = ( 𝐴 + ( 𝑟 / 2 ) )
125 85 86 87 88 89 90 91 92 93 94 95 96 97 120 121 122 123 124 lhop1lem ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) < ( 2 · ( 𝑥 / 2 ) ) )
126 13 rpcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
127 2cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 2 ∈ ℂ )
128 2ne0 ⊢ 2 ≠ 0
129 128 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 2 ≠ 0 )
130 126 127 129 divcan2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( 𝑥 / 2 ) ) = 𝑥 )
131 130 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ( 2 · ( 𝑥 / 2 ) ) = 𝑥 )
132 125 131 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) < 𝑥 )
133 132 expr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) < 𝑥 ) )
134 84 133 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ) → ( ∀ 𝑦 ∈ { 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∣ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 } ( abs ‘ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) / ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) − 𝐶 ) ) < ( 𝑥 / 2 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) < 𝑥 ) )
135 82 134 syl5bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℝ+ ∧ 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) ) ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) < 𝑥 ) )
136 135 expr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → ( 𝑣 ∈ ( 𝐴 (,) if ( 𝐵 ≤ ( 𝑑 + 𝐴 ) , 𝐵 , ( 𝑑 + 𝐴 ) ) ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) < 𝑥 ) ) )
137 62 136 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → ( ( 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) < 𝑥 ) ) )
138 137 expdimp ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) < 𝑥 ) ) )
139 fveq2 ⊢ ( 𝑧 = 𝑣 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑣 ) )
140 fveq2 ⊢ ( 𝑧 = 𝑣 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑣 ) )
141 139 140 oveq12d ⊢ ( 𝑧 = 𝑣 → ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) )
142 eqid ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) )
143 ovex ⊢ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ∈ V
144 141 142 143 fvmpt3i ⊢ ( 𝑣 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) )
145 144 fvoveq1d ⊢ ( 𝑣 ∈ ( 𝐴 (,) 𝐵 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) )
146 145 breq1d ⊢ ( 𝑣 ∈ ( 𝐴 (,) 𝐵 ) → ( ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) < 𝑥 ) )
147 146 imbi2d ⊢ ( 𝑣 ∈ ( 𝐴 (,) 𝐵 ) → ( ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ) ↔ ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) < 𝑥 ) ) )
148 147 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ) ↔ ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) − 𝐶 ) ) < 𝑥 ) ) )
149 138 148 sylibrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ) ) )
150 149 adantld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑣 ≠ 𝐴 ∧ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ) ) )
151 150 com23 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ( ( 𝑣 ≠ 𝐴 ∧ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ) ) )
152 151 ralrimdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑣 ≠ 𝐴 ∧ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ) ) )
153 152 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < ( 𝑥 / 2 ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑣 ≠ 𝐴 ∧ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ) ) )
154 19 153 syld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < 𝑒 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑣 ≠ 𝐴 ∧ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ) ) )
155 154 ralrimdva ⊢ ( 𝜑 → ( ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < 𝑒 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑣 ≠ 𝐴 ∧ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ) ) )
156 155 anim2d ⊢ ( 𝜑 → ( ( 𝐶 ∈ ℂ ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < 𝑒 ) ) → ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑣 ≠ 𝐴 ∧ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ) ) ) )
157 dvf ⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
158 6 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
159 157 158 mpbii ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
160 159 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ℂ )
161 dvf ⊢ ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ
162 7 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ ↔ ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
163 161 162 mpbii ⊢ ( 𝜑 → ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
164 163 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ∈ ℂ )
165 11 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 0 ∈ ran ( ℝ D 𝐺 ) )
166 163 ffnd ⊢ ( 𝜑 → ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) )
167 fnfvelrn ⊢ ( ( ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ∈ ran ( ℝ D 𝐺 ) )
168 166 167 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ∈ ran ( ℝ D 𝐺 ) )
169 eleq1 ⊢ ( ( ( ℝ D 𝐺 ) ‘ 𝑧 ) = 0 → ( ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ∈ ran ( ℝ D 𝐺 ) ↔ 0 ∈ ran ( ℝ D 𝐺 ) ) )
170 168 169 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D 𝐺 ) ‘ 𝑧 ) = 0 → 0 ∈ ran ( ℝ D 𝐺 ) ) )
171 170 necon3bd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ¬ 0 ∈ ran ( ℝ D 𝐺 ) → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ≠ 0 ) )
172 165 171 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ≠ 0 )
173 160 164 172 divcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ∈ ℂ )
174 173 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
175 ax-resscn ⊢ ℝ ⊆ ℂ
176 25 175 sstri ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
177 176 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
178 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
179 174 177 178 ellimc3 ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐴 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ≠ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ‘ 𝑦 ) − 𝐶 ) ) < 𝑒 ) ) ) )
180 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
181 180 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
182 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
183 182 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
184 10 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 0 ∈ ran 𝐺 )
185 5 ffnd ⊢ ( 𝜑 → 𝐺 Fn ( 𝐴 (,) 𝐵 ) )
186 fnfvelrn ⊢ ( ( 𝐺 Fn ( 𝐴 (,) 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 )
187 185 186 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 )
188 eleq1 ⊢ ( ( 𝐺 ‘ 𝑧 ) = 0 → ( ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺 ) )
189 187 188 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐺 ‘ 𝑧 ) = 0 → 0 ∈ ran 𝐺 ) )
190 189 necon3bd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ¬ 0 ∈ ran 𝐺 → ( 𝐺 ‘ 𝑧 ) ≠ 0 ) )
191 184 190 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 )
192 181 183 191 divcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
193 192 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
194 193 177 178 ellimc3 ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐴 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑣 ≠ 𝐴 ∧ ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑑 ) → ( abs ‘ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑣 ) − 𝐶 ) ) < 𝑥 ) ) ) )
195 156 179 194 3imtr4d ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐴 ) → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐴 ) ) )
196 12 195 mpd ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐴 ) )