Metamath Proof Explorer


Theorem cxpcn3lem

Description: Lemma for cxpcn3 . (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses cxpcn3.d D=-1+
cxpcn3.j J=TopOpenfld
cxpcn3.k K=J𝑡0+∞
cxpcn3.l L=J𝑡D
cxpcn3.u U=ifA1A12
cxpcn3.t T=ifUE1UUE1U
Assertion cxpcn3lem ADE+d+a0+∞bDa<dAb<dab<E

Proof

Step Hyp Ref Expression
1 cxpcn3.d D=-1+
2 cxpcn3.j J=TopOpenfld
3 cxpcn3.k K=J𝑡0+∞
4 cxpcn3.l L=J𝑡D
5 cxpcn3.u U=ifA1A12
6 cxpcn3.t T=ifUE1UUE1U
7 1 eleq2i ADA-1+
8 ref :
9 ffn :Fn
10 elpreima FnA-1+AA+
11 8 9 10 mp2b A-1+AA+
12 7 11 bitri ADAA+
13 12 simprbi ADA+
14 13 adantr ADE+A+
15 1rp 1+
16 ifcl A+1+ifA1A1+
17 14 15 16 sylancl ADE+ifA1A1+
18 17 rphalfcld ADE+ifA1A12+
19 5 18 eqeltrid ADE+U+
20 simpr ADE+E+
21 19 rpreccld ADE+1U+
22 21 rpred ADE+1U
23 20 22 rpcxpcld ADE+E1U+
24 19 23 ifcld ADE+ifUE1UUE1U+
25 6 24 eqeltrid ADE+T+
26 elrege0 a0+∞a0a
27 0red ADE+0
28 leloe 0a0a0<a0=a
29 27 28 sylan ADE+a0a0<a0=a
30 elrp a+a0<a
31 simp2l ADE+a+bDa<TAb<Ta+
32 simp2r ADE+a+bDa<TAb<TbD
33 cnvimass -1+dom
34 8 fdmi dom=
35 33 34 sseqtri -1+
36 1 35 eqsstri D
37 36 sseli bDb
38 32 37 syl ADE+a+bDa<TAb<Tb
39 abscxp a+bab=ab
40 31 38 39 syl2anc ADE+a+bDa<TAb<Tab=ab
41 38 recld ADE+a+bDa<TAb<Tb
42 31 41 rpcxpcld ADE+a+bDa<TAb<Tab+
43 42 rpred ADE+a+bDa<TAb<Tab
44 19 3ad2ant1 ADE+a+bDa<TAb<TU+
45 44 rpred ADE+a+bDa<TAb<TU
46 31 45 rpcxpcld ADE+a+bDa<TAb<TaU+
47 46 rpred ADE+a+bDa<TAb<TaU
48 simp1r ADE+a+bDa<TAb<TE+
49 48 rpred ADE+a+bDa<TAb<TE
50 simp1l ADE+a+bDa<TAb<TAD
51 12 simplbi ADA
52 50 51 syl ADE+a+bDa<TAb<TA
53 52 recld ADE+a+bDa<TAb<TA
54 53 rehalfcld ADE+a+bDa<TAb<TA2
55 1re 1
56 min1 A1ifA1A1A
57 53 55 56 sylancl ADE+a+bDa<TAb<TifA1A1A
58 17 3ad2ant1 ADE+a+bDa<TAb<TifA1A1+
59 58 rpred ADE+a+bDa<TAb<TifA1A1
60 2re 2
61 60 a1i ADE+a+bDa<TAb<T2
62 2pos 0<2
63 62 a1i ADE+a+bDa<TAb<T0<2
64 lediv1 ifA1A1A20<2ifA1A1AifA1A12A2
65 59 53 61 63 64 syl112anc ADE+a+bDa<TAb<TifA1A1AifA1A12A2
66 57 65 mpbid ADE+a+bDa<TAb<TifA1A12A2
67 5 66 eqbrtrid ADE+a+bDa<TAb<TUA2
68 53 recnd ADE+a+bDa<TAb<TA
69 68 2halvesd ADE+a+bDa<TAb<TA2+A2=A
70 52 38 resubd ADE+a+bDa<TAb<TAb=Ab
71 52 38 subcld ADE+a+bDa<TAb<TAb
72 71 recld ADE+a+bDa<TAb<TAb
73 71 abscld ADE+a+bDa<TAb<TAb
74 71 releabsd ADE+a+bDa<TAb<TAbAb
75 simp3r ADE+a+bDa<TAb<TAb<T
76 75 6 breqtrdi ADE+a+bDa<TAb<TAb<ifUE1UUE1U
77 23 3ad2ant1 ADE+a+bDa<TAb<TE1U+
78 77 rpred ADE+a+bDa<TAb<TE1U
79 ltmin AbUE1UAb<ifUE1UUE1UAb<UAb<E1U
80 73 45 78 79 syl3anc ADE+a+bDa<TAb<TAb<ifUE1UUE1UAb<UAb<E1U
81 76 80 mpbid ADE+a+bDa<TAb<TAb<UAb<E1U
82 81 simpld ADE+a+bDa<TAb<TAb<U
83 72 73 45 74 82 lelttrd ADE+a+bDa<TAb<TAb<U
84 72 45 54 83 67 ltletrd ADE+a+bDa<TAb<TAb<A2
85 70 84 eqbrtrrd ADE+a+bDa<TAb<TAb<A2
86 53 41 54 ltsubadd2d ADE+a+bDa<TAb<TAb<A2A<b+A2
87 85 86 mpbid ADE+a+bDa<TAb<TA<b+A2
88 69 87 eqbrtrd ADE+a+bDa<TAb<TA2+A2<b+A2
89 54 41 54 ltadd1d ADE+a+bDa<TAb<TA2<bA2+A2<b+A2
90 88 89 mpbird ADE+a+bDa<TAb<TA2<b
91 45 54 41 67 90 lelttrd ADE+a+bDa<TAb<TU<b
92 31 rpred ADE+a+bDa<TAb<Ta
93 55 a1i ADE+a+bDa<TAb<T1
94 31 rprege0d ADE+a+bDa<TAb<Ta0a
95 absid a0aa=a
96 94 95 syl ADE+a+bDa<TAb<Ta=a
97 simp3l ADE+a+bDa<TAb<Ta<T
98 96 97 eqbrtrrd ADE+a+bDa<TAb<Ta<T
99 98 6 breqtrdi ADE+a+bDa<TAb<Ta<ifUE1UUE1U
100 ltmin aUE1Ua<ifUE1UUE1Ua<Ua<E1U
101 92 45 78 100 syl3anc ADE+a+bDa<TAb<Ta<ifUE1UUE1Ua<Ua<E1U
102 99 101 mpbid ADE+a+bDa<TAb<Ta<Ua<E1U
103 102 simpld ADE+a+bDa<TAb<Ta<U
104 rehalfcl 112
105 55 104 mp1i ADE+a+bDa<TAb<T12
106 min2 A1ifA1A11
107 53 55 106 sylancl ADE+a+bDa<TAb<TifA1A11
108 lediv1 ifA1A1120<2ifA1A11ifA1A1212
109 59 93 61 63 108 syl112anc ADE+a+bDa<TAb<TifA1A11ifA1A1212
110 107 109 mpbid ADE+a+bDa<TAb<TifA1A1212
111 5 110 eqbrtrid ADE+a+bDa<TAb<TU12
112 halflt1 12<1
113 112 a1i ADE+a+bDa<TAb<T12<1
114 45 105 93 111 113 lelttrd ADE+a+bDa<TAb<TU<1
115 92 45 93 103 114 lttrd ADE+a+bDa<TAb<Ta<1
116 31 45 115 41 cxplt3d ADE+a+bDa<TAb<TU<bab<aU
117 91 116 mpbid ADE+a+bDa<TAb<Tab<aU
118 44 rpcnne0d ADE+a+bDa<TAb<TUU0
119 recid UU0U1U=1
120 118 119 syl ADE+a+bDa<TAb<TU1U=1
121 120 oveq2d ADE+a+bDa<TAb<TaU1U=a1
122 44 rpreccld ADE+a+bDa<TAb<T1U+
123 122 rpcnd ADE+a+bDa<TAb<T1U
124 31 45 123 cxpmuld ADE+a+bDa<TAb<TaU1U=aU1U
125 31 rpcnd ADE+a+bDa<TAb<Ta
126 125 cxp1d ADE+a+bDa<TAb<Ta1=a
127 121 124 126 3eqtr3d ADE+a+bDa<TAb<TaU1U=a
128 102 simprd ADE+a+bDa<TAb<Ta<E1U
129 127 128 eqbrtrd ADE+a+bDa<TAb<TaU1U<E1U
130 46 rprege0d ADE+a+bDa<TAb<TaU0aU
131 48 rprege0d ADE+a+bDa<TAb<TE0E
132 cxplt2 aU0aUE0E1U+aU<EaU1U<E1U
133 130 131 122 132 syl3anc ADE+a+bDa<TAb<TaU<EaU1U<E1U
134 129 133 mpbird ADE+a+bDa<TAb<TaU<E
135 43 47 49 117 134 lttrd ADE+a+bDa<TAb<Tab<E
136 40 135 eqbrtrd ADE+a+bDa<TAb<Tab<E
137 136 3expia ADE+a+bDa<TAb<Tab<E
138 137 anassrs ADE+a+bDa<TAb<Tab<E
139 138 ralrimiva ADE+a+bDa<TAb<Tab<E
140 30 139 sylan2br ADE+a0<abDa<TAb<Tab<E
141 140 expr ADE+a0<abDa<TAb<Tab<E
142 elpreima Fnb-1+bb+
143 8 9 142 mp2b b-1+bb+
144 143 simprbi b-1+b+
145 144 1 eleq2s bDb+
146 145 rpne0d bDb0
147 fveq2 b=0b=0
148 re0 0=0
149 147 148 eqtrdi b=0b=0
150 149 necon3i b0b0
151 146 150 syl bDb0
152 37 151 0cxpd bD0b=0
153 152 adantl ADE+abD0b=0
154 153 abs00bd ADE+abD0b=0
155 simpllr ADE+abDE+
156 155 rpgt0d ADE+abD0<E
157 154 156 eqbrtrd ADE+abD0b<E
158 fvoveq1 0=a0b=ab
159 158 breq1d 0=a0b<Eab<E
160 157 159 syl5ibcom ADE+abD0=aab<E
161 160 a1dd ADE+abD0=aa<TAb<Tab<E
162 161 ralrimdva ADE+a0=abDa<TAb<Tab<E
163 141 162 jaod ADE+a0<a0=abDa<TAb<Tab<E
164 29 163 sylbid ADE+a0abDa<TAb<Tab<E
165 164 expimpd ADE+a0abDa<TAb<Tab<E
166 26 165 syl5bi ADE+a0+∞bDa<TAb<Tab<E
167 166 ralrimiv ADE+a0+∞bDa<TAb<Tab<E
168 breq2 d=Ta<da<T
169 breq2 d=TAb<dAb<T
170 168 169 anbi12d d=Ta<dAb<da<TAb<T
171 170 imbi1d d=Ta<dAb<dab<Ea<TAb<Tab<E
172 171 2ralbidv d=Ta0+∞bDa<dAb<dab<Ea0+∞bDa<TAb<Tab<E
173 172 rspcev T+a0+∞bDa<TAb<Tab<Ed+a0+∞bDa<dAb<dab<E
174 25 167 173 syl2anc ADE+d+a0+∞bDa<dAb<dab<E