MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  idomringd Structured version   Visualization version   GIF version

Theorem idomringd 20728
Description: An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.)
Hypothesis
Ref Expression
idomringd.1 (𝜑𝑅 ∈ IDomn)
Assertion
Ref Expression
idomringd (𝜑𝑅 ∈ Ring)

Proof of Theorem idomringd
StepHypRef Expression
1 idomringd.1 . . 3 (𝜑𝑅 ∈ IDomn)
21idomcringd 20727 . 2 (𝜑𝑅 ∈ CRing)
32crngringd 20243 1 (𝜑𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  Ringcrg 20230  IDomncidom 20693
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-cring 20233  df-idom 20696
This theorem is referenced by:  fracfld  33310  dvdsruasso  33413  dvdsruasso2  33414  unitpidl1  33452  mxidlirredi  33499  mxidlirred  33500  rsprprmprmidlb  33551  rprmasso  33553  rprmasso2  33554  unitmulrprm  33556  rprmirred  33559  rprmirredb  33560  1arithidomlem1  33563  1arithidomlem2  33564  1arithidom  33565  pidufd  33571  1arithufdlem2  33573  1arithufdlem4  33575  dfufd2lem  33577  dfufd2  33578  r1pid2OLD  33629  assafld  33688  fldextrspunlem1  33725  algextdeglem7  33764  idomnnzpownz  42133  deg1gprod  42141  deg1pow  42142  aks6d1c6lem3  42173  unitscyglem5  42200
  Copyright terms: Public domain W3C validator