This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addcan

Description: Cancellation law for addition. Theorem I.1 of Apostol p. 18. (Contributed by NM, 22-Nov-1994) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

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