Proof of Theorem abelthlem2
Step | Hyp | Ref
| Expression |
1 | | abelth.3 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℝ) |
2 | | abelth.4 |
. 2
⊢ (𝜑 → 0 ≤ 𝑀) |
3 | | 1cnd 10056 |
. . . 4
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 1 ∈
ℂ) |
4 | | 0le0 11110 |
. . . . 5
⊢ 0 ≤
0 |
5 | | simpl 473 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 𝑀 ∈ ℝ) |
6 | 5 | recnd 10068 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 𝑀 ∈ ℂ) |
7 | 6 | mul01d 10235 |
. . . . 5
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → (𝑀 · 0) =
0) |
8 | 4, 7 | syl5breqr 4691 |
. . . 4
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 0 ≤ (𝑀 · 0)) |
9 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑧 = 1 → (1 − 𝑧) = (1 −
1)) |
10 | | 1m1e0 11089 |
. . . . . . . 8
⊢ (1
− 1) = 0 |
11 | 9, 10 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑧 = 1 → (1 − 𝑧) = 0) |
12 | 11 | abs00bd 14031 |
. . . . . 6
⊢ (𝑧 = 1 → (abs‘(1
− 𝑧)) =
0) |
13 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑧 = 1 → (abs‘𝑧) =
(abs‘1)) |
14 | | abs1 14037 |
. . . . . . . . . 10
⊢
(abs‘1) = 1 |
15 | 13, 14 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (abs‘𝑧) = 1) |
16 | 15 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑧 = 1 → (1 −
(abs‘𝑧)) = (1 −
1)) |
17 | 16, 10 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑧 = 1 → (1 −
(abs‘𝑧)) =
0) |
18 | 17 | oveq2d 6666 |
. . . . . 6
⊢ (𝑧 = 1 → (𝑀 · (1 − (abs‘𝑧))) = (𝑀 · 0)) |
19 | 12, 18 | breq12d 4666 |
. . . . 5
⊢ (𝑧 = 1 → ((abs‘(1
− 𝑧)) ≤ (𝑀 · (1 −
(abs‘𝑧))) ↔ 0
≤ (𝑀 ·
0))) |
20 | | abelth.5 |
. . . . 5
⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} |
21 | 19, 20 | elrab2 3366 |
. . . 4
⊢ (1 ∈
𝑆 ↔ (1 ∈ ℂ
∧ 0 ≤ (𝑀 ·
0))) |
22 | 3, 8, 21 | sylanbrc 698 |
. . 3
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 1 ∈ 𝑆) |
23 | | velsn 4193 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {1} ↔ 𝑧 = 1) |
24 | 23 | necon3bbii 2841 |
. . . . . . . . 9
⊢ (¬
𝑧 ∈ {1} ↔ 𝑧 ≠ 1) |
25 | | simprll 802 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑧 ∈
ℂ) |
26 | | 0cn 10032 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℂ |
27 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (abs
∘ − ) = (abs ∘ − ) |
28 | 27 | cnmetdval 22574 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑧(abs
∘ − )0) = (abs‘(𝑧 − 0))) |
29 | 25, 26, 28 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) =
(abs‘(𝑧 −
0))) |
30 | 25 | subid1d 10381 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑧 − 0) = 𝑧) |
31 | 30 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘(𝑧 − 0)) =
(abs‘𝑧)) |
32 | 29, 31 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) =
(abs‘𝑧)) |
33 | | simprlr 803 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) |
34 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
35 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℂ ∧ 𝑧
∈ ℂ) → (1 − 𝑧) ∈ ℂ) |
36 | 34, 25, 35 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (1
− 𝑧) ∈
ℂ) |
37 | 36 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘(1 − 𝑧))
∈ ℝ) |
38 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑀 ∈
ℝ) |
39 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ |
40 | 25 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) ∈
ℝ) |
41 | | resubcl 10345 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ ∧ (abs‘𝑧) ∈ ℝ) → (1 −
(abs‘𝑧)) ∈
ℝ) |
42 | 39, 40, 41 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (1
− (abs‘𝑧))
∈ ℝ) |
43 | 38, 42 | remulcld 10070 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · (1 −
(abs‘𝑧))) ∈
ℝ) |
44 | 37, 43 | lenltd 10183 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧))) ↔
¬ (𝑀 · (1
− (abs‘𝑧)))
< (abs‘(1 − 𝑧)))) |
45 | 33, 44 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ¬
(𝑀 · (1 −
(abs‘𝑧))) <
(abs‘(1 − 𝑧))) |
46 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · 0) =
0) |
47 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑧 ≠ 1) |
48 | 47 | necomd 2849 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 1 ≠
𝑧) |
49 | | subeq0 10307 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℂ ∧ 𝑧
∈ ℂ) → ((1 − 𝑧) = 0 ↔ 1 = 𝑧)) |
50 | 49 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℂ ∧ 𝑧
∈ ℂ) → ((1 − 𝑧) ≠ 0 ↔ 1 ≠ 𝑧)) |
51 | 34, 25, 50 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((1
− 𝑧) ≠ 0 ↔ 1
≠ 𝑧)) |
52 | 48, 51 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (1
− 𝑧) ≠
0) |
53 | | absgt0 14064 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
− 𝑧) ∈ ℂ
→ ((1 − 𝑧) ≠
0 ↔ 0 < (abs‘(1 − 𝑧)))) |
54 | 36, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((1
− 𝑧) ≠ 0 ↔ 0
< (abs‘(1 − 𝑧)))) |
55 | 52, 54 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 0 <
(abs‘(1 − 𝑧))) |
56 | 46, 55 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · 0) < (abs‘(1
− 𝑧))) |
57 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 =
(abs‘𝑧) → (1
− 1) = (1 − (abs‘𝑧))) |
58 | 10, 57 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 =
(abs‘𝑧) → 0 = (1
− (abs‘𝑧))) |
59 | 58 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 =
(abs‘𝑧) → (𝑀 · 0) = (𝑀 · (1 −
(abs‘𝑧)))) |
60 | 59 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
⊢ (1 =
(abs‘𝑧) →
((𝑀 · 0) <
(abs‘(1 − 𝑧))
↔ (𝑀 · (1
− (abs‘𝑧)))
< (abs‘(1 − 𝑧)))) |
61 | 56, 60 | syl5ibcom 235 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (1 =
(abs‘𝑧) → (𝑀 · (1 −
(abs‘𝑧))) <
(abs‘(1 − 𝑧)))) |
62 | 61 | necon3bd 2808 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (¬
(𝑀 · (1 −
(abs‘𝑧))) <
(abs‘(1 − 𝑧))
→ 1 ≠ (abs‘𝑧))) |
63 | 45, 62 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 1 ≠
(abs‘𝑧)) |
64 | | 1red 10055 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 1 ∈
ℝ) |
65 | | resubcl 10345 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((abs‘𝑧)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑧) − 1) ∈ ℝ) |
66 | 40, 39, 65 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) − 1)
∈ ℝ) |
67 | 14 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((abs‘𝑧)
− (abs‘1)) = ((abs‘𝑧) − 1) |
68 | | abs2dif 14072 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℂ ∧ 1 ∈
ℂ) → ((abs‘𝑧) − (abs‘1)) ≤
(abs‘(𝑧 −
1))) |
69 | 25, 34, 68 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) −
(abs‘1)) ≤ (abs‘(𝑧 − 1))) |
70 | 67, 69 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) − 1)
≤ (abs‘(𝑧 −
1))) |
71 | | abssub 14066 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℂ ∧ 1 ∈
ℂ) → (abs‘(𝑧 − 1)) = (abs‘(1 − 𝑧))) |
72 | 25, 34, 71 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘(𝑧 − 1)) =
(abs‘(1 − 𝑧))) |
73 | 70, 72 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) − 1)
≤ (abs‘(1 − 𝑧))) |
74 | 66, 37, 43, 73, 33 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) − 1)
≤ (𝑀 · (1 −
(abs‘𝑧)))) |
75 | 40, 64, 43 | lesubaddd 10624 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(((abs‘𝑧) − 1)
≤ (𝑀 · (1 −
(abs‘𝑧))) ↔
(abs‘𝑧) ≤ ((𝑀 · (1 −
(abs‘𝑧))) +
1))) |
76 | 74, 75 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) ≤ ((𝑀 · (1 −
(abs‘𝑧))) +
1)) |
77 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑀 ∈
ℂ) |
78 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 1 ∈
ℂ) |
79 | 38, 40 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · (abs‘𝑧)) ∈
ℝ) |
80 | 79 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · (abs‘𝑧)) ∈
ℂ) |
81 | 77, 78, 80 | addsubd 10413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 + 1) − (𝑀 · (abs‘𝑧))) = ((𝑀 − (𝑀 · (abs‘𝑧))) + 1)) |
82 | 40 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) ∈
ℂ) |
83 | 77, 78, 82 | subdid 10486 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · (1 −
(abs‘𝑧))) = ((𝑀 · 1) − (𝑀 · (abs‘𝑧)))) |
84 | 77 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · 1) = 𝑀) |
85 | 84 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 · 1) − (𝑀 · (abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧)))) |
86 | 83, 85 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 · (1 −
(abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧)))) |
87 | 86 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 · (1 −
(abs‘𝑧))) + 1) =
((𝑀 − (𝑀 · (abs‘𝑧))) + 1)) |
88 | 81, 87 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 + 1) − (𝑀 · (abs‘𝑧))) = ((𝑀 · (1 − (abs‘𝑧))) + 1)) |
89 | 76, 88 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) ≤ ((𝑀 + 1) − (𝑀 · (abs‘𝑧)))) |
90 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
91 | 38, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 + 1) ∈
ℝ) |
92 | 79, 40, 91 | leaddsub2d 10629 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (((𝑀 · (abs‘𝑧)) + (abs‘𝑧)) ≤ (𝑀 + 1) ↔ (abs‘𝑧) ≤ ((𝑀 + 1) − (𝑀 · (abs‘𝑧))))) |
93 | 89, 92 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 · (abs‘𝑧)) + (abs‘𝑧)) ≤ (𝑀 + 1)) |
94 | 77, 78, 82 | adddird 10065 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) = ((𝑀 · (abs‘𝑧)) + (1 · (abs‘𝑧)))) |
95 | 82 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (1
· (abs‘𝑧)) =
(abs‘𝑧)) |
96 | 95 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 · (abs‘𝑧)) + (1 ·
(abs‘𝑧))) = ((𝑀 · (abs‘𝑧)) + (abs‘𝑧))) |
97 | 94, 96 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) = ((𝑀 · (abs‘𝑧)) + (abs‘𝑧))) |
98 | 91 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑀 + 1) ∈
ℂ) |
99 | 98 | mulid1d 10057 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 + 1) · 1) = (𝑀 + 1)) |
100 | 93, 97, 99 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1)) |
101 | | 0red 10041 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 0 ∈
ℝ) |
102 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 0 ≤
𝑀) |
103 | 38 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑀 < (𝑀 + 1)) |
104 | 101, 38, 91, 102, 103 | lelttrd 10195 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 0 <
(𝑀 + 1)) |
105 | | lemul2 10876 |
. . . . . . . . . . . . . . . . 17
⊢
(((abs‘𝑧)
∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝑀 + 1) ∈ ℝ ∧ 0 < (𝑀 + 1))) → ((abs‘𝑧) ≤ 1 ↔ ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1))) |
106 | 40, 64, 91, 104, 105 | syl112anc 1330 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) ≤ 1
↔ ((𝑀 + 1) ·
(abs‘𝑧)) ≤ ((𝑀 + 1) ·
1))) |
107 | 100, 106 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) ≤
1) |
108 | 40, 64, 107 | leltned 10190 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
((abs‘𝑧) < 1
↔ 1 ≠ (abs‘𝑧))) |
109 | 63, 108 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) →
(abs‘𝑧) <
1) |
110 | 32, 109 | eqbrtrd 4675 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) <
1) |
111 | | cnxmet 22576 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
112 | | 1rp 11836 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ+ |
113 | | rpxr 11840 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
114 | 112, 113 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ* |
115 | | elbl3 22197 |
. . . . . . . . . . . . . 14
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (0 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑧(abs ∘
− )0) < 1)) |
116 | 111, 114,
115 | mpanl12 718 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℂ ∧ 𝑧
∈ ℂ) → (𝑧
∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑧(abs ∘ − )0) <
1)) |
117 | 26, 25, 116 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → (𝑧 ∈ (0(ball‘(abs
∘ − ))1) ↔ (𝑧(abs ∘ − )0) <
1)) |
118 | 110, 117 | mpbird 247 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ ((𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))) ∧
𝑧 ≠ 1)) → 𝑧 ∈ (0(ball‘(abs
∘ − ))1)) |
119 | 118 | expr 643 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ (𝑧 ∈ ℂ ∧
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧))))) →
(𝑧 ≠ 1 → 𝑧 ∈ (0(ball‘(abs
∘ − ))1))) |
120 | 119 | 3impb 1260 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (𝑧 ≠ 1 → 𝑧 ∈ (0(ball‘(abs ∘ −
))1))) |
121 | 24, 120 | syl5bi 232 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (¬ 𝑧 ∈ {1} → 𝑧 ∈ (0(ball‘(abs
∘ − ))1))) |
122 | 121 | orrd 393 |
. . . . . . 7
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (𝑧 ∈ {1} ∨ 𝑧 ∈ (0(ball‘(abs ∘ −
))1))) |
123 | | elun 3753 |
. . . . . . 7
⊢ (𝑧 ∈ ({1} ∪
(0(ball‘(abs ∘ − ))1)) ↔ (𝑧 ∈ {1} ∨ 𝑧 ∈ (0(ball‘(abs ∘ −
))1))) |
124 | 122, 123 | sylibr 224 |
. . . . . 6
⊢ (((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → 𝑧 ∈ ({1} ∪ (0(ball‘(abs ∘
− ))1))) |
125 | 124 | rabssdv 3682 |
. . . . 5
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → {𝑧 ∈ ℂ ∣
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))} ⊆
({1} ∪ (0(ball‘(abs ∘ − ))1))) |
126 | 20, 125 | syl5eqss 3649 |
. . . 4
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → 𝑆 ⊆ ({1} ∪ (0(ball‘(abs
∘ − ))1))) |
127 | | ssundif 4052 |
. . . 4
⊢ (𝑆 ⊆ ({1} ∪
(0(ball‘(abs ∘ − ))1)) ↔ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1)) |
128 | 126, 127 | sylib 208 |
. . 3
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → (𝑆 ∖ {1}) ⊆
(0(ball‘(abs ∘ − ))1)) |
129 | 22, 128 | jca 554 |
. 2
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) |
130 | 1, 2, 129 | syl2anc 693 |
1
⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) |