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 φ A
readdrcl2d.b φ B
readdrcl2d.c φ A + B
Assertion readdrcl2d φ B

Proof

Step Hyp Ref Expression
1 readdrcl2d.a φ A
2 readdrcl2d.b φ B
3 readdrcl2d.c φ A + B
4 1 recnd φ A
5 4 2 pncan2d φ A + B - A = B
6 3 1 resubcld φ A + B - A
7 5 6 eqeltrrd φ B