Metamath Proof Explorer


Theorem cxpsqrtlem

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

Ref Expression
Assertion cxpsqrtlem ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( i · ( √ ‘ 𝐴 ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 ax-icn i ∈ ℂ
2 sqrtcl ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) ∈ ℂ )
3 2 ad2antrr ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( √ ‘ 𝐴 ) ∈ ℂ )
4 mulcl ( ( i ∈ ℂ ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( √ ‘ 𝐴 ) ) ∈ ℂ )
5 1 3 4 sylancr ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( i · ( √ ‘ 𝐴 ) ) ∈ ℂ )
6 imval ( ( i · ( √ ‘ 𝐴 ) ) ∈ ℂ → ( ℑ ‘ ( i · ( √ ‘ 𝐴 ) ) ) = ( ℜ ‘ ( ( i · ( √ ‘ 𝐴 ) ) / i ) ) )
7 5 6 syl ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℑ ‘ ( i · ( √ ‘ 𝐴 ) ) ) = ( ℜ ‘ ( ( i · ( √ ‘ 𝐴 ) ) / i ) ) )
8 ine0 i ≠ 0
9 divcan3 ( ( ( √ ‘ 𝐴 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( i · ( √ ‘ 𝐴 ) ) / i ) = ( √ ‘ 𝐴 ) )
10 1 8 9 mp3an23 ( ( √ ‘ 𝐴 ) ∈ ℂ → ( ( i · ( √ ‘ 𝐴 ) ) / i ) = ( √ ‘ 𝐴 ) )
11 3 10 syl ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ( i · ( √ ‘ 𝐴 ) ) / i ) = ( √ ‘ 𝐴 ) )
12 11 fveq2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( ( i · ( √ ‘ 𝐴 ) ) / i ) ) = ( ℜ ‘ ( √ ‘ 𝐴 ) ) )
13 halfre ( 1 / 2 ) ∈ ℝ
14 13 recni ( 1 / 2 ) ∈ ℂ
15 logcl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
16 mulcl ( ( ( 1 / 2 ) ∈ ℂ ∧ ( log ‘ 𝐴 ) ∈ ℂ ) → ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ∈ ℂ )
17 14 15 16 sylancr ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ∈ ℂ )
18 17 recld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ∈ ℝ )
19 18 reefcld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℝ )
20 17 imcld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ∈ ℝ )
21 20 recoscld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℝ )
22 18 rpefcld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℝ+ )
23 22 rpge0d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 0 ≤ ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) )
24 immul2 ( ( ( 1 / 2 ) ∈ ℝ ∧ ( log ‘ 𝐴 ) ∈ ℂ ) → ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) = ( ( 1 / 2 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
25 13 15 24 sylancr ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) = ( ( 1 / 2 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
26 15 imcld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
27 26 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
28 mulcom ( ( ( 1 / 2 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ) → ( ( 1 / 2 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) · ( 1 / 2 ) ) )
29 14 27 28 sylancr ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 1 / 2 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) · ( 1 / 2 ) ) )
30 25 29 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) · ( 1 / 2 ) ) )
31 logimcl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
32 31 simpld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
33 pire π ∈ ℝ
34 33 renegcli - π ∈ ℝ
35 ltle ( ( - π ∈ ℝ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
36 34 26 35 sylancr ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
37 32 36 mpd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) )
38 31 simprd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π )
39 34 33 elicc2i ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - π [,] π ) ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
40 26 37 38 39 syl3anbrc ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - π [,] π ) )
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 ‘ 𝐴 ) ) ∈ ( - π [,] π ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) · ( 1 / 2 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
54 40 53 syl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) · ( 1 / 2 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
55 30 54 eqeltrd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
56 cosq14ge0 ( ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 0 ≤ ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) )
57 55 56 syl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 0 ≤ ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) )
58 19 21 23 57 mulge0d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 0 ≤ ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) )
59 cxpef ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( 1 / 2 ) ∈ ℂ ) → ( 𝐴𝑐 ( 1 / 2 ) ) = ( exp ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) )
60 14 59 mp3an3 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴𝑐 ( 1 / 2 ) ) = ( exp ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) )
61 efeul ( ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ∈ ℂ → ( exp ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) = ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) )
62 17 61 syl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) = ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) )
63 60 62 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴𝑐 ( 1 / 2 ) ) = ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) )
64 63 fveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( 𝐴𝑐 ( 1 / 2 ) ) ) = ( ℜ ‘ ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) ) )
65 21 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℂ )
66 20 resincld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℝ )
67 66 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℂ )
68 mulcl ( ( i ∈ ℂ ∧ ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℂ ) → ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ∈ ℂ )
69 1 67 68 sylancr ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ∈ ℂ )
70 65 69 addcld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ∈ ℂ )
71 19 70 remul2d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 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 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) = ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) )
73 72 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 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 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( 𝐴𝑐 ( 1 / 2 ) ) ) = ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) )
75 58 74 breqtrrd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 0 ≤ ( ℜ ‘ ( 𝐴𝑐 ( 1 / 2 ) ) ) )
76 75 adantr ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( 𝐴𝑐 ( 1 / 2 ) ) ) )
77 simpr ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) )
78 77 fveq2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴𝑐 ( 1 / 2 ) ) ) = ( ℜ ‘ - ( √ ‘ 𝐴 ) ) )
79 3 renegd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ - ( √ ‘ 𝐴 ) ) = - ( ℜ ‘ ( √ ‘ 𝐴 ) ) )
80 78 79 eqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴𝑐 ( 1 / 2 ) ) ) = - ( ℜ ‘ ( √ ‘ 𝐴 ) ) )
81 76 80 breqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → 0 ≤ - ( ℜ ‘ ( √ ‘ 𝐴 ) ) )
82 3 recld ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( √ ‘ 𝐴 ) ) ∈ ℝ )
83 82 le0neg1d ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) ≤ 0 ↔ 0 ≤ - ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) )
84 81 83 mpbird ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( √ ‘ 𝐴 ) ) ≤ 0 )
85 sqrtrege0 ( 𝐴 ∈ ℂ → 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) )
86 85 ad2antrr ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) )
87 0re 0 ∈ ℝ
88 letri3 ( ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) = 0 ↔ ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) ≤ 0 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) ) )
89 82 87 88 sylancl ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) = 0 ↔ ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) ≤ 0 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) ) )
90 84 86 89 mpbir2and ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( √ ‘ 𝐴 ) ) = 0 )
91 7 12 90 3eqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℑ ‘ ( i · ( √ ‘ 𝐴 ) ) ) = 0 )
92 5 91 reim0bd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( i · ( √ ‘ 𝐴 ) ) ∈ ℝ )