Metamath Proof Explorer

Theorem fldidom

Description: A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015)

Ref Expression
Assertion fldidom ⊢ R ∈ Field → R ∈ IDomn

Proof

Step Hyp Ref Expression
1 isfld ⊢ R ∈ Field ↔ R ∈ DivRing ∧ R ∈ CRing
2 1 simprbi ⊢ R ∈ Field → R ∈ CRing
3 1 simplbi ⊢ R ∈ Field → R ∈ DivRing
4 drngdomn ⊢ R ∈ DivRing → R ∈ Domn
5 3 4 syl ⊢ R ∈ Field → R ∈ Domn
6 isidom ⊢ R ∈ IDomn ↔ R ∈ CRing ∧ R ∈ Domn
7 2 5 6 sylanbrc ⊢ R ∈ Field → R ∈ IDomn