Theorem idomringd 20986

Description: An integral domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.) (Revised by Thierry Arnoux, 22-Mar-2025.)

Hypothesis

Ref	Expression
idomringd.1	⊢ (𝜑 → 𝑅 ∈ IDomn)

Assertion

Ref	Expression
idomringd	⊢ (𝜑 → 𝑅 ∈ Ring)

Proof of Theorem idomringd

Step	Hyp	Ref	Expression
1		idomringd.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ IDomn)
2	1	idomcringd 20985	. 2 ⊢ (𝜑 → 𝑅 ∈ CRing)
3	2	crngringd 20480	1 ⊢ (𝜑 → 𝑅 ∈ Ring)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Ringcrg 20466  IDomncidom 20952

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6496  df-fv 6549  df-cring 20469  df-idom 20955

This theorem is used by:  fracfld  33918  dvdsruasso  33988  dvdsruasso2  33989  mxidlirredi  34044  mxidlirred  34045  rprmasso  34105  rprmasso2  34106  unitmulrprm  34108  rprmirred  34111  rprmirredb  34112  1arithidomlem1  34115  1arithidomlem2  34116  1arithidom  34117  pidufd  34123  1arithufdlem2  34125  1arithufdlem4  34127  dfufd2lem  34129  dfufd2  34130  deg1prod  34163  mplidomlem  34207  vietadeg1  34258  vietalem  34259  vieta  34260  assafld  34317  fldextrspunlem1  34355  algextdeglem7  34403  idomnnzpownz  43289  deg1gprod  43297  deg1pow  43298  aks6d1c6lem3  43329  unitscyglem5  43356