Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
it1ei
Next ⟩
1tiei
Metamath Proof Explorer
Unicode
Structured
Theorem
it1ei
Description:
_i
times 1 equals
_i
.
(Contributed by
SN
, 25-Apr-2025)
Ref
Expression
Assertion
it1ei
|- ( _i x. 1 ) = _i
Proof
Step
Hyp
Ref
Expression
1
ax-icn
|- _i e. CC
2
1
mulridi
|- ( _i x. 1 ) = _i