Theorem fiidomfld

Description: A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypothesis	fidomndrng.b	|- B = ( Base ` R )
Assertion	fiidomfld	|- ( B e. Fin -> ( R e. IDomn <-> R e. Field ) )

Proof

Step	Hyp	Ref	Expression
1		fidomndrng.b	|- B = ( Base ` R )
2	1	fidomndrng	|- ( B e. Fin -> ( R e. Domn <-> R e. DivRing ) )
3	2	anbi2d	|- ( B e. Fin -> ( ( R e. CRing /\ R e. Domn ) <-> ( R e. CRing /\ R e. DivRing ) ) )
4		isidom	|- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
5		isfld	|- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
6	5	biancomi	|- ( R e. Field <-> ( R e. CRing /\ R e. DivRing ) )
7	3 4 6	3bitr4g	|- ( B e. Fin -> ( R e. IDomn <-> R e. Field ) )