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	$⊢ φ \to A \in ℝ$
	readdrcl2d.b	$⊢ φ \to B \in ℂ$
	readdrcl2d.c	$⊢ φ \to A + B \in ℝ$
Assertion	readdrcl2d	$⊢ φ \to B \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		readdrcl2d.a	$⊢ φ \to A \in ℝ$
2		readdrcl2d.b	$⊢ φ \to B \in ℂ$
3		readdrcl2d.c	$⊢ φ \to A + B \in ℝ$
4	1	recnd	$⊢ φ \to A \in ℂ$
5	4 2	pncan2d	$⊢ φ \to A + B - A = B$
6	3 1	resubcld	$⊢ φ \to A + B - A \in ℝ$
7	5 6	eqeltrrd	$⊢ φ \to B \in ℝ$