Metamath Proof Explorer

Theorem addresr

Description: Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996) (New usage is discouraged.)

Ref Expression
Assertion addresr 
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , 0R >. )

Proof

Step Hyp Ref Expression
1 0r 
 |-  0R e. R.
2 addcnsr 
 |-  ( ( ( A e. R. /\ 0R e. R. ) /\ ( B e. R. /\ 0R e. R. ) ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , ( 0R +R 0R ) >. )
3 2 an4s 
 |-  ( ( ( A e. R. /\ B e. R. ) /\ ( 0R e. R. /\ 0R e. R. ) ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , ( 0R +R 0R ) >. )
4 1 1 3 mpanr12 
 |-  ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , ( 0R +R 0R ) >. )
5 0idsr 
 |-  ( 0R e. R. -> ( 0R +R 0R ) = 0R )
6 1 5 ax-mp 
 |-  ( 0R +R 0R ) = 0R
7 6 opeq2i 
 |-  <. ( A +R B ) , ( 0R +R 0R ) >. = <. ( A +R B ) , 0R >.
8 4 7 syl6eq 
 |-  ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , 0R >. )