Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
rei4
Next ⟩
sn-addid0
Metamath Proof Explorer
Ascii
Unicode
Theorem
rei4
Description:
i4
without
ax-mulcom
.
(Contributed by
SN
, 27-May-2024)
Ref
Expression
Assertion
rei4
⊢
i
⁢
i
⁢
i
⁢
i
=
1
Proof
Step
Hyp
Ref
Expression
1
reixi
⊢
i
⁢
i
=
0
-
ℝ
1
2
1
1
oveq12i
⊢
i
⁢
i
⁢
i
⁢
i
=
0
-
ℝ
1
⁢
0
-
ℝ
1
3
1re
⊢
1
∈
ℝ
4
rernegcl
⊢
1
∈
ℝ
→
0
-
ℝ
1
∈
ℝ
5
1red
⊢
1
∈
ℝ
→
1
∈
ℝ
6
4
5
remulneg2d
⊢
1
∈
ℝ
→
0
-
ℝ
1
⁢
0
-
ℝ
1
=
0
-
ℝ
0
-
ℝ
1
⋅
1
7
ax-1rid
⊢
0
-
ℝ
1
∈
ℝ
→
0
-
ℝ
1
⋅
1
=
0
-
ℝ
1
8
4
7
syl
⊢
1
∈
ℝ
→
0
-
ℝ
1
⋅
1
=
0
-
ℝ
1
9
8
oveq2d
⊢
1
∈
ℝ
→
0
-
ℝ
0
-
ℝ
1
⋅
1
=
0
-
ℝ
0
-
ℝ
1
10
renegneg
⊢
1
∈
ℝ
→
0
-
ℝ
0
-
ℝ
1
=
1
11
6
9
10
3eqtrd
⊢
1
∈
ℝ
→
0
-
ℝ
1
⁢
0
-
ℝ
1
=
1
12
3
11
ax-mp
⊢
0
-
ℝ
1
⁢
0
-
ℝ
1
=
1
13
2
12
eqtri
⊢
i
⁢
i
⁢
i
⁢
i
=
1