This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 · ( √ ‘ 𝐴 ) ) ∈ ℝ )