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	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) = 𝐴 ↔ ( 𝐴 = 0 ∨ 𝐴 = 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-ne	⊢ ( 𝐴 ≠ 0 ↔ ¬ 𝐴 = 0 )
2		sqval	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
3		mulid1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
4	3	eqcomd	⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( 𝐴 · 1 ) )
5	2 4	eqeq12d	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) = 𝐴 ↔ ( 𝐴 · 𝐴 ) = ( 𝐴 · 1 ) ) )
6	5	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 ↑ 2 ) = 𝐴 ↔ ( 𝐴 · 𝐴 ) = ( 𝐴 · 1 ) ) )
7		ax-1cn	⊢ 1 ∈ ℂ
8		mulcan	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 𝐴 · 𝐴 ) = ( 𝐴 · 1 ) ↔ 𝐴 = 1 ) )
9	7 8	mp3an2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 𝐴 · 𝐴 ) = ( 𝐴 · 1 ) ↔ 𝐴 = 1 ) )
10	9	anabss5	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 · 𝐴 ) = ( 𝐴 · 1 ) ↔ 𝐴 = 1 ) )
11	6 10	bitrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 ↑ 2 ) = 𝐴 ↔ 𝐴 = 1 ) )
12	11	biimpd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 ↑ 2 ) = 𝐴 → 𝐴 = 1 ) )
13	12	impancom	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) = 𝐴 ) → ( 𝐴 ≠ 0 → 𝐴 = 1 ) )
14	1 13	syl5bir	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) = 𝐴 ) → ( ¬ 𝐴 = 0 → 𝐴 = 1 ) )
15	14	orrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) = 𝐴 ) → ( 𝐴 = 0 ∨ 𝐴 = 1 ) )
16	15	ex	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) = 𝐴 → ( 𝐴 = 0 ∨ 𝐴 = 1 ) ) )
17		sq0	⊢ ( 0 ↑ 2 ) = 0
18		oveq1	⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 2 ) = ( 0 ↑ 2 ) )
19		id	⊢ ( 𝐴 = 0 → 𝐴 = 0 )
20	17 18 19	3eqtr4a	⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 2 ) = 𝐴 )
21		sq1	⊢ ( 1 ↑ 2 ) = 1
22		oveq1	⊢ ( 𝐴 = 1 → ( 𝐴 ↑ 2 ) = ( 1 ↑ 2 ) )
23		id	⊢ ( 𝐴 = 1 → 𝐴 = 1 )
24	21 22 23	3eqtr4a	⊢ ( 𝐴 = 1 → ( 𝐴 ↑ 2 ) = 𝐴 )
25	20 24	jaoi	⊢ ( ( 𝐴 = 0 ∨ 𝐴 = 1 ) → ( 𝐴 ↑ 2 ) = 𝐴 )
26	16 25	impbid1	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) = 𝐴 ↔ ( 𝐴 = 0 ∨ 𝐴 = 1 ) ) )