Theorem creur

Description: The real part of a complex number is unique. Proposition 10-1.3 of Gleason p. 130. (Contributed by NM, 9-May-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	creur	$$⊢A\in ℂ\to \exists !x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$

Proof

Step	Hyp	Ref	Expression
1		cnre	$$⊢A\in ℂ\to \exists z\in ℝ\exists w\in ℝA=z+\mathrm{i}w$$
2		cru	$$⊢\left(\left(x\in ℝ\wedge y\in ℝ\right)\wedge \left(z\in ℝ\wedge w\in ℝ\right)\right)\to \left(x+\mathrm{i}y=z+\mathrm{i}w\leftrightarrow \left(x=z\wedge y=w\right)\right)$$
3	2	ancoms	$$⊢\left(\left(z\in ℝ\wedge w\in ℝ\right)\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \left(x+\mathrm{i}y=z+\mathrm{i}w\leftrightarrow \left(x=z\wedge y=w\right)\right)$$
4		eqcom	$$⊢z+\mathrm{i}w=x+\mathrm{i}y\leftrightarrow x+\mathrm{i}y=z+\mathrm{i}w$$
5		ancom	$$⊢\left(y=w\wedge x=z\right)\leftrightarrow \left(x=z\wedge y=w\right)$$
6	3 4 5	3bitr4g	$$⊢\left(\left(z\in ℝ\wedge w\in ℝ\right)\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \left(z+\mathrm{i}w=x+\mathrm{i}y\leftrightarrow \left(y=w\wedge x=z\right)\right)$$
7	6	anassrs	$$⊢\left(\left(\left(z\in ℝ\wedge w\in ℝ\right)\wedge x\in ℝ\right)\wedge y\in ℝ\right)\to \left(z+\mathrm{i}w=x+\mathrm{i}y\leftrightarrow \left(y=w\wedge x=z\right)\right)$$
8	7	rexbidva	$$⊢\left(\left(z\in ℝ\wedge w\in ℝ\right)\wedge x\in ℝ\right)\to \left(\exists y\in ℝz+\mathrm{i}w=x+\mathrm{i}y\leftrightarrow \exists y\in ℝ\left(y=w\wedge x=z\right)\right)$$
9		biidd	$$⊢y=w\to \left(x=z\leftrightarrow x=z\right)$$
10	9	ceqsrexv	$$⊢w\in ℝ\to \left(\exists y\in ℝ\left(y=w\wedge x=z\right)\leftrightarrow x=z\right)$$
11	10	ad2antlr	$$⊢\left(\left(z\in ℝ\wedge w\in ℝ\right)\wedge x\in ℝ\right)\to \left(\exists y\in ℝ\left(y=w\wedge x=z\right)\leftrightarrow x=z\right)$$
12	8 11	bitrd	$$⊢\left(\left(z\in ℝ\wedge w\in ℝ\right)\wedge x\in ℝ\right)\to \left(\exists y\in ℝz+\mathrm{i}w=x+\mathrm{i}y\leftrightarrow x=z\right)$$
13	12	ralrimiva	$$⊢\left(z\in ℝ\wedge w\in ℝ\right)\to \forall x\in ℝ\left(\exists y\in ℝz+\mathrm{i}w=x+\mathrm{i}y\leftrightarrow x=z\right)$$
14		reu6i	$$⊢\left(z\in ℝ\wedge \forall x\in ℝ\left(\exists y\in ℝz+\mathrm{i}w=x+\mathrm{i}y\leftrightarrow x=z\right)\right)\to \exists !x\in ℝ\exists y\in ℝz+\mathrm{i}w=x+\mathrm{i}y$$
15	13 14	syldan	$$⊢\left(z\in ℝ\wedge w\in ℝ\right)\to \exists !x\in ℝ\exists y\in ℝz+\mathrm{i}w=x+\mathrm{i}y$$
16		eqeq1	$$⊢A=z+\mathrm{i}w\to \left(A=x+\mathrm{i}y\leftrightarrow z+\mathrm{i}w=x+\mathrm{i}y\right)$$
17	16	rexbidv	$$⊢A=z+\mathrm{i}w\to \left(\exists y\in ℝA=x+\mathrm{i}y\leftrightarrow \exists y\in ℝz+\mathrm{i}w=x+\mathrm{i}y\right)$$
18	17	reubidv	$$⊢A=z+\mathrm{i}w\to \left(\exists !x\in ℝ\exists y\in ℝA=x+\mathrm{i}y\leftrightarrow \exists !x\in ℝ\exists y\in ℝz+\mathrm{i}w=x+\mathrm{i}y\right)$$
19	15 18	syl5ibrcom	$$⊢\left(z\in ℝ\wedge w\in ℝ\right)\to \left(A=z+\mathrm{i}w\to \exists !x\in ℝ\exists y\in ℝA=x+\mathrm{i}y\right)$$
20	19	rexlimivv	$$⊢\exists z\in ℝ\exists w\in ℝA=z+\mathrm{i}w\to \exists !x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$
21	1 20	syl	$$⊢A\in ℂ\to \exists !x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$