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

Theorem ipdirilem 22368
 Description: Lemma for ipdiri 22369. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.)
Hypotheses
Ref Expression
ip1i.1
ip1i.2
ip1i.4
ip1i.7
ip1i.9
ipdiri.8
ipdiri.9
ipdiri.10
Assertion
Ref Expression
ipdirilem

Proof of Theorem ipdirilem
StepHypRef Expression
1 2cn 10108 . . . . . . 7
2 2ne0 10121 . . . . . . 7
31, 2recidi 9783 . . . . . 6
43oveq1i 6127 . . . . 5
5 ip1i.9 . . . . . . 7
65phnvi 22355 . . . . . 6
71, 2reccli 9782 . . . . . . 7
8 ipdiri.8 . . . . . . . 8
9 ipdiri.9 . . . . . . . 8
10 ip1i.1 . . . . . . . . 9
11 ip1i.2 . . . . . . . . 9
1210, 11nvgcl 22137 . . . . . . . 8
136, 8, 9, 12mp3an 1280 . . . . . . 7
141, 7, 133pm3.2i 1133 . . . . . 6
15 ip1i.4 . . . . . . 7
1610, 15nvsass 22147 . . . . . 6
176, 14, 16mp2an 655 . . . . 5
1810, 15nvsid 22146 . . . . . 6
196, 13, 18mp2an 655 . . . . 5
204, 17, 193eqtr3i 2471 . . . 4
2120oveq1i 6127 . . 3
22 ip1i.7 . . . 4
2310, 15nvscl 22145 . . . . 5
246, 7, 13, 23mp3an 1280 . . . 4
25 ipdiri.10 . . . 4
2610, 11, 15, 22, 5, 24, 25ip2i 22367 . . 3
2721, 26eqtr3i 2465 . 2
28 neg1cn 10105 . . . . . 6
2910, 15nvscl 22145 . . . . . 6
306, 28, 9, 29mp3an 1280 . . . . 5
3110, 11nvgcl 22137 . . . . 5
326, 8, 30, 31mp3an 1280 . . . 4
3310, 15nvscl 22145 . . . 4
346, 7, 32, 33mp3an 1280 . . 3
3510, 11, 15, 22, 5, 24, 34, 25ip1i 22366 . 2
36 eqid 2443 . . . . . . . . . . . 12
3736nvvc 22132 . . . . . . . . . . 11
386, 37ax-mp 5 . . . . . . . . . 10
3911vafval 22120 . . . . . . . . . . 11
4039vcablo 22074 . . . . . . . . . 10
4138, 40ax-mp 5 . . . . . . . . 9
428, 9pm3.2i 443 . . . . . . . . 9
438, 30pm3.2i 443 . . . . . . . . 9
4410, 11bafval 22121 . . . . . . . . . 10
4544ablo4 21913 . . . . . . . . 9
4641, 42, 43, 45mp3an 1280 . . . . . . . 8
4715smfval 22122 . . . . . . . . . . 11
4839, 47, 44vc2 22072 . . . . . . . . . 10
4938, 8, 48mp2an 655 . . . . . . . . 9
50 eqid 2443 . . . . . . . . . . 11
5110, 11, 15, 50nvrinv 22172 . . . . . . . . . 10
526, 9, 51mp2an 655 . . . . . . . . 9
5349, 52oveq12i 6129 . . . . . . . 8
5410, 15nvscl 22145 . . . . . . . . . 10
556, 1, 8, 54mp3an 1280 . . . . . . . . 9
5610, 11, 50nv0rid 22154 . . . . . . . . 9
576, 55, 56mp2an 655 . . . . . . . 8
5846, 53, 573eqtri 2467 . . . . . . 7
5958oveq2i 6128 . . . . . 6
607, 1, 83pm3.2i 1133 . . . . . . 7
6110, 15nvsass 22147 . . . . . . 7
626, 60, 61mp2an 655 . . . . . 6
6359, 62eqtr4i 2466 . . . . 5
647, 13, 323pm3.2i 1133 . . . . . 6
6510, 11, 15nvdi 22149 . . . . . 6
666, 64, 65mp2an 655 . . . . 5
67 ax-1cn 9086 . . . . . . . 8
6867, 1, 2divcan1i 9796 . . . . . . 7
6968oveq1i 6127 . . . . . 6
7010, 15nvsid 22146 . . . . . . 7
716, 8, 70mp2an 655 . . . . . 6
7269, 71eqtri 2463 . . . . 5
7363, 66, 723eqtr3i 2471 . . . 4
7473oveq1i 6127 . . 3
7528, 7mulcomi 9134 . . . . . . . . 9
7675oveq1i 6127 . . . . . . . 8
7728, 7, 323pm3.2i 1133 . . . . . . . . 9
7810, 15nvsass 22147 . . . . . . . . 9
796, 77, 78mp2an 655 . . . . . . . 8
807, 28, 323pm3.2i 1133 . . . . . . . . . 10
8110, 15nvsass 22147 . . . . . . . . . 10
826, 80, 81mp2an 655 . . . . . . . . 9
8328, 8, 303pm3.2i 1133 . . . . . . . . . . . 12
8410, 11, 15nvdi 22149 . . . . . . . . . . . 12
856, 83, 84mp2an 655 . . . . . . . . . . 11
8667, 67mul2negi 9519 . . . . . . . . . . . . . . 15
87 1t1e1 10164 . . . . . . . . . . . . . . 15
8886, 87eqtri 2463 . . . . . . . . . . . . . 14
8988oveq1i 6127 . . . . . . . . . . . . 13
9028, 28, 93pm3.2i 1133 . . . . . . . . . . . . . 14
9110, 15nvsass 22147 . . . . . . . . . . . . . 14
926, 90, 91mp2an 655 . . . . . . . . . . . . 13
9310, 15nvsid 22146 . . . . . . . . . . . . . 14
946, 9, 93mp2an 655 . . . . . . . . . . . . 13
9589, 92, 943eqtr3i 2471 . . . . . . . . . . . 12
9695oveq2i 6128 . . . . . . . . . . 11
9785, 96eqtri 2463 . . . . . . . . . 10
9897oveq2i 6128 . . . . . . . . 9
9982, 98eqtri 2463 . . . . . . . 8
10076, 79, 993eqtr3i 2471 . . . . . . 7
101100oveq2i 6128 . . . . . 6
10210, 15nvscl 22145 . . . . . . . . . 10
1036, 28, 8, 102mp3an 1280 . . . . . . . . 9
10410, 11nvgcl 22137 . . . . . . . . 9
1056, 103, 9, 104mp3an 1280 . . . . . . . 8
1067, 13, 1053pm3.2i 1133 . . . . . . 7
10710, 11, 15nvdi 22149 . . . . . . 7
1086, 106, 107mp2an 655 . . . . . 6
109101, 108eqtr4i 2466 . . . . 5
110103, 9pm3.2i 443 . . . . . . . . 9
11144ablo4 21913 . . . . . . . . 9
11241, 42, 110, 111mp3an 1280 . . . . . . . 8
11310, 11, 15, 50nvrinv 22172 . . . . . . . . . . 11
1146, 8, 113mp2an 655 . . . . . . . . . 10
115114oveq1i 6127 . . . . . . . . 9
11610, 11nvgcl 22137 . . . . . . . . . . 11
1176, 9, 9, 116mp3an 1280 . . . . . . . . . 10
11810, 11, 50nv0lid 22155 . . . . . . . . . 10
1196, 117, 118mp2an 655 . . . . . . . . 9
120115, 119eqtri 2463 . . . . . . . 8
12139, 47, 44vc2 22072 . . . . . . . . 9
12238, 9, 121mp2an 655 . . . . . . . 8
123112, 120, 1223eqtri 2467 . . . . . . 7
124123oveq2i 6128 . . . . . 6
1257, 1, 93pm3.2i 1133 . . . . . . 7
12610, 15nvsass 22147 . . . . . . 7
1276, 125, 126mp2an 655 . . . . . 6
12868oveq1i 6127 . . . . . 6
129124, 127, 1283eqtr2i 2469 . . . . 5
130109, 129, 943eqtri 2467 . . . 4
131130oveq1i 6127 . . 3
13274, 131oveq12i 6129 . 2
13327, 35, 1323eqtr2i 2469 1
 Colors of variables: wff set class Syntax hints:   wa 360   w3a 937   wceq 1654   wcel 1728  cfv 5489  (class class class)co 6117  c1st 6383  cc 9026  c1 9029   caddc 9031   cmul 9033  cneg 9330   cdiv 9715  c2 10087  cablo 21907  cvc 22062  cnv 22101  cpv 22102  cba 22103  cns 22104  cn0v 22105  cdip 22234  ccphlo 22351 This theorem is referenced by:  ipdiri  22369 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-rep 4351  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736  ax-inf2 7632  ax-cnex 9084  ax-resscn 9085  ax-1cn 9086  ax-icn 9087  ax-addcl 9088  ax-addrcl 9089  ax-mulcl 9090  ax-mulrcl 9091  ax-mulcom 9092  ax-addass 9093  ax-mulass 9094  ax-distr 9095  ax-i2m1 9096  ax-1ne0 9097  ax-1rid 9098  ax-rnegex 9099  ax-rrecex 9100  ax-cnre 9101  ax-pre-lttri 9102  ax-pre-lttrn 9103  ax-pre-ltadd 9104  ax-pre-mulgt0 9105  ax-pre-sup 9106 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-fal 1330  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2717  df-rex 2718  df-reu 2719  df-rmo 2720  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-tp 3851  df-op 3852  df-uni 4045  df-int 4080  df-iun 4124  df-br 4244  df-opab 4298  df-mpt 4299  df-tr 4334  df-eprel 4529  df-id 4533  df-po 4538  df-so 4539  df-fr 4576  df-se 4577  df-we 4578  df-ord 4619  df-on 4620  df-lim 4621  df-suc 4622  df-om 4881  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-fv 5497  df-isom 5498  df-ov 6120  df-oprab 6121  df-mpt2 6122  df-1st 6385  df-2nd 6386  df-riota 6585  df-recs 6669  df-rdg 6704  df-1o 6760  df-oadd 6764  df-er 6941  df-en 7146  df-dom 7147  df-sdom 7148  df-fin 7149  df-sup 7482  df-oi 7515  df-card 7864  df-pnf 9160  df-mnf 9161  df-xr 9162  df-ltxr 9163  df-le 9164  df-sub 9331  df-neg 9332  df-div 9716  df-nn 10039  df-2 10096  df-3 10097  df-4 10098  df-n0 10260  df-z 10321  df-uz 10527  df-rp 10651  df-fz 11082  df-fzo 11174  df-seq 11362  df-exp 11421  df-hash 11657  df-cj 11942  df-re 11943  df-im 11944  df-sqr 12078  df-abs 12079  df-clim 12320  df-sum 12518  df-grpo 21817  df-gid 21818  df-ginv 21819  df-ablo 21908  df-vc 22063  df-nv 22109  df-va 22112  df-ba 22113  df-sm 22114  df-0v 22115  df-nmcv 22117  df-dip 22235  df-ph 22352
 Copyright terms: Public domain W3C validator