| Step | Hyp | Ref
| Expression |
| 1 | | eldif 3961 |
. . 3
⊢ (𝐴 ∈ (ℂ ∖
ℝ+) ↔ (𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈
ℝ+)) |
| 2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴 ∈ (ℂ ∖
ℝ+) ↔ (𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈
ℝ+))) |
| 3 | | imor 854 |
. . . 4
⊢
(((ℑ‘𝐴)
= 0 → (ℜ‘𝐴)
≤ 0) ↔ (¬ (ℑ‘𝐴) = 0 ∨ (ℜ‘𝐴) ≤ 0)) |
| 4 | | sqrtcvallem1.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 5 | 4 | biantrurd 532 |
. . . . . 6
⊢ (𝜑 → (¬ 𝐴 ∈ ℝ ↔ (𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈
ℝ))) |
| 6 | | reim0b 15158 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
| 7 | 4, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)) |
| 8 | 7 | notbid 318 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝐴 ∈ ℝ ↔ ¬
(ℑ‘𝐴) =
0)) |
| 9 | 8 | bicomd 223 |
. . . . . 6
⊢ (𝜑 → (¬
(ℑ‘𝐴) = 0
↔ ¬ 𝐴 ∈
ℝ)) |
| 10 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑥 ∈ ℝ ↔ 𝐴 ∈ ℝ)) |
| 11 | 10 | notbid 318 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ ℝ ↔ ¬ 𝐴 ∈
ℝ)) |
| 12 | 11 | elrab 3692 |
. . . . . . 7
⊢ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ↔ (𝐴 ∈ ℂ ∧ ¬
𝐴 ∈
ℝ)) |
| 13 | 12 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ↔ (𝐴 ∈ ℂ ∧ ¬
𝐴 ∈
ℝ))) |
| 14 | 5, 9, 13 | 3bitr4d 311 |
. . . . 5
⊢ (𝜑 → (¬
(ℑ‘𝐴) = 0
↔ 𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬
𝑥 ∈
ℝ})) |
| 15 | 4 | biantrurd 532 |
. . . . . 6
⊢ (𝜑 → (¬ 0 <
(ℜ‘𝐴) ↔
(𝐴 ∈ ℂ ∧
¬ 0 < (ℜ‘𝐴)))) |
| 16 | 4 | recld 15233 |
. . . . . . 7
⊢ (𝜑 → (ℜ‘𝐴) ∈
ℝ) |
| 17 | | 0red 11264 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
| 18 | 16, 17 | lenltd 11407 |
. . . . . 6
⊢ (𝜑 → ((ℜ‘𝐴) ≤ 0 ↔ ¬ 0 <
(ℜ‘𝐴))) |
| 19 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (ℜ‘𝑥) = (ℜ‘𝐴)) |
| 20 | 19 | breq2d 5155 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (0 < (ℜ‘𝑥) ↔ 0 <
(ℜ‘𝐴))) |
| 21 | 20 | notbid 318 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (¬ 0 < (ℜ‘𝑥) ↔ ¬ 0 <
(ℜ‘𝐴))) |
| 22 | 21 | elrab 3692 |
. . . . . . 7
⊢ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0 <
(ℜ‘𝑥)} ↔
(𝐴 ∈ ℂ ∧
¬ 0 < (ℜ‘𝐴))) |
| 23 | 22 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0 <
(ℜ‘𝑥)} ↔
(𝐴 ∈ ℂ ∧
¬ 0 < (ℜ‘𝐴)))) |
| 24 | 15, 18, 23 | 3bitr4d 311 |
. . . . 5
⊢ (𝜑 → ((ℜ‘𝐴) ≤ 0 ↔ 𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0 <
(ℜ‘𝑥)})) |
| 25 | 14, 24 | orbi12d 919 |
. . . 4
⊢ (𝜑 → ((¬
(ℑ‘𝐴) = 0 ∨
(ℜ‘𝐴) ≤ 0)
↔ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬
𝑥 ∈ ℝ} ∨
𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)}))) |
| 26 | 3, 25 | bitrid 283 |
. . 3
⊢ (𝜑 → (((ℑ‘𝐴) = 0 → (ℜ‘𝐴) ≤ 0) ↔ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ∨ 𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0 <
(ℜ‘𝑥)}))) |
| 27 | | elun 4153 |
. . . 4
⊢ (𝐴 ∈ ({𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ∪ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)})
↔ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬
𝑥 ∈ ℝ} ∨
𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)})) |
| 28 | 27 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴 ∈ ({𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ∪ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)})
↔ (𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬
𝑥 ∈ ℝ} ∨
𝐴 ∈ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)}))) |
| 29 | | ianor 984 |
. . . . . . . . 9
⊢ (¬
(𝑥 ∈ ℝ ∧ 0
< (ℜ‘𝑥))
↔ (¬ 𝑥 ∈
ℝ ∨ ¬ 0 < (ℜ‘𝑥))) |
| 30 | 29 | bicomi 224 |
. . . . . . . 8
⊢ ((¬
𝑥 ∈ ℝ ∨ ¬
0 < (ℜ‘𝑥))
↔ ¬ (𝑥 ∈
ℝ ∧ 0 < (ℜ‘𝑥))) |
| 31 | | elrp 13036 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↔ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
| 32 | | rere 15161 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
(ℜ‘𝑥) = 𝑥) |
| 33 | 32 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (0 <
(ℜ‘𝑥) ↔ 0
< 𝑥)) |
| 34 | 33 | bicomd 223 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → (0 <
𝑥 ↔ 0 <
(ℜ‘𝑥))) |
| 35 | 34 | pm5.32i 574 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 0 <
𝑥) ↔ (𝑥 ∈ ℝ ∧ 0 <
(ℜ‘𝑥))) |
| 36 | 31, 35 | bitri 275 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
↔ (𝑥 ∈ ℝ
∧ 0 < (ℜ‘𝑥))) |
| 37 | 30, 36 | xchbinxr 335 |
. . . . . . 7
⊢ ((¬
𝑥 ∈ ℝ ∨ ¬
0 < (ℜ‘𝑥))
↔ ¬ 𝑥 ∈
ℝ+) |
| 38 | 37 | rabbii 3442 |
. . . . . 6
⊢ {𝑥 ∈ ℂ ∣ (¬
𝑥 ∈ ℝ ∨ ¬
0 < (ℜ‘𝑥))} =
{𝑥 ∈ ℂ ∣
¬ 𝑥 ∈
ℝ+} |
| 39 | | unrab 4315 |
. . . . . 6
⊢ ({𝑥 ∈ ℂ ∣ ¬
𝑥 ∈ ℝ} ∪
{𝑥 ∈ ℂ ∣
¬ 0 < (ℜ‘𝑥)}) = {𝑥 ∈ ℂ ∣ (¬ 𝑥 ∈ ℝ ∨ ¬ 0
< (ℜ‘𝑥))} |
| 40 | | dfdif2 3960 |
. . . . . 6
⊢ (ℂ
∖ ℝ+) = {𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈
ℝ+} |
| 41 | 38, 39, 40 | 3eqtr4i 2775 |
. . . . 5
⊢ ({𝑥 ∈ ℂ ∣ ¬
𝑥 ∈ ℝ} ∪
{𝑥 ∈ ℂ ∣
¬ 0 < (ℜ‘𝑥)}) = (ℂ ∖
ℝ+) |
| 42 | 41 | a1i 11 |
. . . 4
⊢ (𝜑 → ({𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ∪ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)}) =
(ℂ ∖ ℝ+)) |
| 43 | 42 | eleq2d 2827 |
. . 3
⊢ (𝜑 → (𝐴 ∈ ({𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ} ∪ {𝑥 ∈ ℂ ∣ ¬ 0
< (ℜ‘𝑥)})
↔ 𝐴 ∈ (ℂ
∖ ℝ+))) |
| 44 | 26, 28, 43 | 3bitr2d 307 |
. 2
⊢ (𝜑 → (((ℑ‘𝐴) = 0 → (ℜ‘𝐴) ≤ 0) ↔ 𝐴 ∈ (ℂ ∖
ℝ+))) |
| 45 | 4 | biantrurd 532 |
. 2
⊢ (𝜑 → (¬ 𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℂ ∧ ¬
𝐴 ∈
ℝ+))) |
| 46 | 2, 44, 45 | 3bitr4d 311 |
1
⊢ (𝜑 → (((ℑ‘𝐴) = 0 → (ℜ‘𝐴) ≤ 0) ↔ ¬ 𝐴 ∈
ℝ+)) |