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

Theorem pntlemr 21235
 Description: Lemma for pntlemj 21236. (Contributed by Mario Carneiro, 7-Jun-2016.)
Hypotheses
Ref Expression
pntlem1.r ψ
pntlem1.a
pntlem1.b
pntlem1.l
pntlem1.d
pntlem1.f ;
pntlem1.u
pntlem1.u2
pntlem1.e
pntlem1.k
pntlem1.y
pntlem1.x
pntlem1.c
pntlem1.w ;
pntlem1.z
pntlem1.m
pntlem1.n
pntlem1.U
pntlem1.K
pntlem1.o
pntlem1.v
pntlem1.V
pntlem1.j ..^
pntlem1.i
Assertion
Ref Expression
pntlemr
Distinct variable groups:   ,   ,,   ,,,   ,,   ,   ,   ,   ,,,   ,   ,   ,   ,,   ,   ,,,,   ,,
Allowed substitution hints:   (,,,)   (,,,)   (,,,)   (,,)   (,,,)   ()   (,,)   (,,,)   (,,,)   (,)   (,)   ()   (,,)   (,,)   (,,)   (,,)   (,,)   (,)   (,,)   (,)

Proof of Theorem pntlemr
StepHypRef Expression
1 pntlem1.r . . . . . . . . . . . . 13 ψ
2 pntlem1.a . . . . . . . . . . . . 13
3 pntlem1.b . . . . . . . . . . . . 13
4 pntlem1.l . . . . . . . . . . . . 13
5 pntlem1.d . . . . . . . . . . . . 13
6 pntlem1.f . . . . . . . . . . . . 13 ;
71, 2, 3, 4, 5, 6pntlemd 21227 . . . . . . . . . . . 12
87simp1d 969 . . . . . . . . . . 11
9 pntlem1.u . . . . . . . . . . . . 13
10 pntlem1.u2 . . . . . . . . . . . . 13
11 pntlem1.e . . . . . . . . . . . . 13
12 pntlem1.k . . . . . . . . . . . . 13
131, 2, 3, 4, 5, 6, 9, 10, 11, 12pntlemc 21228 . . . . . . . . . . . 12
1413simp1d 969 . . . . . . . . . . 11
158, 14rpmulcld 10610 . . . . . . . . . 10
16 4re 10019 . . . . . . . . . . 11
17 4pos 10032 . . . . . . . . . . 11
1816, 17elrpii 10561 . . . . . . . . . 10
19 rpdivcl 10580 . . . . . . . . . 10
2015, 18, 19sylancl 644 . . . . . . . . 9
2120rpred 10594 . . . . . . . 8
22 pntlem1.y . . . . . . . . . . . 12
23 pntlem1.x . . . . . . . . . . . 12
24 pntlem1.c . . . . . . . . . . . 12
25 pntlem1.w . . . . . . . . . . . 12 ;
26 pntlem1.z . . . . . . . . . . . 12
271, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26pntlemb 21230 . . . . . . . . . . 11 ;
2827simp1d 969 . . . . . . . . . 10
29 pntlem1.v . . . . . . . . . 10
3028, 29rpdivcld 10611 . . . . . . . . 9
3130rpred 10594 . . . . . . . 8
3221, 31remulcld 9063 . . . . . . 7
33 pntlem1.i . . . . . . . . . 10
34 fzfid 11253 . . . . . . . . . 10
3533, 34syl5eqel 2485 . . . . . . . . 9
36 hashcl 11580 . . . . . . . . 9
3735, 36syl 16 . . . . . . . 8
3837nn0red 10221 . . . . . . 7
3932recnd 9061 . . . . . . . . . . . 12
40 1rp 10562 . . . . . . . . . . . . . . . . . 18
41 rpaddcl 10578 . . . . . . . . . . . . . . . . . 18
4240, 15, 41sylancr 645 . . . . . . . . . . . . . . . . 17
4342, 29rpmulcld 10610 . . . . . . . . . . . . . . . 16
4428, 43rpdivcld 10611 . . . . . . . . . . . . . . 15
4544rpred 10594 . . . . . . . . . . . . . 14
46 reflcl 11146 . . . . . . . . . . . . . 14
4745, 46syl 16 . . . . . . . . . . . . 13
4847recnd 9061 . . . . . . . . . . . 12
49 ax-1cn 8995 . . . . . . . . . . . . 13
5049a1i 11 . . . . . . . . . . . 12
5139, 48, 50add32d 9234 . . . . . . . . . . 11
52 peano2re 9185 . . . . . . . . . . . . . 14
5332, 52syl 16 . . . . . . . . . . . . 13
5453, 47readdcld 9062 . . . . . . . . . . . 12
55 reflcl 11146 . . . . . . . . . . . . . 14
5631, 55syl 16 . . . . . . . . . . . . 13
57 peano2re 9185 . . . . . . . . . . . . 13
5856, 57syl 16 . . . . . . . . . . . 12
5915rphalfcld 10606 . . . . . . . . . . . . . . . 16
6059, 30rpmulcld 10610 . . . . . . . . . . . . . . 15
6160rpred 10594 . . . . . . . . . . . . . 14
6261, 45readdcld 9062 . . . . . . . . . . . . 13
63 rpdivcl 10580 . . . . . . . . . . . . . . . . . . . 20
6418, 15, 63sylancr 645 . . . . . . . . . . . . . . . . . . 19
6564rpred 10594 . . . . . . . . . . . . . . . . . 18
6628rpsqrcld 12155 . . . . . . . . . . . . . . . . . . . 20
6766rpred 10594 . . . . . . . . . . . . . . . . . . 19
6827simp3d 971 . . . . . . . . . . . . . . . . . . . 20 ;
6968simp1d 969 . . . . . . . . . . . . . . . . . . 19
7043rpred 10594 . . . . . . . . . . . . . . . . . . . . . . . 24
7113simp2d 970 . . . . . . . . . . . . . . . . . . . . . . . . . 26
72 pntlem1.j . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
73 elfzoelz 11084 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
7472, 73syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7574peano2zd 10324 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7671, 75rpexpcld 11487 . . . . . . . . . . . . . . . . . . . . . . . . 25
7776rpred 10594 . . . . . . . . . . . . . . . . . . . . . . . 24
78 pntlem1.V . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7978simpld 446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8079simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8171rpcnd 10596 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8271, 74rpexpcld 11487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8382rpcnd 10596 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8481, 83mulcomd 9056 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
85 pntlem1.m . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
86 pntlem1.n . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
871, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 85, 86pntlemg 21231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8887simp1d 969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
89 elfzouz 11088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
9072, 89syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
91 nnuz 10467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9291uztrn2 10449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9388, 90, 92syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9493nnnn0d 10220 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9581, 94expp1d 11465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9684, 95eqtr4d 2436 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9780, 96breqtrd 4191 . . . . . . . . . . . . . . . . . . . . . . . . 25
9870, 77, 97ltled 9167 . . . . . . . . . . . . . . . . . . . . . . . 24
99 fzofzp1 11130 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
10072, 99syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1011, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 85, 86pntlemh 21232 . . . . . . . . . . . . . . . . . . . . . . . . . 26
102100, 101mpdan 650 . . . . . . . . . . . . . . . . . . . . . . . . 25
103102simprd 450 . . . . . . . . . . . . . . . . . . . . . . . 24
10470, 77, 67, 98, 103letrd 9173 . . . . . . . . . . . . . . . . . . . . . . 23
10570, 67, 66lemul2d 10634 . . . . . . . . . . . . . . . . . . . . . . 23
106104, 105mpbid 202 . . . . . . . . . . . . . . . . . . . . . 22
10728rprege0d 10601 . . . . . . . . . . . . . . . . . . . . . . 23
108 remsqsqr 12003 . . . . . . . . . . . . . . . . . . . . . . 23
109107, 108syl 16 . . . . . . . . . . . . . . . . . . . . . 22
110106, 109breqtrd 4191 . . . . . . . . . . . . . . . . . . . . 21
11128rpred 10594 . . . . . . . . . . . . . . . . . . . . . 22
11267, 111, 43lemuldivd 10639 . . . . . . . . . . . . . . . . . . . . 21
113110, 112mpbid 202 . . . . . . . . . . . . . . . . . . . 20
11429rpcnd 10596 . . . . . . . . . . . . . . . . . . . . . . . 24
115114mulid2d 9053 . . . . . . . . . . . . . . . . . . . . . . 23
116 1re 9037 . . . . . . . . . . . . . . . . . . . . . . . . 25
117116a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
11842rpred 10594 . . . . . . . . . . . . . . . . . . . . . . . 24
119 ltaddrp 10590 . . . . . . . . . . . . . . . . . . . . . . . . 25
120116, 15, 119sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . 24
121117, 118, 29, 120ltmul1dd 10645 . . . . . . . . . . . . . . . . . . . . . . 23
122115, 121eqbrtrrd 4189 . . . . . . . . . . . . . . . . . . . . . 22
12329, 43, 28ltdiv2d 10617 . . . . . . . . . . . . . . . . . . . . . 22
124122, 123mpbid 202 . . . . . . . . . . . . . . . . . . . . 21
12545, 31, 124ltled 9167 . . . . . . . . . . . . . . . . . . . 20
12667, 45, 31, 113, 125letrd 9173 . . . . . . . . . . . . . . . . . . 19
12765, 67, 31, 69, 126letrd 9173 . . . . . . . . . . . . . . . . . 18
12865, 31, 31, 127leadd2dd 9587 . . . . . . . . . . . . . . . . 17
12930rpcnd 10596 . . . . . . . . . . . . . . . . . 18
1301292timesd 10156 . . . . . . . . . . . . . . . . 17
131128, 130breqtrrd 4193 . . . . . . . . . . . . . . . 16
13231, 65readdcld 9062 . . . . . . . . . . . . . . . . 17
133 2re 10015 . . . . . . . . . . . . . . . . . 18
134 remulcl 9022 . . . . . . . . . . . . . . . . . 18
135133, 31, 134sylancr 645 . . . . . . . . . . . . . . . . 17
136132, 135, 20lemul2d 10634 . . . . . . . . . . . . . . . 16
137131, 136mpbid 202 . . . . . . . . . . . . . . 15
13820rpcnd 10596 . . . . . . . . . . . . . . . . 17
13964rpcnd 10596 . . . . . . . . . . . . . . . . 17
140138, 129, 139adddid 9059 . . . . . . . . . . . . . . . 16
14115rpcnne0d 10603 . . . . . . . . . . . . . . . . . 18
142 rpcnne0 10575 . . . . . . . . . . . . . . . . . . 19
14318, 142mp1i 12 . . . . . . . . . . . . . . . . . 18
144 divcan6 9667 . . . . . . . . . . . . . . . . . 18
145141, 143, 144syl2anc 643 . . . . . . . . . . . . . . . . 17
146145oveq2d 6050 . . . . . . . . . . . . . . . 16
147140, 146eqtrd 2433 . . . . . . . . . . . . . . 15
148 2rp 10563 . . . . . . . . . . . . . . . . . . 19
149 rpcnne0 10575 . . . . . . . . . . . . . . . . . . 19
150148, 149mp1i 12 . . . . . . . . . . . . . . . . . 18
151150simpld 446 . . . . . . . . . . . . . . . . 17
152138, 151, 129mulassd 9058 . . . . . . . . . . . . . . . 16
15315rpcnd 10596 . . . . . . . . . . . . . . . . . . . . 21
154 divdiv1 9671 . . . . . . . . . . . . . . . . . . . . 21
155153, 150, 150, 154syl3anc 1184 . . . . . . . . . . . . . . . . . . . 20
156 2t2e4 10073 . . . . . . . . . . . . . . . . . . . . 21
157156oveq2i 6045 . . . . . . . . . . . . . . . . . . . 20
158155, 157syl6req 2450 . . . . . . . . . . . . . . . . . . 19
159158oveq1d 6049 . . . . . . . . . . . . . . . . . 18
160153halfcld 10158 . . . . . . . . . . . . . . . . . . 19
161150simprd 450 . . . . . . . . . . . . . . . . . . 19
162160, 151, 161divcan1d 9737 . . . . . . . . . . . . . . . . . 18
163159, 162eqtrd 2433 . . . . . . . . . . . . . . . . 17
164163oveq1d 6049 . . . . . . . . . . . . . . . 16
165152, 164eqtr3d 2435 . . . . . . . . . . . . . . 15
166137, 147, 1653brtr3d 4196 . . . . . . . . . . . . . 14
167 flle 11149 . . . . . . . . . . . . . . 15
16845, 167syl 16 . . . . . . . . . . . . . 14
16953, 47, 61, 45, 166, 168le2addd 9590 . . . . . . . . . . . . 13
17059rpred 10594 . . . . . . . . . . . . . . . 16
17142rprecred 10605 . . . . . . . . . . . . . . . 16
172170, 171readdcld 9062 . . . . . . . . . . . . . . 15
17315rpred 10594 . . . . . . . . . . . . . . . . . . . 20
17414rpred 10594 . . . . . . . . . . . . . . . . . . . . 21
1758rpred 10594 . . . . . . . . . . . . . . . . . . . . . . 23
176 eliooord 10916 . . . . . . . . . . . . . . . . . . . . . . . . 25
1774, 176syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
178177simprd 450 . . . . . . . . . . . . . . . . . . . . . . 23
179175, 117, 14, 178ltmul1dd 10645 . . . . . . . . . . . . . . . . . . . . . 22
18014rpcnd 10596 . . . . . . . . . . . . . . . . . . . . . . 23
181180mulid2d 9053 . . . . . . . . . . . . . . . . . . . . . 22
182179, 181breqtrd 4191 . . . . . . . . . . . . . . . . . . . . 21
18313simp3d 971 . . . . . . . . . . . . . . . . . . . . . . . 24
184183simp1d 969 . . . . . . . . . . . . . . . . . . . . . . 23
185 eliooord 10916 . . . . . . . . . . . . . . . . . . . . . . 23
186184, 185syl 16 . . . . . . . . . . . . . . . . . . . . . 22
187186simprd 450 . . . . . . . . . . . . . . . . . . . . 21
188173, 174, 117, 182, 187lttrd 9177 . . . . . . . . . . . . . . . . . . . 20
189173, 117, 117, 188ltadd2dd 9175 . . . . . . . . . . . . . . . . . . 19
190 df-2 10004 . . . . . . . . . . . . . . . . . . 19
191189, 190syl6breqr 4207 . . . . . . . . . . . . . . . . . 18
19242rpregt0d 10600 . . . . . . . . . . . . . . . . . . 19
193133a1i 11 . . . . . . . . . . . . . . . . . . 19
194 2pos 10028 . . . . . . . . . . . . . . . . . . . 20
195194a1i 11 . . . . . . . . . . . . . . . . . . 19
19615rpregt0d 10600 . . . . . . . . . . . . . . . . . . 19
197 ltdiv2 9841 . . . . . . . . . . . . . . . . . . 19
198192, 193, 195, 196, 197syl121anc 1189 . . . . . . . . . . . . . . . . . 18
199191, 198mpbid 202 . . . . . . . . . . . . . . . . 17
20042rpcnd 10596 . . . . . . . . . . . . . . . . . . 19
20142rpcnne0d 10603 . . . . . . . . . . . . . . . . . . 19
202 divsubdir 9656 . . . . . . . . . . . . . . . . . . 19
203200, 50, 201, 202syl3anc 1184 . . . . . . . . . . . . . . . . . 18
204 pncan2 9258 . . . . . . . . . . . . . . . . . . . 20
20549, 153, 204sylancr 645 . . . . . . . . . . . . . . . . . . 19
206205oveq1d 6049 . . . . . . . . . . . . . . . . . 18
207 divid 9651 . . . . . . . . . . . . . . . . . . . 20
208201, 207syl 16 . . . . . . . . . . . . . . . . . . 19
209208oveq1d 6049 . . . . . . . . . . . . . . . . . 18
210203, 206, 2093eqtr3d 2441 . . . . . . . . . . . . . . . . 17
211199, 210breqtrd 4191 . . . . . . . . . . . . . . . 16
212170, 171, 117ltaddsubd 9572 . . . . . . . . . . . . . . . 16
213211, 212mpbird 224 . . . . . . . . . . . . . . 15
214172, 117, 30, 213ltmul1dd 10645 . . . . . . . . . . . . . 14
215 reccl 9631 . . . . . . . . . . . . . . . . 17
216201, 215syl 16 . . . . . . . . . . . . . . . 16
217160, 216, 129adddird 9060 . . . . . . . . . . . . . . 15
218200, 114mulcomd 9056 . . . . . . . . . . . . . . . . . 18
219218oveq2d 6050 . . . . . . . . . . . . . . . . 17
22028rpcnd 10596 . . . . . . . . . . . . . . . . . 18
22129rpcnne0d 10603 . . . . . . . . . . . . . . . . . 18
222 divdiv1 9671 . . . . . . . . . . . . . . . . . 18
223220, 221, 201, 222syl3anc 1184 . . . . . . . . . . . . . . . . 17
22442rpne0d 10599 . . . . . . . . . . . . . . . . . 18
225129, 200, 224divrec2d 9740 . . . . . . . . . . . . . . . . 17
226219, 223, 2253eqtr2d 2439 . . . . . . . . . . . . . . . 16
227226oveq2d 6050 . . . . . . . . . . . . . . 15
228217, 227eqtr4d 2436 . . . . . . . . . . . . . 14
229129mulid2d 9053 . . . . . . . . . . . . . 14
230214, 228, 2293brtr3d 4196 . . . . . . . . . . . . 13
23154, 62, 31, 169, 230lelttrd 9174 . . . . . . . . . . . 12
232 fllep1 11151 . . . . . . . . . . . . 13
23331, 232syl 16 . . . . . . . . . . . 12
23454, 31, 58, 231, 233ltletrd 9176 . . . . . . . . . . 11
23551, 234eqbrtrd 4187 . . . . . . . . . 10
23632, 47readdcld 9062 . . . . . . . . . . 11
237236, 56, 117ltadd1d 9565 . . . . . . . . . 10
238235, 237mpbird 224 . . . . . . . . 9
23932, 47, 56ltaddsubd 9572 . . . . . . . . 9
240238, 239mpbid 202 . . . . . . . 8
24131flcld 11148 . . . . . . . . . . . 12
242 fzval3 11122 . . . . . . . . . . . 12 ..^
243241, 242syl 16 . . . . . . . . . . 11 ..^
24433, 243syl5eq 2445 . . . . . . . . . 10 ..^
245244fveq2d 5686 . . . . . . . . 9 ..^
246 flword2 11161 . . . . . . . . . . . 12
24745, 31, 125, 246syl3anc 1184 . . . . . . . . . . 11
248 eluzp1p1 10457 . . . . . . . . . . 11
249247, 248syl 16 . . . . . . . . . 10
250 hashfzo 11635 . . . . . . . . . 10 ..^
251249, 250syl 16 . . . . . . . . 9 ..^
25256recnd 9061 . . . . . . . . . 10
253252, 48, 50pnpcan2d 9395 . . . . . . . . 9
254245, 251, 2533eqtrd 2437 . . . . . . . 8
255240, 254breqtrrd 4193 . . . . . . 7
25632, 38, 255ltled 9167 . . . . . 6
25721, 38, 30lemuldivd 10639 . . . . . 6
258256, 257mpbid 202 . . . . 5
25929rpred 10594 . . . . . . . . . . . . . . 15
26070, 77, 67, 97, 103ltletrd 9176 . . . . . . . . . . . . . . . 16
261259, 70, 67, 122, 260lttrd 9177 . . . . . . . . . . . . . . 15
262259, 67, 261ltled 9167 . . . . . . . . . . . . . 14
26329rprege0d 10601 . . . . . . . . . . . . . . 15
26466rprege0d 10601 . . . . . . . . . . . . . . 15
265 le2sq 11397 . . . . . . . . . . . . . . 15
266263, 264, 265syl2anc 643 . . . . . . . . . . . . . 14
267262, 266mpbid 202 . . . . . . . . . . . . 13
268 resqrth 12002 . . . . . . . . . . . . . 14
269107, 268syl 16 . . . . . . . . . . . . 13
270267, 269breqtrd 4191 . . . . . . . . . . . 12
271 2z 10258 . . . . . . . . . . . . . . 15
272 rpexpcl 11341 . . . . . . . . . . . . . . 15
27329, 271, 272sylancl 644 . . . . . . . . . . . . . 14
274273rpred 10594 . . . . . . . . . . . . 13
275274, 111, 28lemul2d 10634 . . . . . . . . . . . 12
276270, 275mpbid 202 . . . . . . . . . . 11
277220sqvald 11461 . . . . . . . . . . 11
278276, 277breqtrrd 4193 . . . . . . . . . 10
279111resqcld 11490 . . . . . . . . . . 11
280111, 279, 273lemuldivd 10639 . . . . . . . . . 10
281278, 280mpbid 202 . . . . . . . . 9
28229rpne0d 10599 . . . . . . . . . 10
283220, 114, 282sqdivd 11477 . . . . . . . . 9
284281, 283breqtrrd 4193 . . . . . . . 8
285 rpexpcl 11341 . . . . . . . . . 10
28630, 271, 285sylancl 644 . . . . . . . . 9
28728, 286logled 20461 . . . . . . . 8
288284, 287mpbid 202 . . . . . . 7
289 relogexp 20429 . . . . . . . 8
29030, 271, 289sylancl 644 . . . . . . 7
291288, 290breqtrd 4191 . . . . . 6
29228relogcld 20457 . . . . . . 7
29330relogcld 20457 . . . . . . 7
294 ledivmul 9829 . . . . . . 7
295292, 293, 193, 195, 294syl112anc 1188 . . . . . 6
296291, 295mpbird 224 . . . . 5
29720rprege0d 10601 . . . . . 6
29838, 30rerpdivcld 10621 . . . . . 6
29927simp2d 970 . . . . . . . . . 10
300299simp1d 969 . . . . . . . . 9
301111, 300rplogcld 20463 . . . . . . . 8
302301rphalfcld 10606 . . . . . . 7
303302rprege0d 10601 . . . . . 6
304 lemul12a 9814 . . . . . 6
305297, 298, 303, 293, 304syl22anc 1185 . . . . 5
306258, 296, 305mp2and 661 . . . 4
307301rpcnd 10596 . . . . . 6
308 8nn 10085 . . . . . . . 8
309 nnrp 10567 . . . . . . . 8
310308, 309ax-mp 8 . . . . . . 7
311 rpcnne0 10575 . . . . . . 7
312310, 311mp1i 12 . . . . . 6
313 div23 9643 . . . . . 6
314153, 307, 312, 313syl3anc 1184 . . . . 5
315 divmuldiv 9660 . . . . . . 7
316153, 307, 143, 150, 315syl22anc 1185 . . . . . 6
317 4t2e8 10076 . . . . . . 7
318317oveq2i 6045 . . . . . 6
319316, 318syl6req 2450 . . . . 5
320314, 319eqtr3d 2435 . . . 4
32138recnd 9061 . . . . 5
322293recnd 9061 . . . . 5
32330rpcnne0d 10603 . . . . 5
324 divass 9642 . . . . . 6
325 div23 9643 . . . . . 6
326324, 325eqtr3d 2435 . . . . 5
327321, 322, 323, 326syl3anc 1184 . . . 4
328306, 320, 3273brtr4d 4197 . . 3
329 rpdivcl 10580 . . . . . . 7
33015, 310, 329sylancl 644 . . . . . 6
331330, 301rpmulcld 10610 . . . . 5
332331rpred 10594 . . . 4
333293, 30rerpdivcld 10621 . . . . 5
33438, 333remulcld 9063 . . . 4
335183simp3d 971 . . . 4
336332, 334, 335lemul2d 10634 . . 3
337328, 336mpbid 202 . 2
338335rpcnd 10596 . . 3
339333recnd 9061 . . 3
340338, 321, 339mul12d 9221 . 2
341337, 340breqtrd 4191 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936   wceq 1649   wcel 1721   wne 2564  wral 2663  wrex 2664   class class class wbr 4167   cmpt 4221  cfv 5408  (class class class)co 6034  cfn 7059  cc 8935  cr 8936  cc0 8937  c1 8938   caddc 8940   cmul 8942   cpnf 9064   clt 9067   cle 9068   cmin 9237   cdiv 9623  cn 9946  c2 9995  c3 9996  c4 9997  c8 10001  cn0 10167  cz 10228  ;cdc 10328  cuz 10434  crp 10558  cioo 10862  cico 10864  cicc 10865  cfz 10989  ..^cfzo 11079  cfl 11142  cexp 11323  chash 11559  csqr 11979  cabs 11980  ce 12605  ceu 12606  clog 20391  ψcchp 20814 This theorem is referenced by:  pntlemj  21236 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-inf2 7543  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014  ax-pre-sup 9015  ax-addf 9016  ax-mulf 9017 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-iin 4052  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-se 4497  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-of 6258  df-1st 6302  df-2nd 6303  df-riota 6499  df-recs 6583  df-rdg 6618  df-1o 6674  df-2o 6675  df-oadd 6678  df-er 6855  df-map 6970  df-pm 6971  df-ixp 7014  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-fi 7365  df-sup 7395  df-oi 7426  df-card 7773  df-cda 7995  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-div 9624  df-nn 9947  df-2 10004  df-3 10005  df-4 10006  df-5 10007  df-6 10008  df-7 10009  df-8 10010  df-9 10011  df-10 10012  df-n0 10168  df-z 10229  df-dec 10329  df-uz 10435  df-q 10521  df-rp 10559  df-xneg 10656  df-xadd 10657  df-xmul 10658  df-ioo 10866  df-ioc 10867  df-ico 10868  df-icc 10869  df-fz 10990  df-fzo 11080  df-fl 11143  df-mod 11192  df-seq 11265  df-exp 11324  df-fac 11508  df-bc 11535  df-hash 11560  df-shft 11823  df-cj 11845  df-re 11846  df-im 11847  df-sqr 11981  df-abs 11982  df-limsup 12206  df-clim 12223  df-rlim 12224  df-sum 12421  df-ef 12611  df-e 12612  df-sin 12613  df-cos 12614  df-pi 12616  df-struct 13412  df-ndx 13413  df-slot 13414  df-base 13415  df-sets 13416  df-ress 13417  df-plusg 13483  df-mulr 13484  df-starv 13485  df-sca 13486  df-vsca 13487  df-tset 13489  df-ple 13490  df-ds 13492  df-unif 13493  df-hom 13494  df-cco 13495  df-rest 13591  df-topn 13592  df-topgen 13608  df-pt 13609  df-prds 13612  df-xrs 13667  df-0g 13668  df-gsum 13669  df-qtop 13674  df-imas 13675  df-xps 13677  df-mre 13752  df-mrc 13753  df-acs 13755  df-mnd 14631  df-submnd 14680  df-mulg 14756  df-cntz 15057  df-cmn 15355  df-psmet 16635  df-xmet 16636  df-met 16637  df-bl 16638  df-mopn 16639  df-fbas 16640  df-fg 16641  df-cnfld 16645  df-top 16904  df-bases 16906  df-topon 16907  df-topsp 16908  df-cld 17024  df-ntr 17025  df-cls 17026  df-nei 17103  df-lp 17141  df-perf 17142  df-cn 17231  df-cnp 17232  df-haus 17319  df-tx 17533  df-hmeo 17726  df-fil 17817  df-fm 17909  df-flim 17910  df-flf 17911  df-xms 18289  df-ms 18290  df-tms 18291  df-cncf 18847  df-limc 19692  df-dv 19693  df-log 20393
 Copyright terms: Public domain W3C validator