This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem readdrcl2d

Description: Reverse closure for addition: the second addend is real if the first addend is real and the sum is real. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypotheses	readdrcl2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	readdrcl2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	readdrcl2d.c	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
Assertion	readdrcl2d	⊢ ( 𝜑 → 𝐵 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		readdrcl2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		readdrcl2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		readdrcl2d.c	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
4	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
5	4 2	pncan2d	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − 𝐴 ) = 𝐵 )
6	3 1	resubcld	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − 𝐴 ) ∈ ℝ )
7	5 6	eqeltrrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ )