Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
0tie0
Next ⟩
it1ei
Metamath Proof Explorer
Ascii
Structured
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