Metamath Proof Explorer

Theorem sqrtnegnre

Description: The square root of a negative number is not a real number. (Contributed by AV, 28-Feb-2023)

Ref Expression
Assertion sqrtnegnre 
|- ( ( X e. RR /\ X < 0 ) -> ( sqrt ` X ) e/ RR )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( X e. RR -> X e. CC )
2 1 negnegd 
 |-  ( X e. RR -> -u -u X = X )
3 2 adantr 
 |-  ( ( X e. RR /\ X < 0 ) -> -u -u X = X )
4 3 eqcomd 
 |-  ( ( X e. RR /\ X < 0 ) -> X = -u -u X )
5 4 fveq2d 
 |-  ( ( X e. RR /\ X < 0 ) -> ( sqrt ` X ) = ( sqrt ` -u -u X ) )
6 simpl 
 |-  ( ( X e. RR /\ X < 0 ) -> X e. RR )
7 6 renegcld 
 |-  ( ( X e. RR /\ X < 0 ) -> -u X e. RR )
8 0re 
 |-  0 e. RR
9 ltle 
 |-  ( ( X e. RR /\ 0 e. RR ) -> ( X < 0 -> X <_ 0 ) )
10 8 9 mpan2 
 |-  ( X e. RR -> ( X < 0 -> X <_ 0 ) )
11 10 imp 
 |-  ( ( X e. RR /\ X < 0 ) -> X <_ 0 )
12 le0neg1 
 |-  ( X e. RR -> ( X <_ 0 <-> 0 <_ -u X ) )
13 12 adantr 
 |-  ( ( X e. RR /\ X < 0 ) -> ( X <_ 0 <-> 0 <_ -u X ) )
14 11 13 mpbid 
 |-  ( ( X e. RR /\ X < 0 ) -> 0 <_ -u X )
15 7 14 sqrtnegd 
 |-  ( ( X e. RR /\ X < 0 ) -> ( sqrt ` -u -u X ) = ( _i x. ( sqrt ` -u X ) ) )
16 5 15 eqtrd 
 |-  ( ( X e. RR /\ X < 0 ) -> ( sqrt ` X ) = ( _i x. ( sqrt ` -u X ) ) )
17 ax-icn 
 |-  _i e. CC
18 17 a1i 
 |-  ( ( X e. RR /\ X < 0 ) -> _i e. CC )
19 1 adantr 
 |-  ( ( X e. RR /\ X < 0 ) -> X e. CC )
20 19 negcld 
 |-  ( ( X e. RR /\ X < 0 ) -> -u X e. CC )
21 20 sqrtcld 
 |-  ( ( X e. RR /\ X < 0 ) -> ( sqrt ` -u X ) e. CC )
22 18 21 mulcomd 
 |-  ( ( X e. RR /\ X < 0 ) -> ( _i x. ( sqrt ` -u X ) ) = ( ( sqrt ` -u X ) x. _i ) )
23 7 14 resqrtcld 
 |-  ( ( X e. RR /\ X < 0 ) -> ( sqrt ` -u X ) e. RR )
24 inelr 
 |-  -. _i e. RR
25 24 a1i 
 |-  ( ( X e. RR /\ X < 0 ) -> -. _i e. RR )
26 18 25 eldifd 
 |-  ( ( X e. RR /\ X < 0 ) -> _i e. ( CC \ RR ) )
27 lt0neg1 
 |-  ( X e. RR -> ( X < 0 <-> 0 < -u X ) )
28 8 a1i 
 |-  ( X e. RR -> 0 e. RR )
29 ltne 
 |-  ( ( 0 e. RR /\ 0 < -u X ) -> -u X =/= 0 )
30 28 29 sylan 
 |-  ( ( X e. RR /\ 0 < -u X ) -> -u X =/= 0 )
31 simpl 
 |-  ( ( X e. RR /\ 0 < -u X ) -> X e. RR )
32 31 renegcld 
 |-  ( ( X e. RR /\ 0 < -u X ) -> -u X e. RR )
33 10 27 12 3imtr3d 
 |-  ( X e. RR -> ( 0 < -u X -> 0 <_ -u X ) )
34 33 imp 
 |-  ( ( X e. RR /\ 0 < -u X ) -> 0 <_ -u X )
35 sqrt00 
 |-  ( ( -u X e. RR /\ 0 <_ -u X ) -> ( ( sqrt ` -u X ) = 0 <-> -u X = 0 ) )
36 32 34 35 syl2anc 
 |-  ( ( X e. RR /\ 0 < -u X ) -> ( ( sqrt ` -u X ) = 0 <-> -u X = 0 ) )
37 36 bicomd 
 |-  ( ( X e. RR /\ 0 < -u X ) -> ( -u X = 0 <-> ( sqrt ` -u X ) = 0 ) )
38 37 necon3bid 
 |-  ( ( X e. RR /\ 0 < -u X ) -> ( -u X =/= 0 <-> ( sqrt ` -u X ) =/= 0 ) )
39 30 38 mpbid 
 |-  ( ( X e. RR /\ 0 < -u X ) -> ( sqrt ` -u X ) =/= 0 )
40 39 ex 
 |-  ( X e. RR -> ( 0 < -u X -> ( sqrt ` -u X ) =/= 0 ) )
41 27 40 sylbid 
 |-  ( X e. RR -> ( X < 0 -> ( sqrt ` -u X ) =/= 0 ) )
42 41 imp 
 |-  ( ( X e. RR /\ X < 0 ) -> ( sqrt ` -u X ) =/= 0 )
43 23 26 42 recnmulnred 
 |-  ( ( X e. RR /\ X < 0 ) -> ( ( sqrt ` -u X ) x. _i ) e/ RR )
44 df-nel 
 |-  ( ( ( sqrt ` -u X ) x. _i ) e/ RR <-> -. ( ( sqrt ` -u X ) x. _i ) e. RR )
45 43 44 sylib 
 |-  ( ( X e. RR /\ X < 0 ) -> -. ( ( sqrt ` -u X ) x. _i ) e. RR )
46 22 45 eqneltrd 
 |-  ( ( X e. RR /\ X < 0 ) -> -. ( _i x. ( sqrt ` -u X ) ) e. RR )
47 16 46 eqneltrd 
 |-  ( ( X e. RR /\ X < 0 ) -> -. ( sqrt ` X ) e. RR )
48 df-nel 
 |-  ( ( sqrt ` X ) e/ RR <-> -. ( sqrt ` X ) e. RR )
49 47 48 sylibr 
 |-  ( ( X e. RR /\ X < 0 ) -> ( sqrt ` X ) e/ RR )