sublimc

Description: Subtraction of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	sublimc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	sublimc.2	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
	sublimc.3	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) )
	sublimc.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	sublimc.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
	sublimc.6	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 lim_ℂ 𝐷 ) )
	sublimc.7	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐺 lim_ℂ 𝐷 ) )
Assertion	sublimc	⊢ ( 𝜑 → ( 𝐸 − 𝐼 ) ∈ ( 𝐻 lim_ℂ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		sublimc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		sublimc.2	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
3		sublimc.3	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) )
4		sublimc.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5		sublimc.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
6		sublimc.6	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 lim_ℂ 𝐷 ) )
7		sublimc.7	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐺 lim_ℂ 𝐷 ) )
8		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ - 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ - 𝐶 )
9		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) )
10	5	negcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ∈ ℂ )
11	2 8 5 7	neglimc	⊢ ( 𝜑 → - 𝐼 ∈ ( ( 𝑥 ∈ 𝐴 ↦ - 𝐶 ) lim_ℂ 𝐷 ) )
12	1 8 9 4 10 6 11	addlimc	⊢ ( 𝜑 → ( 𝐸 + - 𝐼 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) lim_ℂ 𝐷 ) )
13		limccl	⊢ ( 𝐹 lim_ℂ 𝐷 ) ⊆ ℂ
14	13 6	sselid	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
15		limccl	⊢ ( 𝐺 lim_ℂ 𝐷 ) ⊆ ℂ
16	15 7	sselid	⊢ ( 𝜑 → 𝐼 ∈ ℂ )
17	14 16	negsubd	⊢ ( 𝜑 → ( 𝐸 + - 𝐼 ) = ( 𝐸 − 𝐼 ) )
18	17	eqcomd	⊢ ( 𝜑 → ( 𝐸 − 𝐼 ) = ( 𝐸 + - 𝐼 ) )
19	4 5	negsubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
20	19	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 − 𝐶 ) = ( 𝐵 + - 𝐶 ) )
21	20	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) )
22	3 21	syl5eq	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) )
23	22	oveq1d	⊢ ( 𝜑 → ( 𝐻 lim_ℂ 𝐷 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) lim_ℂ 𝐷 ) )
24	12 18 23	3eltr4d	⊢ ( 𝜑 → ( 𝐸 − 𝐼 ) ∈ ( 𝐻 lim_ℂ 𝐷 ) )

Metamath Proof Explorer

Theorem sublimc

Proof