Metamath Proof Explorer


Theorem reofld

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

Ref Expression
Assertion reofld
|- RRfld e. oField

Proof

Step Hyp Ref Expression
1 refld
 |-  RRfld e. Field
2 isfld
 |-  ( RRfld e. Field <-> ( RRfld e. DivRing /\ RRfld e. CRing ) )
3 2 simplbi
 |-  ( RRfld e. Field -> RRfld e. DivRing )
4 drngring
 |-  ( RRfld e. DivRing -> RRfld e. Ring )
5 1 3 4 mp2b
 |-  RRfld e. Ring
6 ringgrp
 |-  ( RRfld e. Ring -> RRfld e. Grp )
7 5 6 ax-mp
 |-  RRfld e. Grp
8 grpmnd
 |-  ( RRfld e. Grp -> RRfld e. Mnd )
9 7 8 ax-mp
 |-  RRfld e. Mnd
10 retos
 |-  RRfld e. Toset
11 simpl
 |-  ( ( a e. RR /\ ( b e. RR /\ c e. RR /\ a <_ b ) ) -> a e. RR )
12 simpr1
 |-  ( ( a e. RR /\ ( b e. RR /\ c e. RR /\ a <_ b ) ) -> b e. RR )
13 simpr2
 |-  ( ( a e. RR /\ ( b e. RR /\ c e. RR /\ a <_ b ) ) -> c e. RR )
14 simpr3
 |-  ( ( a e. RR /\ ( b e. RR /\ c e. RR /\ a <_ b ) ) -> a <_ b )
15 11 12 13 14 leadd1dd
 |-  ( ( a e. RR /\ ( b e. RR /\ c e. RR /\ a <_ b ) ) -> ( a + c ) <_ ( b + c ) )
16 15 3anassrs
 |-  ( ( ( ( a e. RR /\ b e. RR ) /\ c e. RR ) /\ a <_ b ) -> ( a + c ) <_ ( b + c ) )
17 16 ex
 |-  ( ( ( a e. RR /\ b e. RR ) /\ c e. RR ) -> ( a <_ b -> ( a + c ) <_ ( b + c ) ) )
18 17 3impa
 |-  ( ( a e. RR /\ b e. RR /\ c e. RR ) -> ( a <_ b -> ( a + c ) <_ ( b + c ) ) )
19 18 rgen3
 |-  A. a e. RR A. b e. RR A. c e. RR ( a <_ b -> ( a + c ) <_ ( b + c ) )
20 rebase
 |-  RR = ( Base ` RRfld )
21 replusg
 |-  + = ( +g ` RRfld )
22 rele2
 |-  <_ = ( le ` RRfld )
23 20 21 22 isomnd
 |-  ( RRfld e. oMnd <-> ( RRfld e. Mnd /\ RRfld e. Toset /\ A. a e. RR A. b e. RR A. c e. RR ( a <_ b -> ( a + c ) <_ ( b + c ) ) ) )
24 9 10 19 23 mpbir3an
 |-  RRfld e. oMnd
25 isogrp
 |-  ( RRfld e. oGrp <-> ( RRfld e. Grp /\ RRfld e. oMnd ) )
26 7 24 25 mpbir2an
 |-  RRfld e. oGrp
27 mulge0
 |-  ( ( ( a e. RR /\ 0 <_ a ) /\ ( b e. RR /\ 0 <_ b ) ) -> 0 <_ ( a x. b ) )
28 27 an4s
 |-  ( ( ( a e. RR /\ b e. RR ) /\ ( 0 <_ a /\ 0 <_ b ) ) -> 0 <_ ( a x. b ) )
29 28 ex
 |-  ( ( a e. RR /\ b e. RR ) -> ( ( 0 <_ a /\ 0 <_ b ) -> 0 <_ ( a x. b ) ) )
30 29 rgen2
 |-  A. a e. RR A. b e. RR ( ( 0 <_ a /\ 0 <_ b ) -> 0 <_ ( a x. b ) )
31 re0g
 |-  0 = ( 0g ` RRfld )
32 remulr
 |-  x. = ( .r ` RRfld )
33 20 31 32 22 isorng
 |-  ( RRfld e. oRing <-> ( RRfld e. Ring /\ RRfld e. oGrp /\ A. a e. RR A. b e. RR ( ( 0 <_ a /\ 0 <_ b ) -> 0 <_ ( a x. b ) ) ) )
34 5 26 30 33 mpbir3an
 |-  RRfld e. oRing
35 isofld
 |-  ( RRfld e. oField <-> ( RRfld e. Field /\ RRfld e. oRing ) )
36 1 34 35 mpbir2an
 |-  RRfld e. oField