Proof of Theorem cxpsqrt
Step | Hyp | Ref
| Expression |
1 | | halfcn 11247 |
. . . . . 6
⊢ (1 / 2)
∈ ℂ |
2 | | halfre 11246 |
. . . . . . 7
⊢ (1 / 2)
∈ ℝ |
3 | | halfgt0 11248 |
. . . . . . 7
⊢ 0 < (1
/ 2) |
4 | 2, 3 | gt0ne0ii 10564 |
. . . . . 6
⊢ (1 / 2)
≠ 0 |
5 | | 0cxp 24412 |
. . . . . 6
⊢ (((1 / 2)
∈ ℂ ∧ (1 / 2) ≠ 0) → (0↑𝑐(1 /
2)) = 0) |
6 | 1, 4, 5 | mp2an 708 |
. . . . 5
⊢
(0↑𝑐(1 / 2)) = 0 |
7 | | sqrt0 13982 |
. . . . 5
⊢
(√‘0) = 0 |
8 | 6, 7 | eqtr4i 2647 |
. . . 4
⊢
(0↑𝑐(1 / 2)) =
(√‘0) |
9 | | oveq1 6657 |
. . . 4
⊢ (𝐴 = 0 → (𝐴↑𝑐(1 / 2)) =
(0↑𝑐(1 / 2))) |
10 | | fveq2 6191 |
. . . 4
⊢ (𝐴 = 0 → (√‘𝐴) =
(√‘0)) |
11 | 8, 9, 10 | 3eqtr4a 2682 |
. . 3
⊢ (𝐴 = 0 → (𝐴↑𝑐(1 / 2)) =
(√‘𝐴)) |
12 | 11 | a1i 11 |
. 2
⊢ (𝐴 ∈ ℂ → (𝐴 = 0 → (𝐴↑𝑐(1 / 2)) =
(√‘𝐴))) |
13 | | ax-icn 9995 |
. . . . . . . . . . . . . . . . 17
⊢ i ∈
ℂ |
14 | | sqrtcl 14101 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
(√‘𝐴) ∈
ℂ) |
15 | 14 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (√‘𝐴)
∈ ℂ) |
16 | | sqmul 12926 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ (√‘𝐴) ∈ ℂ) → ((i ·
(√‘𝐴))↑2)
= ((i↑2) · ((√‘𝐴)↑2))) |
17 | 13, 15, 16 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((i · (√‘𝐴))↑2) = ((i↑2) ·
((√‘𝐴)↑2))) |
18 | | i2 12965 |
. . . . . . . . . . . . . . . . . 18
⊢
(i↑2) = -1 |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (i↑2) = -1) |
20 | | sqrtth 14104 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((√‘𝐴)↑2)
= 𝐴) |
21 | 20 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((√‘𝐴)↑2) = 𝐴) |
22 | 19, 21 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((i↑2) · ((√‘𝐴)↑2)) = (-1 · 𝐴)) |
23 | | mulm1 10471 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → (-1
· 𝐴) = -𝐴) |
24 | 23 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (-1 · 𝐴) =
-𝐴) |
25 | 17, 22, 24 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((i · (√‘𝐴))↑2) = -𝐴) |
26 | | cxpsqrtlem 24448 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (i · (√‘𝐴)) ∈ ℝ) |
27 | 26 | resqcld 13035 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((i · (√‘𝐴))↑2) ∈ ℝ) |
28 | 25, 27 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ -𝐴 ∈
ℝ) |
29 | | negeq0 10335 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ ℂ → (𝐴 = 0 ↔ -𝐴 = 0)) |
30 | 29 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ -𝐴 ≠ 0)) |
31 | 30 | biimpa 501 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -𝐴 ≠ 0) |
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ -𝐴 ≠
0) |
33 | 25, 32 | eqnetrd 2861 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((i · (√‘𝐴))↑2) ≠ 0) |
34 | | sq0i 12956 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
· (√‘𝐴))
= 0 → ((i · (√‘𝐴))↑2) = 0) |
35 | 34 | necon3i 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (((i
· (√‘𝐴))↑2) ≠ 0 → (i ·
(√‘𝐴)) ≠
0) |
36 | 33, 35 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (i · (√‘𝐴)) ≠ 0) |
37 | 26, 36 | sqgt0d 13037 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ 0 < ((i · (√‘𝐴))↑2)) |
38 | 37, 25 | breqtrd 4679 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ 0 < -𝐴) |
39 | 28, 38 | elrpd 11869 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ -𝐴 ∈
ℝ+) |
40 | | logneg 24334 |
. . . . . . . . . . . . 13
⊢ (-𝐴 ∈ ℝ+
→ (log‘--𝐴) =
((log‘-𝐴) + (i
· π))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (log‘--𝐴) =
((log‘-𝐴) + (i
· π))) |
42 | | negneg 10331 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴) |
43 | 42 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ --𝐴 = 𝐴) |
44 | 43 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (log‘--𝐴) =
(log‘𝐴)) |
45 | 39 | relogcld 24369 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (log‘-𝐴)
∈ ℝ) |
46 | 45 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (log‘-𝐴)
∈ ℂ) |
47 | | picn 24211 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℂ |
48 | 13, 47 | mulcli 10045 |
. . . . . . . . . . . . 13
⊢ (i
· π) ∈ ℂ |
49 | | addcom 10222 |
. . . . . . . . . . . . 13
⊢
(((log‘-𝐴)
∈ ℂ ∧ (i · π) ∈ ℂ) →
((log‘-𝐴) + (i
· π)) = ((i · π) + (log‘-𝐴))) |
50 | 46, 48, 49 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((log‘-𝐴) + (i
· π)) = ((i · π) + (log‘-𝐴))) |
51 | 41, 44, 50 | 3eqtr3d 2664 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (log‘𝐴) = ((i
· π) + (log‘-𝐴))) |
52 | 51 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((1 / 2) · (log‘𝐴)) = ((1 / 2) · ((i · π) +
(log‘-𝐴)))) |
53 | | adddi 10025 |
. . . . . . . . . . . 12
⊢ (((1 / 2)
∈ ℂ ∧ (i · π) ∈ ℂ ∧ (log‘-𝐴) ∈ ℂ) → ((1 /
2) · ((i · π) + (log‘-𝐴))) = (((1 / 2) · (i · π))
+ ((1 / 2) · (log‘-𝐴)))) |
54 | 1, 48, 53 | mp3an12 1414 |
. . . . . . . . . . 11
⊢
((log‘-𝐴)
∈ ℂ → ((1 / 2) · ((i · π) + (log‘-𝐴))) = (((1 / 2) · (i
· π)) + ((1 / 2) · (log‘-𝐴)))) |
55 | 46, 54 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((1 / 2) · ((i · π) + (log‘-𝐴))) = (((1 / 2) · (i · π))
+ ((1 / 2) · (log‘-𝐴)))) |
56 | 52, 55 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((1 / 2) · (log‘𝐴)) = (((1 / 2) · (i · π)) +
((1 / 2) · (log‘-𝐴)))) |
57 | | 2cn 11091 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
58 | | 2ne0 11113 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
59 | | divrec2 10702 |
. . . . . . . . . . . 12
⊢ (((i
· π) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((i
· π) / 2) = ((1 / 2) · (i · π))) |
60 | 48, 57, 58, 59 | mp3an 1424 |
. . . . . . . . . . 11
⊢ ((i
· π) / 2) = ((1 / 2) · (i · π)) |
61 | 13, 47, 57, 58 | divassi 10781 |
. . . . . . . . . . 11
⊢ ((i
· π) / 2) = (i · (π / 2)) |
62 | 60, 61 | eqtr3i 2646 |
. . . . . . . . . 10
⊢ ((1 / 2)
· (i · π)) = (i · (π / 2)) |
63 | 62 | oveq1i 6660 |
. . . . . . . . 9
⊢ (((1 / 2)
· (i · π)) + ((1 / 2) · (log‘-𝐴))) = ((i · (π / 2)) + ((1 / 2)
· (log‘-𝐴))) |
64 | 56, 63 | syl6eq 2672 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((1 / 2) · (log‘𝐴)) = ((i · (π / 2)) + ((1 / 2)
· (log‘-𝐴)))) |
65 | 64 | fveq2d 6195 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (exp‘((1 / 2) · (log‘𝐴))) = (exp‘((i · (π / 2)) +
((1 / 2) · (log‘-𝐴))))) |
66 | 47, 57, 58 | divcli 10767 |
. . . . . . . . 9
⊢ (π /
2) ∈ ℂ |
67 | 13, 66 | mulcli 10045 |
. . . . . . . 8
⊢ (i
· (π / 2)) ∈ ℂ |
68 | | mulcl 10020 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℂ ∧ (log‘-𝐴) ∈ ℂ) → ((1 / 2) ·
(log‘-𝐴)) ∈
ℂ) |
69 | 1, 46, 68 | sylancr 695 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((1 / 2) · (log‘-𝐴)) ∈ ℂ) |
70 | | efadd 14824 |
. . . . . . . 8
⊢ (((i
· (π / 2)) ∈ ℂ ∧ ((1 / 2) · (log‘-𝐴)) ∈ ℂ) →
(exp‘((i · (π / 2)) + ((1 / 2) · (log‘-𝐴)))) = ((exp‘(i ·
(π / 2))) · (exp‘((1 / 2) · (log‘-𝐴))))) |
71 | 67, 69, 70 | sylancr 695 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (exp‘((i · (π / 2)) + ((1 / 2) ·
(log‘-𝐴)))) =
((exp‘(i · (π / 2))) · (exp‘((1 / 2) ·
(log‘-𝐴))))) |
72 | | efhalfpi 24223 |
. . . . . . . . 9
⊢
(exp‘(i · (π / 2))) = i |
73 | 72 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (exp‘(i · (π / 2))) = i) |
74 | | negcl 10281 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) |
75 | 74 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ -𝐴 ∈
ℂ) |
76 | 1 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (1 / 2) ∈ ℂ) |
77 | | cxpef 24411 |
. . . . . . . . . 10
⊢ ((-𝐴 ∈ ℂ ∧ -𝐴 ≠ 0 ∧ (1 / 2) ∈
ℂ) → (-𝐴↑𝑐(1 / 2)) =
(exp‘((1 / 2) · (log‘-𝐴)))) |
78 | 75, 32, 76, 77 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (-𝐴↑𝑐(1 / 2)) =
(exp‘((1 / 2) · (log‘-𝐴)))) |
79 | | ax-1cn 9994 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
80 | | 2halves 11260 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℂ → ((1 / 2) + (1 / 2)) = 1) |
81 | 79, 80 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((1 / 2)
+ (1 / 2)) = 1 |
82 | 81 | oveq2i 6661 |
. . . . . . . . . . . 12
⊢ (-𝐴↑𝑐((1 /
2) + (1 / 2))) = (-𝐴↑𝑐1) |
83 | | cxp1 24417 |
. . . . . . . . . . . . 13
⊢ (-𝐴 ∈ ℂ → (-𝐴↑𝑐1) =
-𝐴) |
84 | 75, 83 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (-𝐴↑𝑐1) = -𝐴) |
85 | 82, 84 | syl5eq 2668 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (-𝐴↑𝑐((1 / 2) + (1 /
2))) = -𝐴) |
86 | | rpcxpcl 24422 |
. . . . . . . . . . . . . . 15
⊢ ((-𝐴 ∈ ℝ+
∧ (1 / 2) ∈ ℝ) → (-𝐴↑𝑐(1 / 2)) ∈
ℝ+) |
87 | 39, 2, 86 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (-𝐴↑𝑐(1 / 2)) ∈
ℝ+) |
88 | 87 | rpcnd 11874 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (-𝐴↑𝑐(1 / 2)) ∈
ℂ) |
89 | 88 | sqvald 13005 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((-𝐴↑𝑐(1 / 2))↑2) =
((-𝐴↑𝑐(1 / 2)) ·
(-𝐴↑𝑐(1 /
2)))) |
90 | | cxpadd 24425 |
. . . . . . . . . . . . 13
⊢ (((-𝐴 ∈ ℂ ∧ -𝐴 ≠ 0) ∧ (1 / 2) ∈
ℂ ∧ (1 / 2) ∈ ℂ) → (-𝐴↑𝑐((1 / 2) + (1 /
2))) = ((-𝐴↑𝑐(1 / 2)) ·
(-𝐴↑𝑐(1 /
2)))) |
91 | 75, 32, 76, 76, 90 | syl211anc 1332 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (-𝐴↑𝑐((1 / 2) + (1 /
2))) = ((-𝐴↑𝑐(1 / 2)) ·
(-𝐴↑𝑐(1 /
2)))) |
92 | 89, 91 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((-𝐴↑𝑐(1 / 2))↑2) =
(-𝐴↑𝑐((1 / 2) + (1 /
2)))) |
93 | 75 | sqsqrtd 14178 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((√‘-𝐴)↑2) = -𝐴) |
94 | 85, 92, 93 | 3eqtr4d 2666 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((-𝐴↑𝑐(1 / 2))↑2) =
((√‘-𝐴)↑2)) |
95 | 87 | rprege0d 11879 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((-𝐴↑𝑐(1 / 2)) ∈
ℝ ∧ 0 ≤ (-𝐴↑𝑐(1 /
2)))) |
96 | 39 | rpsqrtcld 14150 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (√‘-𝐴)
∈ ℝ+) |
97 | 96 | rprege0d 11879 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((√‘-𝐴)
∈ ℝ ∧ 0 ≤ (√‘-𝐴))) |
98 | | sq11 12936 |
. . . . . . . . . . 11
⊢
((((-𝐴↑𝑐(1 / 2)) ∈
ℝ ∧ 0 ≤ (-𝐴↑𝑐(1 / 2))) ∧
((√‘-𝐴) ∈
ℝ ∧ 0 ≤ (√‘-𝐴))) → (((-𝐴↑𝑐(1 / 2))↑2) =
((√‘-𝐴)↑2)
↔ (-𝐴↑𝑐(1 / 2)) =
(√‘-𝐴))) |
99 | 95, 97, 98 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (((-𝐴↑𝑐(1 / 2))↑2) =
((√‘-𝐴)↑2)
↔ (-𝐴↑𝑐(1 / 2)) =
(√‘-𝐴))) |
100 | 94, 99 | mpbid 222 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (-𝐴↑𝑐(1 / 2)) =
(√‘-𝐴)) |
101 | 78, 100 | eqtr3d 2658 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (exp‘((1 / 2) · (log‘-𝐴))) = (√‘-𝐴)) |
102 | 73, 101 | oveq12d 6668 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ ((exp‘(i · (π / 2))) · (exp‘((1 / 2)
· (log‘-𝐴))))
= (i · (√‘-𝐴))) |
103 | 65, 71, 102 | 3eqtrd 2660 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (exp‘((1 / 2) · (log‘𝐴))) = (i · (√‘-𝐴))) |
104 | | cxpef 24411 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ (1 / 2) ∈
ℂ) → (𝐴↑𝑐(1 / 2)) =
(exp‘((1 / 2) · (log‘𝐴)))) |
105 | 1, 104 | mp3an3 1413 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴↑𝑐(1 /
2)) = (exp‘((1 / 2) · (log‘𝐴)))) |
106 | 105 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (𝐴↑𝑐(1 / 2)) =
(exp‘((1 / 2) · (log‘𝐴)))) |
107 | 43 | fveq2d 6195 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (√‘--𝐴)
= (√‘𝐴)) |
108 | 39 | rpge0d 11876 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ 0 ≤ -𝐴) |
109 | 28, 108 | sqrtnegd 14160 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (√‘--𝐴)
= (i · (√‘-𝐴))) |
110 | 107, 109 | eqtr3d 2658 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (√‘𝐴) =
(i · (√‘-𝐴))) |
111 | 103, 106,
110 | 3eqtr4d 2666 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴))
→ (𝐴↑𝑐(1 / 2)) =
(√‘𝐴)) |
112 | 111 | ex 450 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝐴↑𝑐(1 /
2)) = -(√‘𝐴)
→ (𝐴↑𝑐(1 / 2)) =
(√‘𝐴))) |
113 | 81 | oveq2i 6661 |
. . . . . . . . 9
⊢ (𝐴↑𝑐((1 /
2) + (1 / 2))) = (𝐴↑𝑐1) |
114 | | cxpadd 24425 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (1 / 2) ∈
ℂ ∧ (1 / 2) ∈ ℂ) → (𝐴↑𝑐((1 / 2) + (1 /
2))) = ((𝐴↑𝑐(1 / 2)) ·
(𝐴↑𝑐(1 /
2)))) |
115 | 1, 1, 114 | mp3an23 1416 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴↑𝑐((1 /
2) + (1 / 2))) = ((𝐴↑𝑐(1 / 2)) ·
(𝐴↑𝑐(1 /
2)))) |
116 | | cxp1 24417 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐1) =
𝐴) |
117 | 116 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴↑𝑐1) =
𝐴) |
118 | 113, 115,
117 | 3eqtr3a 2680 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝐴↑𝑐(1 /
2)) · (𝐴↑𝑐(1 / 2))) = 𝐴) |
119 | | cxpcl 24420 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ (1 / 2)
∈ ℂ) → (𝐴↑𝑐(1 / 2)) ∈
ℂ) |
120 | 1, 119 | mpan2 707 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐(1 /
2)) ∈ ℂ) |
121 | 120 | sqvald 13005 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((𝐴↑𝑐(1 /
2))↑2) = ((𝐴↑𝑐(1 / 2)) ·
(𝐴↑𝑐(1 /
2)))) |
122 | 121 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝐴↑𝑐(1 /
2))↑2) = ((𝐴↑𝑐(1 / 2)) ·
(𝐴↑𝑐(1 /
2)))) |
123 | 20 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((√‘𝐴)↑2)
= 𝐴) |
124 | 118, 122,
123 | 3eqtr4d 2666 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝐴↑𝑐(1 /
2))↑2) = ((√‘𝐴)↑2)) |
125 | | sqeqor 12978 |
. . . . . . . . 9
⊢ (((𝐴↑𝑐(1 /
2)) ∈ ℂ ∧ (√‘𝐴) ∈ ℂ) → (((𝐴↑𝑐(1 /
2))↑2) = ((√‘𝐴)↑2) ↔ ((𝐴↑𝑐(1 / 2)) =
(√‘𝐴) ∨
(𝐴↑𝑐(1 / 2)) =
-(√‘𝐴)))) |
126 | 120, 14, 125 | syl2anc 693 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (((𝐴↑𝑐(1 /
2))↑2) = ((√‘𝐴)↑2) ↔ ((𝐴↑𝑐(1 / 2)) =
(√‘𝐴) ∨
(𝐴↑𝑐(1 / 2)) =
-(√‘𝐴)))) |
127 | 126 | biimpa 501 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ ((𝐴↑𝑐(1 /
2))↑2) = ((√‘𝐴)↑2)) → ((𝐴↑𝑐(1 / 2)) =
(√‘𝐴) ∨
(𝐴↑𝑐(1 / 2)) =
-(√‘𝐴))) |
128 | 124, 127 | syldan 487 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝐴↑𝑐(1 /
2)) = (√‘𝐴)
∨ (𝐴↑𝑐(1 / 2)) =
-(√‘𝐴))) |
129 | 128 | ord 392 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (¬ (𝐴↑𝑐(1 /
2)) = (√‘𝐴)
→ (𝐴↑𝑐(1 / 2)) =
-(√‘𝐴))) |
130 | 129 | con1d 139 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (¬ (𝐴↑𝑐(1 /
2)) = -(√‘𝐴)
→ (𝐴↑𝑐(1 / 2)) =
(√‘𝐴))) |
131 | 112, 130 | pm2.61d 170 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴↑𝑐(1 /
2)) = (√‘𝐴)) |
132 | 131 | ex 450 |
. 2
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 → (𝐴↑𝑐(1 /
2)) = (√‘𝐴))) |
133 | 12, 132 | pm2.61dne 2880 |
1
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐(1 /
2)) = (√‘𝐴)) |