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 φ A : 0
abelth.2 φ seq 0 + A dom
abelth.3 φ M
abelth.4 φ 0 M
abelth.5 S = z | 1 z M 1 z
Assertion abelthlem2 φ 1 S S 1 0 ball abs 1

Proof

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