Metamath Proof Explorer

Theorem addid2

Description: 0 is a left identity for addition. This used to be one of our complex number axioms, until it was discovered that it was dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion addid2 
|- ( A e. CC -> ( 0 + A ) = A )

Proof

Step Hyp Ref Expression
1 cnegex 
 |-  ( A e. CC -> E. x e. CC ( A + x ) = 0 )
2 cnegex 
 |-  ( x e. CC -> E. y e. CC ( x + y ) = 0 )
3 2 ad2antrl 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) ) -> E. y e. CC ( x + y ) = 0 )
4 0cn 
 |-  0 e. CC
5 addass 
 |-  ( ( 0 e. CC /\ 0 e. CC /\ y e. CC ) -> ( ( 0 + 0 ) + y ) = ( 0 + ( 0 + y ) ) )
6 4 4 5 mp3an12 
 |-  ( y e. CC -> ( ( 0 + 0 ) + y ) = ( 0 + ( 0 + y ) ) )
7 6 adantr 
 |-  ( ( y e. CC /\ ( x + y ) = 0 ) -> ( ( 0 + 0 ) + y ) = ( 0 + ( 0 + y ) ) )
8 7 3ad2ant3 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( ( 0 + 0 ) + y ) = ( 0 + ( 0 + y ) ) )
9 00id 
 |-  ( 0 + 0 ) = 0
10 9 oveq1i 
 |-  ( ( 0 + 0 ) + y ) = ( 0 + y )
11 simp1 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> A e. CC )
12 simp2l 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> x e. CC )
13 simp3l 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> y e. CC )
14 11 12 13 addassd 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( ( A + x ) + y ) = ( A + ( x + y ) ) )
15 simp2r 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( A + x ) = 0 )
16 15 oveq1d 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( ( A + x ) + y ) = ( 0 + y ) )
17 simp3r 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( x + y ) = 0 )
18 17 oveq2d 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( A + ( x + y ) ) = ( A + 0 ) )
19 14 16 18 3eqtr3rd 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( A + 0 ) = ( 0 + y ) )
20 addid1 
 |-  ( A e. CC -> ( A + 0 ) = A )
21 20 3ad2ant1 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( A + 0 ) = A )
22 19 21 eqtr3d 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( 0 + y ) = A )
23 10 22 eqtrid 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( ( 0 + 0 ) + y ) = A )
24 22 oveq2d 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( 0 + ( 0 + y ) ) = ( 0 + A ) )
25 8 23 24 3eqtr3rd 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) /\ ( y e. CC /\ ( x + y ) = 0 ) ) -> ( 0 + A ) = A )
26 25 3expia 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) ) -> ( ( y e. CC /\ ( x + y ) = 0 ) -> ( 0 + A ) = A ) )
27 26 expd 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) ) -> ( y e. CC -> ( ( x + y ) = 0 -> ( 0 + A ) = A ) ) )
28 27 rexlimdv 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) ) -> ( E. y e. CC ( x + y ) = 0 -> ( 0 + A ) = A ) )
29 3 28 mpd 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( A + x ) = 0 ) ) -> ( 0 + A ) = A )
30 1 29 rexlimddv 
 |-  ( A e. CC -> ( 0 + A ) = A )