Metamath Proof Explorer

Theorem reusq0

Description: A complex number is the square of exactly one complex number iff the given complex number is zero. (Contributed by AV, 21-Jun-2023)

Ref Expression
Assertion reusq0 
|- ( X e. CC -> ( E! x e. CC ( x ^ 2 ) = X <-> X = 0 ) )

Proof

Step Hyp Ref Expression
1 2a1 
 |-  ( X = 0 -> ( X e. CC -> ( E! x e. CC ( x ^ 2 ) = X -> X = 0 ) ) )
2 sqrtcl 
 |-  ( X e. CC -> ( sqrt ` X ) e. CC )
3 2 adantr 
 |-  ( ( X e. CC /\ -. X = 0 ) -> ( sqrt ` X ) e. CC )
4 2 negcld 
 |-  ( X e. CC -> -u ( sqrt ` X ) e. CC )
5 4 adantr 
 |-  ( ( X e. CC /\ -. X = 0 ) -> -u ( sqrt ` X ) e. CC )
6 2 eqnegd 
 |-  ( X e. CC -> ( ( sqrt ` X ) = -u ( sqrt ` X ) <-> ( sqrt ` X ) = 0 ) )
7 simpl 
 |-  ( ( X e. CC /\ ( sqrt ` X ) = 0 ) -> X e. CC )
