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

Metamath Proof Explorer

Theorem negeu

Description: Existential uniqueness of negatives. Theorem I.2 of Apostol p. 18. (Contributed by NM, 22-Nov-1994) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion negeu 
|- ( ( A e. CC /\ B e. CC ) -> E! x e. CC ( A + x ) = B )

Proof

Step Hyp Ref Expression
1 cnegex 
 |-  ( A e. CC -> E. y e. CC ( A + y ) = 0 )
2 1 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> E. y e. CC ( A + y ) = 0 )
3 simpl 
 |-  ( ( y e. CC /\ ( A + y ) = 0 ) -> y e. CC )
4 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
5 addcl 
 |-  ( ( y e. CC /\ B e. CC ) -> ( y + B ) e. CC )
6 3 4 5 syl2anr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) -> ( y + B ) e. CC )
7 simplrr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( A + y ) = 0 )
8 7 oveq1d 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( ( A + y ) + B ) = ( 0 + B ) )
9 simplll 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> A e. CC )
10 simplrl 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> y e. CC )
11 simpllr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> B e. CC )
12 9 10 11 addassd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( ( A + y ) + B ) = ( A + ( y + B ) ) )
13 11 addlidd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( 0 + B ) = B )
14 8 12 13 3eqtr3rd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> B = ( A + ( y + B ) ) )
15 14 eqeq2d 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( ( A + x ) = B <-> ( A + x ) = ( A + ( y + B ) ) ) )
16 simpr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> x e. CC )
17 10 11 addcld 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( y + B ) e. CC )
18 9 16 17 addcand 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( ( A + x ) = ( A + ( y + B ) ) <-> x = ( y + B ) ) )
19 15 18 bitrd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( ( A + x ) = B <-> x = ( y + B ) ) )
20 19 ralrimiva 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) -> A. x e. CC ( ( A + x ) = B <-> x = ( y + B ) ) )
21 reu6i 
 |-  ( ( ( y + B ) e. CC /\ A. x e. CC ( ( A + x ) = B <-> x = ( y + B ) ) ) -> E! x e. CC ( A + x ) = B )
22 6 20 21 syl2anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) -> E! x e. CC ( A + x ) = B )
23 2 22 rexlimddv 
 |-  ( ( A e. CC /\ B e. CC ) -> E! x e. CC ( A + x ) = B )