Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
sn-1ticom
Next ⟩
sn-mulid2
Metamath Proof Explorer
Ascii
Unicode
Theorem
sn-1ticom
Description:
Lemma for
sn-mulid2
and
it1ei
.
(Contributed by
SN
, 27-May-2024)
Ref
Expression
Assertion
sn-1ticom
⊢
1
⁢
i
=
i
⋅
1
Proof
Step
Hyp
Ref
Expression
1
ax-icn
⊢
i
∈
ℂ
2
1
1
mulcli
⊢
i
⁢
i
∈
ℂ
3
2
2
1
mulassi
⊢
i
⁢
i
⁢
i
⁢
i
⁢
i
=
i
⁢
i
⁢
i
⁢
i
⁢
i
4
1
2
mulcli
⊢
i
⁢
i
⁢
i
∈
ℂ
5
1
1
4
mulassi
⊢
i
⁢
i
⁢
i
⁢
i
⁢
i
=
i
⁢
i
⁢
i
⁢
i
⁢
i
6
1
1
1
mulassi
⊢
i
⁢
i
⁢
i
=
i
⁢
i
⁢
i
7
6
oveq2i
⊢
i
⁢
i
⁢
i
⁢
i
⁢
i
=
i
⁢
i
⁢
i
⁢
i
⁢
i
8
1
1
2
mulassi
⊢
i
⁢
i
⁢
i
⁢
i
=
i
⁢
i
⁢
i
⁢
i
9
8
oveq2i
⊢
i
⁢
i
⁢
i
⁢
i
⁢
i
=
i
⁢
i
⁢
i
⁢
i
⁢
i
10
5
7
9
3eqtr4i
⊢
i
⁢
i
⁢
i
⁢
i
⁢
i
=
i
⁢
i
⁢
i
⁢
i
⁢
i
11
3
10
eqtri
⊢
i
⁢
i
⁢
i
⁢
i
⁢
i
=
i
⁢
i
⁢
i
⁢
i
⁢
i
12
rei4
⊢
i
⁢
i
⁢
i
⁢
i
=
1
13
12
oveq1i
⊢
i
⁢
i
⁢
i
⁢
i
⁢
i
=
1
⁢
i
14
12
oveq2i
⊢
i
⁢
i
⁢
i
⁢
i
⁢
i
=
i
⋅
1
15
11
13
14
3eqtr3i
⊢
1
⁢
i
=
i
⋅
1