Step |
Hyp |
Ref |
Expression |
1 |
|
ax-icn |
⊢ i ∈ ℂ |
2 |
|
resqrtcl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ ) |
3 |
|
recn |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( √ ‘ 𝐴 ) ∈ ℂ ) |
4 |
2 3
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℂ ) |
5 |
|
sqmul |
⊢ ( ( i ∈ ℂ ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) → ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = ( ( i ↑ 2 ) · ( ( √ ‘ 𝐴 ) ↑ 2 ) ) ) |
6 |
1 4 5
|
sylancr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = ( ( i ↑ 2 ) · ( ( √ ‘ 𝐴 ) ↑ 2 ) ) ) |
7 |
|
i2 |
⊢ ( i ↑ 2 ) = - 1 |
8 |
7
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( i ↑ 2 ) = - 1 ) |
9 |
|
resqrtth |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ) |
10 |
8 9
|
oveq12d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( i ↑ 2 ) · ( ( √ ‘ 𝐴 ) ↑ 2 ) ) = ( - 1 · 𝐴 ) ) |
11 |
|
recn |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) |
12 |
11
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℂ ) |
13 |
12
|
mulm1d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( - 1 · 𝐴 ) = - 𝐴 ) |
14 |
6 10 13
|
3eqtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = - 𝐴 ) |
15 |
|
renegcl |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → - ( √ ‘ 𝐴 ) ∈ ℝ ) |
16 |
|
0re |
⊢ 0 ∈ ℝ |
17 |
|
reim0 |
⊢ ( - ( √ ‘ 𝐴 ) ∈ ℝ → ( ℑ ‘ - ( √ ‘ 𝐴 ) ) = 0 ) |
18 |
|
recn |
⊢ ( - ( √ ‘ 𝐴 ) ∈ ℝ → - ( √ ‘ 𝐴 ) ∈ ℂ ) |
19 |
|
imre |
⊢ ( - ( √ ‘ 𝐴 ) ∈ ℂ → ( ℑ ‘ - ( √ ‘ 𝐴 ) ) = ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) ) |
20 |
18 19
|
syl |
⊢ ( - ( √ ‘ 𝐴 ) ∈ ℝ → ( ℑ ‘ - ( √ ‘ 𝐴 ) ) = ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) ) |
21 |
17 20
|
eqtr3d |
⊢ ( - ( √ ‘ 𝐴 ) ∈ ℝ → 0 = ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) ) |
22 |
|
eqle |
⊢ ( ( 0 ∈ ℝ ∧ 0 = ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) ) → 0 ≤ ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) ) |
23 |
16 21 22
|
sylancr |
⊢ ( - ( √ ‘ 𝐴 ) ∈ ℝ → 0 ≤ ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) ) |
24 |
2 15 23
|
3syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) ) |
25 |
|
mul2neg |
⊢ ( ( i ∈ ℂ ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) → ( - i · - ( √ ‘ 𝐴 ) ) = ( i · ( √ ‘ 𝐴 ) ) ) |
26 |
1 4 25
|
sylancr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( - i · - ( √ ‘ 𝐴 ) ) = ( i · ( √ ‘ 𝐴 ) ) ) |
27 |
26
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) = ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) ) |
28 |
24 27
|
breqtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) ) |
29 |
|
ixi |
⊢ ( i · i ) = - 1 |
30 |
29
|
oveq1i |
⊢ ( ( i · i ) · ( √ ‘ 𝐴 ) ) = ( - 1 · ( √ ‘ 𝐴 ) ) |
31 |
|
mulass |
⊢ ( ( i ∈ ℂ ∧ i ∈ ℂ ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) → ( ( i · i ) · ( √ ‘ 𝐴 ) ) = ( i · ( i · ( √ ‘ 𝐴 ) ) ) ) |
32 |
1 1 31
|
mp3an12 |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℂ → ( ( i · i ) · ( √ ‘ 𝐴 ) ) = ( i · ( i · ( √ ‘ 𝐴 ) ) ) ) |
33 |
|
mulm1 |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℂ → ( - 1 · ( √ ‘ 𝐴 ) ) = - ( √ ‘ 𝐴 ) ) |
34 |
30 32 33
|
3eqtr3a |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℂ → ( i · ( i · ( √ ‘ 𝐴 ) ) ) = - ( √ ‘ 𝐴 ) ) |
35 |
4 34
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( i · ( i · ( √ ‘ 𝐴 ) ) ) = - ( √ ‘ 𝐴 ) ) |
36 |
|
sqrtge0 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( √ ‘ 𝐴 ) ) |
37 |
|
le0neg2 |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( 0 ≤ ( √ ‘ 𝐴 ) ↔ - ( √ ‘ 𝐴 ) ≤ 0 ) ) |
38 |
|
lenlt |
⊢ ( ( - ( √ ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( - ( √ ‘ 𝐴 ) ≤ 0 ↔ ¬ 0 < - ( √ ‘ 𝐴 ) ) ) |
39 |
15 16 38
|
sylancl |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( - ( √ ‘ 𝐴 ) ≤ 0 ↔ ¬ 0 < - ( √ ‘ 𝐴 ) ) ) |
40 |
37 39
|
bitrd |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( 0 ≤ ( √ ‘ 𝐴 ) ↔ ¬ 0 < - ( √ ‘ 𝐴 ) ) ) |
41 |
2 40
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 0 ≤ ( √ ‘ 𝐴 ) ↔ ¬ 0 < - ( √ ‘ 𝐴 ) ) ) |
42 |
36 41
|
mpbid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ¬ 0 < - ( √ ‘ 𝐴 ) ) |
43 |
|
elrp |
⊢ ( - ( √ ‘ 𝐴 ) ∈ ℝ+ ↔ ( - ( √ ‘ 𝐴 ) ∈ ℝ ∧ 0 < - ( √ ‘ 𝐴 ) ) ) |
44 |
2 15
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → - ( √ ‘ 𝐴 ) ∈ ℝ ) |
45 |
44
|
biantrurd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 0 < - ( √ ‘ 𝐴 ) ↔ ( - ( √ ‘ 𝐴 ) ∈ ℝ ∧ 0 < - ( √ ‘ 𝐴 ) ) ) ) |
46 |
43 45
|
bitr4id |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( - ( √ ‘ 𝐴 ) ∈ ℝ+ ↔ 0 < - ( √ ‘ 𝐴 ) ) ) |
47 |
42 46
|
mtbird |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ¬ - ( √ ‘ 𝐴 ) ∈ ℝ+ ) |
48 |
35 47
|
eqneltrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ¬ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∈ ℝ+ ) |
49 |
|
df-nel |
⊢ ( ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ↔ ¬ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∈ ℝ+ ) |
50 |
48 49
|
sylibr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) |
51 |
14 28 50
|
3jca |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) ) |