Metamath Proof Explorer

Theorem reofld

Description: The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018)

Ref Expression
Assertion reofld ⊢ℝfld∈oField

Proof

Step Hyp Ref Expression
1 refld ⊢ℝfld∈Field
2 isfld ⊢ℝfld∈Field↔ℝfld∈DivRing∧ℝfld∈CRing
3 2 simplbi ⊢ℝfld∈Field→ℝfld∈DivRing
4 drngring ⊢ℝfld∈DivRing→ℝfld∈Ring
5 1 3 4 mp2b ⊢ℝfld∈Ring
6 ringgrp ⊢ℝfld∈Ring→ℝfld∈Grp
7 5 6 ax-mp ⊢ℝfld∈Grp
8 grpmnd ⊢ℝfld∈Grp→ℝfld∈Mnd
9 7 8 ax-mp ⊢ℝfld∈Mnd
10 retos ⊢ℝfld∈Toset
11 simpl ⊢a∈ℝ∧b∈ℝ∧c∈ℝ∧a≤b→a∈ℝ
12 simpr1 ⊢a∈ℝ∧b∈ℝ∧c∈ℝ∧a≤b→b∈ℝ
13 simpr2 ⊢a∈ℝ∧b∈ℝ∧c∈ℝ∧a≤b→c∈ℝ
14 simpr3 ⊢a∈ℝ∧b∈ℝ∧c∈ℝ∧a≤b→a≤b
15 11 12 13 14 leadd1dd ⊢a∈ℝ∧b∈ℝ∧c∈ℝ∧a≤b→a+c≤b+c
16 15 3anassrs ⊢a∈ℝ∧b∈ℝ∧c∈ℝ∧a≤b→a+c≤b+c
17 16 ex ⊢a∈ℝ∧b∈ℝ∧c∈ℝ→a≤b→a+c≤b+c
18 17 3impa ⊢a∈ℝ∧b∈ℝ∧c∈ℝ→a≤b→a+c≤b+c
19 18 rgen3 ⊢∀a∈ℝ∀b∈ℝ∀c∈ℝa≤b→a+c≤b+c
20 rebase ⊢ℝ=Baseℝfld
21 replusg ⊢+=+ℝfld
22 rele2 ⊢≤=≤ℝfld
23 20 21 22 isomnd ⊢ℝfld∈oMnd↔ℝfld∈Mnd∧ℝfld∈Toset∧∀a∈ℝ∀b∈ℝ∀c∈ℝa≤b→a+c≤b+c
24 9 10 19 23 mpbir3an ⊢ℝfld∈oMnd
25 isogrp ⊢ℝfld∈oGrp↔ℝfld∈Grp∧ℝfld∈oMnd
26 7 24 25 mpbir2an ⊢ℝfld∈oGrp
27 mulge0 ⊢a∈ℝ∧0≤a∧b∈ℝ∧0≤b→0≤a⁢b
28 27 an4s ⊢a∈ℝ∧b∈ℝ∧0≤a∧0≤b→0≤a⁢b
29 28 ex ⊢a∈ℝ∧b∈ℝ→0≤a∧0≤b→0≤a⁢b
30 29 rgen2 ⊢∀a∈ℝ∀b∈ℝ0≤a∧0≤b→0≤a⁢b
31 re0g ⊢0=0ℝfld
32 remulr ⊢×=⋅ℝfld
33 20 31 32 22 isorng ⊢ℝfld∈oRing↔ℝfld∈Ring∧ℝfld∈oGrp∧∀a∈ℝ∀b∈ℝ0≤a∧0≤b→0≤a⁢b
34 5 26 30 33 mpbir3an ⊢ℝfld∈oRing
35 isofld ⊢ℝfld∈oField↔ℝfld∈Field∧ℝfld∈oRing
36 1 34 35 mpbir2an ⊢ℝfld∈oField