Metamath Proof Explorer

Theorem m1r

Description: The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion m1r 
|- -1R e. R.

Proof

Step Hyp Ref Expression
1 1pr 
 |-  1P e. P.
2 addclpr 
 |-  ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
3 1 1 2 mp2an 
 |-  ( 1P +P. 1P ) e. P.
4 opelxpi 
 |-  ( ( 1P e. P. /\ ( 1P +P. 1P ) e. P. ) -> <. 1P , ( 1P +P. 1P ) >. e. ( P. X. P. ) )
5 1 3 4 mp2an 
 |-  <. 1P , ( 1P +P. 1P ) >. e. ( P. X. P. )
6 enrex 
 |-  ~R e. _V
7 6 ecelqsi 
 |-  ( <. 1P , ( 1P +P. 1P ) >. e. ( P. X. P. ) -> [ <. 1P , ( 1P +P. 1P ) >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
8 5 7 ax-mp 
 |-  [ <. 1P , ( 1P +P. 1P ) >. ] ~R e. ( ( P. X. P. ) /. ~R )
9 df-m1r 
 |-  -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
10 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
11 8 9 10 3eltr4i 
 |-  -1R e. R.