8 simpr 
 |-  ( ( X e. CC /\ ( sqrt ` X ) = 0 ) -> ( sqrt ` X ) = 0 )
9 7 8 sqr00d 
 |-  ( ( X e. CC /\ ( sqrt ` X ) = 0 ) -> X = 0 )
10 9 ex 
 |-  ( X e. CC -> ( ( sqrt ` X ) = 0 -> X = 0 ) )
11 6 10 sylbid 
 |-  ( X e. CC -> ( ( sqrt ` X ) = -u ( sqrt ` X ) -> X = 0 ) )
12 11 necon3bd 
 |-  ( X e. CC -> ( -. X = 0 -> ( sqrt ` X ) =/= -u ( sqrt ` X ) ) )
13 12 imp 
 |-  ( ( X e. CC /\ -. X = 0 ) -> ( sqrt ` X ) =/= -u ( sqrt ` X ) )
14 3 5 13 3jca 
 |-  ( ( X e. CC /\ -. X = 0 ) -> ( ( sqrt ` X ) e. CC /\ -u ( sqrt ` X ) e. CC /\ ( sqrt ` X ) =/= -u ( sqrt ` X ) ) )
15 sqrtth 
 |-  ( X e. CC -> ( ( sqrt ` X ) ^ 2 ) = X )
16 sqneg 
 |-  ( ( sqrt ` X ) e. CC -> ( -u ( sqrt ` X ) ^ 2 ) = ( ( sqrt ` X ) ^ 2 ) )
17 2 16 syl 
 |-  ( X e. CC -> ( -u ( sqrt ` X ) ^ 2 ) = ( ( sqrt ` X ) ^ 2 ) )
18 17 15 eqtrd 
 |-  ( X e. CC -> ( -u ( sqrt ` X ) ^ 2 ) = X )
19 15 18 jca 
 |-  ( X e. CC -> ( ( ( sqrt ` X ) ^ 2 ) = X /\ ( -u ( sqrt ` X ) ^ 2 ) = X ) )
20 19 adantr 
 |-  ( ( X e. CC /\ -. X = 0 ) -> ( ( ( sqrt ` X ) ^ 2 ) = X /\ ( -u ( sqrt ` X ) ^ 2 ) = X ) )
21 oveq1 
 |-  ( x = ( sqrt ` X ) -> ( x ^ 2 ) = ( ( sqrt ` X ) ^ 2 ) )
22 21 eqeq1d 
 |-  ( x = ( sqrt ` X ) -> ( ( x ^ 2 ) = X <-> ( ( sqrt ` X ) ^ 2 ) = X ) )
23 oveq1 
 |-  ( x = -u ( sqrt ` X ) -> ( x ^ 2 ) = ( -u ( sqrt ` X ) ^ 2 ) )
24 23 eqeq1d 
 |-  ( x = -u ( sqrt ` X ) -> ( ( x ^ 2 ) = X <-> ( -u ( sqrt ` X ) ^ 2 ) = X ) )
25 22 24 2nreu 
 |-  ( ( ( sqrt ` X ) e. CC /\ -u ( sqrt ` X ) e. CC /\ ( sqrt ` X ) =/= -u ( sqrt ` X ) ) -> ( ( ( ( sqrt ` X ) ^ 2 ) = X /\ ( -u ( sqrt ` X ) ^ 2 ) = X ) -> -. E! x e. CC ( x ^ 2 ) = X ) )
26 14 20 25 sylc 
 |-  ( ( X e. CC /\ -. X = 0 ) -> -. E! x e. CC ( x ^ 2 ) = X )
27 26 pm2.21d 
 |-  ( ( X e. CC /\ -. X = 0 ) -> ( E! x e. CC ( x ^ 2 ) = X -> X = 0 ) )
28 27 expcom 
 |-  ( -. X = 0 -> ( X e. CC -> ( E! x e. CC ( x ^ 2 ) = X -> X = 0 ) ) )
29 1 28 pm2.61i 
 |-  ( X e. CC -> ( E! x e. CC ( x ^ 2 ) = X -> X = 0 ) )
30 2nn 
 |-  2 e. NN
31 0cnd 
 |-  ( 2 e. NN -> 0 e. CC )
32 oveq1 
 |-  ( x = 0 -> ( x ^ 2 ) = ( 0 ^ 2 ) )
33 32 eqeq1d 
 |-  ( x = 0 -> ( ( x ^ 2 ) = 0 <-> ( 0 ^ 2 ) = 0 ) )
34 eqeq1 
 |-  ( x = 0 -> ( x = y <-> 0 = y ) )
35 34 imbi2d 
 |-  ( x = 0 -> ( ( ( y ^ 2 ) = 0 -> x = y ) <-> ( ( y ^ 2 ) = 0 -> 0 = y ) ) )
36 35 ralbidv 
 |-  ( x = 0 -> ( A. y e. CC ( ( y ^ 2 ) = 0 -> x = y ) <-> A. y e. CC ( ( y ^ 2 ) = 0 -> 0 = y ) ) )
37 33 36 anbi12d 
 |-  ( x = 0 -> ( ( ( x ^ 2 ) = 0 /\ A. y e. CC ( ( y ^ 2 ) = 0 -> x = y ) ) <-> ( ( 0 ^ 2 ) = 0 /\ A. y e. CC ( ( y ^ 2 ) = 0 -> 0 = y ) ) ) )
38 37 adantl 
 |-  ( ( 2 e. NN /\ x = 0 ) -> ( ( ( x ^ 2 ) = 0 /\ A. y e. CC ( ( y ^ 2 ) = 0 -> x = y ) ) <-> ( ( 0 ^ 2 ) = 0 /\ A. y e. CC ( ( y ^ 2 ) = 0 -> 0 = y ) ) ) )
39 0exp 
 |-  ( 2 e. NN -> ( 0 ^ 2 ) = 0 )
40 sqeq0 
 |-  ( y e. CC -> ( ( y ^ 2 ) = 0 <-> y = 0 ) )
41 40 biimpd 
 |-  ( y e. CC -> ( ( y ^ 2 ) = 0 -> y = 0 ) )
42 eqcom 
 |-  ( 0 = y <-> y = 0 )
43 41 42 syl6ibr 
 |-  ( y e. CC -> ( ( y ^ 2 ) = 0 -> 0 = y ) )
44 43 adantl 
 |-  ( ( 2 e. NN /\ y e. CC ) -> ( ( y ^ 2 ) = 0 -> 0 = y ) )
45 44 ralrimiva 
 |-  ( 2 e. NN -> A. y e. CC ( ( y ^ 2 ) = 0 -> 0 = y ) )
46 39 45 jca 
 |-  ( 2 e. NN -> ( ( 0 ^ 2 ) = 0 /\ A. y e. CC ( ( y ^ 2 ) = 0 -> 0 = y ) ) )
47 31 38 46 rspcedvd 
 |-  ( 2 e. NN -> E. x e. CC ( ( x ^ 2 ) = 0 /\ A. y e. CC ( ( y ^ 2 ) = 0 -> x = y ) ) )
48 30 47 mp1i 
 |-  ( X = 0 -> E. x e. CC ( ( x ^ 2 ) = 0 /\ A. y e. CC ( ( y ^ 2 ) = 0 -> x = y ) ) )
49 eqeq2 
 |-  ( X = 0 -> ( ( x ^ 2 ) = X <-> ( x ^ 2 ) = 0 ) )
50 eqeq2 
 |-  ( X = 0 -> ( ( y ^ 2 ) = X <-> ( y ^ 2 ) = 0 ) )
51 50 imbi1d 
 |-  ( X = 0 -> ( ( ( y ^ 2 ) = X -> x = y ) <-> ( ( y ^ 2 ) = 0 -> x = y ) ) )
52 51 ralbidv 
 |-  ( X = 0 -> ( A. y e. CC ( ( y ^ 2 ) = X -> x = y ) <-> A. y e. CC ( ( y ^ 2 ) = 0 -> x = y ) ) )
53 49 52 anbi12d 
 |-  ( X = 0 -> ( ( ( x ^ 2 ) = X /\ A. y e. CC ( ( y ^ 2 ) = X -> x = y ) ) <-> ( ( x ^ 2 ) = 0 /\ A. y e. CC ( ( y ^ 2 ) = 0 -> x = y ) ) ) )
54 53 rexbidv 
 |-  ( X = 0 -> ( E. x e. CC ( ( x ^ 2 ) = X /\ A. y e. CC ( ( y ^ 2 ) = X -> x = y ) ) <-> E. x e. CC ( ( x ^ 2 ) = 0 /\ A. y e. CC ( ( y ^ 2 ) = 0 -> x = y ) ) ) )
55 48 54 mpbird 
 |-  ( X = 0 -> E. x e. CC ( ( x ^ 2 ) = X /\ A. y e. CC ( ( y ^ 2 ) = X -> x = y ) ) )
56 55 a1i 
 |-  ( X e. CC -> ( X = 0 -> E. x e. CC ( ( x ^ 2 ) = X /\ A. y e. CC ( ( y ^ 2 ) = X -> x = y ) ) ) )
57 oveq1 
 |-  ( x = y -> ( x ^ 2 ) = ( y ^ 2 ) )
58 57 eqeq1d 
 |-  ( x = y -> ( ( x ^ 2 ) = X <-> ( y ^ 2 ) = X ) )
59 58 reu8 
 |-  ( E! x e. CC ( x ^ 2 ) = X <-> E. x e. CC ( ( x ^ 2 ) = X /\ A. y e. CC ( ( y ^ 2 ) = X -> x = y ) ) )
60 56 59 syl6ibr 
 |-  ( X e. CC -> ( X = 0 -> E! x e. CC ( x ^ 2 ) = X ) )
61 29 60 impbid 
 |-  ( X e. CC -> ( E! x e. CC ( x ^ 2 ) = X <-> X = 0 ) )