Metamath Proof Explorer

Theorem et-sqrtnegnre

Description: The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A < 0 /\ A e. RR ) -> A e. RR )
2 id 
 |-  ( A e. RR -> A e. RR )
3 0red 
 |-  ( A e. RR -> 0 e. RR )
4 2 3 ltnled 
 |-  ( A e. RR -> ( A < 0 <-> -. 0 <_ A ) )
5 4 biimpd 
 |-  ( A e. RR -> ( A < 0 -> -. 0 <_ A ) )
6 5 impcom 
 |-  ( ( A < 0 /\ A e. RR ) -> -. 0 <_ A )
7 1 6 jcnd 
 |-  ( ( A < 0 /\ A e. RR ) -> -. ( A e. RR -> 0 <_ A ) )
8 7 ancoms 
 |-  ( ( A e. RR /\ A < 0 ) -> -. ( A e. RR -> 0 <_ A ) )
9 recn 
 |-  ( A e. RR -> A e. CC )
10 9 sqsqrtd 
 |-  ( A e. RR -> ( ( sqrt ` A ) ^ 2 ) = A )
11 sqge0 
 |-  ( ( sqrt ` A ) e. RR -> 0 <_ ( ( sqrt ` A ) ^ 2 ) )
12 breq2 
 |-  ( ( ( sqrt ` A ) ^ 2 ) = A -> ( 0 <_ ( ( sqrt ` A ) ^ 2 ) <-> 0 <_ A ) )
13 12 biimpd 
 |-  ( ( ( sqrt ` A ) ^ 2 ) = A -> ( 0 <_ ( ( sqrt ` A ) ^ 2 ) -> 0 <_ A ) )
14 10 11 13 syl2imc 
 |-  ( ( sqrt ` A ) e. RR -> ( A e. RR -> 0 <_ A ) )
15 8 14 nsyl 
 |-  ( ( A e. RR /\ A < 0 ) -> -. ( sqrt ` A ) e. RR )