Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  addsrpr Structured version   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

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opex 4462 . 2
2 opex 4462 . 2
3 opex 4462 . 2
4 enrex 8983 . 2
5 enrer 8981 . 2
6 df-enr 8972 . 2
7 oveq12 6126 . . . 4
8 oveq12 6126 . . . 4
97, 8eqeqan12d 2458 . . 3
109an42s 802 . 2
11 oveq12 6126 . . . 4
12 oveq12 6126 . . . 4
1311, 12eqeqan12d 2458 . . 3
1413an42s 802 . 2
15 df-plpr 8970 . 2
16 oveq12 6126 . . . 4
17 oveq12 6126 . . . 4
18 opeq12 4015 . . . 4
1916, 17, 18syl2an 465 . . 3
2019an4s 801 . 2
21 oveq12 6126 . . . 4
22 oveq12 6126 . . . 4
23 opeq12 4015 . . . 4
2421, 22, 23syl2an 465 . . 3
2524an4s 801 . 2
26 oveq12 6126 . . . 4
27 oveq12 6126 . . . 4
28 opeq12 4015 . . . 4
2926, 27, 28syl2an 465 . . 3
3029an4s 801 . 2
31 df-plr 8974 . 2
32 df-nr 8973 . 2