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 
|- RRfld e. DivRing

Proof

Step Hyp Ref Expression
1 bj-fldssdrng 
 |-  Field C_ DivRing
2 refld 
 |-  RRfld e. Field
3 1 2 sselii 
 |-  RRfld e. DivRing