Metamath Proof Explorer


Theorem subresre

Description: Subtraction restricted to the reals. (Contributed by SN, 5-May-2024)

Ref Expression
Assertion subresre - = 2

Proof

Step Hyp Ref Expression
1 resubeqsub x y x - y = x y
2 1 3adant1 x y x - y = x y
3 ax-resscn
4 3 a1i
5 resubf - : 2
6 5 a1i - : 2
7 sn-subf : ×
8 7 a1i : ×
9 2 4 6 8 oprres - = 2
10 9 mptru - = 2