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 
|- ( 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 mulrid 
 |-  ( 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 biimtrrid 
 |-  ( ( 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 ) ) )