This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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