Metamath Proof Explorer

Theorem m1p1sr

Description: Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996) (New usage is discouraged.)

Ref Expression
Assertion m1p1sr 
|- ( -1R +R 1R ) = 0R

Proof

Step Hyp Ref Expression
1 df-m1r 
 |-  -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
2 df-1r 
 |-  1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
3 1 2 oveq12i 
 |-  ( -1R +R 1R ) = ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R +R [ <. ( 1P +P. 1P ) , 1P >. ] ~R )
4 df-0r 
 |-  0R = [ <. 1P , 1P >. ] ~R
5 1pr 
 |-  1P e. P.
6 addclpr 
 |-  ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
7 5 5 6 mp2an 
 |-  ( 1P +P. 1P ) e. P.
8 addsrpr 
 |-  ( ( ( 1P e. P. /\ ( 1P +P. 1P ) e. P. ) /\ ( ( 1P +P. 1P ) e. P. /\ 1P e. P. ) ) -> ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R +R [ <. ( 1P +P. 1P ) , 1P >. ] ~R ) = [ <. ( 1P +P. ( 1P +P. 1P ) ) , ( ( 1P +P. 1P ) +P. 1P ) >. ] ~R )
9 5 7 7 5 8 mp4an 
 |-  ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R +R [ <. ( 1P +P. 1P ) , 1P >. ] ~R ) = [ <. ( 1P +P. ( 1P +P. 1P ) ) , ( ( 1P +P. 1P ) +P. 1P ) >. ] ~R
10 addasspr 
 |-  ( ( 1P +P. 1P ) +P. 1P ) = ( 1P +P. ( 1P +P. 1P ) )
11 10 oveq2i 
 |-  ( 1P +P. ( ( 1P +P. 1P ) +P. 1P ) ) = ( 1P +P. ( 1P +P. ( 1P +P. 1P ) ) )
12 addclpr 
 |-  ( ( 1P e. P. /\ ( 1P +P. 1P ) e. P. ) -> ( 1P +P. ( 1P +P. 1P ) ) e. P. )
13 5 7 12 mp2an 
 |-  ( 1P +P. ( 1P +P. 1P ) ) e. P.
14 addclpr 
 |-  ( ( ( 1P +P. 1P ) e. P. /\ 1P e. P. ) -> ( ( 1P +P. 1P ) +P. 1P ) e. P. )
15 7 5 14 mp2an 
 |-  ( ( 1P +P. 1P ) +P. 1P ) e. P.
16 enreceq 
 |-  ( ( ( 1P e. P. /\ 1P e. P. ) /\ ( ( 1P +P. ( 1P +P. 1P ) ) e. P. /\ ( ( 1P +P. 1P ) +P. 1P ) e. P. ) ) -> ( [ <. 1P , 1P >. ] ~R = [ <. ( 1P +P. ( 1P +P. 1P ) ) , ( ( 1P +P. 1P ) +P. 1P ) >. ] ~R <-> ( 1P +P. ( ( 1P +P. 1P ) +P. 1P ) ) = ( 1P +P. ( 1P +P. ( 1P +P. 1P ) ) ) ) )
17 5 5 13 15 16 mp4an 
 |-  ( [ <. 1P , 1P >. ] ~R = [ <. ( 1P +P. ( 1P +P. 1P ) ) , ( ( 1P +P. 1P ) +P. 1P ) >. ] ~R <-> ( 1P +P. ( ( 1P +P. 1P ) +P. 1P ) ) = ( 1P +P. ( 1P +P. ( 1P +P. 1P ) ) ) )
18 11 17 mpbir 
 |-  [ <. 1P , 1P >. ] ~R = [ <. ( 1P +P. ( 1P +P. 1P ) ) , ( ( 1P +P. 1P ) +P. 1P ) >. ] ~R
19 9 18 eqtr4i 
 |-  ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R +R [ <. ( 1P +P. 1P ) , 1P >. ] ~R ) = [ <. 1P , 1P >. ] ~R
20 4 19 eqtr4i 
 |-  0R = ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R +R [ <. ( 1P +P. 1P ) , 1P >. ] ~R )
21 3 20 eqtr4i 
 |-  ( -1R +R 1R ) = 0R