| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > idomringd | Structured version Visualization version GIF version | ||
| Description: An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| Ref | Expression |
|---|---|
| idomringd.1 | ⊢ (𝜑 → 𝑅 ∈ IDomn) |
| Ref | Expression |
|---|---|
| idomringd | ⊢ (𝜑 → 𝑅 ∈ Ring) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | idomringd.1 | . . 3 ⊢ (𝜑 → 𝑅 ∈ IDomn) | |
| 2 | 1 | idomcringd 20631 | . 2 ⊢ (𝜑 → 𝑅 ∈ CRing) |
| 3 | 2 | crngringd 20150 | 1 ⊢ (𝜑 → 𝑅 ∈ Ring) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2109 Ringcrg 20137 IDomncidom 20597 |
| 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 2008 ax-8 2111 ax-9 2119 ax-ext 2701 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-rab 3397 df-v 3440 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-br 5096 df-iota 6442 df-fv 6494 df-cring 20140 df-idom 20600 |
| This theorem is referenced by: fracfld 33266 dvdsruasso 33341 dvdsruasso2 33342 unitpidl1 33380 mxidlirredi 33427 mxidlirred 33428 rsprprmprmidlb 33479 rprmasso 33481 rprmasso2 33482 unitmulrprm 33484 rprmirred 33487 rprmirredb 33488 1arithidomlem1 33491 1arithidomlem2 33492 1arithidom 33493 pidufd 33499 1arithufdlem2 33501 1arithufdlem4 33503 dfufd2lem 33505 dfufd2 33506 r1pid2OLD 33560 assafld 33623 fldextrspunlem1 33661 algextdeglem7 33709 idomnnzpownz 42125 deg1gprod 42133 deg1pow 42134 aks6d1c6lem3 42165 unitscyglem5 42192 |
| Copyright terms: Public domain | W3C validator |