Metamath Proof Explorer

Theorem 0lt1sr

Description: 0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion 0lt1sr 
|- 0R

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 ltaddpr 
 |-  ( ( ( 1P +P. 1P ) e. P. /\ 1P e. P. ) -> ( 1P +P. 1P )
5 3 1 4 mp2an 
 |-  ( 1P +P. 1P )
6 addcompr 
 |-  ( 1P +P. ( 1P +P. 1P ) ) = ( ( 1P +P. 1P ) +P. 1P )
7 5 6 breqtrri 
 |-  ( 1P +P. 1P )
8 ltsrpr 
 |-  ( [ <. 1P , 1P >. ] ~R . ] ~R <-> ( 1P +P. 1P )
9 7 8 mpbir 
 |-  [ <. 1P , 1P >. ] ~R . ] ~R
10 df-0r 
 |-  0R = [ <. 1P , 1P >. ] ~R
11 df-1r 
 |-  1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
12 9 10 11 3brtr4i 
 |-  0R