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