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-flddrng Field ⊆ DivRing
2 refld fld ∈ Field
3 1 2 sselii fld ∈ DivRing