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

Theorem rge0srg 18255
 Description: The nonnegative real numbers form a semiring (commutative by subcmn 16638). (Contributed by Thierry Arnoux, 6-Sep-2018.)
Assertion
Ref Expression
rge0srg flds SRing

Proof of Theorem rge0srg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnrng 18211 . . . 4 fld
2 rngcmn 17016 . . . 4 fld fld CMnd
31, 2ax-mp 5 . . 3 fld CMnd
4 rge0ssre 11624 . . . . . 6
5 ax-resscn 9545 . . . . . 6
64, 5sstri 3513 . . . . 5
7 0e0icopnf 11626 . . . . 5
8 ge0addcl 11628 . . . . . 6
98rgen2 2889 . . . . 5
106, 7, 93pm3.2i 1174 . . . 4
11 rngmnd 16995 . . . . . 6 fld fld
121, 11ax-mp 5 . . . . 5 fld
13 cnfldbas 18195 . . . . . 6 fld
14 cnfld0 18213 . . . . . 6 fld
15 cnfldadd 18196 . . . . . 6 fld
1613, 14, 15issubm 15788 . . . . 5 fld SubMndfld
1712, 16ax-mp 5 . . . 4 SubMndfld
1810, 17mpbir 209 . . 3 SubMndfld
19 eqid 2467 . . . 4 flds flds
2019submcmn 16639 . . 3 fld CMnd SubMndfld flds CMnd
213, 18, 20mp2an 672 . 2 flds CMnd
22 1re 9591 . . . . . 6
23 0le1 10072 . . . . . 6
24 ltpnf 11327 . . . . . . 7
2522, 24ax-mp 5 . . . . . 6
26 0re 9592 . . . . . . 7
27 pnfxr 11317 . . . . . . 7
28 elico2 11584 . . . . . . 7
2926, 27, 28mp2an 672 . . . . . 6
3022, 23, 25, 29mpbir3an 1178 . . . . 5
31 ge0mulcl 11629 . . . . . 6
3231rgen2 2889 . . . . 5
336, 30, 323pm3.2i 1174 . . . 4
34 eqid 2467 . . . . . 6 mulGrpfld mulGrpfld
3534rngmgp 16992 . . . . 5 fld mulGrpfld
3634, 13mgpbas 16937 . . . . . 6 mulGrpfld
37 cnfld1 18214 . . . . . . 7 fld
3834, 37rngidval 16945 . . . . . 6 mulGrpfld
39 cnfldmul 18197 . . . . . . 7 fld
4034, 39mgpplusg 16935 . . . . . 6 mulGrpfld
4136, 38, 40issubm 15788 . . . . 5 mulGrpfld SubMndmulGrpfld
421, 35, 41mp2b 10 . . . 4 SubMndmulGrpfld
4333, 42mpbir 209 . . 3 SubMndmulGrpfld
44 eqid 2467 . . . 4 mulGrpflds mulGrpflds
4544submmnd 15795 . . 3 SubMndmulGrpfld mulGrpflds
4643, 45ax-mp 5 . 2 mulGrpflds
47 simpll 753 . . . . . . . . 9
486, 47sseldi 3502 . . . . . . . 8
49 simplr 754 . . . . . . . . 9
506, 49sseldi 3502 . . . . . . . 8
51 simpr 461 . . . . . . . . 9
526, 51sseldi 3502 . . . . . . . 8
5348, 50, 52adddid 9616 . . . . . . 7
5448, 50, 52adddird 9617 . . . . . . 7
5553, 54jca 532 . . . . . 6
5655ralrimiva 2878 . . . . 5
5756ralrimiva 2878 . . . 4
586sseli 3500 . . . . 5
5958mul02d 9773 . . . 4
6058mul01d 9774 . . . 4
6157, 59, 60jca32 535 . . 3
6261rgen 2824 . 2
6319, 13ressbas2 14542 . . . 4 flds
646, 63ax-mp 5 . . 3 flds
65 cnfldex 18194 . . . 4 fld
66 ovex 6307 . . . 4
6719, 34mgpress 16942 . . . 4 fld mulGrpflds mulGrpflds
6865, 66, 67mp2an 672 . . 3 mulGrpflds mulGrpflds
6919, 15ressplusg 14593 . . . 4 flds
7066, 69ax-mp 5 . . 3 flds
7119, 39ressmulr 14604 . . . 4 flds
7266, 71ax-mp 5 . . 3 flds
7319, 13, 14ress0g 15763 . . . 4 fld flds
7412, 7, 6, 73mp3an 1324 . . 3 flds
7564, 68, 70, 72, 74issrg 16949 . 2 flds SRing flds CMnd mulGrpflds
7621, 46, 62, 75mpbir3an 1178 1 flds SRing
 Colors of variables: wff setvar class Syntax hints:   wb 184   wa 369   w3a 973   wceq 1379   wcel 1767  wral 2814  cvv 3113   wss 3476   class class class wbr 4447  cfv 5586  (class class class)co 6282  cc 9486  cr 9487  cc0 9488  c1 9489   caddc 9491   cmul 9493   cpnf 9621  cxr 9623   clt 9624   cle 9625  cico 11527  cbs 14486   ↾s cress 14487   cplusg 14551  cmulr 14552  c0g 14691  cmnd 15722  SubMndcsubmnd 15776  CMndccmn 16594  mulGrpcmgp 16931  SRingcsrg 16947  crg 16986  ℂfldccnfld 18191 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 6574  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565  ax-addf 9567  ax-mulf 9568 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 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-nn 10533  df-2 10590  df-3 10591  df-4 10592  df-5 10593  df-6 10594  df-7 10595  df-8 10596  df-9 10597  df-10 10598  df-n0 10792  df-z 10861  df-dec 10973  df-uz 11079  df-ico 11531  df-fz 11669  df-struct 14488  df-ndx 14489  df-slot 14490  df-base 14491  df-sets 14492  df-ress 14493  df-plusg 14564  df-mulr 14565  df-starv 14566  df-tset 14570  df-ple 14571  df-ds 14573  df-unif 14574  df-0g 14693  df-mnd 15728  df-submnd 15778  df-grp 15858  df-minusg 15859  df-cmn 16596  df-abl 16597  df-mgp 16932  df-ur 16944  df-srg 16948  df-rng 16988  df-cring 16989  df-cnfld 18192 This theorem is referenced by:  xrge0slmod  27497
 Copyright terms: Public domain W3C validator