Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
subresre
Next ⟩
addinvcom
Metamath Proof Explorer
Ascii
Unicode
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