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
|- ( ph -> A e. RR )
readdrcl2d.b
|- ( ph -> B e. CC )
readdrcl2d.c
|- ( ph -> ( A + B ) e. RR )
Assertion readdrcl2d
|- ( ph -> B e. RR )

Proof

Step Hyp Ref Expression
1 readdrcl2d.a
 |-  ( ph -> A e. RR )
2 readdrcl2d.b
 |-  ( ph -> B e. CC )
3 readdrcl2d.c
 |-  ( ph -> ( A + B ) e. RR )
4 1 recnd
 |-  ( ph -> A e. CC )
5 4 2 pncan2d
 |-  ( ph -> ( ( A + B ) - A ) = B )
6 3 1 resubcld
 |-  ( ph -> ( ( A + B ) - A ) e. RR )
7 5 6 eqeltrrd
 |-  ( ph -> B e. RR )