Metamath Proof Explorer

Theorem cxpsqrtlem

Description: Lemma for cxpsqrt . (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpsqrtlem ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → i ⁢ A ∈ ℝ

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 sqrtcl ⊢ A ∈ ℂ → A ∈ ℂ
3 2 ad2antrr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → A ∈ ℂ
4 mulcl ⊢ i ∈ ℂ ∧ A ∈ ℂ → i ⁢ A ∈ ℂ
5 1 3 4 sylancr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → i ⁢ A ∈ ℂ
6 imval ⊢ i ⁢ A ∈ ℂ → ℑ ⁡ i ⁢ A = ℜ ⁡ i ⁢ A i
7 5 6 syl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → ℑ ⁡ i ⁢ A = ℜ ⁡ i ⁢ A i
8 ine0 ⊢ i ≠ 0
9 divcan3 ⊢ A ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 → i ⁢ A i = A
10 1 8 9 mp3an23 ⊢ A ∈ ℂ → i ⁢ A i = A
11 3 10 syl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → i ⁢ A i = A
12 11 fveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → ℜ ⁡ i ⁢ A i = ℜ ⁡ A
13 halfre ⊢ 1 2 ∈ ℝ
14 13 recni ⊢ 1 2 ∈ ℂ
15 logcl ⊢ A ∈ ℂ ∧ A ≠ 0 → log ⁡ A ∈ ℂ
16 mulcl ⊢ 1 2 ∈ ℂ ∧ log ⁡ A ∈ ℂ → 1 2 ⁢ log ⁡ A ∈ ℂ
17 14 15 16 sylancr ⊢ A ∈ ℂ ∧ A ≠ 0 → 1 2 ⁢ log ⁡ A ∈ ℂ
18 17 recld ⊢ A ∈ ℂ ∧ A ≠ 0 → ℜ ⁡ 1 2 ⁢ log ⁡ A ∈ ℝ
19 18 reefcld ⊢ A ∈ ℂ ∧ A ≠ 0 → e ℜ ⁡ 1 2 ⁢ log ⁡ A ∈ ℝ
20 17 imcld ⊢ A ∈ ℂ ∧ A ≠ 0 → ℑ ⁡ 1 2 ⁢ log ⁡ A ∈ ℝ
21 20 recoscld ⊢ A ∈ ℂ ∧ A ≠ 0 → cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A ∈ ℝ
22 18 rpefcld ⊢ A ∈ ℂ ∧ A ≠ 0 → e ℜ ⁡ 1 2 ⁢ log ⁡ A ∈ ℝ +
23 22 rpge0d ⊢ A ∈ ℂ ∧ A ≠ 0 → 0 ≤ e ℜ ⁡ 1 2 ⁢ log ⁡ A
24 immul2 ⊢ 1 2 ∈ ℝ ∧ log ⁡ A ∈ ℂ → ℑ ⁡ 1 2 ⁢ log ⁡ A = 1 2 ⁢ ℑ ⁡ log ⁡ A
25 13 15 24 sylancr ⊢ A ∈ ℂ ∧ A ≠ 0 → ℑ ⁡ 1 2 ⁢ log ⁡ A = 1 2 ⁢ ℑ ⁡ log ⁡ A
26 15 imcld ⊢ A ∈ ℂ ∧ A ≠ 0 → ℑ ⁡ log ⁡ A ∈ ℝ
27 26 recnd ⊢ A ∈ ℂ ∧ A ≠ 0 → ℑ ⁡ log ⁡ A ∈ ℂ
28 mulcom ⊢ 1 2 ∈ ℂ ∧ ℑ ⁡ log ⁡ A ∈ ℂ → 1 2 ⁢ ℑ ⁡ log ⁡ A = ℑ ⁡ log ⁡ A ⁢ 1 2
29 14 27 28 sylancr ⊢ A ∈ ℂ ∧ A ≠ 0 → 1 2 ⁢ ℑ ⁡ log ⁡ A = ℑ ⁡ log ⁡ A ⁢ 1 2
30 25 29 eqtrd ⊢ A ∈ ℂ ∧ A ≠ 0 → ℑ ⁡ 1 2 ⁢ log ⁡ A = ℑ ⁡ log ⁡ A ⁢ 1 2
31 logimcl ⊢ A ∈ ℂ ∧ A ≠ 0 → − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
32 31 simpld ⊢ A ∈ ℂ ∧ A ≠ 0 → − π < ℑ ⁡ log ⁡ A
33 pire ⊢ π ∈ ℝ
34 33 renegcli ⊢ − π ∈ ℝ
35 ltle ⊢ − π ∈ ℝ ∧ ℑ ⁡ log ⁡ A ∈ ℝ → − π < ℑ ⁡ log ⁡ A → − π ≤ ℑ ⁡ log ⁡ A
36 34 26 35 sylancr ⊢ A ∈ ℂ ∧ A ≠ 0 → − π < ℑ ⁡ log ⁡ A → − π ≤ ℑ ⁡ log ⁡ A
37 32 36 mpd ⊢ A ∈ ℂ ∧ A ≠ 0 → − π ≤ ℑ ⁡ log ⁡ A
38 31 simprd ⊢ A ∈ ℂ ∧ A ≠ 0 → ℑ ⁡ log ⁡ A ≤ π
39 34 33 elicc2i ⊢ ℑ ⁡ log ⁡ A ∈ − π π ↔ ℑ ⁡ log ⁡ A ∈ ℝ ∧ − π ≤ ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
40 26 37 38 39 syl3anbrc ⊢ A ∈ ℂ ∧ A ≠ 0 → ℑ ⁡ log ⁡ A ∈ − π π
41 halfgt0 ⊢ 0 < 1 2
42 13 41 elrpii ⊢ 1 2 ∈ ℝ +
43 33 recni ⊢ π ∈ ℂ
44 2cn ⊢ 2 ∈ ℂ
45 2ne0 ⊢ 2 ≠ 0
46 divneg ⊢ π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → − π 2 = − π 2
47 43 44 45 46 mp3an ⊢ − π 2 = − π 2
48 34 recni ⊢ − π ∈ ℂ
49 48 44 45 divreci ⊢ − π 2 = − π ⁢ 1 2
50 47 49 eqtr2i ⊢ − π ⁢ 1 2 = − π 2
51 43 44 45 divreci ⊢ π 2 = π ⁢ 1 2
52 51 eqcomi ⊢ π ⁢ 1 2 = π 2
53 34 33 42 50 52 iccdili ⊢ ℑ ⁡ log ⁡ A ∈ − π π → ℑ ⁡ log ⁡ A ⁢ 1 2 ∈ − π 2 π 2
54 40 53 syl ⊢ A ∈ ℂ ∧ A ≠ 0 → ℑ ⁡ log ⁡ A ⁢ 1 2 ∈ − π 2 π 2
55 30 54 eqeltrd ⊢ A ∈ ℂ ∧ A ≠ 0 → ℑ ⁡ 1 2 ⁢ log ⁡ A ∈ − π 2 π 2
56 cosq14ge0 ⊢ ℑ ⁡ 1 2 ⁢ log ⁡ A ∈ − π 2 π 2 → 0 ≤ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A
57 55 56 syl ⊢ A ∈ ℂ ∧ A ≠ 0 → 0 ≤ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A
58 19 21 23 57 mulge0d ⊢ A ∈ ℂ ∧ A ≠ 0 → 0 ≤ e ℜ ⁡ 1 2 ⁢ log ⁡ A ⁢ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A
59 cxpef ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ 1 2 ∈ ℂ → A 1 2 = e 1 2 ⁢ log ⁡ A
60 14 59 mp3an3 ⊢ A ∈ ℂ ∧ A ≠ 0 → A 1 2 = e 1 2 ⁢ log ⁡ A
61 efeul ⊢ 1 2 ⁢ log ⁡ A ∈ ℂ → e 1 2 ⁢ log ⁡ A = e ℜ ⁡ 1 2 ⁢ log ⁡ A ⁢ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A + i ⁢ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A
62 17 61 syl ⊢ A ∈ ℂ ∧ A ≠ 0 → e 1 2 ⁢ log ⁡ A = e ℜ ⁡ 1 2 ⁢ log ⁡ A ⁢ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A + i ⁢ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A
63 60 62 eqtrd ⊢ A ∈ ℂ ∧ A ≠ 0 → A 1 2 = e ℜ ⁡ 1 2 ⁢ log ⁡ A ⁢ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A + i ⁢ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A
64 63 fveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 → ℜ ⁡ A 1 2 = ℜ ⁡ e ℜ ⁡ 1 2 ⁢ log ⁡ A ⁢ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A + i ⁢ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A
65 21 recnd ⊢ A ∈ ℂ ∧ A ≠ 0 → cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A ∈ ℂ
66 20 resincld ⊢ A ∈ ℂ ∧ A ≠ 0 → sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A ∈ ℝ
67 66 recnd ⊢ A ∈ ℂ ∧ A ≠ 0 → sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A ∈ ℂ
68 mulcl ⊢ i ∈ ℂ ∧ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A ∈ ℂ → i ⁢ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A ∈ ℂ
69 1 67 68 sylancr ⊢ A ∈ ℂ ∧ A ≠ 0 → i ⁢ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A ∈ ℂ
70 65 69 addcld ⊢ A ∈ ℂ ∧ A ≠ 0 → cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A + i ⁢ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A ∈ ℂ
71 19 70 remul2d ⊢ A ∈ ℂ ∧ A ≠ 0 → ℜ ⁡ e ℜ ⁡ 1 2 ⁢ log ⁡ A ⁢ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A + i ⁢ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A = e ℜ ⁡ 1 2 ⁢ log ⁡ A ⁢ ℜ ⁡ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A + i ⁢ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A
72 21 66 crred ⊢ A ∈ ℂ ∧ A ≠ 0 → ℜ ⁡ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A + i ⁢ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A = cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A
73 72 oveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 → e ℜ ⁡ 1 2 ⁢ log ⁡ A ⁢ ℜ ⁡ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A + i ⁢ sin ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A = e ℜ ⁡ 1 2 ⁢ log ⁡ A ⁢ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A
74 64 71 73 3eqtrd ⊢ A ∈ ℂ ∧ A ≠ 0 → ℜ ⁡ A 1 2 = e ℜ ⁡ 1 2 ⁢ log ⁡ A ⁢ cos ⁡ ℑ ⁡ 1 2 ⁢ log ⁡ A
75 58 74 breqtrrd ⊢ A ∈ ℂ ∧ A ≠ 0 → 0 ≤ ℜ ⁡ A 1 2
76 75 adantr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → 0 ≤ ℜ ⁡ A 1 2
77 simpr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → A 1 2 = − A
78 77 fveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → ℜ ⁡ A 1 2 = ℜ ⁡ − A
79 3 renegd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → ℜ ⁡ − A = − ℜ ⁡ A
80 78 79 eqtrd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → ℜ ⁡ A 1 2 = − ℜ ⁡ A
81 76 80 breqtrd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → 0 ≤ − ℜ ⁡ A
82 3 recld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → ℜ ⁡ A ∈ ℝ
83 82 le0neg1d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → ℜ ⁡ A ≤ 0 ↔ 0 ≤ − ℜ ⁡ A
84 81 83 mpbird ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → ℜ ⁡ A ≤ 0
85 sqrtrege0 ⊢ A ∈ ℂ → 0 ≤ ℜ ⁡ A
86 85 ad2antrr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → 0 ≤ ℜ ⁡ A
87 0re ⊢ 0 ∈ ℝ
88 letri3 ⊢ ℜ ⁡ A ∈ ℝ ∧ 0 ∈ ℝ → ℜ ⁡ A = 0 ↔ ℜ ⁡ A ≤ 0 ∧ 0 ≤ ℜ ⁡ A
89 82 87 88 sylancl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → ℜ ⁡ A = 0 ↔ ℜ ⁡ A ≤ 0 ∧ 0 ≤ ℜ ⁡ A
90 84 86 89 mpbir2and ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → ℜ ⁡ A = 0
91 7 12 90 3eqtrd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → ℑ ⁡ i ⁢ A = 0
92 5 91 reim0bd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A 1 2 = − A → i ⁢ A ∈ ℝ