Metamath Proof Explorer


Theorem reladdrsub

Description: Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023)

Ref Expression
Hypotheses reladdrsub.1
|- ( ph -> A e. RR )
reladdrsub.2
|- ( ph -> B e. RR )
reladdrsub.3
|- ( ph -> ( A + B ) = C )
Assertion reladdrsub
|- ( ph -> B = ( C -R A ) )

Proof

Step Hyp Ref Expression
1 reladdrsub.1
 |-  ( ph -> A e. RR )
2 reladdrsub.2
 |-  ( ph -> B e. RR )
3 reladdrsub.3
 |-  ( ph -> ( A + B ) = C )
4 1 2 readdcld
 |-  ( ph -> ( A + B ) e. RR )
5 3 4 eqeltrrd
 |-  ( ph -> C e. RR )
6 resubadd
 |-  ( ( C e. RR /\ A e. RR /\ B e. RR ) -> ( ( C -R A ) = B <-> ( A + B ) = C ) )
7 3 6 syl5ibrcom
 |-  ( ph -> ( ( C e. RR /\ A e. RR /\ B e. RR ) -> ( C -R A ) = B ) )
8 5 1 2 7 mp3and
 |-  ( ph -> ( C -R A ) = B )
9 8 eqcomd
 |-  ( ph -> B = ( C -R A ) )