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

Metamath Proof Explorer

Theorem axrnegex

Description: Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rnegex . (Contributed by NM, 15-May-1996) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 elreal2 
 |-  ( A e. RR <-> ( ( 1st ` A ) e. R. /\ A = <. ( 1st ` A ) , 0R >. ) )
2 1 simplbi 
 |-  ( A e. RR -> ( 1st ` A ) e. R. )
3 m1r 
 |-  -1R e. R.
4 mulclsr 
 |-  ( ( ( 1st ` A ) e. R. /\ -1R e. R. ) -> ( ( 1st ` A ) .R -1R ) e. R. )
5 2 3 4 sylancl 
 |-  ( A e. RR -> ( ( 1st ` A ) .R -1R ) e. R. )
6 opelreal 
 |-  ( <. ( ( 1st ` A ) .R -1R ) , 0R >. e. RR <-> ( ( 1st ` A ) .R -1R ) e. R. )
7 5 6 sylibr 
 |-  ( A e. RR -> <. ( ( 1st ` A ) .R -1R ) , 0R >. e. RR )
8 1 simprbi 
 |-  ( A e. RR -> A = <. ( 1st ` A ) , 0R >. )
9 8 oveq1d 
 |-  ( A e. RR -> ( A + <. ( ( 1st ` A ) .R -1R ) , 0R >. ) = ( <. ( 1st ` A ) , 0R >. + <. ( ( 1st ` A ) .R -1R ) , 0R >. ) )
10 addresr 
 |-  ( ( ( 1st ` A ) e. R. /\ ( ( 1st ` A ) .R -1R ) e. R. ) -> ( <. ( 1st ` A ) , 0R >. + <. ( ( 1st ` A ) .R -1R ) , 0R >. ) = <. ( ( 1st ` A ) +R ( ( 1st ` A ) .R -1R ) ) , 0R >. )
11 2 5 10 syl2anc 
 |-  ( A e. RR -> ( <. ( 1st ` A ) , 0R >. + <. ( ( 1st ` A ) .R -1R ) , 0R >. ) = <. ( ( 1st ` A ) +R ( ( 1st ` A ) .R -1R ) ) , 0R >. )
12 pn0sr 
 |-  ( ( 1st ` A ) e. R. -> ( ( 1st ` A ) +R ( ( 1st ` A ) .R -1R ) ) = 0R )
13 12 opeq1d 
 |-  ( ( 1st ` A ) e. R. -> <. ( ( 1st ` A ) +R ( ( 1st ` A ) .R -1R ) ) , 0R >. = <. 0R , 0R >. )
14 df-0 
 |-  0 = <. 0R , 0R >.
15 13 14 eqtr4di 
 |-  ( ( 1st ` A ) e. R. -> <. ( ( 1st ` A ) +R ( ( 1st ` A ) .R -1R ) ) , 0R >. = 0 )
16 2 15 syl 
 |-  ( A e. RR -> <. ( ( 1st ` A ) +R ( ( 1st ` A ) .R -1R ) ) , 0R >. = 0 )
17 9 11 16 3eqtrd 
 |-  ( A e. RR -> ( A + <. ( ( 1st ` A ) .R -1R ) , 0R >. ) = 0 )
18 oveq2 
 |-  ( x = <. ( ( 1st ` A ) .R -1R ) , 0R >. -> ( A + x ) = ( A + <. ( ( 1st ` A ) .R -1R ) , 0R >. ) )
19 18 eqeq1d 
 |-  ( x = <. ( ( 1st ` A ) .R -1R ) , 0R >. -> ( ( A + x ) = 0 <-> ( A + <. ( ( 1st ` A ) .R -1R ) , 0R >. ) = 0 ) )
20 19 rspcev 
 |-  ( ( <. ( ( 1st ` A ) .R -1R ) , 0R >. e. RR /\ ( A + <. ( ( 1st ` A ) .R -1R ) , 0R >. ) = 0 ) -> E. x e. RR ( A + x ) = 0 )
21 7 17 20 syl2anc 
 |-  ( A e. RR -> E. x e. RR ( A + x ) = 0 )