Metamath Proof Explorer

Theorem subadd

Description: Relationship between subtraction and addition. (Contributed by NM, 20-Jan-1997) (Revised by Mario Carneiro, 21-Dec-2013)

Ref Expression
Assertion subadd 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( B + C ) = A ) )

Proof

Step Hyp Ref Expression
1 subval 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) = ( iota_ x e. CC ( B + x ) = A ) )
2 1 eqeq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) = C <-> ( iota_ x e. CC ( B + x ) = A ) = C ) )
3 2 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( iota_ x e. CC ( B + x ) = A ) = C ) )
4 negeu 
 |-  ( ( B e. CC /\ A e. CC ) -> E! x e. CC ( 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 e. CC /\ E! x e. CC ( B + x ) = A ) -> ( ( B + C ) = A <-> ( iota_ x e. CC ( B + x ) = A ) = C ) )
8 4 7 sylan2 
 |-  ( ( C e. CC /\ ( B e. CC /\ A e. CC ) ) -> ( ( B + C ) = A <-> ( iota_ x e. CC ( B + x ) = A ) = C ) )
9 8 3impb 
 |-  ( ( C e. CC /\ B e. CC /\ A e. CC ) -> ( ( B + C ) = A <-> ( iota_ x e. CC ( B + x ) = A ) = C ) )
10 9 3com13 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B + C ) = A <-> ( iota_ x e. CC ( B + x ) = A ) = C ) )
11 3 10 bitr4d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( B + C ) = A ) )