Description: Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013) (Proof shortened by Mario Carneiro, 27-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | subadd2 | |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( C + B ) = A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | subadd | |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( B + C ) = A ) ) |
|
| 2 | simp2 | |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC ) |
|
| 3 | simp3 | |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC ) |
|
| 4 | 2 3 | addcomd | |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B + C ) = ( C + B ) ) |
| 5 | 4 | eqeq1d | |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B + C ) = A <-> ( C + B ) = A ) ) |
| 6 | 1 5 | bitrd | |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( C + B ) = A ) ) |