Proof of Theorem sqrtneglem
| Step | Hyp | Ref
| Expression |
| 1 | | ax-icn 11214 |
. . . 4
⊢ i ∈
ℂ |
| 2 | | resqrtcl 15292 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(√‘𝐴) ∈
ℝ) |
| 3 | | recn 11245 |
. . . . 5
⊢
((√‘𝐴)
∈ ℝ → (√‘𝐴) ∈ ℂ) |
| 4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(√‘𝐴) ∈
ℂ) |
| 5 | | sqmul 14159 |
. . . 4
⊢ ((i
∈ ℂ ∧ (√‘𝐴) ∈ ℂ) → ((i ·
(√‘𝐴))↑2)
= ((i↑2) · ((√‘𝐴)↑2))) |
| 6 | 1, 4, 5 | sylancr 587 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((i ·
(√‘𝐴))↑2)
= ((i↑2) · ((√‘𝐴)↑2))) |
| 7 | | i2 14241 |
. . . . 5
⊢
(i↑2) = -1 |
| 8 | 7 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (i↑2) =
-1) |
| 9 | | resqrtth 15294 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
((√‘𝐴)↑2)
= 𝐴) |
| 10 | 8, 9 | oveq12d 7449 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((i↑2)
· ((√‘𝐴)↑2)) = (-1 · 𝐴)) |
| 11 | | recn 11245 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 12 | 11 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 𝐴 ∈ ℂ) |
| 13 | 12 | mulm1d 11715 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (-1 ·
𝐴) = -𝐴) |
| 14 | 6, 10, 13 | 3eqtrd 2781 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((i ·
(√‘𝐴))↑2)
= -𝐴) |
| 15 | | renegcl 11572 |
. . . 4
⊢
((√‘𝐴)
∈ ℝ → -(√‘𝐴) ∈ ℝ) |
| 16 | | 0re 11263 |
. . . . 5
⊢ 0 ∈
ℝ |
| 17 | | reim0 15157 |
. . . . . 6
⊢
(-(√‘𝐴)
∈ ℝ → (ℑ‘-(√‘𝐴)) = 0) |
| 18 | | recn 11245 |
. . . . . . 7
⊢
(-(√‘𝐴)
∈ ℝ → -(√‘𝐴) ∈ ℂ) |
| 19 | | imre 15147 |
. . . . . . 7
⊢
(-(√‘𝐴)
∈ ℂ → (ℑ‘-(√‘𝐴)) = (ℜ‘(-i ·
-(√‘𝐴)))) |
| 20 | 18, 19 | syl 17 |
. . . . . 6
⊢
(-(√‘𝐴)
∈ ℝ → (ℑ‘-(√‘𝐴)) = (ℜ‘(-i ·
-(√‘𝐴)))) |
| 21 | 17, 20 | eqtr3d 2779 |
. . . . 5
⊢
(-(√‘𝐴)
∈ ℝ → 0 = (ℜ‘(-i · -(√‘𝐴)))) |
| 22 | | eqle 11363 |
. . . . 5
⊢ ((0
∈ ℝ ∧ 0 = (ℜ‘(-i · -(√‘𝐴)))) → 0 ≤
(ℜ‘(-i · -(√‘𝐴)))) |
| 23 | 16, 21, 22 | sylancr 587 |
. . . 4
⊢
(-(√‘𝐴)
∈ ℝ → 0 ≤ (ℜ‘(-i · -(√‘𝐴)))) |
| 24 | 2, 15, 23 | 3syl 18 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 0 ≤
(ℜ‘(-i · -(√‘𝐴)))) |
| 25 | | mul2neg 11702 |
. . . . 5
⊢ ((i
∈ ℂ ∧ (√‘𝐴) ∈ ℂ) → (-i ·
-(√‘𝐴)) = (i
· (√‘𝐴))) |
| 26 | 1, 4, 25 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (-i ·
-(√‘𝐴)) = (i
· (√‘𝐴))) |
| 27 | 26 | fveq2d 6910 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (ℜ‘(-i
· -(√‘𝐴))) = (ℜ‘(i ·
(√‘𝐴)))) |
| 28 | 24, 27 | breqtrd 5169 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 0 ≤
(ℜ‘(i · (√‘𝐴)))) |
| 29 | | ixi 11892 |
. . . . . . 7
⊢ (i
· i) = -1 |
| 30 | 29 | oveq1i 7441 |
. . . . . 6
⊢ ((i
· i) · (√‘𝐴)) = (-1 · (√‘𝐴)) |
| 31 | | mulass 11243 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ (√‘𝐴) ∈ ℂ) → ((i · i)
· (√‘𝐴))
= (i · (i · (√‘𝐴)))) |
| 32 | 1, 1, 31 | mp3an12 1453 |
. . . . . 6
⊢
((√‘𝐴)
∈ ℂ → ((i · i) · (√‘𝐴)) = (i · (i ·
(√‘𝐴)))) |
| 33 | | mulm1 11704 |
. . . . . 6
⊢
((√‘𝐴)
∈ ℂ → (-1 · (√‘𝐴)) = -(√‘𝐴)) |
| 34 | 30, 32, 33 | 3eqtr3a 2801 |
. . . . 5
⊢
((√‘𝐴)
∈ ℂ → (i · (i · (√‘𝐴))) = -(√‘𝐴)) |
| 35 | 4, 34 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (i · (i
· (√‘𝐴))) = -(√‘𝐴)) |
| 36 | | sqrtge0 15296 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 0 ≤
(√‘𝐴)) |
| 37 | | le0neg2 11772 |
. . . . . . . 8
⊢
((√‘𝐴)
∈ ℝ → (0 ≤ (√‘𝐴) ↔ -(√‘𝐴) ≤ 0)) |
| 38 | | lenlt 11339 |
. . . . . . . . 9
⊢
((-(√‘𝐴)
∈ ℝ ∧ 0 ∈ ℝ) → (-(√‘𝐴) ≤ 0 ↔ ¬ 0 <
-(√‘𝐴))) |
| 39 | 15, 16, 38 | sylancl 586 |
. . . . . . . 8
⊢
((√‘𝐴)
∈ ℝ → (-(√‘𝐴) ≤ 0 ↔ ¬ 0 <
-(√‘𝐴))) |
| 40 | 37, 39 | bitrd 279 |
. . . . . . 7
⊢
((√‘𝐴)
∈ ℝ → (0 ≤ (√‘𝐴) ↔ ¬ 0 < -(√‘𝐴))) |
| 41 | 2, 40 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0 ≤
(√‘𝐴) ↔
¬ 0 < -(√‘𝐴))) |
| 42 | 36, 41 | mpbid 232 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ¬ 0 <
-(√‘𝐴)) |
| 43 | | elrp 13036 |
. . . . . 6
⊢
(-(√‘𝐴)
∈ ℝ+ ↔ (-(√‘𝐴) ∈ ℝ ∧ 0 <
-(√‘𝐴))) |
| 44 | 2, 15 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
-(√‘𝐴) ∈
ℝ) |
| 45 | 44 | biantrurd 532 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (0 <
-(√‘𝐴) ↔
(-(√‘𝐴) ∈
ℝ ∧ 0 < -(√‘𝐴)))) |
| 46 | 43, 45 | bitr4id 290 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(-(√‘𝐴) ∈
ℝ+ ↔ 0 < -(√‘𝐴))) |
| 47 | 42, 46 | mtbird 325 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ¬
-(√‘𝐴) ∈
ℝ+) |
| 48 | 35, 47 | eqneltrd 2861 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ¬ (i ·
(i · (√‘𝐴))) ∈
ℝ+) |
| 49 | | df-nel 3047 |
. . 3
⊢ ((i
· (i · (√‘𝐴))) ∉ ℝ+ ↔ ¬
(i · (i · (√‘𝐴))) ∈
ℝ+) |
| 50 | 48, 49 | sylibr 234 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (i · (i
· (√‘𝐴))) ∉
ℝ+) |
| 51 | 14, 28, 50 | 3jca 1129 |
1
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (((i ·
(√‘𝐴))↑2)
= -𝐴 ∧ 0 ≤
(ℜ‘(i · (√‘𝐴))) ∧ (i · (i ·
(√‘𝐴))) ∉
ℝ+)) |