Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
1tiei
Next ⟩
itrere
Metamath Proof Explorer
Ascii
Unicode
Theorem
1tiei
Description:
1 times
_i
equals
_i
.
(Contributed by
SN
, 25-Apr-2025)
Ref
Expression
Assertion
1tiei
⊢
1
⁢
i
=
i
Proof
Step
Hyp
Ref
Expression
1
ax-icn
⊢
i
∈
ℂ
2
1
mullidi
⊢
1
⁢
i
=
i