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