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 e. CC -> ( ( A ^ 2 ) = A <-> ( A = 0 \/ A = 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-ne	|- ( A =/= 0 <-> -. A = 0 )
2		sqval	|- ( A e. CC -> ( A ^ 2 ) = ( A x. A ) )
3		mulid1	|- ( A e. CC -> ( A x. 1 ) = A )
4	3	eqcomd	|- ( A e. CC -> A = ( A x. 1 ) )
5	2 4	eqeq12d	|- ( A e. CC -> ( ( A ^ 2 ) = A <-> ( A x. A ) = ( A x. 1 ) ) )
6	5	adantr	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( A ^ 2 ) = A <-> ( A x. A ) = ( A x. 1 ) ) )
7		ax-1cn	|- 1 e. CC
8		mulcan	|- ( ( A e. CC /\ 1 e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( A x. A ) = ( A x. 1 ) <-> A = 1 ) )
9	7 8	mp3an2	|- ( ( A e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( A x. A ) = ( A x. 1 ) <-> A = 1 ) )
10	9	anabss5	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( A x. A ) = ( A x. 1 ) <-> A = 1 ) )
11	6 10	bitrd	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( A ^ 2 ) = A <-> A = 1 ) )
12	11	biimpd	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( A ^ 2 ) = A -> A = 1 ) )
13	12	impancom	|- ( ( A e. CC /\ ( A ^ 2 ) = A ) -> ( A =/= 0 -> A = 1 ) )
14	1 13	syl5bir	|- ( ( A e. CC /\ ( A ^ 2 ) = A ) -> ( -. A = 0 -> A = 1 ) )
15	14	orrd	|- ( ( A e. CC /\ ( A ^ 2 ) = A ) -> ( A = 0 \/ A = 1 ) )
16	15	ex	|- ( A e. CC -> ( ( A ^ 2 ) = A -> ( A = 0 \/ A = 1 ) ) )
17		sq0	|- ( 0 ^ 2 ) = 0
18		oveq1	|- ( A = 0 -> ( A ^ 2 ) = ( 0 ^ 2 ) )
19		id	|- ( A = 0 -> A = 0 )
20	17 18 19	3eqtr4a	|- ( A = 0 -> ( A ^ 2 ) = A )
21		sq1	|- ( 1 ^ 2 ) = 1
22		oveq1	|- ( A = 1 -> ( A ^ 2 ) = ( 1 ^ 2 ) )
23		id	|- ( A = 1 -> A = 1 )
24	21 22 23	3eqtr4a	|- ( A = 1 -> ( A ^ 2 ) = A )
25	20 24	jaoi	|- ( ( A = 0 \/ A = 1 ) -> ( A ^ 2 ) = A )
26	16 25	impbid1	|- ( A e. CC -> ( ( A ^ 2 ) = A <-> ( A = 0 \/ A = 1 ) ) )