# Metamath Proof Explorer

## Theorem mulid1

Description: The number 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion mulid1 ${⊢}{A}\in ℂ\to {A}\cdot 1={A}$

### Proof

Step Hyp Ref Expression
1 cnre ${⊢}{A}\in ℂ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}={x}+\mathrm{i}{y}$
2 recn ${⊢}{x}\in ℝ\to {x}\in ℂ$
3 ax-icn ${⊢}\mathrm{i}\in ℂ$
4 recn ${⊢}{y}\in ℝ\to {y}\in ℂ$
5 mulcl ${⊢}\left(\mathrm{i}\in ℂ\wedge {y}\in ℂ\right)\to \mathrm{i}{y}\in ℂ$
6 3 4 5 sylancr ${⊢}{y}\in ℝ\to \mathrm{i}{y}\in ℂ$
7 ax-1cn ${⊢}1\in ℂ$
8 adddir ${⊢}\left({x}\in ℂ\wedge \mathrm{i}{y}\in ℂ\wedge 1\in ℂ\right)\to \left({x}+\mathrm{i}{y}\right)\cdot 1={x}\cdot 1+\mathrm{i}{y}\cdot 1$
9 7 8 mp3an3 ${⊢}\left({x}\in ℂ\wedge \mathrm{i}{y}\in ℂ\right)\to \left({x}+\mathrm{i}{y}\right)\cdot 1={x}\cdot 1+\mathrm{i}{y}\cdot 1$
10 2 6 9 syl2an ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left({x}+\mathrm{i}{y}\right)\cdot 1={x}\cdot 1+\mathrm{i}{y}\cdot 1$
11 ax-1rid ${⊢}{x}\in ℝ\to {x}\cdot 1={x}$
12 mulass ${⊢}\left(\mathrm{i}\in ℂ\wedge {y}\in ℂ\wedge 1\in ℂ\right)\to \mathrm{i}{y}\cdot 1=\mathrm{i}{y}\cdot 1$
13 3 7 12 mp3an13 ${⊢}{y}\in ℂ\to \mathrm{i}{y}\cdot 1=\mathrm{i}{y}\cdot 1$
14 4 13 syl ${⊢}{y}\in ℝ\to \mathrm{i}{y}\cdot 1=\mathrm{i}{y}\cdot 1$
15 ax-1rid ${⊢}{y}\in ℝ\to {y}\cdot 1={y}$
16 15 oveq2d ${⊢}{y}\in ℝ\to \mathrm{i}{y}\cdot 1=\mathrm{i}{y}$
17 14 16 eqtrd ${⊢}{y}\in ℝ\to \mathrm{i}{y}\cdot 1=\mathrm{i}{y}$
18 11 17 oveqan12d ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to {x}\cdot 1+\mathrm{i}{y}\cdot 1={x}+\mathrm{i}{y}$
19 10 18 eqtrd ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left({x}+\mathrm{i}{y}\right)\cdot 1={x}+\mathrm{i}{y}$
20 oveq1 ${⊢}{A}={x}+\mathrm{i}{y}\to {A}\cdot 1=\left({x}+\mathrm{i}{y}\right)\cdot 1$
21 id ${⊢}{A}={x}+\mathrm{i}{y}\to {A}={x}+\mathrm{i}{y}$
22 20 21 eqeq12d ${⊢}{A}={x}+\mathrm{i}{y}\to \left({A}\cdot 1={A}↔\left({x}+\mathrm{i}{y}\right)\cdot 1={x}+\mathrm{i}{y}\right)$
23 19 22 syl5ibrcom ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left({A}={x}+\mathrm{i}{y}\to {A}\cdot 1={A}\right)$
24 23 rexlimivv ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}={x}+\mathrm{i}{y}\to {A}\cdot 1={A}$
25 1 24 syl ${⊢}{A}\in ℂ\to {A}\cdot 1={A}$