Description: 0 times _i equals 0. (Contributed by SN, 25-Apr-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | 0tie0 | |- ( 0 x. _i ) = 0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-icn | |- _i e. CC |
|
2 | 0cn | |- 0 e. CC |
|
3 | it0e0 | |- ( _i x. 0 ) = 0 |
|
4 | 1 2 3 | mulcomli | |- ( 0 x. _i ) = 0 |