Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Some deductions from the field axioms for complex numbers
mullidd
Next ⟩
addcld
Metamath Proof Explorer
Ascii
Unicode
Theorem
mullidd
Description:
Identity law for multiplication.
(Contributed by
Mario Carneiro
, 27-May-2016)
Ref
Expression
Hypothesis
addcld.1
⊢
φ
→
A
∈
ℂ
Assertion
mullidd
⊢
φ
→
1
⁢
A
=
A
Proof
Step
Hyp
Ref
Expression
1
addcld.1
⊢
φ
→
A
∈
ℂ
2
mullid
⊢
A
∈
ℂ
→
1
⁢
A
=
A
3
1
2
syl
⊢
φ
→
1
⁢
A
=
A