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	biimtrid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ∧ ( 𝑑 ∈ ℝ⁺ ∧ 𝑣 ∈ ( 𝐴 (,) 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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ℂ )
161		dvf	⊢ ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ
162	7	feq2d	⊢ ( 𝜑 → ( ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ ↔ ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
163	161 162	mpbii	⊢ ( 𝜑 → ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
164	163	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ 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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
181	180	recnd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
182	5	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
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_ℂ 𝐴 ) )

Metamath Proof Explorer

Theorem lhop1

Proof