MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abelthlem2 Unicode version

Theorem abelthlem2 20026
Description: Lemma for abelth 20035. The peculiar region  S, known as a Stolz 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.)
Hypotheses
Ref Expression
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
Ref Expression
abelthlem2  |-  ( ph  ->  ( 1  e.  S  /\  ( S  \  {
1 } )  C_  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) ) )
Distinct variable groups:    z, M    z, A
Allowed substitution hints:    ph( z)    S( z)

Proof of Theorem abelthlem2
StepHypRef Expression
1 abelth.3 . 2  |-  ( ph  ->  M  e.  RR )
2 abelth.4 . 2  |-  ( ph  ->  0  <_  M )
3 ax-1cn 8942 . . . . 5  |-  1  e.  CC
43a1i 10 . . . 4  |-  ( ( M  e.  RR  /\  0  <_  M )  -> 
1  e.  CC )
5 0le0 9974 . . . . 5  |-  0  <_  0
6 simpl 443 . . . . . . 7  |-  ( ( M  e.  RR  /\  0  <_  M )  ->  M  e.  RR )
76recnd 9008 . . . . . 6  |-  ( ( M  e.  RR  /\  0  <_  M )  ->  M  e.  CC )
87mul01d 9158 . . . . 5  |-  ( ( M  e.  RR  /\  0  <_  M )  -> 
( M  x.  0 )  =  0 )
95, 8syl5breqr 4161 . . . 4  |-  ( ( M  e.  RR  /\  0  <_  M )  -> 
0  <_  ( M  x.  0 ) )
10 oveq2 5989 . . . . . . . . 9  |-  ( z  =  1  ->  (
1  -  z )  =  ( 1  -  1 ) )
11 1m1e0 9961 . . . . . . . . 9  |-  ( 1  -  1 )  =  0
1210, 11syl6eq 2414 . . . . . . . 8  |-  ( z  =  1  ->  (
1  -  z )  =  0 )
1312fveq2d 5636 . . . . . . 7  |-  ( z  =  1  ->  ( abs `  ( 1  -  z ) )  =  ( abs `  0
) )
14 abs0 11977 . . . . . . 7  |-  ( abs `  0 )  =  0
1513, 14syl6eq 2414 . . . . . 6  |-  ( z  =  1  ->  ( abs `  ( 1  -  z ) )  =  0 )
16 fveq2 5632 . . . . . . . . . 10  |-  ( z  =  1  ->  ( abs `  z )  =  ( abs `  1
) )
17 abs1 11989 . . . . . . . . . 10  |-  ( abs `  1 )  =  1
1816, 17syl6eq 2414 . . . . . . . . 9  |-  ( z  =  1  ->  ( abs `  z )  =  1 )
1918oveq2d 5997 . . . . . . . 8  |-  ( z  =  1  ->  (
1  -  ( abs `  z ) )  =  ( 1  -  1 ) )
2019, 11syl6eq 2414 . . . . . . 7  |-  ( z  =  1  ->  (
1  -  ( abs `  z ) )  =  0 )
2120oveq2d 5997 . . . . . 6  |-  ( z  =  1  ->  ( M  x.  ( 1  -  ( abs `  z
) ) )  =  ( M  x.  0 ) )
2215, 21breq12d 4138 . . . . 5  |-  ( z  =  1  ->  (
( abs `  (
1  -  z ) )  <_  ( M  x.  ( 1  -  ( abs `  z ) ) )  <->  0  <_  ( M  x.  0 ) ) )
23 abelth.5 . . . . 5  |-  S  =  { z  e.  CC  |  ( abs `  (
1  -  z ) )  <_  ( M  x.  ( 1  -  ( abs `  z ) ) ) }
2422, 23elrab2 3011 . . . 4  |-  ( 1  e.  S  <->  ( 1  e.  CC  /\  0  <_  ( M  x.  0 ) ) )
254, 9, 24sylanbrc 645 . . 3  |-  ( ( M  e.  RR  /\  0  <_  M )  -> 
1  e.  S )
26 elsn 3744 . . . . . . . . . 10  |-  ( z  e.  { 1 }  <-> 
z  =  1 )
2726necon3bbii 2560 . . . . . . . . 9  |-  ( -.  z  e.  { 1 }  <->  z  =/=  1
)
28 simprll 738 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  z  e.  CC )
29 0cn 8978 . . . . . . . . . . . . . . 15  |-  0  e.  CC
30 eqid 2366 . . . . . . . . . . . . . . . 16  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
3130cnmetdval 18493 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  CC  /\  0  e.  CC )  ->  ( z ( abs 
o.  -  ) 0 )  =  ( abs `  ( z  -  0 ) ) )
3228, 29, 31sylancl 643 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
3328subid1d 9293 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
z  -  0 )  =  z )
3433fveq2d 5636 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( abs `  ( z  - 
0 ) )  =  ( abs `  z
) )
3532, 34eqtrd 2398 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
z ( abs  o.  -  ) 0 )  =  ( abs `  z
) )
36 simprlr 739 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
37 subcl 9198 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  CC  /\  z  e.  CC )  ->  ( 1  -  z
)  e.  CC )
383, 28, 37sylancr 644 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
1  -  z )  e.  CC )
3938abscld 12125 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( abs `  ( 1  -  z ) )  e.  RR )
40 simpll 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  M  e.  RR )
41 1re 8984 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  RR
4228abscld 12125 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( abs `  z )  e.  RR )
43 resubcl 9258 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  RR  /\  ( abs `  z )  e.  RR )  -> 
( 1  -  ( abs `  z ) )  e.  RR )
4441, 42, 43sylancr 644 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
1  -  ( abs `  z ) )  e.  RR )
4540, 44remulcld 9010 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
4639, 45lenltd 9112 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )  <->  -.  ( M  x.  ( 1  -  ( abs `  z ) ) )  <  ( abs `  ( 1  -  z
) ) ) )
4736, 46mpbid 201 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
488adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( M  x.  0 )  =  0 )
49 simprr 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  z  =/=  1 )
5049necomd 2612 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  1  =/=  z )
51 subeq0 9220 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1  e.  CC  /\  z  e.  CC )  ->  ( ( 1  -  z )  =  0  <->  1  =  z ) )
5251necon3bid 2564 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  CC  /\  z  e.  CC )  ->  ( ( 1  -  z )  =/=  0  <->  1  =/=  z ) )
533, 28, 52sylancr 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
( 1  -  z
)  =/=  0  <->  1  =/=  z ) )
5450, 53mpbird 223 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
1  -  z )  =/=  0 )
55 absgt0 12015 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  -  z )  e.  CC  ->  (
( 1  -  z
)  =/=  0  <->  0  <  ( abs `  (
1  -  z ) ) ) )
5638, 55syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) ) ) )
5754, 56mpbid 201 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  0  <  ( abs `  (
1  -  z ) ) )
5848, 57eqbrtrd 4145 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( M  x.  0 )  <  ( abs `  (
1  -  z ) ) )
59 oveq2 5989 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  =  ( abs `  z
)  ->  ( 1  -  1 )  =  ( 1  -  ( abs `  z ) ) )
6011, 59syl5eqr 2412 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  =  ( abs `  z
)  ->  0  =  ( 1  -  ( abs `  z ) ) )
6160oveq2d 5997 . . . . . . . . . . . . . . . . . 18  |-  ( 1  =  ( abs `  z
)  ->  ( M  x.  0 )  =  ( M  x.  ( 1  -  ( abs `  z
) ) ) )
6261breq1d 4135 . . . . . . . . . . . . . . . . 17  |-  ( 1  =  ( abs `  z
)  ->  ( ( M  x.  0 )  <  ( abs `  (
1  -  z ) )  <->  ( M  x.  ( 1  -  ( abs `  z ) ) )  <  ( abs `  ( 1  -  z
) ) ) )
6358, 62syl5ibcom 211 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
6463necon3bd 2566 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
6547, 64mpd 14 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  1  =/=  ( abs `  z
) )
6641a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  1  e.  RR )
67 resubcl 9258 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( abs `  z
)  e.  RR  /\  1  e.  RR )  ->  ( ( abs `  z
)  -  1 )  e.  RR )
6842, 41, 67sylancl 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
( abs `  z
)  -  1 )  e.  RR )
6917oveq2i 5992 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( abs `  z )  -  ( abs `  1
) )  =  ( ( abs `  z
)  -  1 )
70 abs2dif 12023 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( z  e.  CC  /\  1  e.  CC )  ->  ( ( abs `  z
)  -  ( abs `  1 ) )  <_  ( abs `  (
z  -  1 ) ) )
7128, 3, 70sylancl 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) ) )
7269, 71syl5eqbrr 4159 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
( abs `  z
)  -  1 )  <_  ( abs `  (
z  -  1 ) ) )
73 abssub 12017 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( z  e.  CC  /\  1  e.  CC )  ->  ( abs `  (
z  -  1 ) )  =  ( abs `  ( 1  -  z
) ) )
7428, 3, 73sylancl 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( abs `  ( z  - 
1 ) )  =  ( abs `  (
1  -  z ) ) )
7572, 74breqtrd 4149 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
( abs `  z
)  -  1 )  <_  ( abs `  (
1  -  z ) ) )
7668, 39, 45, 75, 36letrd 9120 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) ) )
7742, 66, 45lesubaddd 9516 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) )
7876, 77mpbid 201 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) )
797adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  M  e.  CC )
803a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  1  e.  CC )
8140, 42remulcld 9010 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( M  x.  ( abs `  z ) )  e.  RR )
8281recnd 9008 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( M  x.  ( abs `  z ) )  e.  CC )
8379, 80, 82addsubd 9325 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) )
8442recnd 9008 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( abs `  z )  e.  CC )
8579, 80, 84subdid 9382 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) ) ) )
8679mulid1d 8999 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( M  x.  1 )  =  M )
8786oveq1d 5996 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) ) ) )
8885, 87eqtrd 2398 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 ) ) ) )
8988oveq1d 5996 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) )
9083, 89eqtr4d 2401 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) )
9178, 90breqtrrd 4151 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) ) )
92 peano2re 9132 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  RR  ->  ( M  +  1 )  e.  RR )
9340, 92syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( M  +  1 )  e.  RR )
9481, 42, 93leaddsub2d 9521 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) ) ) )
9591, 94mpbird 223 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
9679, 80, 84adddird 9007 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) )  +  ( 1  x.  ( abs `  z
) ) ) )
9784mulid2d 9000 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
1  x.  ( abs `  z ) )  =  ( abs `  z
) )
9897oveq2d 5997 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
( M  x.  ( abs `  z ) )  +  ( 1  x.  ( abs `  z
) ) )  =  ( ( M  x.  ( abs `  z ) )  +  ( abs `  z ) ) )
9996, 98eqtrd 2398 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) )
10093recnd 9008 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( M  +  1 )  e.  CC )
101100mulid1d 8999 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
( M  +  1 )  x.  1 )  =  ( M  + 
1 ) )
10295, 99, 1013brtr4d 4155 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) )
103 0re 8985 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  RR
104103a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  0  e.  RR )
105 simplr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  0  <_  M )
10640ltp1d 9834 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  M  <  ( M  +  1 ) )
107104, 40, 93, 105, 106lelttrd 9121 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  0  <  ( M  +  1 ) )
108 lemul2 9756 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) )
10942, 66, 93, 107, 108syl112anc 1187 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
110102, 109mpbird 223 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( abs `  z )  <_ 
1 )
11142, 66, 110leltned 9117 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
( abs `  z
)  <  1  <->  1  =/=  ( abs `  z ) ) )
11265, 111mpbird 223 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  ( abs `  z )  <  1 )
11335, 112eqbrtrd 4145 . . . . . . . . . . . 12  |-  ( ( ( M  e.  RR  /\  0  <_  M )  /\  ( ( z  e.  CC  /\  ( abs `  ( 1  -  z
) )  <_  ( M  x.  ( 1  -  ( abs `  z
) ) ) )  /\  z  =/=  1
) )  ->  (
z ( abs  o.  -  ) 0 )  <  1 )
114 cnxmet 18495 . . . . . . . . . . . . . 14  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
115 1rp 10509 . . . . . . . . . . . . . . 15  |-  1  e.  RR+
116 rpxr 10512 . . . . . . . . . . . . . . 15  |-  ( 1  e.  RR+  ->  1  e. 
RR* )
117115, 116ax-mp 8 . . . . . . . . . . . . . 14  |-  1  e.  RR*
118 elbl3 18164 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) )
119114, 117, 118mpanl12 663 . . . . . . . . . . . . 13  |-  ( ( 0  e.  CC  /\  z  e.  CC )  ->  ( z  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( z
( abs  o.  -  )
0 )  <  1
) )
12029, 28, 119sylancr 644 . . . . . . . . . . . 12  |-  ( ( ( 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
) )
121113, 120mpbird 223 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
122121expr 598 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
1231223impb 1148 . . . . . . . . 9  |-  ( ( ( 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 ) ) )
12427, 123syl5bi 208 . . . . . . . 8  |-  ( ( ( 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 ) ) )
125124orrd 367 . . . . . . 7  |-  ( ( ( 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 ) ) )
126 elun 3404 . . . . . . 7  |-  ( z  e.  ( { 1 }  u.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  <->  ( z  e.  { 1 }  \/  z  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) ) )
127125, 126sylibr 203 . . . . . 6  |-  ( ( ( 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 ) ) )
128127rabssdv 3339 . . . . 5  |-  ( ( M  e.  RR  /\  0  <_  M )  ->  { z  e.  CC  |  ( abs `  (
1  -  z ) )  <_  ( M  x.  ( 1  -  ( abs `  z ) ) ) }  C_  ( { 1 }  u.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) ) )
12923, 128syl5eqss 3308 . . . 4  |-  ( ( M  e.  RR  /\  0  <_  M )  ->  S  C_  ( { 1 }  u.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) ) )
130 ssundif 3626 . . . 4  |-  ( S 
C_  ( { 1 }  u.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  <->  ( S  \  { 1 } ) 
C_  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 ) )
131129, 130sylib 188 . . 3  |-  ( ( M  e.  RR  /\  0  <_  M )  -> 
( S  \  {
1 } )  C_  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )
13225, 131jca 518 . 2  |-  ( ( M  e.  RR  /\  0  <_  M )  -> 
( 1  e.  S  /\  ( S  \  {
1 } )  C_  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) ) )
1331, 2, 132syl2anc 642 1  |-  ( ph  ->  ( 1  e.  S  /\  ( S  \  {
1 } )  C_  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 935    = wceq 1647    e. wcel 1715    =/= wne 2529   {crab 2632    \ cdif 3235    u. cun 3236    C_ wss 3238   {csn 3729   class class class wbr 4125   dom cdm 4792    o. ccom 4796   -->wf 5354   ` cfv 5358  (class class class)co 5981   CCcc 8882   RRcr 8883   0cc0 8884   1c1 8885    + caddc 8887    x. cmul 8889   RR*cxr 9013    < clt 9014    <_ cle 9015    - cmin 9184   NN0cn0 10114   RR+crp 10505    seq cseq 11210   abscabs 11926    ~~> cli 12165   * Metcxmt 16579   ballcbl 16581
This theorem is referenced by:  abelthlem3  20027  abelthlem6  20030  abelthlem7  20032  abelthlem8  20033  abelthlem9  20034  abelth  20035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615  ax-cnex 8940  ax-resscn 8941  ax-1cn 8942  ax-icn 8943  ax-addcl 8944  ax-addrcl 8945  ax-mulcl 8946  ax-mulrcl 8947  ax-mulcom 8948  ax-addass 8949  ax-mulass 8950  ax-distr 8951  ax-i2m1 8952  ax-1ne0 8953  ax-1rid 8954  ax-rnegex 8955  ax-rrecex 8956  ax-cnre 8957  ax-pre-lttri 8958  ax-pre-lttrn 8959  ax-pre-ltadd 8960  ax-pre-mulgt0 8961  ax-pre-sup 8962
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 936  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-nel 2532  df-ral 2633  df-rex 2634  df-reu 2635  df-rmo 2636  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-pss 3254  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-tp 3737  df-op 3738  df-uni 3930  df-iun 4009  df-br 4126  df-opab 4180  df-mpt 4181  df-tr 4216  df-eprel 4408  df-id 4412  df-po 4417  df-so 4418  df-fr 4455  df-we 4457  df-ord 4498  df-on 4499  df-lim 4500  df-suc 4501  df-om 4760  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-ov 5984  df-oprab 5985  df-mpt2 5986  df-1st 6249  df-2nd 6250  df-riota 6446  df-recs 6530  df-rdg 6565  df-er 6802  df-map 6917  df-en 7007  df-dom 7008  df-sdom 7009  df-sup 7341  df-pnf 9016  df-mnf 9017  df-xr 9018  df-ltxr 9019  df-le 9020  df-sub 9186  df-neg 9187  df-div 9571  df-nn 9894  df-2 9951  df-3 9952  df-n0 10115  df-z 10176  df-uz 10382  df-rp 10506  df-xadd 10604  df-seq 11211  df-exp 11270  df-cj 11791  df-re 11792  df-im 11793  df-sqr 11927  df-abs 11928  df-xmet 16586  df-met 16587  df-bl 16588
  Copyright terms: Public domain W3C validator