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 ( ( 𝑋 ∈ ℝ ∧ 𝑋 < 0 ) → ( √ ‘ 𝑋 ) ∉ ℝ )

Proof

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