Description: Define subtraction between real numbers. This operator saves a few axioms over df-sub in certain situations. Theorem resubval shows its value, resubadd relates it to addition, and rersubcl proves its closure. It is the restriction of df-sub to the reals: subresre . (Contributed by Steven Nguyen, 7-Jan-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | df-resub | |- -R = ( x e. RR , y e. RR |-> ( iota_ z e. RR ( y + z ) = x ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cresub | |- -R |
|
1 | vx | |- x |
|
2 | cr | |- RR |
|
3 | vy | |- y |
|
4 | vz | |- z |
|
5 | 3 | cv | |- y |
6 | caddc | |- + |
|
7 | 4 | cv | |- z |
8 | 5 7 6 | co | |- ( y + z ) |
9 | 1 | cv | |- x |
10 | 8 9 | wceq | |- ( y + z ) = x |
11 | 10 4 2 | crio | |- ( iota_ z e. RR ( y + z ) = x ) |
12 | 1 3 2 2 11 | cmpo | |- ( x e. RR , y e. RR |-> ( iota_ z e. RR ( y + z ) = x ) ) |
13 | 0 12 | wceq | |- -R = ( x e. RR , y e. RR |-> ( iota_ z e. RR ( y + z ) = x ) ) |