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 AA2=AA=0A=1

Proof

Step Hyp Ref Expression
1 df-ne A0¬A=0
2 sqval AA2=AA
3 mulid1 AA1=A
4 3 eqcomd AA=A1
5 2 4 eqeq12d AA2=AAA=A1
6 5 adantr AA0A2=AAA=A1
7 ax-1cn 1
8 mulcan A1AA0AA=A1A=1
9 7 8 mp3an2 AAA0AA=A1A=1
10 9 anabss5 AA0AA=A1A=1
11 6 10 bitrd AA0A2=AA=1
12 11 biimpd AA0A2=AA=1
13 12 impancom AA2=AA0A=1
14 1 13 syl5bir AA2=A¬A=0A=1
15 14 orrd AA2=AA=0A=1
16 15 ex AA2=AA=0A=1
17 sq0 02=0
18 oveq1 A=0A2=02
19 id A=0A=0
20 17 18 19 3eqtr4a A=0A2=A
21 sq1 12=1
22 oveq1 A=1A2=12
23 id A=1A=1
24 21 22 23 3eqtr4a A=1A2=A
25 20 24 jaoi A=0A=1A2=A
26 16 25 impbid1 AA2=AA=0A=1