Step |
Hyp |
Ref |
Expression |
1 |
|
df-nel |
⊢ ( - ( i · 𝐴 ) ∉ ℝ+ ↔ ¬ - ( i · 𝐴 ) ∈ ℝ+ ) |
2 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ℜ ‘ 𝐴 ) = 0 ) |
3 |
|
0le0 |
⊢ 0 ≤ 0 |
4 |
2 3
|
eqbrtrdi |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ℜ ‘ 𝐴 ) ≤ 0 ) |
5 |
4
|
biantrurd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( - ( i · 𝐴 ) ∉ ℝ+ ↔ ( ( ℜ ‘ 𝐴 ) ≤ 0 ∧ - ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
6 |
1 5
|
bitr3id |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ¬ - ( i · 𝐴 ) ∈ ℝ+ ↔ ( ( ℜ ‘ 𝐴 ) ≤ 0 ∧ - ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
7 |
6
|
con1bid |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ¬ ( ( ℜ ‘ 𝐴 ) ≤ 0 ∧ - ( i · 𝐴 ) ∉ ℝ+ ) ↔ - ( i · 𝐴 ) ∈ ℝ+ ) ) |
8 |
|
ax-icn |
⊢ i ∈ ℂ |
9 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ ) |
10 |
8 9
|
mpan |
⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ ) |
11 |
|
reim0b |
⊢ ( ( i · 𝐴 ) ∈ ℂ → ( ( i · 𝐴 ) ∈ ℝ ↔ ( ℑ ‘ ( i · 𝐴 ) ) = 0 ) ) |
12 |
10 11
|
syl |
⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ∈ ℝ ↔ ( ℑ ‘ ( i · 𝐴 ) ) = 0 ) ) |
13 |
|
imre |
⊢ ( ( i · 𝐴 ) ∈ ℂ → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) ) |
14 |
10 13
|
syl |
⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) ) |
15 |
|
ine0 |
⊢ i ≠ 0 |
16 |
|
divrec2 |
⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( i · 𝐴 ) / i ) = ( ( 1 / i ) · ( i · 𝐴 ) ) ) |
17 |
8 15 16
|
mp3an23 |
⊢ ( ( i · 𝐴 ) ∈ ℂ → ( ( i · 𝐴 ) / i ) = ( ( 1 / i ) · ( i · 𝐴 ) ) ) |
18 |
10 17
|
syl |
⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) / i ) = ( ( 1 / i ) · ( i · 𝐴 ) ) ) |
19 |
|
irec |
⊢ ( 1 / i ) = - i |
20 |
19
|
oveq1i |
⊢ ( ( 1 / i ) · ( i · 𝐴 ) ) = ( - i · ( i · 𝐴 ) ) |
21 |
18 20
|
eqtrdi |
⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) / i ) = ( - i · ( i · 𝐴 ) ) ) |
22 |
|
divcan3 |
⊢ ( ( 𝐴 ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( i · 𝐴 ) / i ) = 𝐴 ) |
23 |
8 15 22
|
mp3an23 |
⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) / i ) = 𝐴 ) |
24 |
21 23
|
eqtr3d |
⊢ ( 𝐴 ∈ ℂ → ( - i · ( i · 𝐴 ) ) = 𝐴 ) |
25 |
24
|
fveq2d |
⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) = ( ℜ ‘ 𝐴 ) ) |
26 |
14 25
|
eqtrd |
⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ 𝐴 ) ) |
27 |
26
|
eqeq1d |
⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ ( i · 𝐴 ) ) = 0 ↔ ( ℜ ‘ 𝐴 ) = 0 ) ) |
28 |
12 27
|
bitrd |
⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ∈ ℝ ↔ ( ℜ ‘ 𝐴 ) = 0 ) ) |
29 |
28
|
biimpar |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( i · 𝐴 ) ∈ ℝ ) |
30 |
29
|
adantlr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( i · 𝐴 ) ∈ ℝ ) |
31 |
|
mulne0 |
⊢ ( ( ( i ∈ ℂ ∧ i ≠ 0 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( i · 𝐴 ) ≠ 0 ) |
32 |
8 15 31
|
mpanl12 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( i · 𝐴 ) ≠ 0 ) |
33 |
32
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( i · 𝐴 ) ≠ 0 ) |
34 |
|
rpneg |
⊢ ( ( ( i · 𝐴 ) ∈ ℝ ∧ ( i · 𝐴 ) ≠ 0 ) → ( ( i · 𝐴 ) ∈ ℝ+ ↔ ¬ - ( i · 𝐴 ) ∈ ℝ+ ) ) |
35 |
30 33 34
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( i · 𝐴 ) ∈ ℝ+ ↔ ¬ - ( i · 𝐴 ) ∈ ℝ+ ) ) |
36 |
35
|
con2bid |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( - ( i · 𝐴 ) ∈ ℝ+ ↔ ¬ ( i · 𝐴 ) ∈ ℝ+ ) ) |
37 |
|
df-nel |
⊢ ( ( i · 𝐴 ) ∉ ℝ+ ↔ ¬ ( i · 𝐴 ) ∈ ℝ+ ) |
38 |
36 37
|
bitr4di |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( - ( i · 𝐴 ) ∈ ℝ+ ↔ ( i · 𝐴 ) ∉ ℝ+ ) ) |
39 |
3 2
|
breqtrrid |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → 0 ≤ ( ℜ ‘ 𝐴 ) ) |
40 |
39
|
biantrurd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( i · 𝐴 ) ∉ ℝ+ ↔ ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
41 |
7 38 40
|
3bitrrd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ↔ ¬ ( ( ℜ ‘ 𝐴 ) ≤ 0 ∧ - ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
42 |
28
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( i · 𝐴 ) ∈ ℝ ↔ ( ℜ ‘ 𝐴 ) = 0 ) ) |
43 |
42
|
necon3bbid |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ¬ ( i · 𝐴 ) ∈ ℝ ↔ ( ℜ ‘ 𝐴 ) ≠ 0 ) ) |
44 |
43
|
biimpar |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ¬ ( i · 𝐴 ) ∈ ℝ ) |
45 |
|
rpre |
⊢ ( ( i · 𝐴 ) ∈ ℝ+ → ( i · 𝐴 ) ∈ ℝ ) |
46 |
44 45
|
nsyl |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ¬ ( i · 𝐴 ) ∈ ℝ+ ) |
47 |
46 37
|
sylibr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( i · 𝐴 ) ∉ ℝ+ ) |
48 |
47
|
biantrud |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 0 ≤ ( ℜ ‘ 𝐴 ) ↔ ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
49 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℜ ‘ 𝐴 ) ≠ 0 ) |
50 |
49
|
biantrud |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 0 ≤ ( ℜ ‘ 𝐴 ) ↔ ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) ) ) |
51 |
|
0re |
⊢ 0 ∈ ℝ |
52 |
|
recl |
⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ ) |
53 |
|
ltlen |
⊢ ( ( 0 ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( 0 < ( ℜ ‘ 𝐴 ) ↔ ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) ) ) |
54 |
|
ltnle |
⊢ ( ( 0 ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( 0 < ( ℜ ‘ 𝐴 ) ↔ ¬ ( ℜ ‘ 𝐴 ) ≤ 0 ) ) |
55 |
53 54
|
bitr3d |
⊢ ( ( 0 ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) ↔ ¬ ( ℜ ‘ 𝐴 ) ≤ 0 ) ) |
56 |
51 52 55
|
sylancr |
⊢ ( 𝐴 ∈ ℂ → ( ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) ↔ ¬ ( ℜ ‘ 𝐴 ) ≤ 0 ) ) |
57 |
56
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) ↔ ¬ ( ℜ ‘ 𝐴 ) ≤ 0 ) ) |
58 |
50 57
|
bitrd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 0 ≤ ( ℜ ‘ 𝐴 ) ↔ ¬ ( ℜ ‘ 𝐴 ) ≤ 0 ) ) |
59 |
48 58
|
bitr3d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ↔ ¬ ( ℜ ‘ 𝐴 ) ≤ 0 ) ) |
60 |
|
renegcl |
⊢ ( - ( i · 𝐴 ) ∈ ℝ → - - ( i · 𝐴 ) ∈ ℝ ) |
61 |
10
|
negnegd |
⊢ ( 𝐴 ∈ ℂ → - - ( i · 𝐴 ) = ( i · 𝐴 ) ) |
62 |
61
|
eleq1d |
⊢ ( 𝐴 ∈ ℂ → ( - - ( i · 𝐴 ) ∈ ℝ ↔ ( i · 𝐴 ) ∈ ℝ ) ) |
63 |
62
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( - - ( i · 𝐴 ) ∈ ℝ ↔ ( i · 𝐴 ) ∈ ℝ ) ) |
64 |
60 63
|
syl5ib |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( - ( i · 𝐴 ) ∈ ℝ → ( i · 𝐴 ) ∈ ℝ ) ) |
65 |
44 64
|
mtod |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ¬ - ( i · 𝐴 ) ∈ ℝ ) |
66 |
|
rpre |
⊢ ( - ( i · 𝐴 ) ∈ ℝ+ → - ( i · 𝐴 ) ∈ ℝ ) |
67 |
65 66
|
nsyl |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ¬ - ( i · 𝐴 ) ∈ ℝ+ ) |
68 |
67 1
|
sylibr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - ( i · 𝐴 ) ∉ ℝ+ ) |
69 |
68
|
biantrud |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ℜ ‘ 𝐴 ) ≤ 0 ↔ ( ( ℜ ‘ 𝐴 ) ≤ 0 ∧ - ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
70 |
69
|
notbid |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ¬ ( ℜ ‘ 𝐴 ) ≤ 0 ↔ ¬ ( ( ℜ ‘ 𝐴 ) ≤ 0 ∧ - ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
71 |
59 70
|
bitrd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ↔ ¬ ( ( ℜ ‘ 𝐴 ) ≤ 0 ∧ - ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
72 |
41 71
|
pm2.61dane |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ↔ ¬ ( ( ℜ ‘ 𝐴 ) ≤ 0 ∧ - ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
73 |
|
reneg |
⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) ) |
74 |
73
|
breq2d |
⊢ ( 𝐴 ∈ ℂ → ( 0 ≤ ( ℜ ‘ - 𝐴 ) ↔ 0 ≤ - ( ℜ ‘ 𝐴 ) ) ) |
75 |
52
|
le0neg1d |
⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 𝐴 ) ≤ 0 ↔ 0 ≤ - ( ℜ ‘ 𝐴 ) ) ) |
76 |
74 75
|
bitr4d |
⊢ ( 𝐴 ∈ ℂ → ( 0 ≤ ( ℜ ‘ - 𝐴 ) ↔ ( ℜ ‘ 𝐴 ) ≤ 0 ) ) |
77 |
|
mulneg2 |
⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) ) |
78 |
8 77
|
mpan |
⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) = - ( i · 𝐴 ) ) |
79 |
|
neleq1 |
⊢ ( ( i · - 𝐴 ) = - ( i · 𝐴 ) → ( ( i · - 𝐴 ) ∉ ℝ+ ↔ - ( i · 𝐴 ) ∉ ℝ+ ) ) |
80 |
78 79
|
syl |
⊢ ( 𝐴 ∈ ℂ → ( ( i · - 𝐴 ) ∉ ℝ+ ↔ - ( i · 𝐴 ) ∉ ℝ+ ) ) |
81 |
76 80
|
anbi12d |
⊢ ( 𝐴 ∈ ℂ → ( ( 0 ≤ ( ℜ ‘ - 𝐴 ) ∧ ( i · - 𝐴 ) ∉ ℝ+ ) ↔ ( ( ℜ ‘ 𝐴 ) ≤ 0 ∧ - ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
82 |
81
|
notbid |
⊢ ( 𝐴 ∈ ℂ → ( ¬ ( 0 ≤ ( ℜ ‘ - 𝐴 ) ∧ ( i · - 𝐴 ) ∉ ℝ+ ) ↔ ¬ ( ( ℜ ‘ 𝐴 ) ≤ 0 ∧ - ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
83 |
82
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ¬ ( 0 ≤ ( ℜ ‘ - 𝐴 ) ∧ ( i · - 𝐴 ) ∉ ℝ+ ) ↔ ¬ ( ( ℜ ‘ 𝐴 ) ≤ 0 ∧ - ( i · 𝐴 ) ∉ ℝ+ ) ) ) |
84 |
72 83
|
bitr4d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ↔ ¬ ( 0 ≤ ( ℜ ‘ - 𝐴 ) ∧ ( i · - 𝐴 ) ∉ ℝ+ ) ) ) |