Proof of Theorem abelthlem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | abelth.3 | . 2
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 2 |  | abelth.4 | . 2
⊢ (𝜑 → 0 ≤ 𝑀) | 
| 3 |  | 1cnd 11257 | . . . 4
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 1 ∈
ℂ) | 
| 4 |  | 0le0 12368 | . . . . 5
⊢ 0 ≤
0 | 
| 5 |  | simpl 482 | . . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 𝑀 ∈ ℝ) | 
| 6 | 5 | recnd 11290 | . . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 𝑀 ∈ ℂ) | 
| 7 | 6 | mul01d 11461 | . . . . 5
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → (𝑀 · 0) =
0) | 
| 8 | 4, 7 | breqtrrid 5180 | . . . 4
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 0 ≤ (𝑀 · 0)) | 
| 9 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑧 = 1 → (1 − 𝑧) = (1 −
1)) | 
| 10 |  | 1m1e0 12339 | . . . . . . . 8
⊢ (1
− 1) = 0 | 
| 11 | 9, 10 | eqtrdi 2792 | . . . . . . 7
⊢ (𝑧 = 1 → (1 − 𝑧) = 0) | 
| 12 | 11 | abs00bd 15331 | . . . . . 6
⊢ (𝑧 = 1 → (abs‘(1
− 𝑧)) =
0) | 
| 13 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑧 = 1 → (abs‘𝑧) =
(abs‘1)) | 
| 14 |  | abs1 15337 | . . . . . . . . . 10
⊢
(abs‘1) = 1 | 
| 15 | 13, 14 | eqtrdi 2792 | . . . . . . . . 9
⊢ (𝑧 = 1 → (abs‘𝑧) = 1) | 
| 16 | 15 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑧 = 1 → (1 −
(abs‘𝑧)) = (1 −
1)) | 
| 17 | 16, 10 | eqtrdi 2792 | . . . . . . 7
⊢ (𝑧 = 1 → (1 −
(abs‘𝑧)) =
0) | 
| 18 | 17 | oveq2d 7448 | . . . . . 6
⊢ (𝑧 = 1 → (𝑀 · (1 − (abs‘𝑧))) = (𝑀 · 0)) | 
| 19 | 12, 18 | breq12d 5155 | . . . . 5
⊢ (𝑧 = 1 → ((abs‘(1
− 𝑧)) ≤ (𝑀 · (1 −
(abs‘𝑧))) ↔ 0
≤ (𝑀 ·
0))) | 
| 20 |  | abelth.5 | . . . . 5
⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} | 
| 21 | 19, 20 | elrab2 3694 | . . . 4
⊢ (1 ∈
𝑆 ↔ (1 ∈ ℂ
∧ 0 ≤ (𝑀 ·
0))) | 
| 22 | 3, 8, 21 | sylanbrc 583 | . . 3
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 1 ∈ 𝑆) | 
| 23 |  | velsn 4641 | . . . . . . . . . 10
⊢ (𝑧 ∈ {1} ↔ 𝑧 = 1) | 
| 24 | 23 | necon3bbii 2987 | . . . . . . . . 9
⊢ (¬
𝑧 ∈ {1} ↔ 𝑧 ≠ 1) | 
| 25 |  | simprll 778 | . . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑧 ∈
ℂ) | 
| 26 |  | 0cn 11254 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
ℂ | 
| 27 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 28 | 27 | cnmetdval 24792 | . . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑧(abs
∘ − )0) = (abs‘(𝑧 − 0))) | 
| 29 | 25, 26, 28 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) =
(abs‘(𝑧 −
0))) | 
| 30 | 25 | subid1d 11610 | . . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑧 − 0) = 𝑧) | 
| 31 | 30 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘(𝑧 − 0)) =
(abs‘𝑧)) | 
| 32 | 29, 31 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) =
(abs‘𝑧)) | 
| 33 | 25 | abscld 15476 | . . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) ∈
ℝ) | 
| 34 |  | 1red 11263 | . . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 1 ∈
ℝ) | 
| 35 |  | 1re 11262 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ | 
| 36 |  | resubcl 11574 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((abs‘𝑧)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑧) − 1) ∈ ℝ) | 
| 37 | 33, 35, 36 | sylancl 586 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) − 1)
∈ ℝ) | 
| 38 |  | ax-1cn 11214 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℂ | 
| 39 |  | subcl 11508 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℂ ∧ 𝑧
∈ ℂ) → (1 − 𝑧) ∈ ℂ) | 
| 40 | 38, 25, 39 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (1
− 𝑧) ∈
ℂ) | 
| 41 | 40 | abscld 15476 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘(1 − 𝑧))
∈ ℝ) | 
| 42 |  | simpll 766 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑀 ∈
ℝ) | 
| 43 |  | resubcl 11574 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℝ ∧ (abs‘𝑧) ∈ ℝ) → (1 −
(abs‘𝑧)) ∈
ℝ) | 
| 44 | 35, 33, 43 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (1
− (abs‘𝑧))
∈ ℝ) | 
| 45 | 42, 44 | remulcld 11292 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · (1 −
(abs‘𝑧))) ∈
ℝ) | 
| 46 | 14 | oveq2i 7443 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((abs‘𝑧)
− (abs‘1)) = ((abs‘𝑧) − 1) | 
| 47 |  | abs2dif 15372 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℂ ∧ 1 ∈
ℂ) → ((abs‘𝑧) − (abs‘1)) ≤
(abs‘(𝑧 −
1))) | 
| 48 | 25, 38, 47 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) −
(abs‘1)) ≤ (abs‘(𝑧 − 1))) | 
| 49 | 46, 48 | eqbrtrrid 5178 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) − 1)
≤ (abs‘(𝑧 −
1))) | 
| 50 |  | abssub 15366 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℂ ∧ 1 ∈
ℂ) → (abs‘(𝑧 − 1)) = (abs‘(1 − 𝑧))) | 
| 51 | 25, 38, 50 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘(𝑧 − 1)) =
(abs‘(1 − 𝑧))) | 
| 52 | 49, 51 | breqtrd 5168 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) − 1)
≤ (abs‘(1 − 𝑧))) | 
| 53 |  | simprlr 779 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) | 
| 54 | 37, 41, 45, 52, 53 | letrd 11419 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) − 1)
≤ (𝑀 · (1 −
(abs‘𝑧)))) | 
| 55 | 33, 34, 45 | lesubaddd 11861 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(((abs‘𝑧) − 1)
≤ (𝑀 · (1 −
(abs‘𝑧))) ↔
(abs‘𝑧) ≤ ((𝑀 · (1 −
(abs‘𝑧))) +
1))) | 
| 56 | 54, 55 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) ≤ ((𝑀 · (1 −
(abs‘𝑧))) +
1)) | 
| 57 | 6 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑀 ∈
ℂ) | 
| 58 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 1 ∈
ℂ) | 
| 59 | 42, 33 | remulcld 11292 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · (abs‘𝑧)) ∈
ℝ) | 
| 60 | 59 | recnd 11290 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · (abs‘𝑧)) ∈
ℂ) | 
| 61 | 57, 58, 60 | addsubd 11642 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 + 1) − (𝑀 · (abs‘𝑧))) = ((𝑀 − (𝑀 · (abs‘𝑧))) + 1)) | 
| 62 | 33 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) ∈
ℂ) | 
| 63 | 57, 58, 62 | subdid 11720 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · (1 −
(abs‘𝑧))) = ((𝑀 · 1) − (𝑀 · (abs‘𝑧)))) | 
| 64 | 57 | mulridd 11279 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · 1) = 𝑀) | 
| 65 | 64 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 · 1) − (𝑀 · (abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧)))) | 
| 66 | 63, 65 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · (1 −
(abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧)))) | 
| 67 | 66 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 · (1 −
(abs‘𝑧))) + 1) =
((𝑀 − (𝑀 · (abs‘𝑧))) + 1)) | 
| 68 | 61, 67 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 + 1) − (𝑀 · (abs‘𝑧))) = ((𝑀 · (1 − (abs‘𝑧))) + 1)) | 
| 69 | 56, 68 | breqtrrd 5170 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) ≤ ((𝑀 + 1) − (𝑀 · (abs‘𝑧)))) | 
| 70 |  | peano2re 11435 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) | 
| 71 | 42, 70 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 + 1) ∈
ℝ) | 
| 72 | 59, 33, 71 | leaddsub2d 11866 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (((𝑀 · (abs‘𝑧)) + (abs‘𝑧)) ≤ (𝑀 + 1) ↔ (abs‘𝑧) ≤ ((𝑀 + 1) − (𝑀 · (abs‘𝑧))))) | 
| 73 | 69, 72 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 · (abs‘𝑧)) + (abs‘𝑧)) ≤ (𝑀 + 1)) | 
| 74 | 57, 62 | adddirp1d 11288 | . . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) = ((𝑀 · (abs‘𝑧)) + (abs‘𝑧))) | 
| 75 | 71 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 + 1) ∈
ℂ) | 
| 76 | 75 | mulridd 11279 | . . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 + 1) · 1) = (𝑀 + 1)) | 
| 77 | 73, 74, 76 | 3brtr4d 5174 | . . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1)) | 
| 78 |  | 0red 11265 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 0 ∈
ℝ) | 
| 79 |  | simplr 768 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 0 ≤
𝑀) | 
| 80 | 42 | ltp1d 12199 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑀 < (𝑀 + 1)) | 
| 81 | 78, 42, 71, 79, 80 | lelttrd 11420 | . . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 0 <
(𝑀 + 1)) | 
| 82 |  | lemul2 12121 | . . . . . . . . . . . . . . . 16
⊢
(((abs‘𝑧)
∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝑀 + 1) ∈ ℝ ∧ 0 < (𝑀 + 1))) → ((abs‘𝑧) ≤ 1 ↔ ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1))) | 
| 83 | 33, 34, 71, 81, 82 | syl112anc 1375 | . . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) ≤ 1
↔ ((𝑀 + 1) ·
(abs‘𝑧)) ≤ ((𝑀 + 1) ·
1))) | 
| 84 | 77, 83 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) ≤
1) | 
| 85 | 41, 45, 53 | lensymd 11413 | . . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ¬
(𝑀 · (1 −
(abs‘𝑧))) <
(abs‘(1 − 𝑧))) | 
| 86 | 7 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · 0) =
0) | 
| 87 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑧 ≠ 1) | 
| 88 | 87 | necomd 2995 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 1 ≠
𝑧) | 
| 89 |  | subeq0 11536 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℂ ∧ 𝑧
∈ ℂ) → ((1 − 𝑧) = 0 ↔ 1 = 𝑧)) | 
| 90 | 89 | necon3bid 2984 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℂ ∧ 𝑧
∈ ℂ) → ((1 − 𝑧) ≠ 0 ↔ 1 ≠ 𝑧)) | 
| 91 | 38, 25, 90 | sylancr 587 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((1
− 𝑧) ≠ 0 ↔ 1
≠ 𝑧)) | 
| 92 | 88, 91 | mpbird 257 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (1
− 𝑧) ≠
0) | 
| 93 |  | absgt0 15364 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((1
− 𝑧) ∈ ℂ
→ ((1 − 𝑧) ≠
0 ↔ 0 < (abs‘(1 − 𝑧)))) | 
| 94 | 40, 93 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((1
− 𝑧) ≠ 0 ↔ 0
< (abs‘(1 − 𝑧)))) | 
| 95 | 92, 94 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 0 <
(abs‘(1 − 𝑧))) | 
| 96 | 86, 95 | eqbrtrd 5164 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · 0) < (abs‘(1
− 𝑧))) | 
| 97 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . 20
⊢ (1 =
(abs‘𝑧) → (1
− 1) = (1 − (abs‘𝑧))) | 
| 98 | 10, 97 | eqtr3id 2790 | . . . . . . . . . . . . . . . . . . 19
⊢ (1 =
(abs‘𝑧) → 0 = (1
− (abs‘𝑧))) | 
| 99 | 98 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ (1 =
(abs‘𝑧) → (𝑀 · 0) = (𝑀 · (1 −
(abs‘𝑧)))) | 
| 100 | 99 | breq1d 5152 | . . . . . . . . . . . . . . . . 17
⊢ (1 =
(abs‘𝑧) →
((𝑀 · 0) <
(abs‘(1 − 𝑧))
↔ (𝑀 · (1
− (abs‘𝑧)))
< (abs‘(1 − 𝑧)))) | 
| 101 | 96, 100 | syl5ibcom 245 | . . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (1 =
(abs‘𝑧) → (𝑀 · (1 −
(abs‘𝑧))) <
(abs‘(1 − 𝑧)))) | 
| 102 | 101 | necon3bd 2953 | . . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (¬
(𝑀 · (1 −
(abs‘𝑧))) <
(abs‘(1 − 𝑧))
→ 1 ≠ (abs‘𝑧))) | 
| 103 | 85, 102 | mpd 15 | . . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 1 ≠
(abs‘𝑧)) | 
| 104 | 33, 34, 84, 103 | leneltd 11416 | . . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) <
1) | 
| 105 | 32, 104 | eqbrtrd 5164 | . . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) <
1) | 
| 106 |  | cnxmet 24794 | . . . . . . . . . . . . . 14
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) | 
| 107 |  | 1xr 11321 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ* | 
| 108 |  | elbl3 24403 | . . . . . . . . . . . . . 14
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (0 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑧(abs ∘
− )0) < 1)) | 
| 109 | 106, 107,
108 | mpanl12 702 | . . . . . . . . . . . . 13
⊢ ((0
∈ ℂ ∧ 𝑧
∈ ℂ) → (𝑧
∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑧(abs ∘ − )0) <
1)) | 
| 110 | 26, 25, 109 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑧 ∈ (0(ball‘(abs
∘ − ))1) ↔ (𝑧(abs ∘ − )0) <
1)) | 
| 111 | 105, 110 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑧 ∈ (0(ball‘(abs
∘ − ))1)) | 
| 112 | 111 | expr 456 | . . . . . . . . . 10
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ (𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧))))) →
(𝑧 ≠ 1 → 𝑧 ∈ (0(ball‘(abs
∘ − ))1))) | 
| 113 | 112 | 3impb 1114 | . . . . . . . . 9
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (𝑧 ≠ 1 → 𝑧 ∈ (0(ball‘(abs ∘ −
))1))) | 
| 114 | 24, 113 | biimtrid 242 | . . . . . . . 8
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (¬ 𝑧 ∈ {1} → 𝑧 ∈ (0(ball‘(abs
∘ − ))1))) | 
| 115 | 114 | orrd 863 | . . . . . . 7
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (𝑧 ∈ {1} ∨ 𝑧 ∈ (0(ball‘(abs ∘ −
))1))) | 
| 116 |  | elun 4152 | . . . . . . 7
⊢ (𝑧 ∈ ({1} ∪
(0(ball‘(abs ∘ − ))1)) ↔ (𝑧 ∈ {1} ∨ 𝑧 ∈ (0(ball‘(abs ∘ −
))1))) | 
| 117 | 115, 116 | sylibr 234 | . . . . . 6
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → 𝑧 ∈ ({1} ∪ (0(ball‘(abs ∘
− ))1))) | 
| 118 | 117 | rabssdv 4074 | . . . . 5
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → {𝑧 ∈ ℂ ∣
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))} ⊆
({1} ∪ (0(ball‘(abs ∘ − ))1))) | 
| 119 | 20, 118 | eqsstrid 4021 | . . . 4
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 𝑆 ⊆ ({1} ∪ (0(ball‘(abs
∘ − ))1))) | 
| 120 |  | ssundif 4487 | . . . 4
⊢ (𝑆 ⊆ ({1} ∪
(0(ball‘(abs ∘ − ))1)) ↔ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1)) | 
| 121 | 119, 120 | sylib 218 | . . 3
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → (𝑆 ∖ {1}) ⊆
(0(ball‘(abs ∘ − ))1)) | 
| 122 | 22, 121 | jca 511 | . 2
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) | 
| 123 | 1, 2, 122 | syl2anc 584 | 1
⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) |