Step |
Hyp |
Ref |
Expression |
1 |
|
sqrtcvallem1.1 |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
2 |
|
eldif |
⊢ ( 𝐴 ∈ ( ℂ ∖ ℝ+ ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ+ ) ) |
3 |
2
|
a1i |
⊢ ( 𝜑 → ( 𝐴 ∈ ( ℂ ∖ ℝ+ ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ+ ) ) ) |
4 |
|
imor |
⊢ ( ( ( ℑ ‘ 𝐴 ) = 0 → ( ℜ ‘ 𝐴 ) ≤ 0 ) ↔ ( ¬ ( ℑ ‘ 𝐴 ) = 0 ∨ ( ℜ ‘ 𝐴 ) ≤ 0 ) ) |
5 |
1
|
biantrurd |
⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ℝ ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ ) ) ) |
6 |
|
reim0b |
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) ) |
7 |
1 6
|
syl |
⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) ) |
8 |
7
|
notbid |
⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ℝ ↔ ¬ ( ℑ ‘ 𝐴 ) = 0 ) ) |
9 |
8
|
bicomd |
⊢ ( 𝜑 → ( ¬ ( ℑ ‘ 𝐴 ) = 0 ↔ ¬ 𝐴 ∈ ℝ ) ) |
10 |
|
eleq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ℝ ↔ 𝐴 ∈ ℝ ) ) |
11 |
10
|
notbid |
⊢ ( 𝑥 = 𝐴 → ( ¬ 𝑥 ∈ ℝ ↔ ¬ 𝐴 ∈ ℝ ) ) |
12 |
11
|
elrab |
⊢ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ ) ) |
13 |
12
|
a1i |
⊢ ( 𝜑 → ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ ) ) ) |
14 |
5 9 13
|
3bitr4d |
⊢ ( 𝜑 → ( ¬ ( ℑ ‘ 𝐴 ) = 0 ↔ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ) ) |
15 |
1
|
biantrurd |
⊢ ( 𝜑 → ( ¬ 0 < ( ℜ ‘ 𝐴 ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ 0 < ( ℜ ‘ 𝐴 ) ) ) ) |
16 |
1
|
recld |
⊢ ( 𝜑 → ( ℜ ‘ 𝐴 ) ∈ ℝ ) |
17 |
|
0red |
⊢ ( 𝜑 → 0 ∈ ℝ ) |
18 |
16 17
|
lenltd |
⊢ ( 𝜑 → ( ( ℜ ‘ 𝐴 ) ≤ 0 ↔ ¬ 0 < ( ℜ ‘ 𝐴 ) ) ) |
19 |
|
fveq2 |
⊢ ( 𝑥 = 𝐴 → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ 𝐴 ) ) |
20 |
19
|
breq2d |
⊢ ( 𝑥 = 𝐴 → ( 0 < ( ℜ ‘ 𝑥 ) ↔ 0 < ( ℜ ‘ 𝐴 ) ) ) |
21 |
20
|
notbid |
⊢ ( 𝑥 = 𝐴 → ( ¬ 0 < ( ℜ ‘ 𝑥 ) ↔ ¬ 0 < ( ℜ ‘ 𝐴 ) ) ) |
22 |
21
|
elrab |
⊢ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ↔ ( 𝐴 ∈ ℂ ∧ ¬ 0 < ( ℜ ‘ 𝐴 ) ) ) |
23 |
22
|
a1i |
⊢ ( 𝜑 → ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ↔ ( 𝐴 ∈ ℂ ∧ ¬ 0 < ( ℜ ‘ 𝐴 ) ) ) ) |
24 |
15 18 23
|
3bitr4d |
⊢ ( 𝜑 → ( ( ℜ ‘ 𝐴 ) ≤ 0 ↔ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ) |
25 |
14 24
|
orbi12d |
⊢ ( 𝜑 → ( ( ¬ ( ℑ ‘ 𝐴 ) = 0 ∨ ( ℜ ‘ 𝐴 ) ≤ 0 ) ↔ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∨ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ) ) |
26 |
4 25
|
syl5bb |
⊢ ( 𝜑 → ( ( ( ℑ ‘ 𝐴 ) = 0 → ( ℜ ‘ 𝐴 ) ≤ 0 ) ↔ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∨ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ) ) |
27 |
|
elun |
⊢ ( 𝐴 ∈ ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ↔ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∨ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ) |
28 |
27
|
a1i |
⊢ ( 𝜑 → ( 𝐴 ∈ ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ↔ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∨ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ) ) |
29 |
|
ianor |
⊢ ( ¬ ( 𝑥 ∈ ℝ ∧ 0 < ( ℜ ‘ 𝑥 ) ) ↔ ( ¬ 𝑥 ∈ ℝ ∨ ¬ 0 < ( ℜ ‘ 𝑥 ) ) ) |
30 |
29
|
bicomi |
⊢ ( ( ¬ 𝑥 ∈ ℝ ∨ ¬ 0 < ( ℜ ‘ 𝑥 ) ) ↔ ¬ ( 𝑥 ∈ ℝ ∧ 0 < ( ℜ ‘ 𝑥 ) ) ) |
31 |
|
elrp |
⊢ ( 𝑥 ∈ ℝ+ ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) |
32 |
|
rere |
⊢ ( 𝑥 ∈ ℝ → ( ℜ ‘ 𝑥 ) = 𝑥 ) |
33 |
32
|
breq2d |
⊢ ( 𝑥 ∈ ℝ → ( 0 < ( ℜ ‘ 𝑥 ) ↔ 0 < 𝑥 ) ) |
34 |
33
|
bicomd |
⊢ ( 𝑥 ∈ ℝ → ( 0 < 𝑥 ↔ 0 < ( ℜ ‘ 𝑥 ) ) ) |
35 |
34
|
pm5.32i |
⊢ ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 < ( ℜ ‘ 𝑥 ) ) ) |
36 |
31 35
|
bitri |
⊢ ( 𝑥 ∈ ℝ+ ↔ ( 𝑥 ∈ ℝ ∧ 0 < ( ℜ ‘ 𝑥 ) ) ) |
37 |
30 36
|
xchbinxr |
⊢ ( ( ¬ 𝑥 ∈ ℝ ∨ ¬ 0 < ( ℜ ‘ 𝑥 ) ) ↔ ¬ 𝑥 ∈ ℝ+ ) |
38 |
37
|
rabbii |
⊢ { 𝑥 ∈ ℂ ∣ ( ¬ 𝑥 ∈ ℝ ∨ ¬ 0 < ( ℜ ‘ 𝑥 ) ) } = { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ+ } |
39 |
|
unrab |
⊢ ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) = { 𝑥 ∈ ℂ ∣ ( ¬ 𝑥 ∈ ℝ ∨ ¬ 0 < ( ℜ ‘ 𝑥 ) ) } |
40 |
|
dfdif2 |
⊢ ( ℂ ∖ ℝ+ ) = { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ+ } |
41 |
38 39 40
|
3eqtr4i |
⊢ ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) = ( ℂ ∖ ℝ+ ) |
42 |
41
|
a1i |
⊢ ( 𝜑 → ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) = ( ℂ ∖ ℝ+ ) ) |
43 |
42
|
eleq2d |
⊢ ( 𝜑 → ( 𝐴 ∈ ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ↔ 𝐴 ∈ ( ℂ ∖ ℝ+ ) ) ) |
44 |
26 28 43
|
3bitr2d |
⊢ ( 𝜑 → ( ( ( ℑ ‘ 𝐴 ) = 0 → ( ℜ ‘ 𝐴 ) ≤ 0 ) ↔ 𝐴 ∈ ( ℂ ∖ ℝ+ ) ) ) |
45 |
1
|
biantrurd |
⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ+ ) ) ) |
46 |
3 44 45
|
3bitr4d |
⊢ ( 𝜑 → ( ( ( ℑ ‘ 𝐴 ) = 0 → ( ℜ ‘ 𝐴 ) ≤ 0 ) ↔ ¬ 𝐴 ∈ ℝ+ ) ) |