Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
0tie0
Next ⟩
it1ei
Metamath Proof Explorer
Ascii
Unicode
Theorem
0tie0
Description:
0 times
_i
equals 0.
(Contributed by
SN
, 25-Apr-2025)
Ref
Expression
Assertion
0tie0
⊢
0
⋅
i
=
0
Proof
Step
Hyp
Ref
Expression
1
ax-icn
⊢
i
∈
ℂ
2
0cn
⊢
0
∈
ℂ
3
it0e0
⊢
i
⋅
0
=
0
4
1
2
3
mulcomli
⊢
0
⋅
i
=
0