Proof of Theorem cxpsqrtlem
Step | Hyp | Ref
| Expression |
1 | | ax-icn 10788 |
. . 3
⊢ i ∈
ℂ |
2 | | sqrtcl 14925 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(√‘𝐴) ∈
ℂ) |
3 | 2 | ad2antrr 726 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (√‘𝐴)
∈ ℂ) |
4 | | mulcl 10813 |
. . 3
⊢ ((i
∈ ℂ ∧ (√‘𝐴) ∈ ℂ) → (i ·
(√‘𝐴)) ∈
ℂ) |
5 | 1, 3, 4 | sylancr 590 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (i · (√‘𝐴)) ∈ ℂ) |
6 | | imval 14670 |
. . . 4
⊢ ((i
· (√‘𝐴))
∈ ℂ → (ℑ‘(i · (√‘𝐴))) = (ℜ‘((i ·
(√‘𝐴)) /
i))) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (ℑ‘(i · (√‘𝐴))) = (ℜ‘((i ·
(√‘𝐴)) /
i))) |
8 | | ine0 11267 |
. . . . . 6
⊢ i ≠
0 |
9 | | divcan3 11516 |
. . . . . 6
⊢
(((√‘𝐴)
∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0) → ((i ·
(√‘𝐴)) / i) =
(√‘𝐴)) |
10 | 1, 8, 9 | mp3an23 1455 |
. . . . 5
⊢
((√‘𝐴)
∈ ℂ → ((i · (√‘𝐴)) / i) = (√‘𝐴)) |
11 | 3, 10 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((i · (√‘𝐴)) / i) = (√‘𝐴)) |
12 | 11 | fveq2d 6721 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (ℜ‘((i · (√‘𝐴)) / i)) =
(ℜ‘(√‘𝐴))) |
13 | | halfre 12044 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ |
14 | 13 | recni 10847 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℂ |
15 | | logcl 25457 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) |
16 | | mulcl 10813 |
. . . . . . . . . . . 12
⊢ (((1 / 2)
∈ ℂ ∧ (log‘𝐴) ∈ ℂ) → ((1 / 2) ·
(log‘𝐴)) ∈
ℂ) |
17 | 14, 15, 16 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((1 / 2)
· (log‘𝐴))
∈ ℂ) |
18 | 17 | recld 14757 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℜ‘((1 / 2) · (log‘𝐴))) ∈ ℝ) |
19 | 18 | reefcld 15649 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(ℜ‘((1 / 2) · (log‘𝐴)))) ∈ ℝ) |
20 | 17 | imcld 14758 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℑ‘((1 / 2) · (log‘𝐴))) ∈ ℝ) |
21 | 20 | recoscld 15705 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(cos‘(ℑ‘((1 / 2) · (log‘𝐴)))) ∈ ℝ) |
22 | 18 | rpefcld 15666 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(ℜ‘((1 / 2) · (log‘𝐴)))) ∈
ℝ+) |
23 | 22 | rpge0d 12632 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 0 ≤
(exp‘(ℜ‘((1 / 2) · (log‘𝐴))))) |
24 | | immul2 14700 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℝ ∧ (log‘𝐴) ∈ ℂ) → (ℑ‘((1
/ 2) · (log‘𝐴))) = ((1 / 2) ·
(ℑ‘(log‘𝐴)))) |
25 | 13, 15, 24 | sylancr 590 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℑ‘((1 / 2) · (log‘𝐴))) = ((1 / 2) ·
(ℑ‘(log‘𝐴)))) |
26 | 15 | imcld 14758 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℑ‘(log‘𝐴)) ∈ ℝ) |
27 | 26 | recnd 10861 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℑ‘(log‘𝐴)) ∈ ℂ) |
28 | | mulcom 10815 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℂ ∧ (ℑ‘(log‘𝐴)) ∈ ℂ) → ((1 / 2) ·
(ℑ‘(log‘𝐴))) = ((ℑ‘(log‘𝐴)) · (1 /
2))) |
29 | 14, 27, 28 | sylancr 590 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((1 / 2)
· (ℑ‘(log‘𝐴))) = ((ℑ‘(log‘𝐴)) · (1 /
2))) |
30 | 25, 29 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℑ‘((1 / 2) · (log‘𝐴))) = ((ℑ‘(log‘𝐴)) · (1 /
2))) |
31 | | logimcl 25458 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
32 | 31 | simpld 498 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -π <
(ℑ‘(log‘𝐴))) |
33 | | pire 25348 |
. . . . . . . . . . . . . . . 16
⊢ π
∈ ℝ |
34 | 33 | renegcli 11139 |
. . . . . . . . . . . . . . 15
⊢ -π
∈ ℝ |
35 | | ltle 10921 |
. . . . . . . . . . . . . . 15
⊢ ((-π
∈ ℝ ∧ (ℑ‘(log‘𝐴)) ∈ ℝ) → (-π <
(ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) |
36 | 34, 26, 35 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π <
(ℑ‘(log‘𝐴)) → -π ≤
(ℑ‘(log‘𝐴)))) |
37 | 32, 36 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -π ≤
(ℑ‘(log‘𝐴))) |
38 | 31 | simprd 499 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℑ‘(log‘𝐴)) ≤ π) |
39 | 34, 33 | elicc2i 13001 |
. . . . . . . . . . . . 13
⊢
((ℑ‘(log‘𝐴)) ∈ (-π[,]π) ↔
((ℑ‘(log‘𝐴)) ∈ ℝ ∧ -π ≤
(ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) |
40 | 26, 37, 38, 39 | syl3anbrc 1345 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℑ‘(log‘𝐴)) ∈ (-π[,]π)) |
41 | | halfgt0 12046 |
. . . . . . . . . . . . . 14
⊢ 0 < (1
/ 2) |
42 | 13, 41 | elrpii 12589 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ+ |
43 | 33 | recni 10847 |
. . . . . . . . . . . . . . 15
⊢ π
∈ ℂ |
44 | | 2cn 11905 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
45 | | 2ne0 11934 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
0 |
46 | | divneg 11524 |
. . . . . . . . . . . . . . 15
⊢ ((π
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) =
(-π / 2)) |
47 | 43, 44, 45, 46 | mp3an 1463 |
. . . . . . . . . . . . . 14
⊢ -(π /
2) = (-π / 2) |
48 | 34 | recni 10847 |
. . . . . . . . . . . . . . 15
⊢ -π
∈ ℂ |
49 | 48, 44, 45 | divreci 11577 |
. . . . . . . . . . . . . 14
⊢ (-π /
2) = (-π · (1 / 2)) |
50 | 47, 49 | eqtr2i 2766 |
. . . . . . . . . . . . 13
⊢ (-π
· (1 / 2)) = -(π / 2) |
51 | 43, 44, 45 | divreci 11577 |
. . . . . . . . . . . . . 14
⊢ (π /
2) = (π · (1 / 2)) |
52 | 51 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢ (π
· (1 / 2)) = (π / 2) |
53 | 34, 33, 42, 50, 52 | iccdili 13079 |
. . . . . . . . . . . 12
⊢
((ℑ‘(log‘𝐴)) ∈ (-π[,]π) →
((ℑ‘(log‘𝐴)) · (1 / 2)) ∈ (-(π /
2)[,](π / 2))) |
54 | 40, 53 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((ℑ‘(log‘𝐴)) · (1 / 2)) ∈ (-(π /
2)[,](π / 2))) |
55 | 30, 54 | eqeltrd 2838 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℑ‘((1 / 2) · (log‘𝐴))) ∈ (-(π / 2)[,](π /
2))) |
56 | | cosq14ge0 25401 |
. . . . . . . . . 10
⊢
((ℑ‘((1 / 2) · (log‘𝐴))) ∈ (-(π / 2)[,](π / 2)) →
0 ≤ (cos‘(ℑ‘((1 / 2) · (log‘𝐴))))) |
57 | 55, 56 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 0 ≤
(cos‘(ℑ‘((1 / 2) · (log‘𝐴))))) |
58 | 19, 21, 23, 57 | mulge0d 11409 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 0 ≤
((exp‘(ℜ‘((1 / 2) · (log‘𝐴)))) · (cos‘(ℑ‘((1
/ 2) · (log‘𝐴)))))) |
59 | | cxpef 25553 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ (1 / 2) ∈
ℂ) → (𝐴↑𝑐(1 / 2)) =
(exp‘((1 / 2) · (log‘𝐴)))) |
60 | 14, 59 | mp3an3 1452 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴↑𝑐(1 /
2)) = (exp‘((1 / 2) · (log‘𝐴)))) |
61 | | efeul 15723 |
. . . . . . . . . . . 12
⊢ (((1 / 2)
· (log‘𝐴))
∈ ℂ → (exp‘((1 / 2) · (log‘𝐴))) = ((exp‘(ℜ‘((1 / 2)
· (log‘𝐴))))
· ((cos‘(ℑ‘((1 / 2) · (log‘𝐴)))) + (i ·
(sin‘(ℑ‘((1 / 2) · (log‘𝐴)))))))) |
62 | 17, 61 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘((1 /
2) · (log‘𝐴)))
= ((exp‘(ℜ‘((1 / 2) · (log‘𝐴)))) · ((cos‘(ℑ‘((1
/ 2) · (log‘𝐴)))) + (i ·
(sin‘(ℑ‘((1 / 2) · (log‘𝐴)))))))) |
63 | 60, 62 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴↑𝑐(1 /
2)) = ((exp‘(ℜ‘((1 / 2) · (log‘𝐴)))) · ((cos‘(ℑ‘((1
/ 2) · (log‘𝐴)))) + (i ·
(sin‘(ℑ‘((1 / 2) · (log‘𝐴)))))))) |
64 | 63 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℜ‘(𝐴↑𝑐(1 / 2))) =
(ℜ‘((exp‘(ℜ‘((1 / 2) · (log‘𝐴)))) ·
((cos‘(ℑ‘((1 / 2) · (log‘𝐴)))) + (i ·
(sin‘(ℑ‘((1 / 2) · (log‘𝐴))))))))) |
65 | 21 | recnd 10861 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(cos‘(ℑ‘((1 / 2) · (log‘𝐴)))) ∈ ℂ) |
66 | 20 | resincld 15704 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(sin‘(ℑ‘((1 / 2) · (log‘𝐴)))) ∈ ℝ) |
67 | 66 | recnd 10861 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(sin‘(ℑ‘((1 / 2) · (log‘𝐴)))) ∈ ℂ) |
68 | | mulcl 10813 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (sin‘(ℑ‘((1 / 2) ·
(log‘𝐴)))) ∈
ℂ) → (i · (sin‘(ℑ‘((1 / 2) ·
(log‘𝐴))))) ∈
ℂ) |
69 | 1, 67, 68 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (i ·
(sin‘(ℑ‘((1 / 2) · (log‘𝐴))))) ∈ ℂ) |
70 | 65, 69 | addcld 10852 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((cos‘(ℑ‘((1 / 2) · (log‘𝐴)))) + (i ·
(sin‘(ℑ‘((1 / 2) · (log‘𝐴)))))) ∈ ℂ) |
71 | 19, 70 | remul2d 14790 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℜ‘((exp‘(ℜ‘((1 / 2) · (log‘𝐴)))) ·
((cos‘(ℑ‘((1 / 2) · (log‘𝐴)))) + (i ·
(sin‘(ℑ‘((1 / 2) · (log‘𝐴)))))))) = ((exp‘(ℜ‘((1 /
2) · (log‘𝐴)))) ·
(ℜ‘((cos‘(ℑ‘((1 / 2) · (log‘𝐴)))) + (i ·
(sin‘(ℑ‘((1 / 2) · (log‘𝐴))))))))) |
72 | 21, 66 | crred 14794 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℜ‘((cos‘(ℑ‘((1 / 2) · (log‘𝐴)))) + (i ·
(sin‘(ℑ‘((1 / 2) · (log‘𝐴))))))) = (cos‘(ℑ‘((1 / 2)
· (log‘𝐴))))) |
73 | 72 | oveq2d 7229 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((exp‘(ℜ‘((1 / 2) · (log‘𝐴)))) ·
(ℜ‘((cos‘(ℑ‘((1 / 2) · (log‘𝐴)))) + (i ·
(sin‘(ℑ‘((1 / 2) · (log‘𝐴)))))))) = ((exp‘(ℜ‘((1 /
2) · (log‘𝐴)))) · (cos‘(ℑ‘((1
/ 2) · (log‘𝐴)))))) |
74 | 64, 71, 73 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(ℜ‘(𝐴↑𝑐(1 / 2))) =
((exp‘(ℜ‘((1 / 2) · (log‘𝐴)))) · (cos‘(ℑ‘((1
/ 2) · (log‘𝐴)))))) |
75 | 58, 74 | breqtrrd 5081 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 0 ≤
(ℜ‘(𝐴↑𝑐(1 /
2)))) |
76 | 75 | adantr 484 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ 0 ≤ (ℜ‘(𝐴↑𝑐(1 /
2)))) |
77 | | simpr 488 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (𝐴↑𝑐(1 / 2)) =
-(√‘𝐴)) |
78 | 77 | fveq2d 6721 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (ℜ‘(𝐴↑𝑐(1 / 2))) =
(ℜ‘-(√‘𝐴))) |
79 | 3 | renegd 14772 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (ℜ‘-(√‘𝐴)) = -(ℜ‘(√‘𝐴))) |
80 | 78, 79 | eqtrd 2777 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (ℜ‘(𝐴↑𝑐(1 / 2))) =
-(ℜ‘(√‘𝐴))) |
81 | 76, 80 | breqtrd 5079 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ 0 ≤ -(ℜ‘(√‘𝐴))) |
82 | 3 | recld 14757 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (ℜ‘(√‘𝐴)) ∈ ℝ) |
83 | 82 | le0neg1d 11403 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((ℜ‘(√‘𝐴)) ≤ 0 ↔ 0 ≤
-(ℜ‘(√‘𝐴)))) |
84 | 81, 83 | mpbird 260 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (ℜ‘(√‘𝐴)) ≤ 0) |
85 | | sqrtrege0 14929 |
. . . . 5
⊢ (𝐴 ∈ ℂ → 0 ≤
(ℜ‘(√‘𝐴))) |
86 | 85 | ad2antrr 726 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ 0 ≤ (ℜ‘(√‘𝐴))) |
87 | | 0re 10835 |
. . . . 5
⊢ 0 ∈
ℝ |
88 | | letri3 10918 |
. . . . 5
⊢
(((ℜ‘(√‘𝐴)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((ℜ‘(√‘𝐴)) = 0 ↔
((ℜ‘(√‘𝐴)) ≤ 0 ∧ 0 ≤
(ℜ‘(√‘𝐴))))) |
89 | 82, 87, 88 | sylancl 589 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((ℜ‘(√‘𝐴)) = 0 ↔
((ℜ‘(√‘𝐴)) ≤ 0 ∧ 0 ≤
(ℜ‘(√‘𝐴))))) |
90 | 84, 86, 89 | mpbir2and 713 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (ℜ‘(√‘𝐴)) = 0) |
91 | 7, 12, 90 | 3eqtrd 2781 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (ℑ‘(i · (√‘𝐴))) = 0) |
92 | 5, 91 | reim0bd 14763 |
1
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (i · (√‘𝐴)) ∈ ℝ) |