Metamath Proof Explorer

Theorem drngnzr

Description: All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015)

		Ref	Expression
	Assertion	drngnzr	$⊢ R \in DivRing \to R \in NzRing$

Step	Hyp	Ref	Expression
1		drngring	$⊢ R \in DivRing \to R \in Ring$
2		eqid	$⊢ 0_{R} = 0_{R}$
3		eqid	$⊢ 1_{R} = 1_{R}$
4	2 3	drngunz	$⊢ R \in DivRing \to 1_{R} \neq 0_{R}$
5	3 2	isnzr	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land 1_{R} \neq 0_{R})$
6	1 4 5	sylanbrc	$⊢ R \in DivRing \to R \in NzRing$