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

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opex 4395 . 2
2 opex 4395 . 2
3 opex 4395 . 2
4 enrex 8909 . 2
5 enrer 8907 . 2
6 df-enr 8898 . 2
7 oveq12 6057 . . . 4
8 oveq12 6057 . . . 4
97, 8eqeqan12d 2427 . . 3
109an42s 801 . 2
11 oveq12 6057 . . . 4
12 oveq12 6057 . . . 4
1311, 12eqeqan12d 2427 . . 3
1413an42s 801 . 2
15 df-plpr 8896 . 2
16 oveq12 6057 . . . 4
17 oveq12 6057 . . . 4
18 opeq12 3954 . . . 4
1916, 17, 18syl2an 464 . . 3
2019an4s 800 . 2
21 oveq12 6057 . . . 4
22 oveq12 6057 . . . 4
23 opeq12 3954 . . . 4
2421, 22, 23syl2an 464 . . 3
2524an4s 800 . 2
26 oveq12 6057 . . . 4
27 oveq12 6057 . . . 4
28 opeq12 3954 . . . 4
2926, 27, 28syl2an 464 . . 3
3029an4s 800 . 2
31 df-plr 8900 . 2
32 df-nr 8899 . 2