Theorem rlimdiv

Description: Limit of the quotient of two converging functions. Proposition 12-2.1(a) of Gleason p. 168. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Hypotheses	rlimadd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	rlimadd.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
	rlimadd.5	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
	rlimadd.6	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 )
	rlimdiv.7	⊢ ( 𝜑 → 𝐸 ≠ 0 )
	rlimdiv.8	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≠ 0 )
Assertion	rlimdiv	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 / 𝐶 ) ) ⇝𝑟 ( 𝐷 / 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		rlimadd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		rlimadd.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
3		rlimadd.5	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
4		rlimadd.6	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 )
5		rlimdiv.7	⊢ ( 𝜑 → 𝐸 ≠ 0 )
6		rlimdiv.8	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≠ 0 )
7	1 3	rlimmptrcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
8	2 4	rlimmptrcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
9	8 6	reccld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 / 𝐶 ) ∈ ℂ )
10		eldifsn	⊢ ( 𝐶 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
11	8 6 10	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( ℂ ∖ { 0 } ) )
12	11	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ( ℂ ∖ { 0 } ) )
13		rlimcl	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 → 𝐸 ∈ ℂ )
14	4 13	syl	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
15		eldifsn	⊢ ( 𝐸 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) )
16	14 5 15	sylanbrc	⊢ ( 𝜑 → 𝐸 ∈ ( ℂ ∖ { 0 } ) )
17		eldifsn	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
18		reccl	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 1 / 𝑦 ) ∈ ℂ )
19	17 18	sylbi	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑦 ) ∈ ℂ )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 1 / 𝑦 ) ∈ ℂ )
21	20	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ )
22		eqid	⊢ ( if ( 1 ≤ ( ( abs ‘ 𝐸 ) · 𝑧 ) , 1 , ( ( abs ‘ 𝐸 ) · 𝑧 ) ) · ( ( abs ‘ 𝐸 ) / 2 ) ) = ( if ( 1 ≤ ( ( abs ‘ 𝐸 ) · 𝑧 ) , 1 , ( ( abs ‘ 𝐸 ) · 𝑧 ) ) · ( ( abs ‘ 𝐸 ) / 2 ) )
23	22	reccn2	⊢ ( ( 𝐸 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑧 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) )
24	16 23	sylan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) )
25		oveq2	⊢ ( 𝑦 = 𝑣 → ( 1 / 𝑦 ) = ( 1 / 𝑣 ) )
26		eqid	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) )
27		ovex	⊢ ( 1 / 𝑣 ) ∈ V
28	25 26 27	fvmpt	⊢ ( 𝑣 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) = ( 1 / 𝑣 ) )
29		oveq2	⊢ ( 𝑦 = 𝐸 → ( 1 / 𝑦 ) = ( 1 / 𝐸 ) )
30		ovex	⊢ ( 1 / 𝐸 ) ∈ V
31	29 26 30	fvmpt	⊢ ( 𝐸 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) = ( 1 / 𝐸 ) )
32	16 31	syl	⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) = ( 1 / 𝐸 ) )
33	28 32	oveqan12rd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) = ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) )
34	33	fveq2d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) = ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) )
35	34	breq1d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ↔ ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) )
36	35	imbi2d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ) ↔ ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) ) )
37	36	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ) ↔ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) ) )
38	37	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ) ↔ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) ) )
39	38	biimpar	⊢ ( ( 𝜑 ∧ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ) )
40	24 39	syldan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ) )
41	12 16 4 21 40	rlimcn1	⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) ⇝𝑟 ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) )
42		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
43		eqidd	⊢ ( 𝜑 → ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) )
44		oveq2	⊢ ( 𝑦 = 𝐶 → ( 1 / 𝑦 ) = ( 1 / 𝐶 ) )
45	11 42 43 44	fmptco	⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐶 ) ) )
46	41 45 32	3brtr3d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐶 ) ) ⇝𝑟 ( 1 / 𝐸 ) )
47	7 9 3 46	rlimmul	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 1 / 𝐶 ) ) ) ⇝𝑟 ( 𝐷 · ( 1 / 𝐸 ) ) )
48	7 8 6	divrecd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 / 𝐶 ) = ( 𝐵 · ( 1 / 𝐶 ) ) )
49	48	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 / 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 1 / 𝐶 ) ) ) )
50		rlimcl	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 → 𝐷 ∈ ℂ )
51	3 50	syl	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
52	51 14 5	divrecd	⊢ ( 𝜑 → ( 𝐷 / 𝐸 ) = ( 𝐷 · ( 1 / 𝐸 ) ) )
53	47 49 52	3brtr4d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 / 𝐶 ) ) ⇝𝑟 ( 𝐷 / 𝐸 ) )