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 |