Step | Hyp | Ref
| Expression |
1 | | eldif 3864 |
. . 3
⊢ (𝐴 ∈ (ℂ ∖
ℝ+) ↔ (𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈
ℝ+)) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴 ∈ (ℂ ∖
ℝ+) ↔ (𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈
ℝ+))) |
3 | | imor 851 |
. . . 4
⊢
(((ℑ‘𝐴)
= 0 → (ℜ‘𝐴)
≤ 0) ↔ (¬ (ℑ‘𝐴) = 0 ∨ (ℜ‘𝐴) ≤ 0)) |
4 | | sqrtcvallem1.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
5 | 4 | biantrurd 537 |
. . . . . 6
⊢ (𝜑 → (¬ 𝐴 ∈ ℝ ↔ (𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈
ℝ))) |
6 | | reim0b 14511 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
7 | 4, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)) |
8 | 7 | notbid 322 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝐴 ∈ ℝ ↔ ¬
(ℑ‘𝐴) =
0)) |
9 | 8 | bicomd 226 |
. . . . . 6
⊢ (𝜑 → (¬
(ℑ‘𝐴) = 0
↔ ¬ 𝐴 ∈
ℝ)) |
10 | | eleq1 2838 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑥 ∈ ℝ ↔ 𝐴 ∈ ℝ)) |
11 | 10 | notbid 322 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ ℝ ↔ ¬ 𝐴 ∈
ℝ)) |
12 | 11 | elrab 3600 |
. . . . . . 7
⊢ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ↔ (𝐴 ∈ ℂ ∧ ¬
𝐴 ∈
ℝ)) |
13 | 12 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ↔ (𝐴 ∈ ℂ ∧ ¬
𝐴 ∈
ℝ))) |
14 | 5, 9, 13 | 3bitr4d 315 |
. . . . 5
⊢ (𝜑 → (¬
(ℑ‘𝐴) = 0
↔ 𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬
𝑥 ∈
ℝ})) |
15 | 4 | biantrurd 537 |
. . . . . 6
⊢ (𝜑 → (¬ 0 <
(ℜ‘𝐴) ↔
(𝐴 ∈ ℂ ∧
¬ 0 < (ℜ‘𝐴)))) |
16 | 4 | recld 14586 |
. . . . . . 7
⊢ (𝜑 → (ℜ‘𝐴) ∈
ℝ) |
17 | | 0red 10667 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
18 | 16, 17 | lenltd 10809 |
. . . . . 6
⊢ (𝜑 → ((ℜ‘𝐴) ≤ 0 ↔ ¬ 0 <
(ℜ‘𝐴))) |
19 | | fveq2 6651 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (ℜ‘𝑥) = (ℜ‘𝐴)) |
20 | 19 | breq2d 5037 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (0 < (ℜ‘𝑥) ↔ 0 <
(ℜ‘𝐴))) |
21 | 20 | notbid 322 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (¬ 0 < (ℜ‘𝑥) ↔ ¬ 0 <
(ℜ‘𝐴))) |
22 | 21 | elrab 3600 |
. . . . . . 7
⊢ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0 <
(ℜ‘𝑥)} ↔
(𝐴 ∈ ℂ ∧
¬ 0 < (ℜ‘𝐴))) |
23 | 22 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0 <
(ℜ‘𝑥)} ↔
(𝐴 ∈ ℂ ∧
¬ 0 < (ℜ‘𝐴)))) |
24 | 15, 18, 23 | 3bitr4d 315 |
. . . . 5
⊢ (𝜑 → ((ℜ‘𝐴) ≤ 0 ↔ 𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0 <
(ℜ‘𝑥)})) |
25 | 14, 24 | orbi12d 917 |
. . . 4
⊢ (𝜑 → ((¬
(ℑ‘𝐴) = 0 ∨
(ℜ‘𝐴) ≤ 0)
↔ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬
𝑥 ∈ ℝ} ∨
𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)}))) |
26 | 3, 25 | syl5bb 286 |
. . 3
⊢ (𝜑 → (((ℑ‘𝐴) = 0 → (ℜ‘𝐴) ≤ 0) ↔ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ∨ 𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0 <
(ℜ‘𝑥)}))) |
27 | | elun 4050 |
. . . 4
⊢ (𝐴 ∈ ({𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ∪ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)})
↔ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬
𝑥 ∈ ℝ} ∨
𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)})) |
28 | 27 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴 ∈ ({𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ∪ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)})
↔ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬
𝑥 ∈ ℝ} ∨
𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)}))) |
29 | | ianor 980 |
. . . . . . . . 9
⊢ (¬
(𝑥 ∈ ℝ ∧ 0
< (ℜ‘𝑥))
↔ (¬ 𝑥 ∈
ℝ ∨ ¬ 0 < (ℜ‘𝑥))) |
30 | 29 | bicomi 227 |
. . . . . . . 8
⊢ ((¬
𝑥 ∈ ℝ ∨ ¬
0 < (ℜ‘𝑥))
↔ ¬ (𝑥 ∈
ℝ ∧ 0 < (ℜ‘𝑥))) |
31 | | elrp 12417 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↔ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
32 | | rere 14514 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
(ℜ‘𝑥) = 𝑥) |
33 | 32 | breq2d 5037 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (0 <
(ℜ‘𝑥) ↔ 0
< 𝑥)) |
34 | 33 | bicomd 226 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → (0 <
𝑥 ↔ 0 <
(ℜ‘𝑥))) |
35 | 34 | pm5.32i 579 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 0 <
𝑥) ↔ (𝑥 ∈ ℝ ∧ 0 <
(ℜ‘𝑥))) |
36 | 31, 35 | bitri 278 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
↔ (𝑥 ∈ ℝ
∧ 0 < (ℜ‘𝑥))) |
37 | 30, 36 | xchbinxr 339 |
. . . . . . 7
⊢ ((¬
𝑥 ∈ ℝ ∨ ¬
0 < (ℜ‘𝑥))
↔ ¬ 𝑥 ∈
ℝ+) |
38 | 37 | rabbii 3383 |
. . . . . 6
⊢ {𝑥 ∈ ℂ ∣ (¬
𝑥 ∈ ℝ ∨ ¬
0 < (ℜ‘𝑥))} =
{𝑥 ∈ ℂ ∣
¬ 𝑥 ∈
ℝ+} |
39 | | unrab 4204 |
. . . . . 6
⊢ ({𝑥 ∈ ℂ ∣ ¬
𝑥 ∈ ℝ} ∪
{𝑥 ∈ ℂ ∣
¬ 0 < (ℜ‘𝑥)}) = {𝑥 ∈ ℂ ∣ (¬ 𝑥 ∈ ℝ ∨ ¬ 0
< (ℜ‘𝑥))} |
40 | | dfdif2 3863 |
. . . . . 6
⊢ (ℂ
∖ ℝ+) = {𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈
ℝ+} |
41 | 38, 39, 40 | 3eqtr4i 2792 |
. . . . 5
⊢ ({𝑥 ∈ ℂ ∣ ¬
𝑥 ∈ ℝ} ∪
{𝑥 ∈ ℂ ∣
¬ 0 < (ℜ‘𝑥)}) = (ℂ ∖
ℝ+) |
42 | 41 | a1i 11 |
. . . 4
⊢ (𝜑 → ({𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ∪ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)}) =
(ℂ ∖ ℝ+)) |
43 | 42 | eleq2d 2836 |
. . 3
⊢ (𝜑 → (𝐴 ∈ ({𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ∪ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)})
↔ 𝐴 ∈ (ℂ
∖ ℝ+))) |
44 | 26, 28, 43 | 3bitr2d 311 |
. 2
⊢ (𝜑 → (((ℑ‘𝐴) = 0 → (ℜ‘𝐴) ≤ 0) ↔ 𝐴 ∈ (ℂ ∖
ℝ+))) |
45 | 4 | biantrurd 537 |
. 2
⊢ (𝜑 → (¬ 𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℂ ∧ ¬
𝐴 ∈
ℝ+))) |
46 | 2, 44, 45 | 3bitr4d 315 |
1
⊢ (𝜑 → (((ℑ‘𝐴) = 0 → (ℜ‘𝐴) ≤ 0) ↔ ¬ 𝐴 ∈
ℝ+)) |