divlimc

Description: Limit of the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	divlimc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	divlimc.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
	divlimc.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 / 𝐶 ) )
	divlimc.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	divlimc.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( ℂ ∖ { 0 } ) )
	divlimc.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 lim_ℂ 𝐷 ) )
	divlimc.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐺 lim_ℂ 𝐷 ) )
	divlimc.yne0	⊢ ( 𝜑 → 𝑌 ≠ 0 )
	divlimc.cne0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≠ 0 )
Assertion	divlimc	⊢ ( 𝜑 → ( 𝑋 / 𝑌 ) ∈ ( 𝐻 lim_ℂ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		divlimc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		divlimc.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
3		divlimc.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 / 𝐶 ) )
4		divlimc.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5		divlimc.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( ℂ ∖ { 0 } ) )
6		divlimc.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 lim_ℂ 𝐷 ) )
7		divlimc.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐺 lim_ℂ 𝐷 ) )
8		divlimc.yne0	⊢ ( 𝜑 → 𝑌 ≠ 0 )
9		divlimc.cne0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≠ 0 )
10		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐶 ) )
11		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 1 / 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 1 / 𝐶 ) ) )
12	5	eldifad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
13	12 9	reccld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 / 𝐶 ) ∈ ℂ )
14	2 10 5 7 8	reclimc	⊢ ( 𝜑 → ( 1 / 𝑌 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐶 ) ) lim_ℂ 𝐷 ) )
15	1 10 11 4 13 6 14	mullimc	⊢ ( 𝜑 → ( 𝑋 · ( 1 / 𝑌 ) ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 1 / 𝐶 ) ) ) lim_ℂ 𝐷 ) )
16		limccl	⊢ ( 𝐹 lim_ℂ 𝐷 ) ⊆ ℂ
17	16 6	sseldi	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
18		limccl	⊢ ( 𝐺 lim_ℂ 𝐷 ) ⊆ ℂ
19	18 7	sseldi	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
20	17 19 8	divrecd	⊢ ( 𝜑 → ( 𝑋 / 𝑌 ) = ( 𝑋 · ( 1 / 𝑌 ) ) )
21	4 12 9	divrecd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 / 𝐶 ) = ( 𝐵 · ( 1 / 𝐶 ) ) )
22	21	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 / 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 1 / 𝐶 ) ) ) )
23	3 22	syl5eq	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 1 / 𝐶 ) ) ) )
24	23	oveq1d	⊢ ( 𝜑 → ( 𝐻 lim_ℂ 𝐷 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 1 / 𝐶 ) ) ) lim_ℂ 𝐷 ) )
25	15 20 24	3eltr4d	⊢ ( 𝜑 → ( 𝑋 / 𝑌 ) ∈ ( 𝐻 lim_ℂ 𝐷 ) )

Metamath Proof Explorer

Theorem divlimc

Proof