Metamath Proof Explorer

Theorem addcan2

Description: Cancellation law for addition. (Contributed by NM, 30-Jul-2004) (Revised by Scott Fenton, 3-Jan-2013)

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

Proof

Step Hyp Ref Expression
1 cnegex 
 |-  ( C e. CC -> E. x e. CC ( C + x ) = 0 )
2 1 3ad2ant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> E. x e. CC ( C + x ) = 0 )
3 oveq1 
 |-  ( ( A + C ) = ( B + C ) -> ( ( A + C ) + x ) = ( ( B + C ) + x ) )
4 simpl1 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> A e. CC )
5 simpl3 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> C e. CC )
6 simprl 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> x e. CC )
7 4 5 6 addassd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( ( A + C ) + x ) = ( A + ( C + x ) ) )
8 simprr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( C + x ) = 0 )
9 8 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( A + ( C + x ) ) = ( A + 0 ) )
10 addrid 
 |-  ( A e. CC -> ( A + 0 ) = A )
11 4 10 syl 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( A + 0 ) = A )
12 7 9 11 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( ( A + C ) + x ) = A )
13 simpl2 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> B e. CC )
14 13 5 6 addassd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( ( B + C ) + x ) = ( B + ( C + x ) ) )
15 8 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( B + ( C + x ) ) = ( B + 0 ) )
16 addrid 
 |-  ( B e. CC -> ( B + 0 ) = B )
17 13 16 syl 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( B + 0 ) = B )
18 14 15 17 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( ( B + C ) + x ) = B )
19 12 18 eqeq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( ( ( A + C ) + x ) = ( ( B + C ) + x ) <-> A = B ) )
20 3 19 imbitrid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( ( A + C ) = ( B + C ) -> A = B ) )
21 oveq1 
 |-  ( A = B -> ( A + C ) = ( B + C ) )
22 20 21 impbid1 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( x e. CC /\ ( C + x ) = 0 ) ) -> ( ( A + C ) = ( B + C ) <-> A = B ) )
23 2 22 rexlimddv 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) = ( B + C ) <-> A = B ) )