This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mulrid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 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 biimtrrid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 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 ) ) )