Metamath Proof Explorer

Theorem 1sr

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

Ref Expression
Assertion 1sr 
|- 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 +P. 1P ) e. P. /\ 1P e. P. ) -> <. ( 1P +P. 1P ) , 1P >. e. ( P. X. P. ) )
5 3 1 4 mp2an 
 |-  <. ( 1P +P. 1P ) , 1P >. e. ( P. X. P. )
6 enrex 
 |-  ~R e. _V
7 6 ecelqsi 
 |-  ( <. ( 1P +P. 1P ) , 1P >. e. ( P. X. P. ) -> [ <. ( 1P +P. 1P ) , 1P >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
8 5 7 ax-mp 
 |-  [ <. ( 1P +P. 1P ) , 1P >. ] ~R e. ( ( P. X. P. ) /. ~R )
9 df-1r 
 |-  1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
10 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
11 8 9 10 3eltr4i 
 |-  1R e. R.