Description: The unit element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | qrng.q | |- Q = ( CCfld |`s QQ ) |
|
| Assertion | qrng1 | |- 1 = ( 1r ` Q ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | qrng.q | |- Q = ( CCfld |`s QQ ) |
|
| 2 | qsubdrg | |- ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) |
|
| 3 | 2 | simpli | |- QQ e. ( SubRing ` CCfld ) |
| 4 | cnfld1 | |- 1 = ( 1r ` CCfld ) |
|
| 5 | 1 4 | subrg1 | |- ( QQ e. ( SubRing ` CCfld ) -> 1 = ( 1r ` Q ) ) |
| 6 | 3 5 | ax-mp | |- 1 = ( 1r ` Q ) |