Proof of Theorem dstregt0
Step | Hyp | Ref
| Expression |
1 | | dstregt0.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖
ℝ)) |
2 | 1 | eldifad 3899 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | 2 | imcld 14906 |
. . . . 5
⊢ (𝜑 → (ℑ‘𝐴) ∈
ℝ) |
4 | 3 | recnd 11003 |
. . . 4
⊢ (𝜑 → (ℑ‘𝐴) ∈
ℂ) |
5 | 1 | eldifbd 3900 |
. . . . . 6
⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) |
6 | | reim0b 14830 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
7 | 2, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)) |
8 | 5, 7 | mtbid 324 |
. . . . 5
⊢ (𝜑 → ¬ (ℑ‘𝐴) = 0) |
9 | 8 | neqned 2950 |
. . . 4
⊢ (𝜑 → (ℑ‘𝐴) ≠ 0) |
10 | 4, 9 | absrpcld 15160 |
. . 3
⊢ (𝜑 →
(abs‘(ℑ‘𝐴)) ∈
ℝ+) |
11 | 10 | rphalfcld 12784 |
. 2
⊢ (𝜑 →
((abs‘(ℑ‘𝐴)) / 2) ∈
ℝ+) |
12 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ ℂ) |
13 | | recn 10961 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
14 | 13 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
15 | 12, 14 | imsubd 14928 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘(𝐴 − 𝑦)) = ((ℑ‘𝐴) − (ℑ‘𝑦))) |
16 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
17 | 16 | reim0d 14936 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘𝑦) = 0) |
18 | 17 | oveq2d 7291 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((ℑ‘𝐴) − (ℑ‘𝑦)) = ((ℑ‘𝐴) − 0)) |
19 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘𝐴) ∈
ℂ) |
20 | 19 | subid1d 11321 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((ℑ‘𝐴) − 0) =
(ℑ‘𝐴)) |
21 | 15, 18, 20 | 3eqtrrd 2783 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘𝐴) = (ℑ‘(𝐴 − 𝑦))) |
22 | 21 | fveq2d 6778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘𝐴)) = (abs‘(ℑ‘(𝐴 − 𝑦)))) |
23 | 22 | oveq1d 7290 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((abs‘(ℑ‘𝐴)) / 2) = ((abs‘(ℑ‘(𝐴 − 𝑦))) / 2)) |
24 | 21, 19 | eqeltrrd 2840 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘(𝐴 − 𝑦)) ∈ ℂ) |
25 | 24 | abscld 15148 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘(𝐴 − 𝑦))) ∈ ℝ) |
26 | 25 | rehalfcld 12220 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((abs‘(ℑ‘(𝐴 − 𝑦))) / 2) ∈ ℝ) |
27 | 12, 14 | subcld 11332 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐴 − 𝑦) ∈ ℂ) |
28 | 27 | abscld 15148 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (abs‘(𝐴 − 𝑦)) ∈ ℝ) |
29 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘𝐴) ≠ 0) |
30 | 21, 29 | eqnetrrd 3012 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (ℑ‘(𝐴 − 𝑦)) ≠ 0) |
31 | 24, 30 | absrpcld 15160 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘(𝐴 − 𝑦))) ∈
ℝ+) |
32 | | rphalflt 12759 |
. . . . . 6
⊢
((abs‘(ℑ‘(𝐴 − 𝑦))) ∈ ℝ+ →
((abs‘(ℑ‘(𝐴 − 𝑦))) / 2) <
(abs‘(ℑ‘(𝐴 − 𝑦)))) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((abs‘(ℑ‘(𝐴 − 𝑦))) / 2) <
(abs‘(ℑ‘(𝐴 − 𝑦)))) |
34 | | absimle 15021 |
. . . . . 6
⊢ ((𝐴 − 𝑦) ∈ ℂ →
(abs‘(ℑ‘(𝐴 − 𝑦))) ≤ (abs‘(𝐴 − 𝑦))) |
35 | 27, 34 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
(abs‘(ℑ‘(𝐴 − 𝑦))) ≤ (abs‘(𝐴 − 𝑦))) |
36 | 26, 25, 28, 33, 35 | ltletrd 11135 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((abs‘(ℑ‘(𝐴 − 𝑦))) / 2) < (abs‘(𝐴 − 𝑦))) |
37 | 23, 36 | eqbrtrd 5096 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴 − 𝑦))) |
38 | 37 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ ℝ
((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴 − 𝑦))) |
39 | | breq1 5077 |
. . . 4
⊢ (𝑥 =
((abs‘(ℑ‘𝐴)) / 2) → (𝑥 < (abs‘(𝐴 − 𝑦)) ↔ ((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴 − 𝑦)))) |
40 | 39 | ralbidv 3112 |
. . 3
⊢ (𝑥 =
((abs‘(ℑ‘𝐴)) / 2) → (∀𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴 − 𝑦)) ↔ ∀𝑦 ∈ ℝ
((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴 − 𝑦)))) |
41 | 40 | rspcev 3561 |
. 2
⊢
((((abs‘(ℑ‘𝐴)) / 2) ∈ ℝ+ ∧
∀𝑦 ∈ ℝ
((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴 − 𝑦))) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴 − 𝑦))) |
42 | 11, 38, 41 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴 − 𝑦))) |