Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  addsrpr Unicode version

 Description: Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.)
Assertion
Ref Expression

StepHypRef Expression
1 opex 4130 . 2
2 opex 4130 . 2
3 opex 4130 . 2
4 enrex 8572 . 2
5 enrer 8570 . 2
6 df-enr 8561 . 2
7 oveq12 5719 . . . 4
8 oveq12 5719 . . . 4
97, 8eqeqan12d 2268 . . 3
109an42s 803 . 2
11 oveq12 5719 . . . 4
12 oveq12 5719 . . . 4
1311, 12eqeqan12d 2268 . . 3
1413an42s 803 . 2
15 df-plpr 8559 . 2
16 oveq12 5719 . . . 4
17 oveq12 5719 . . . 4
18 opeq12 3698 . . . 4
1916, 17, 18syl2an 465 . . 3
2019an4s 802 . 2
21 oveq12 5719 . . . 4
22 oveq12 5719 . . . 4
23 opeq12 3698 . . . 4
2421, 22, 23syl2an 465 . . 3
2524an4s 802 . 2
26 oveq12 5719 . . . 4
27 oveq12 5719 . . . 4
28 opeq12 3698 . . . 4
2926, 27, 28syl2an 465 . . 3
3029an4s 802 . 2
31 df-plr 8563 . 2
32 df-nr 8562 . 2