Metamath Proof Explorer

Theorem sqrmo

Description: Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013) (Revised by NM, 17-Jun-2017)

Ref Expression
Assertion sqrmo 
|- ( A e. CC -> E* x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )

Proof

Step Hyp Ref Expression
1 simplr1 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> ( x ^ 2 ) = A )
2 simprr1 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> ( y ^ 2 ) = A )
3 1 2 eqtr4d 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> ( x ^ 2 ) = ( y ^ 2 ) )
4 sqeqor 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( x ^ 2 ) = ( y ^ 2 ) <-> ( x = y \/ x = -u y ) ) )
5 4 ad2ant2r 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> ( ( x ^ 2 ) = ( y ^ 2 ) <-> ( x = y \/ x = -u y ) ) )
6 3 5 mpbid 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> ( x = y \/ x = -u y ) )
7 6 ord 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> ( -. x = y -> x = -u y ) )
8 3simpc 
 |-  ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) -> ( 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
9 fveq2 
 |-  ( x = -u y -> ( Re ` x ) = ( Re ` -u y ) )
10 9 breq2d 
 |-  ( x = -u y -> ( 0 <_ ( Re ` x ) <-> 0 <_ ( Re ` -u y ) ) )
11 oveq2 
 |-  ( x = -u y -> ( _i x. x ) = ( _i x. -u y ) )
12 neleq1 
 |-  ( ( _i x. x ) = ( _i x. -u y ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. -u y ) e/ RR+ ) )
13 11 12 syl 
 |-  ( x = -u y -> ( ( _i x. x ) e/ RR+ <-> ( _i x. -u y ) e/ RR+ ) )
14 10 13 anbi12d 
 |-  ( x = -u y -> ( ( 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( 0 <_ ( Re ` -u y ) /\ ( _i x. -u y ) e/ RR+ ) ) )
15 8 14 syl5ibcom 
 |-  ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) -> ( x = -u y -> ( 0 <_ ( Re ` -u y ) /\ ( _i x. -u y ) e/ RR+ ) ) )
16 15 ad2antlr 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> ( x = -u y -> ( 0 <_ ( Re ` -u y ) /\ ( _i x. -u y ) e/ RR+ ) ) )
17 7 16 syld 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> ( -. x = y -> ( 0 <_ ( Re ` -u y ) /\ ( _i x. -u y ) e/ RR+ ) ) )
18 negeq 
 |-  ( y = 0 -> -u y = -u 0 )
19 neg0 
 |-  -u 0 = 0
20 18 19 eqtrdi 
 |-  ( y = 0 -> -u y = 0 )
21 20 eqeq2d 
 |-  ( y = 0 -> ( x = -u y <-> x = 0 ) )
22 eqeq2 
 |-  ( y = 0 -> ( x = y <-> x = 0 ) )
23 21 22 bitr4d 
 |-  ( y = 0 -> ( x = -u y <-> x = y ) )
24 23 biimpcd 
 |-  ( x = -u y -> ( y = 0 -> x = y ) )
25 24 necon3bd 
 |-  ( x = -u y -> ( -. x = y -> y =/= 0 ) )
26 7 25 syli 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> ( -. x = y -> y =/= 0 ) )
27 3simpc 
 |-  ( ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) -> ( 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) )
28 cnpart 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( ( 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) <-> -. ( 0 <_ ( Re ` -u y ) /\ ( _i x. -u y ) e/ RR+ ) ) )
29 27 28 imbitrid 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) -> -. ( 0 <_ ( Re ` -u y ) /\ ( _i x. -u y ) e/ RR+ ) ) )
30 29 impancom 
 |-  ( ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) -> ( y =/= 0 -> -. ( 0 <_ ( Re ` -u y ) /\ ( _i x. -u y ) e/ RR+ ) ) )
31 30 adantl 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> ( y =/= 0 -> -. ( 0 <_ ( Re ` -u y ) /\ ( _i x. -u y ) e/ RR+ ) ) )
32 26 31 syld 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> ( -. x = y -> -. ( 0 <_ ( Re ` -u y ) /\ ( _i x. -u y ) e/ RR+ ) ) )
33 17 32 pm2.65d 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> -. -. x = y )
34 33 notnotrd 
 |-  ( ( ( x e. CC /\ ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) /\ ( y e. CC /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> x = y )
35 34 an4s 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) -> x = y )
36 35 ex 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) -> x = y ) )
37 36 a1i 
 |-  ( A e. CC -> ( ( x e. CC /\ y e. CC ) -> ( ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) -> x = y ) ) )
38 37 ralrimivv 
 |-  ( A e. CC -> A. x e. CC A. y e. CC ( ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) -> x = y ) )
39 oveq1 
 |-  ( x = y -> ( x ^ 2 ) = ( y ^ 2 ) )
40 39 eqeq1d 
 |-  ( x = y -> ( ( x ^ 2 ) = A <-> ( y ^ 2 ) = A ) )
41 fveq2 
 |-  ( x = y -> ( Re ` x ) = ( Re ` y ) )
42 41 breq2d 
 |-  ( x = y -> ( 0 <_ ( Re ` x ) <-> 0 <_ ( Re ` y ) ) )
43 oveq2 
 |-  ( x = y -> ( _i x. x ) = ( _i x. y ) )
44 neleq1 
 |-  ( ( _i x. x ) = ( _i x. y ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. y ) e/ RR+ ) )
45 43 44 syl 
 |-  ( x = y -> ( ( _i x. x ) e/ RR+ <-> ( _i x. y ) e/ RR+ ) )
46 40 42 45 3anbi123d 
 |-  ( x = y -> ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) )
47 46 rmo4 
 |-  ( E* x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> A. x e. CC A. y e. CC ( ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) /\ ( ( y ^ 2 ) = A /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) -> x = y ) )
48 38 47 sylibr 
 |-  ( A e. CC -> E* x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )