Proof of Theorem sqrtnegnre
Step | Hyp | Ref
| Expression |
1 | | recn 10819 |
. . . . . . . 8
⊢ (𝑋 ∈ ℝ → 𝑋 ∈
ℂ) |
2 | 1 | negnegd 11180 |
. . . . . . 7
⊢ (𝑋 ∈ ℝ → --𝑋 = 𝑋) |
3 | 2 | adantr 484 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → --𝑋 = 𝑋) |
4 | 3 | eqcomd 2743 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → 𝑋 = --𝑋) |
5 | 4 | fveq2d 6721 |
. . . 4
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) →
(√‘𝑋) =
(√‘--𝑋)) |
6 | | simpl 486 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → 𝑋 ∈
ℝ) |
7 | 6 | renegcld 11259 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → -𝑋 ∈
ℝ) |
8 | | 0re 10835 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
9 | | ltle 10921 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 0 ∈
ℝ) → (𝑋 < 0
→ 𝑋 ≤
0)) |
10 | 8, 9 | mpan2 691 |
. . . . . . 7
⊢ (𝑋 ∈ ℝ → (𝑋 < 0 → 𝑋 ≤ 0)) |
11 | 10 | imp 410 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → 𝑋 ≤ 0) |
12 | | le0neg1 11340 |
. . . . . . 7
⊢ (𝑋 ∈ ℝ → (𝑋 ≤ 0 ↔ 0 ≤ -𝑋)) |
13 | 12 | adantr 484 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → (𝑋 ≤ 0 ↔ 0 ≤ -𝑋)) |
14 | 11, 13 | mpbid 235 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → 0 ≤ -𝑋) |
15 | 7, 14 | sqrtnegd 14985 |
. . . 4
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) →
(√‘--𝑋) = (i
· (√‘-𝑋))) |
16 | 5, 15 | eqtrd 2777 |
. . 3
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) →
(√‘𝑋) = (i
· (√‘-𝑋))) |
17 | | ax-icn 10788 |
. . . . . 6
⊢ i ∈
ℂ |
18 | 17 | a1i 11 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → i ∈
ℂ) |
19 | 1 | adantr 484 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → 𝑋 ∈
ℂ) |
20 | 19 | negcld 11176 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → -𝑋 ∈
ℂ) |
21 | 20 | sqrtcld 15001 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) →
(√‘-𝑋) ∈
ℂ) |
22 | 18, 21 | mulcomd 10854 |
. . . 4
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → (i ·
(√‘-𝑋)) =
((√‘-𝑋)
· i)) |
23 | 7, 14 | resqrtcld 14981 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) →
(√‘-𝑋) ∈
ℝ) |
24 | | inelr 11820 |
. . . . . . . 8
⊢ ¬ i
∈ ℝ |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → ¬ i ∈
ℝ) |
26 | 18, 25 | eldifd 3877 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → i ∈
(ℂ ∖ ℝ)) |
27 | | lt0neg1 11338 |
. . . . . . . 8
⊢ (𝑋 ∈ ℝ → (𝑋 < 0 ↔ 0 < -𝑋)) |
28 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℝ → 0 ∈
ℝ) |
29 | | ltne 10929 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 0 < -𝑋) → -𝑋 ≠ 0) |
30 | 28, 29 | sylan 583 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℝ ∧ 0 <
-𝑋) → -𝑋 ≠ 0) |
31 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ ℝ ∧ 0 <
-𝑋) → 𝑋 ∈
ℝ) |
32 | 31 | renegcld 11259 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℝ ∧ 0 <
-𝑋) → -𝑋 ∈
ℝ) |
33 | 10, 27, 12 | 3imtr3d 296 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℝ → (0 <
-𝑋 → 0 ≤ -𝑋)) |
34 | 33 | imp 410 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℝ ∧ 0 <
-𝑋) → 0 ≤ -𝑋) |
35 | | sqrt00 14827 |
. . . . . . . . . . . . 13
⊢ ((-𝑋 ∈ ℝ ∧ 0 ≤
-𝑋) →
((√‘-𝑋) = 0
↔ -𝑋 =
0)) |
36 | 32, 34, 35 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧ 0 <
-𝑋) →
((√‘-𝑋) = 0
↔ -𝑋 =
0)) |
37 | 36 | bicomd 226 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℝ ∧ 0 <
-𝑋) → (-𝑋 = 0 ↔
(√‘-𝑋) =
0)) |
38 | 37 | necon3bid 2985 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℝ ∧ 0 <
-𝑋) → (-𝑋 ≠ 0 ↔
(√‘-𝑋) ≠
0)) |
39 | 30, 38 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ ∧ 0 <
-𝑋) →
(√‘-𝑋) ≠
0) |
40 | 39 | ex 416 |
. . . . . . . 8
⊢ (𝑋 ∈ ℝ → (0 <
-𝑋 →
(√‘-𝑋) ≠
0)) |
41 | 27, 40 | sylbid 243 |
. . . . . . 7
⊢ (𝑋 ∈ ℝ → (𝑋 < 0 →
(√‘-𝑋) ≠
0)) |
42 | 41 | imp 410 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) →
(√‘-𝑋) ≠
0) |
43 | 23, 26, 42 | recnmulnred 44470 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) →
((√‘-𝑋)
· i) ∉ ℝ) |
44 | | df-nel 3047 |
. . . . 5
⊢
(((√‘-𝑋)
· i) ∉ ℝ ↔ ¬ ((√‘-𝑋) · i) ∈
ℝ) |
45 | 43, 44 | sylib 221 |
. . . 4
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → ¬
((√‘-𝑋)
· i) ∈ ℝ) |
46 | 22, 45 | eqneltrd 2857 |
. . 3
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → ¬ (i
· (√‘-𝑋)) ∈ ℝ) |
47 | 16, 46 | eqneltrd 2857 |
. 2
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → ¬
(√‘𝑋) ∈
ℝ) |
48 | | df-nel 3047 |
. 2
⊢
((√‘𝑋)
∉ ℝ ↔ ¬ (√‘𝑋) ∈ ℝ) |
49 | 47, 48 | sylibr 237 |
1
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) →
(√‘𝑋) ∉
ℝ) |