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 X < 0 X

Proof

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