Proof of Theorem dstregt0
| Step | Hyp | Ref
| Expression |
| 1 | | dstregt0.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖
ℝ)) |
| 2 | 1 | eldifad 3963 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 3 | 2 | imcld 15234 |
. . . . 5
⊢ (𝜑 → (ℑ‘𝐴) ∈
ℝ) |
| 4 | 3 | recnd 11289 |
. . . 4
⊢ (𝜑 → (ℑ‘𝐴) ∈
ℂ) |
| 5 | 1 | eldifbd 3964 |
. . . . . 6
⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) |
| 6 | | reim0b 15158 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
| 7 | 2, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)) |
| 8 | 5, 7 | mtbid 324 |
. . . . 5
⊢ (𝜑 → ¬ (ℑ‘𝐴) = 0) |
| 9 | 8 | neqned 2947 |
. . . 4
⊢ (𝜑 → (ℑ‘𝐴) ≠ 0) |
| 10 | 4, 9 | absrpcld 15487 |
. . 3
⊢ (𝜑 →
(abs‘(ℑ‘𝐴)) ∈
ℝ+) |
| 11 | 10 | rphalfcld 13089 |
. 2
⊢ (𝜑 →
((abs‘(ℑ‘𝐴)) / 2) ∈
ℝ+) |
| 12 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ ℂ) |
| 13 | | recn 11245 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
| 14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
| 15 | 12, 14 | imsubd 15256 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘(𝐴 − 𝑦)) = ((ℑ‘𝐴) − (ℑ‘𝑦))) |
| 16 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
| 17 | 16 | reim0d 15264 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘𝑦) = 0) |
| 18 | 17 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((ℑ‘𝐴) − (ℑ‘𝑦)) = ((ℑ‘𝐴) − 0)) |
| 19 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘𝐴) ∈
ℂ) |
| 20 | 19 | subid1d 11609 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((ℑ‘𝐴) − 0) =
(ℑ‘𝐴)) |
| 21 | 15, 18, 20 | 3eqtrrd 2782 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘𝐴) = (ℑ‘(𝐴 − 𝑦))) |
| 22 | 21 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘𝐴)) = (abs‘(ℑ‘(𝐴 − 𝑦)))) |
| 23 | 22 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((abs‘(ℑ‘𝐴)) / 2) = ((abs‘(ℑ‘(𝐴 − 𝑦))) / 2)) |
| 24 | 21, 19 | eqeltrrd 2842 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘(𝐴 − 𝑦)) ∈ ℂ) |
| 25 | 24 | abscld 15475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘(𝐴 − 𝑦))) ∈ ℝ) |
| 26 | 25 | rehalfcld 12513 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((abs‘(ℑ‘(𝐴 − 𝑦))) / 2) ∈ ℝ) |
| 27 | 12, 14 | subcld 11620 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐴 − 𝑦) ∈ ℂ) |
| 28 | 27 | abscld 15475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (abs‘(𝐴 − 𝑦)) ∈ ℝ) |
| 29 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘𝐴) ≠ 0) |
| 30 | 21, 29 | eqnetrrd 3009 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘(𝐴 − 𝑦)) ≠ 0) |
| 31 | 24, 30 | absrpcld 15487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘(𝐴 − 𝑦))) ∈
ℝ+) |
| 32 | | rphalflt 13064 |
. . . . . 6
⊢
((abs‘(ℑ‘(𝐴 − 𝑦))) ∈ ℝ+ →
((abs‘(ℑ‘(𝐴 − 𝑦))) / 2) <
(abs‘(ℑ‘(𝐴 − 𝑦)))) |
| 33 | 31, 32 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((abs‘(ℑ‘(𝐴 − 𝑦))) / 2) <
(abs‘(ℑ‘(𝐴 − 𝑦)))) |
| 34 | | absimle 15348 |
. . . . . 6
⊢ ((𝐴 − 𝑦) ∈ ℂ →
(abs‘(ℑ‘(𝐴 − 𝑦))) ≤ (abs‘(𝐴 − 𝑦))) |
| 35 | 27, 34 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘(𝐴 − 𝑦))) ≤ (abs‘(𝐴 − 𝑦))) |
| 36 | 26, 25, 28, 33, 35 | ltletrd 11421 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((abs‘(ℑ‘(𝐴 − 𝑦))) / 2) < (abs‘(𝐴 − 𝑦))) |
| 37 | 23, 36 | eqbrtrd 5165 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴 − 𝑦))) |
| 38 | 37 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ ℝ
((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴 − 𝑦))) |
| 39 | | breq1 5146 |
. . . 4
⊢ (𝑥 =
((abs‘(ℑ‘𝐴)) / 2) → (𝑥 < (abs‘(𝐴 − 𝑦)) ↔ ((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴 − 𝑦)))) |
| 40 | 39 | ralbidv 3178 |
. . 3
⊢ (𝑥 =
((abs‘(ℑ‘𝐴)) / 2) → (∀𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴 − 𝑦)) ↔ ∀𝑦 ∈ ℝ
((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴 − 𝑦)))) |
| 41 | 40 | rspcev 3622 |
. 2
⊢
((((abs‘(ℑ‘𝐴)) / 2) ∈ ℝ+ ∧
∀𝑦 ∈ ℝ
((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴 − 𝑦))) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴 − 𝑦))) |
| 42 | 11, 38, 41 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴 − 𝑦))) |