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

Theorem nrginvrcnlem 20962
 Description: Lemma for nrginvrcn 20963. Compare this proof with reccn2 13382, the elementary proof of continuity of division. (Contributed by Mario Carneiro, 6-Oct-2015.)
Hypotheses
Ref Expression
nrginvrcn.x
nrginvrcn.u Unit
nrginvrcn.i
nrginvrcn.n
nrginvrcn.d
nrginvrcn.r NrmRing
nrginvrcn.z NzRing
nrginvrcn.a
nrginvrcn.b
nrginvrcn.t
Assertion
Ref Expression
nrginvrcnlem
Distinct variable groups:   ,,   ,   ,,   ,,   ,,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   (,)   (,)

Proof of Theorem nrginvrcnlem
StepHypRef Expression
1 nrginvrcn.t . . 3
2 1rp 11224 . . . . 5
3 nrginvrcn.r . . . . . . . 8 NrmRing
4 nrgngp 20934 . . . . . . . 8 NrmRing NrmGrp
53, 4syl 16 . . . . . . 7 NrmGrp
6 nrginvrcn.x . . . . . . . . 9
7 nrginvrcn.u . . . . . . . . 9 Unit
86, 7unitss 17110 . . . . . . . 8
9 nrginvrcn.a . . . . . . . 8
108, 9sseldi 3502 . . . . . . 7
11 nrginvrcn.z . . . . . . . 8 NzRing
12 eqid 2467 . . . . . . . . 9
137, 12nzrunit 17714 . . . . . . . 8 NzRing
1411, 9, 13syl2anc 661 . . . . . . 7
15 nrginvrcn.n . . . . . . . 8
166, 15, 12nmrpcl 20902 . . . . . . 7 NrmGrp
175, 10, 14, 16syl3anc 1228 . . . . . 6
18 nrginvrcn.b . . . . . 6
1917, 18rpmulcld 11272 . . . . 5
20 ifcl 3981 . . . . 5
212, 19, 20sylancr 663 . . . 4
2217rphalfcld 11268 . . . 4
2321, 22rpmulcld 11272 . . 3
241, 23syl5eqel 2559 . 2
255adantr 465 . . . . . . . . . . 11 NrmGrp
269adantr 465 . . . . . . . . . . . 12
276, 7unitcl 17109 . . . . . . . . . . . 12
2826, 27syl 16 . . . . . . . . . . 11
296, 15nmcl 20898 . . . . . . . . . . 11 NrmGrp
3025, 28, 29syl2anc 661 . . . . . . . . . 10
3130recnd 9622 . . . . . . . . 9
32 simprl 755 . . . . . . . . . . . 12
338, 32sseldi 3502 . . . . . . . . . . 11
346, 15nmcl 20898 . . . . . . . . . . 11 NrmGrp
3525, 33, 34syl2anc 661 . . . . . . . . . 10
3635recnd 9622 . . . . . . . . 9
37 ngpgrp 20882 . . . . . . . . . . . . 13 NrmGrp
3825, 37syl 16 . . . . . . . . . . . 12
39 nrgrng 20935 . . . . . . . . . . . . . . 15 NrmRing
403, 39syl 16 . . . . . . . . . . . . . 14
4140adantr 465 . . . . . . . . . . . . 13
42 nrginvrcn.i . . . . . . . . . . . . . 14
437, 42, 6rnginvcl 17126 . . . . . . . . . . . . 13
4441, 26, 43syl2anc 661 . . . . . . . . . . . 12
457, 42, 6rnginvcl 17126 . . . . . . . . . . . . 13
4641, 32, 45syl2anc 661 . . . . . . . . . . . 12
47 eqid 2467 . . . . . . . . . . . . 13
486, 47grpsubcl 15928 . . . . . . . . . . . 12
4938, 44, 46, 48syl3anc 1228 . . . . . . . . . . 11
506, 15nmcl 20898 . . . . . . . . . . 11 NrmGrp
5125, 49, 50syl2anc 661 . . . . . . . . . 10
5251recnd 9622 . . . . . . . . 9
5331, 36, 52mul32d 9789 . . . . . . . 8
543adantr 465 . . . . . . . . . . 11 NrmRing
55 eqid 2467 . . . . . . . . . . . 12
566, 15, 55nmmul 20936 . . . . . . . . . . 11 NrmRing
5754, 28, 49, 56syl3anc 1228 . . . . . . . . . 10
586, 55, 47, 41, 28, 44, 46rngsubdi 17046 . . . . . . . . . . . 12
59 eqid 2467 . . . . . . . . . . . . . . 15
607, 42, 55, 59unitrinv 17128 . . . . . . . . . . . . . 14
6141, 26, 60syl2anc 661 . . . . . . . . . . . . 13
6261oveq1d 6299 . . . . . . . . . . . 12
6358, 62eqtrd 2508 . . . . . . . . . . 11
6463fveq2d 5870 . . . . . . . . . 10
6557, 64eqtr3d 2510 . . . . . . . . 9
6665oveq1d 6299 . . . . . . . 8
676, 59rngidcl 17020 . . . . . . . . . . . 12
6841, 67syl 16 . . . . . . . . . . 11
696, 55rngcl 17013 . . . . . . . . . . . 12
7041, 28, 46, 69syl3anc 1228 . . . . . . . . . . 11
716, 47grpsubcl 15928 . . . . . . . . . . 11
7238, 68, 70, 71syl3anc 1228 . . . . . . . . . 10
736, 15, 55nmmul 20936 . . . . . . . . . 10 NrmRing
7454, 72, 33, 73syl3anc 1228 . . . . . . . . 9
756, 55, 47, 41, 68, 70, 33rngsubdir 17047 . . . . . . . . . . 11
766, 55, 59rnglidm 17023 . . . . . . . . . . . . 13
7741, 33, 76syl2anc 661 . . . . . . . . . . . 12
786, 55rngass 17016 . . . . . . . . . . . . . 14
7941, 28, 46, 33, 78syl13anc 1230 . . . . . . . . . . . . 13
807, 42, 55, 59unitlinv 17127 . . . . . . . . . . . . . . 15
8141, 32, 80syl2anc 661 . . . . . . . . . . . . . 14
8281oveq2d 6300 . . . . . . . . . . . . 13
836, 55, 59rngridm 17024 . . . . . . . . . . . . . 14
8441, 28, 83syl2anc 661 . . . . . . . . . . . . 13
8579, 82, 843eqtrd 2512 . . . . . . . . . . . 12
8677, 85oveq12d 6302 . . . . . . . . . . 11
8775, 86eqtrd 2508 . . . . . . . . . 10
8887fveq2d 5870 . . . . . . . . 9
8974, 88eqtr3d 2510 . . . . . . . 8
9053, 66, 893eqtrd 2512 . . . . . . 7
916, 47grpsubcl 15928 . . . . . . . . . . 11
9238, 33, 28, 91syl3anc 1228 . . . . . . . . . 10
936, 15nmcl 20898 . . . . . . . . . 10 NrmGrp
9425, 92, 93syl2anc 661 . . . . . . . . 9
9594recnd 9622 . . . . . . . 8
9617adantr 465 . . . . . . . . . . 11
9711adantr 465 . . . . . . . . . . . . 13 NzRing
987, 12nzrunit 17714 . . . . . . . . . . . . 13 NzRing
9997, 32, 98syl2anc 661 . . . . . . . . . . . 12
1006, 15, 12nmrpcl 20902 . . . . . . . . . . . 12 NrmGrp
10125, 33, 99, 100syl3anc 1228 . . . . . . . . . . 11
10296, 101rpmulcld 11272 . . . . . . . . . 10
103102rpred 11256 . . . . . . . . 9
104103recnd 9622 . . . . . . . 8
105102rpne0d 11261 . . . . . . . 8
10695, 104, 52, 105divmuld 10342 . . . . . . 7
10790, 106mpbird 232 . . . . . 6
108 nrginvrcn.d . . . . . . . . 9
10915, 6, 47, 108ngpdsr 20887 . . . . . . . 8 NrmGrp
11025, 28, 33, 109syl3anc 1228 . . . . . . 7
111110oveq1d 6299 . . . . . 6
11215, 6, 47, 108ngpds 20886 . . . . . . 7 NrmGrp
11325, 44, 46, 112syl3anc 1228 . . . . . 6
114107, 111, 1133eqtr4rd 2519 . . . . 5
115110, 94eqeltrd 2555 . . . . . . 7
11624adantr 465 . . . . . . . 8
117116rpred 11256 . . . . . . 7
11818adantr 465 . . . . . . . . 9
119118rpred 11256 . . . . . . . 8
120103, 119remulcld 9624 . . . . . . 7
121 simprr 756 . . . . . . 7
12219adantr 465 . . . . . . . . . 10
12396rphalfcld 11268 . . . . . . . . . 10
124122, 123rpmulcld 11272 . . . . . . . . 9
125124rpred 11256 . . . . . . . 8
126 1re 9595 . . . . . . . . . . 11
127122rpred 11256 . . . . . . . . . . 11
128 min2 11390 . . . . . . . . . . 11
129126, 127, 128sylancr 663 . . . . . . . . . 10
13021adantr 465 . . . . . . . . . . . 12
131130rpred 11256 . . . . . . . . . . 11
132131, 127, 123lemul1d 11295 . . . . . . . . . 10
133129, 132mpbid 210 . . . . . . . . 9
1341, 133syl5eqbr 4480 . . . . . . . 8
135123rpred 11256 . . . . . . . . . 10
136312halvesd 10784 . . . . . . . . . . . 12
13730, 35resubcld 9987 . . . . . . . . . . . . . 14
1386, 15, 47nm2dif 20907 . . . . . . . . . . . . . . . 16 NrmGrp
13925, 28, 33, 138syl3anc 1228 . . . . . . . . . . . . . . 15
14015, 6, 47, 108ngpds 20886 . . . . . . . . . . . . . . . 16 NrmGrp
14125, 28, 33, 140syl3anc 1228 . . . . . . . . . . . . . . 15
142139, 141breqtrrd 4473 . . . . . . . . . . . . . 14
143 min1 11389 . . . . . . . . . . . . . . . . . . 19
144126, 127, 143sylancr 663 . . . . . . . . . . . . . . . . . 18
145 1red 9611 . . . . . . . . . . . . . . . . . . 19
146131, 145, 123lemul1d 11295 . . . . . . . . . . . . . . . . . 18
147144, 146mpbid 210 . . . . . . . . . . . . . . . . 17
1481, 147syl5eqbr 4480 . . . . . . . . . . . . . . . 16
149135recnd 9622 . . . . . . . . . . . . . . . . 17
150149mulid2d 9614 . . . . . . . . . . . . . . . 16
151148, 150breqtrd 4471 . . . . . . . . . . . . . . 15
152115, 117, 135, 121, 151ltletrd 9741 . . . . . . . . . . . . . 14
153137, 115, 135, 142, 152lelttrd 9739 . . . . . . . . . . . . 13
15430, 35, 135ltsubadd2d 10150 . . . . . . . . . . . . 13
155153, 154mpbid 210 . . . . . . . . . . . 12
156136, 155eqbrtrd 4467 . . . . . . . . . . 11
157135, 35, 135ltadd1d 10145 . . . . . . . . . . 11
158156, 157mpbird 232 . . . . . . . . . 10
159135, 35, 122, 158ltmul2dd 11308 . . . . . . . . 9
160119recnd 9622 . . . . . . . . . 10
16131, 36, 160mul32d 9789 . . . . . . . . 9
162159, 161breqtrrd 4473 . . . . . . . 8
163117, 125, 120, 134, 162lelttrd 9739 . . . . . . 7
164115, 117, 120, 121, 163lttrd 9742 . . . . . 6
165115, 119, 102ltdivmuld 11303 . . . . . 6
166164, 165mpbird 232 . . . . 5
167114, 166eqbrtrd 4467 . . . 4
168167expr 615 . . 3
169168ralrimiva 2878 . 2
170 breq2 4451 . . . . 5
171170imbi1d 317 . . . 4
172171ralbidv 2903 . . 3
173172rspcev 3214 . 2
17424, 169, 173syl2anc 661 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1379   wcel 1767   wne 2662  wral 2814  wrex 2815  cif 3939   class class class wbr 4447  cfv 5588  (class class class)co 6284  cr 9491  c1 9493   caddc 9495   cmul 9497   clt 9628   cle 9629   cmin 9805   cdiv 10206  c2 10585  crp 11220  cbs 14490  cmulr 14556  cds 14564  c0g 14695  cgrp 15727  csg 15730  cur 16955  crg 17000  Unitcui 17089  cinvr 17121  NzRingcnzr 17704  cnm 20860  NrmGrpcngp 20861  NrmRingcnrg 20863 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569  ax-pre-sup 9570 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-1st 6784  df-2nd 6785  df-tpos 6955  df-recs 7042  df-rdg 7076  df-1o 7130  df-oadd 7134  df-er 7311  df-map 7422  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-sup 7901  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-div 10207  df-nn 10537  df-2 10594  df-3 10595  df-4 10596  df-5 10597  df-6 10598  df-7 10599  df-8 10600  df-9 10601  df-10 10602  df-n0 10796  df-z 10865  df-dec 10977  df-uz 11083  df-q 11183  df-rp 11221  df-xneg 11318  df-xadd 11319  df-xmul 11320  df-fz 11673  df-seq 12076  df-exp 12135  df-cj 12895  df-re 12896  df-im 12897  df-sqrt 13031  df-abs 13032  df-struct 14492  df-ndx 14493  df-slot 14494  df-base 14495  df-sets 14496  df-ress 14497  df-plusg 14568  df-mulr 14569  df-tset 14574  df-ple 14575  df-ds 14577  df-0g 14697  df-topgen 14699  df-xrs 14757  df-mnd 15732  df-grp 15867  df-minusg 15868  df-sbg 15869  df-mgp 16944  df-ur 16956  df-rng 17002  df-oppr 17073  df-dvdsr 17091  df-unit 17092  df-invr 17122  df-abv 17266  df-nzr 17705  df-psmet 18210  df-xmet 18211  df-met 18212  df-bl 18213  df-mopn 18214  df-top 19194  df-bases 19196  df-topon 19197  df-topsp 19198  df-xms 20586  df-ms 20587  df-nm 20866  df-ngp 20867  df-nrg 20869 This theorem is referenced by:  nrginvrcn  20963
 Copyright terms: Public domain W3C validator