Theorem mulrid

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	mulrid	$$⊢A\in ℂ\to A\cdot 1=A$$

Proof

Step	Hyp	Ref	Expression
1		cnre	$$⊢A\in ℂ\to \exists x\in ℝ\exists y\in ℝ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\leftrightarrow \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 ℝ\exists y\in ℝA=x+\mathrm{i}y\to A\cdot 1=A$$
25	1 24	syl	$$⊢A\in ℂ\to A\cdot 1=A$$