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 ) ) |
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 ) ) |