Theorem sq01

Description: If a complex number equals its square, it must be 0 or 1. (Contributed by NM, 6-Jun-2006)

	Ref	Expression
Assertion	sq01	$$⊢A\in ℂ\to \left(A^2=A\leftrightarrow \left(A=0\vee A=1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$$⊢A\ne 0\leftrightarrow \neg A=0$$
2		sqval	$$⊢A\in ℂ\to A^2=AA$$
3		mulid1	$$⊢A\in ℂ\to A\cdot 1=A$$
4	3	eqcomd	$$⊢A\in ℂ\to A=A\cdot 1$$
5	2 4	eqeq12d	$$⊢A\in ℂ\to \left(A^2=A\leftrightarrow AA=A\cdot 1\right)$$
6	5	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(A^2=A\leftrightarrow AA=A\cdot 1\right)$$
7		ax-1cn	$$⊢1\in ℂ$$
8		mulcan	$$⊢\left(A\in ℂ\wedge 1\in ℂ\wedge \left(A\in ℂ\wedge A\ne 0\right)\right)\to \left(AA=A\cdot 1\leftrightarrow A=1\right)$$
9	7 8	mp3an2	$$⊢\left(A\in ℂ\wedge \left(A\in ℂ\wedge A\ne 0\right)\right)\to \left(AA=A\cdot 1\leftrightarrow A=1\right)$$
10	9	anabss5	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(AA=A\cdot 1\leftrightarrow A=1\right)$$
11	6 10	bitrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(A^2=A\leftrightarrow A=1\right)$$
12	11	biimpd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(A^2=A\to A=1\right)$$
13	12	impancom	$$⊢\left(A\in ℂ\wedge A^2=A\right)\to \left(A\ne 0\to A=1\right)$$
14	1 13	syl5bir	$$⊢\left(A\in ℂ\wedge A^2=A\right)\to \left(\neg A=0\to A=1\right)$$
15	14	orrd	$$⊢\left(A\in ℂ\wedge A^2=A\right)\to \left(A=0\vee A=1\right)$$
16	15	ex	$$⊢A\in ℂ\to \left(A^2=A\to \left(A=0\vee A=1\right)\right)$$
17		sq0	$$⊢0^2=0$$
18		oveq1	$$⊢A=0\to A^2=0^2$$
19		id	$$⊢A=0\to A=0$$
20	17 18 19	3eqtr4a	$$⊢A=0\to A^2=A$$
21		sq1	$$⊢1^2=1$$
22		oveq1	$$⊢A=1\to A^2=1^2$$
23		id	$$⊢A=1\to A=1$$
24	21 22 23	3eqtr4a	$$⊢A=1\to A^2=A$$
25	20 24	jaoi	$$⊢\left(A=0\vee A=1\right)\to A^2=A$$
26	16 25	impbid1	$$⊢A\in ℂ\to \left(A^2=A\leftrightarrow \left(A=0\vee A=1\right)\right)$$