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 
|- ( ph -> A : NN0 --> CC )
abelth.2 
|- ( ph -> seq 0 ( + , A ) e. dom ~~> )
abelth.3 
|- ( ph -> M e. RR )
abelth.4 
|- ( ph -> 0 <_ M )
abelth.5 
|- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }
Assertion abelthlem2 
|- ( ph -> ( 1 e. S /\ ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) ) )

Proof

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