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 = TopOpen fld
cxpcn3.k K = J 𝑡 0 +∞
cxpcn3.l L = J 𝑡 D
cxpcn3.u U = if A 1 A 1 2
cxpcn3.t T = if U E 1 U U E 1 U
Assertion cxpcn3lem A D E + d + a 0 +∞ b D a < d A b < d a b < E

Proof

Step Hyp Ref Expression
1 cxpcn3.d D = -1 +
2 cxpcn3.j J = TopOpen fld
3 cxpcn3.k K = J 𝑡 0 +∞
4 cxpcn3.l L = J 𝑡 D
5 cxpcn3.u U = if A 1 A 1 2
6 cxpcn3.t T = if U E 1 U U E 1 U
7 1 eleq2i A D A -1 +
8 ref :
9 ffn : Fn
10 elpreima Fn A -1 + A A +
11 8 9 10 mp2b A -1 + A A +
12 7 11 bitri A D A A +
13 12 simprbi A D A +
14 13 adantr A D E + A +
15 1rp 1 +
16 ifcl A + 1 + if A 1 A 1 +
17 14 15 16 sylancl A D E + if A 1 A 1 +
18 17 rphalfcld A D E + if A 1 A 1 2 +
19 5 18 eqeltrid A D E + U +
20 simpr A D E + E +
21 19 rpreccld A D E + 1 U +
22 21 rpred A D E + 1 U
23 20 22 rpcxpcld A D E + E 1 U +
24 19 23 ifcld A D E + if U E 1 U U E 1 U +
25 6 24 eqeltrid A D E + T +
26 elrege0 a 0 +∞ a 0 a
27 0red A D E + 0
28 leloe 0 a 0 a 0 < a 0 = a
29 27 28 sylan A D E + a 0 a 0 < a 0 = a
30 elrp a + a 0 < a
31 simp2l A D E + a + b D a < T A b < T a +
32 simp2r A D E + a + b D a < T A b < T b D
33 cnvimass -1 + dom
34 8 fdmi dom =
35 33 34 sseqtri -1 +
36 1 35 eqsstri D
37 36 sseli b D b
38 32 37 syl A D E + a + b D a < T A b < T b
39 abscxp a + b a b = a b
40 31 38 39 syl2anc A D E + a + b D a < T A b < T a b = a b
41 38 recld A D E + a + b D a < T A b < T b
42 31 41 rpcxpcld A D E + a + b D a < T A b < T a b +
43 42 rpred A D E + a + b D a < T A b < T a b
44 19 3ad2ant1 A D E + a + b D a < T A b < T U +
45 44 rpred A D E + a + b D a < T A b < T U
46 31 45 rpcxpcld A D E + a + b D a < T A b < T a U +
47 46 rpred A D E + a + b D a < T A b < T a U
48 simp1r A D E + a + b D a < T A b < T E +
49 48 rpred A D E + a + b D a < T A b < T E
50 simp1l A D E + a + b D a < T A b < T A D
51 12 simplbi A D A
52 50 51 syl A D E + a + b D a < T A b < T A
53 52 recld A D E + a + b D a < T A b < T A
54 53 rehalfcld A D E + a + b D a < T A b < T A 2
55 1re 1
56 min1 A 1 if A 1 A 1 A
57 53 55 56 sylancl A D E + a + b D a < T A b < T if A 1 A 1 A
58 17 3ad2ant1 A D E + a + b D a < T A b < T if A 1 A 1 +
59 58 rpred A D E + a + b D a < T A b < T if A 1 A 1
60 2re 2
61 60 a1i A D E + a + b D a < T A b < T 2
62 2pos 0 < 2
63 62 a1i A D E + a + b D a < T A b < T 0 < 2
64 lediv1 if A 1 A 1 A 2 0 < 2 if A 1 A 1 A if A 1 A 1 2 A 2
65 59 53 61 63 64 syl112anc A D E + a + b D a < T A b < T if A 1 A 1 A if A 1 A 1 2 A 2
66 57 65 mpbid A D E + a + b D a < T A b < T if A 1 A 1 2 A 2
67 5 66 eqbrtrid A D E + a + b D a < T A b < T U A 2
68 53 recnd A D E + a + b D a < T A b < T A
69 68 2halvesd A D E + a + b D a < T A b < T A 2 + A 2 = A
70 52 38 resubd A D E + a + b D a < T A b < T A b = A b
71 52 38 subcld A D E + a + b D a < T A b < T A b
72 71 recld A D E + a + b D a < T A b < T A b
73 71 abscld A D E + a + b D a < T A b < T A b
74 71 releabsd A D E + a + b D a < T A b < T A b A b
75 simp3r A D E + a + b D a < T A b < T A b < T
76 75 6 breqtrdi A D E + a + b D a < T A b < T A b < if U E 1 U U E 1 U
77 23 3ad2ant1 A D E + a + b D a < T A b < T E 1 U +
78 77 rpred A D E + a + b D a < T A b < T E 1 U
79 ltmin A b U E 1 U A b < if U E 1 U U E 1 U A b < U A b < E 1 U
80 73 45 78 79 syl3anc A D E + a + b D a < T A b < T A b < if U E 1 U U E 1 U A b < U A b < E 1 U
81 76 80 mpbid A D E + a + b D a < T A b < T A b < U A b < E 1 U
82 81 simpld A D E + a + b D a < T A b < T A b < U
83 72 73 45 74 82 lelttrd A D E + a + b D a < T A b < T A b < U
84 72 45 54 83 67 ltletrd A D E + a + b D a < T A b < T A b < A 2
85 70 84 eqbrtrrd A D E + a + b D a < T A b < T A b < A 2
86 53 41 54 ltsubadd2d A D E + a + b D a < T A b < T A b < A 2 A < b + A 2
87 85 86 mpbid A D E + a + b D a < T A b < T A < b + A 2
88 69 87 eqbrtrd A D E + a + b D a < T A b < T A 2 + A 2 < b + A 2
89 54 41 54 ltadd1d A D E + a + b D a < T A b < T A 2 < b A 2 + A 2 < b + A 2
90 88 89 mpbird A D E + a + b D a < T A b < T A 2 < b
91 45 54 41 67 90 lelttrd A D E + a + b D a < T A b < T U < b
92 31 rpred A D E + a + b D a < T A b < T a
93 55 a1i A D E + a + b D a < T A b < T 1
94 31 rprege0d A D E + a + b D a < T A b < T a 0 a
95 absid a 0 a a = a
96 94 95 syl A D E + a + b D a < T A b < T a = a
97 simp3l A D E + a + b D a < T A b < T a < T
98 96 97 eqbrtrrd A D E + a + b D a < T A b < T a < T
99 98 6 breqtrdi A D E + a + b D a < T A b < T a < if U E 1 U U E 1 U
100 ltmin a U E 1 U a < if U E 1 U U E 1 U a < U a < E 1 U
101 92 45 78 100 syl3anc A D E + a + b D a < T A b < T a < if U E 1 U U E 1 U a < U a < E 1 U
102 99 101 mpbid A D E + a + b D a < T A b < T a < U a < E 1 U
103 102 simpld A D E + a + b D a < T A b < T a < U
104 rehalfcl 1 1 2
105 55 104 mp1i A D E + a + b D a < T A b < T 1 2
106 min2 A 1 if A 1 A 1 1
107 53 55 106 sylancl A D E + a + b D a < T A b < T if A 1 A 1 1
108 lediv1 if A 1 A 1 1 2 0 < 2 if A 1 A 1 1 if A 1 A 1 2 1 2
109 59 93 61 63 108 syl112anc A D E + a + b D a < T A b < T if A 1 A 1 1 if A 1 A 1 2 1 2
110 107 109 mpbid A D E + a + b D a < T A b < T if A 1 A 1 2 1 2
111 5 110 eqbrtrid A D E + a + b D a < T A b < T U 1 2
112 halflt1 1 2 < 1
113 112 a1i A D E + a + b D a < T A b < T 1 2 < 1
114 45 105 93 111 113 lelttrd A D E + a + b D a < T A b < T U < 1
115 92 45 93 103 114 lttrd A D E + a + b D a < T A b < T a < 1
116 31 45 115 41 cxplt3d A D E + a + b D a < T A b < T U < b a b < a U
117 91 116 mpbid A D E + a + b D a < T A b < T a b < a U
118 44 rpcnne0d A D E + a + b D a < T A b < T U U 0
119 recid U U 0 U 1 U = 1
120 118 119 syl A D E + a + b D a < T A b < T U 1 U = 1
121 120 oveq2d A D E + a + b D a < T A b < T a U 1 U = a 1
122 44 rpreccld A D E + a + b D a < T A b < T 1 U +
123 122 rpcnd A D E + a + b D a < T A b < T 1 U
124 31 45 123 cxpmuld A D E + a + b D a < T A b < T a U 1 U = a U 1 U
125 31 rpcnd A D E + a + b D a < T A b < T a
126 125 cxp1d A D E + a + b D a < T A b < T a 1 = a
127 121 124 126 3eqtr3d A D E + a + b D a < T A b < T a U 1 U = a
128 102 simprd A D E + a + b D a < T A b < T a < E 1 U
129 127 128 eqbrtrd A D E + a + b D a < T A b < T a U 1 U < E 1 U
130 46 rprege0d A D E + a + b D a < T A b < T a U 0 a U
131 48 rprege0d A D E + a + b D a < T A b < T E 0 E
132 cxplt2 a U 0 a U E 0 E 1 U + a U < E a U 1 U < E 1 U
133 130 131 122 132 syl3anc A D E + a + b D a < T A b < T a U < E a U 1 U < E 1 U
134 129 133 mpbird A D E + a + b D a < T A b < T a U < E
135 43 47 49 117 134 lttrd A D E + a + b D a < T A b < T a b < E
136 40 135 eqbrtrd A D E + a + b D a < T A b < T a b < E
137 136 3expia A D E + a + b D a < T A b < T a b < E
138 137 anassrs A D E + a + b D a < T A b < T a b < E
139 138 ralrimiva A D E + a + b D a < T A b < T a b < E
140 30 139 sylan2br A D E + a 0 < a b D a < T A b < T a b < E
141 140 expr A D E + a 0 < a b D a < T A b < T a b < E
142 elpreima Fn b -1 + b b +
143 8 9 142 mp2b b -1 + b b +
144 143 simprbi b -1 + b +
145 144 1 eleq2s b D b +
146 145 rpne0d b D b 0
147 fveq2 b = 0 b = 0
148 re0 0 = 0
149 147 148 syl6eq b = 0 b = 0
150 149 necon3i b 0 b 0
151 146 150 syl b D b 0
152 37 151 0cxpd b D 0 b = 0
153 152 adantl A D E + a b D 0 b = 0
154 153 abs00bd A D E + a b D 0 b = 0
155 simpllr A D E + a b D E +
156 155 rpgt0d A D E + a b D 0 < E
157 154 156 eqbrtrd A D E + a b D 0 b < E
158 fvoveq1 0 = a 0 b = a b
159 158 breq1d 0 = a 0 b < E a b < E
160 157 159 syl5ibcom A D E + a b D 0 = a a b < E
161 160 a1dd A D E + a b D 0 = a a < T A b < T a b < E
162 161 ralrimdva A D E + a 0 = a b D a < T A b < T a b < E
163 141 162 jaod A D E + a 0 < a 0 = a b D a < T A b < T a b < E
164 29 163 sylbid A D E + a 0 a b D a < T A b < T a b < E
165 164 expimpd A D E + a 0 a b D a < T A b < T a b < E
166 26 165 syl5bi A D E + a 0 +∞ b D a < T A b < T a b < E
167 166 ralrimiv A D E + a 0 +∞ b D a < T A b < T a b < E
168 breq2 d = T a < d a < T
169 breq2 d = T A b < d A b < T
170 168 169 anbi12d d = T a < d A b < d a < T A b < T
171 170 imbi1d d = T a < d A b < d a b < E a < T A b < T a b < E
172 171 2ralbidv d = T a 0 +∞ b D a < d A b < d a b < E a 0 +∞ b D a < T A b < T a b < E
173 172 rspcev T + a 0 +∞ b D a < T A b < T a b < E d + a 0 +∞ b D a < d A b < d a b < E
174 25 167 173 syl2anc A D E + d + a 0 +∞ b D a < d A b < d a b < E