Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Affine, Euclidean, and Cartesian geometry
Real vector spaces
bj-rrdrg
Next ⟩
bj-isclm
Metamath Proof Explorer
Ascii
Unicode
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