Metamath Proof Explorer

Theorem cxpsqrtlem

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

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

Proof

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