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 ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) ) → 𝑎 ∈ ℝ )
12 simpr1 ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) ) → 𝑏 ∈ ℝ )
13 simpr2 ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) ) → 𝑐 ∈ ℝ )
14 simpr3 ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) ) → 𝑎 ≤ 𝑏 )
15 11 12 13 14 leadd1dd ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) )
16 15 3anassrs ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑎 ≤ 𝑏 ) → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) )
17 16 ex ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ 𝑐 ∈ ℝ ) → ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) )
18 17 3impa ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) )
19 18 rgen3 ⊢ ∀ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ℝ ∀ 𝑐 ∈ ℝ ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) )
20 rebase ⊢ ℝ = ( Base ‘ ℝfld )
21 replusg ⊢ + = ( +g ‘ ℝfld )
22 rele2 ⊢ ≤ = ( le ‘ ℝfld )
23 20 21 22 isomnd ⊢ ( ℝfld ∈ oMnd ↔ ( ℝfld ∈ Mnd ∧ ℝfld ∈ Toset ∧ ∀ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ℝ ∀ 𝑐 ∈ ℝ ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) )
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 ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 0 ≤ 𝑎 ) ∧ ( 𝑏 ∈ ℝ ∧ 0 ≤ 𝑏 ) ) → 0 ≤ ( 𝑎 · 𝑏 ) )
28 27 an4s ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) ) → 0 ≤ ( 𝑎 · 𝑏 ) )
29 28 ex ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑎 · 𝑏 ) ) )
30 29 rgen2 ⊢ ∀ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ℝ ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑎 · 𝑏 ) )
31 re0g ⊢ 0 = ( 0g ‘ ℝfld )
32 remulr ⊢ · = ( .r ‘ ℝfld )
33 20 31 32 22 isorng ⊢ ( ℝfld ∈ oRing ↔ ( ℝfld ∈ Ring ∧ ℝfld ∈ oGrp ∧ ∀ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ℝ ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑎 · 𝑏 ) ) ) )
34 5 26 30 33 mpbir3an ⊢ ℝfld ∈ oRing
35 isofld ⊢ ( ℝfld ∈ oField ↔ ( ℝfld ∈ Field ∧ ℝfld ∈ oRing ) )
36 1 34 35 mpbir2an ⊢ ℝfld ∈ oField