This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abelthlem2

Description: Lemma for abelth . The peculiar region S , known as aStolz angle , is a teardrop-shaped subset of the closed unit ball containing 1 . Indeed, except for 1 itself, the rest of the Stolz angle is enclosed in the open unit ball. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
Assertion abelthlem2 ( 𝜑 → ( 1 ∈ 𝑆 ∧ ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )

Proof

Step Hyp Ref Expression
1 abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
2 abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
3 abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
4 abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
5 abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
6 1cnd ⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → 1 ∈ ℂ )
7 0le0 ⊢ 0 ≤ 0
8 simpl ⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → 𝑀 ∈ ℝ )
9 8 recnd ⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → 𝑀 ∈ ℂ )
10 9 mul01d ⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → ( 𝑀 · 0 ) = 0 )
11 7 10 breqtrrid ⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → 0 ≤ ( 𝑀 · 0 ) )
12 oveq2 ⊢ ( 𝑧 = 1 → ( 1 − 𝑧 ) = ( 1 − 1 ) )
13 1m1e0 ⊢ ( 1 − 1 ) = 0
14 12 13 eqtrdi ⊢ ( 𝑧 = 1 → ( 1 − 𝑧 ) = 0 )
15 14 abs00bd ⊢ ( 𝑧 = 1 → ( abs ‘ ( 1 − 𝑧 ) ) = 0 )
16 fveq2 ⊢ ( 𝑧 = 1 → ( abs ‘ 𝑧 ) = ( abs ‘ 1 ) )
17 abs1 ⊢ ( abs ‘ 1 ) = 1
18 16 17 eqtrdi ⊢ ( 𝑧 = 1 → ( abs ‘ 𝑧 ) = 1 )
19 18 oveq2d ⊢ ( 𝑧 = 1 → ( 1 − ( abs ‘ 𝑧 ) ) = ( 1 − 1 ) )
20 19 13 eqtrdi ⊢ ( 𝑧 = 1 → ( 1 − ( abs ‘ 𝑧 ) ) = 0 )
21 20 oveq2d ⊢ ( 𝑧 = 1 → ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) = ( 𝑀 · 0 ) )
22 15 21 breq12d ⊢ ( 𝑧 = 1 → ( ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ↔ 0 ≤ ( 𝑀 · 0 ) ) )
23 22 5 elrab2 ⊢ ( 1 ∈ 𝑆 ↔ ( 1 ∈ ℂ ∧ 0 ≤ ( 𝑀 · 0 ) ) )
24 6 11 23 sylanbrc ⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → 1 ∈ 𝑆 )
25 velsn ⊢ ( 𝑧 ∈ { 1 } ↔ 𝑧 = 1 )
26 25 necon3bbii ⊢ ( ¬ 𝑧 ∈ { 1 } ↔ 𝑧 ≠ 1 )
27 simprll ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 𝑧 ∈ ℂ )
28 0cn ⊢ 0 ∈ ℂ
29 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
30 29 cnmetdval ⊢ ( ( 𝑧 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑧 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑧 − 0 ) ) )
31 27 28 30 sylancl ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑧 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑧 − 0 ) ) )
32 27 subid1d ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑧 − 0 ) = 𝑧 )
33 32 fveq2d ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( abs ‘ ( 𝑧 − 0 ) ) = ( abs ‘ 𝑧 ) )
34 31 33 eqtrd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑧 ( abs ∘ − ) 0 ) = ( abs ‘ 𝑧 ) )
35 27 abscld ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( abs ‘ 𝑧 ) ∈ ℝ )
36 1red ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 1 ∈ ℝ )
37 1re ⊢ 1 ∈ ℝ
38 resubcl ⊢ ( ( ( abs ‘ 𝑧 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝑧 ) − 1 ) ∈ ℝ )
39 35 37 38 sylancl ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( abs ‘ 𝑧 ) − 1 ) ∈ ℝ )
40 ax-1cn ⊢ 1 ∈ ℂ
41 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 1 − 𝑧 ) ∈ ℂ )
42 40 27 41 sylancr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 1 − 𝑧 ) ∈ ℂ )
43 42 abscld ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( abs ‘ ( 1 − 𝑧 ) ) ∈ ℝ )
44 simpll ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 𝑀 ∈ ℝ )
45 resubcl ⊢ ( ( 1 ∈ ℝ ∧ ( abs ‘ 𝑧 ) ∈ ℝ ) → ( 1 − ( abs ‘ 𝑧 ) ) ∈ ℝ )
46 37 35 45 sylancr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 1 − ( abs ‘ 𝑧 ) ) ∈ ℝ )
47 44 46 remulcld ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ∈ ℝ )
48 17 oveq2i ⊢ ( ( abs ‘ 𝑧 ) − ( abs ‘ 1 ) ) = ( ( abs ‘ 𝑧 ) − 1 )
49 abs2dif ⊢ ( ( 𝑧 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( abs ‘ 𝑧 ) − ( abs ‘ 1 ) ) ≤ ( abs ‘ ( 𝑧 − 1 ) ) )
50 27 40 49 sylancl ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( abs ‘ 𝑧 ) − ( abs ‘ 1 ) ) ≤ ( abs ‘ ( 𝑧 − 1 ) ) )
51 48 50 eqbrtrrid ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( abs ‘ 𝑧 ) − 1 ) ≤ ( abs ‘ ( 𝑧 − 1 ) ) )
52 abssub ⊢ ( ( 𝑧 ∈ ℂ ∧ 1 ∈ ℂ ) → ( abs ‘ ( 𝑧 − 1 ) ) = ( abs ‘ ( 1 − 𝑧 ) ) )
53 27 40 52 sylancl ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( abs ‘ ( 𝑧 − 1 ) ) = ( abs ‘ ( 1 − 𝑧 ) ) )
54 51 53 breqtrd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( abs ‘ 𝑧 ) − 1 ) ≤ ( abs ‘ ( 1 − 𝑧 ) ) )
55 simprlr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) )
56 39 43 47 54 55 letrd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( abs ‘ 𝑧 ) − 1 ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) )
57 35 36 47 lesubaddd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( ( abs ‘ 𝑧 ) − 1 ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ↔ ( abs ‘ 𝑧 ) ≤ ( ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) + 1 ) ) )
58 56 57 mpbid ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( abs ‘ 𝑧 ) ≤ ( ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) + 1 ) )
59 9 adantr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 𝑀 ∈ ℂ )
60 1cnd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 1 ∈ ℂ )
61 44 35 remulcld ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑀 · ( abs ‘ 𝑧 ) ) ∈ ℝ )
62 61 recnd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑀 · ( abs ‘ 𝑧 ) ) ∈ ℂ )
63 59 60 62 addsubd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( 𝑀 + 1 ) − ( 𝑀 · ( abs ‘ 𝑧 ) ) ) = ( ( 𝑀 − ( 𝑀 · ( abs ‘ 𝑧 ) ) ) + 1 ) )
64 35 recnd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( abs ‘ 𝑧 ) ∈ ℂ )
65 59 60 64 subdid ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) = ( ( 𝑀 · 1 ) − ( 𝑀 · ( abs ‘ 𝑧 ) ) ) )
66 59 mulridd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑀 · 1 ) = 𝑀 )
67 66 oveq1d ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( 𝑀 · 1 ) − ( 𝑀 · ( abs ‘ 𝑧 ) ) ) = ( 𝑀 − ( 𝑀 · ( abs ‘ 𝑧 ) ) ) )
68 65 67 eqtrd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) = ( 𝑀 − ( 𝑀 · ( abs ‘ 𝑧 ) ) ) )
69 68 oveq1d ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) + 1 ) = ( ( 𝑀 − ( 𝑀 · ( abs ‘ 𝑧 ) ) ) + 1 ) )
70 63 69 eqtr4d ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( 𝑀 + 1 ) − ( 𝑀 · ( abs ‘ 𝑧 ) ) ) = ( ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) + 1 ) )
71 58 70 breqtrrd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( abs ‘ 𝑧 ) ≤ ( ( 𝑀 + 1 ) − ( 𝑀 · ( abs ‘ 𝑧 ) ) ) )
72 peano2re ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 + 1 ) ∈ ℝ )
73 44 72 syl ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑀 + 1 ) ∈ ℝ )
74 61 35 73 leaddsub2d ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( ( 𝑀 · ( abs ‘ 𝑧 ) ) + ( abs ‘ 𝑧 ) ) ≤ ( 𝑀 + 1 ) ↔ ( abs ‘ 𝑧 ) ≤ ( ( 𝑀 + 1 ) − ( 𝑀 · ( abs ‘ 𝑧 ) ) ) ) )
75 71 74 mpbird ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( 𝑀 · ( abs ‘ 𝑧 ) ) + ( abs ‘ 𝑧 ) ) ≤ ( 𝑀 + 1 ) )
76 59 64 adddirp1d ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( 𝑀 + 1 ) · ( abs ‘ 𝑧 ) ) = ( ( 𝑀 · ( abs ‘ 𝑧 ) ) + ( abs ‘ 𝑧 ) ) )
77 73 recnd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑀 + 1 ) ∈ ℂ )
78 77 mulridd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( 𝑀 + 1 ) · 1 ) = ( 𝑀 + 1 ) )
79 75 76 78 3brtr4d ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( 𝑀 + 1 ) · ( abs ‘ 𝑧 ) ) ≤ ( ( 𝑀 + 1 ) · 1 ) )
80 0red ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 0 ∈ ℝ )
81 simplr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 0 ≤ 𝑀 )
82 44 ltp1d ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 𝑀 < ( 𝑀 + 1 ) )
83 80 44 73 81 82 lelttrd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 0 < ( 𝑀 + 1 ) )
84 lemul2 ⊢ ( ( ( abs ‘ 𝑧 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝑀 + 1 ) ∈ ℝ ∧ 0 < ( 𝑀 + 1 ) ) ) → ( ( abs ‘ 𝑧 ) ≤ 1 ↔ ( ( 𝑀 + 1 ) · ( abs ‘ 𝑧 ) ) ≤ ( ( 𝑀 + 1 ) · 1 ) ) )
85 35 36 73 83 84 syl112anc ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( abs ‘ 𝑧 ) ≤ 1 ↔ ( ( 𝑀 + 1 ) · ( abs ‘ 𝑧 ) ) ≤ ( ( 𝑀 + 1 ) · 1 ) ) )
86 79 85 mpbird ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( abs ‘ 𝑧 ) ≤ 1 )
87 43 47 55 lensymd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ¬ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) < ( abs ‘ ( 1 − 𝑧 ) ) )
88 10 adantr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑀 · 0 ) = 0 )
89 simprr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 𝑧 ≠ 1 )
90 89 necomd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 1 ≠ 𝑧 )
91 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 1 − 𝑧 ) = 0 ↔ 1 = 𝑧 ) )
92 91 necon3bid ⊢ ( ( 1 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 1 − 𝑧 ) ≠ 0 ↔ 1 ≠ 𝑧 ) )
93 40 27 92 sylancr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( 1 − 𝑧 ) ≠ 0 ↔ 1 ≠ 𝑧 ) )
94 90 93 mpbird ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 1 − 𝑧 ) ≠ 0 )
95 absgt0 ⊢ ( ( 1 − 𝑧 ) ∈ ℂ → ( ( 1 − 𝑧 ) ≠ 0 ↔ 0 < ( abs ‘ ( 1 − 𝑧 ) ) ) )
96 42 95 syl ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ( 1 − 𝑧 ) ≠ 0 ↔ 0 < ( abs ‘ ( 1 − 𝑧 ) ) ) )
97 94 96 mpbid ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 0 < ( abs ‘ ( 1 − 𝑧 ) ) )
98 88 97 eqbrtrd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑀 · 0 ) < ( abs ‘ ( 1 − 𝑧 ) ) )
99 oveq2 ⊢ ( 1 = ( abs ‘ 𝑧 ) → ( 1 − 1 ) = ( 1 − ( abs ‘ 𝑧 ) ) )
100 13 99 eqtr3id ⊢ ( 1 = ( abs ‘ 𝑧 ) → 0 = ( 1 − ( abs ‘ 𝑧 ) ) )
101 100 oveq2d ⊢ ( 1 = ( abs ‘ 𝑧 ) → ( 𝑀 · 0 ) = ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) )
102 101 breq1d ⊢ ( 1 = ( abs ‘ 𝑧 ) → ( ( 𝑀 · 0 ) < ( abs ‘ ( 1 − 𝑧 ) ) ↔ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) < ( abs ‘ ( 1 − 𝑧 ) ) ) )
103 98 102 syl5ibcom ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 1 = ( abs ‘ 𝑧 ) → ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) < ( abs ‘ ( 1 − 𝑧 ) ) ) )
104 103 necon3bd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( ¬ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) < ( abs ‘ ( 1 − 𝑧 ) ) → 1 ≠ ( abs ‘ 𝑧 ) ) )
105 87 104 mpd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 1 ≠ ( abs ‘ 𝑧 ) )
106 35 36 86 105 leneltd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( abs ‘ 𝑧 ) < 1 )
107 34 106 eqbrtrd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑧 ( abs ∘ − ) 0 ) < 1 )
108 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
109 1xr ⊢ 1 ∈ ℝ*
110 elbl3 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℝ* ) ∧ ( 0 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑧 ( abs ∘ − ) 0 ) < 1 ) )
111 108 109 110 mpanl12 ⊢ ( ( 0 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑧 ( abs ∘ − ) 0 ) < 1 ) )
112 28 27 111 sylancr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → ( 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑧 ( abs ∘ − ) 0 ) < 1 ) )
113 107 112 mpbird ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ∧ 𝑧 ≠ 1 ) ) → 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
114 113 expr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) ) → ( 𝑧 ≠ 1 → 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
115 114 3impb ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) → ( 𝑧 ≠ 1 → 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
116 26 115 biimtrid ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) → ( ¬ 𝑧 ∈ { 1 } → 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
117 116 orrd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) → ( 𝑧 ∈ { 1 } ∨ 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
118 elun ⊢ ( 𝑧 ∈ ( { 1 } ∪ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ↔ ( 𝑧 ∈ { 1 } ∨ 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
119 117 118 sylibr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ 𝑧 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) ) → 𝑧 ∈ ( { 1 } ∪ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
120 119 rabssdv ⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) } ⊆ ( { 1 } ∪ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
121 5 120 eqsstrid ⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → 𝑆 ⊆ ( { 1 } ∪ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
122 ssundif ⊢ ( 𝑆 ⊆ ( { 1 } ∪ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ↔ ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
123 121 122 sylib ⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
124 24 123 jca ⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → ( 1 ∈ 𝑆 ∧ ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
125 3 4 124 syl2anc ⊢ ( 𝜑 → ( 1 ∈ 𝑆 ∧ ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )