Metamath Proof Explorer


Theorem bj-rrdrg

Description: The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024)

Ref Expression
Assertion bj-rrdrg fld DivRing

Proof

Step Hyp Ref Expression
1 bj-fldssdrng Field DivRing
2 refld fld Field
3 1 2 sselii fld DivRing