Description: The multiplicative neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | re1r | |- 1 = ( 1r ` RRfld ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | resubdrg | |- ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing ) |
|
| 2 | 1 | simpli | |- RR e. ( SubRing ` CCfld ) |
| 3 | df-refld | |- RRfld = ( CCfld |`s RR ) |
|
| 4 | cnfld1 | |- 1 = ( 1r ` CCfld ) |
|
| 5 | 3 4 | subrg1 | |- ( RR e. ( SubRing ` CCfld ) -> 1 = ( 1r ` RRfld ) ) |
| 6 | 2 5 | ax-mp | |- 1 = ( 1r ` RRfld ) |