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

Proof

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