Metamath Proof Explorer

Theorem cnegex2

Description: Existence of a left inverse for addition. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion cnegex2 
|- ( A e. CC -> E. x e. CC ( x + A ) = 0 )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 1 1 mulcli 
 |-  ( _i x. _i ) e. CC
3 mulcl 
 |-  ( ( ( _i x. _i ) e. CC /\ A e. CC ) -> ( ( _i x. _i ) x. A ) e. CC )
4 2 3 mpan 
 |-  ( A e. CC -> ( ( _i x. _i ) x. A ) e. CC )
5 mullid 
 |-  ( A e. CC -> ( 1 x. A ) = A )
6 5 oveq2d 
 |-  ( A e. CC -> ( ( ( _i x. _i ) x. A ) + ( 1 x. A ) ) = ( ( ( _i x. _i ) x. A ) + A ) )
7 ax-i2m1 
 |-  ( ( _i x. _i ) + 1 ) = 0
8 7 oveq1i 
 |-  ( ( ( _i x. _i ) + 1 ) x. A ) = ( 0 x. A )
9 ax-1cn 
 |-  1 e. CC
10 adddir 
 |-  ( ( ( _i x. _i ) e. CC /\ 1 e. CC /\ A e. CC ) -> ( ( ( _i x. _i ) + 1 ) x. A ) = ( ( ( _i x. _i ) x. A ) + ( 1 x. A ) ) )
11 2 9 10 mp3an12 
 |-  ( A e. CC -> ( ( ( _i x. _i ) + 1 ) x. A ) = ( ( ( _i x. _i ) x. A ) + ( 1 x. A ) ) )
12 mul02 
 |-  ( A e. CC -> ( 0 x. A ) = 0 )
13 8 11 12 3eqtr3a 
 |-  ( A e. CC -> ( ( ( _i x. _i ) x. A ) + ( 1 x. A ) ) = 0 )
14 6 13 eqtr3d 
 |-  ( A e. CC -> ( ( ( _i x. _i ) x. A ) + A ) = 0 )
15 oveq1 
 |-  ( x = ( ( _i x. _i ) x. A ) -> ( x + A ) = ( ( ( _i x. _i ) x. A ) + A ) )
16 15 eqeq1d 
 |-  ( x = ( ( _i x. _i ) x. A ) -> ( ( x + A ) = 0 <-> ( ( ( _i x. _i ) x. A ) + A ) = 0 ) )
17 16 rspcev 
 |-  ( ( ( ( _i x. _i ) x. A ) e. CC /\ ( ( ( _i x. _i ) x. A ) + A ) = 0 ) -> E. x e. CC ( x + A ) = 0 )
18 4 14 17 syl2anc 
 |-  ( A e. CC -> E. x e. CC ( x + A ) = 0 )