Metamath Proof Explorer


Theorem resubadd

Description: Relation between real subtraction and addition. Based on subadd . (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion resubadd A B C A - B = C B + C = A

Proof

Step Hyp Ref Expression
1 resubval A B A - B = ι x | B + x = A
2 1 eqeq1d A B A - B = C ι x | B + x = A = C
3 2 3adant3 A B C A - B = C ι x | B + x = A = C
4 resubeu B A ∃! x B + x = A
5 oveq2 x = C B + x = B + C
6 5 eqeq1d x = C B + x = A B + C = A
7 6 riota2 C ∃! x B + x = A B + C = A ι x | B + x = A = C
8 4 7 sylan2 C B A B + C = A ι x | B + x = A = C
9 8 3impb C B A B + C = A ι x | B + x = A = C
10 9 3com13 A B C B + C = A ι x | B + x = A = C
11 3 10 bitr4d A B C A - B = C B + C = A