Description: The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | qrng.q | |- Q = ( CCfld |`s QQ ) |
|
| Assertion | qrng0 | |- 0 = ( 0g ` 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 | subrgsubg | |- ( QQ e. ( SubRing ` CCfld ) -> QQ e. ( SubGrp ` CCfld ) ) |
|
| 5 | cnfld0 | |- 0 = ( 0g ` CCfld ) |
|
| 6 | 1 5 | subg0 | |- ( QQ e. ( SubGrp ` CCfld ) -> 0 = ( 0g ` Q ) ) |
| 7 | 3 4 6 | mp2b | |- 0 = ( 0g ` Q ) |