Description: The field of rational numbers is a field. (Contributed by Thierry Arnoux, 19-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | qfld.1 | |- Q = ( CCfld |`s QQ ) |
|
| Assertion | qfld | |- Q e. Field |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | qfld.1 | |- Q = ( CCfld |`s QQ ) |
|
| 2 | 1 | qdrng | |- Q e. DivRing |
| 3 | cncrng | |- CCfld e. CRing |
|
| 4 | qsubdrg | |- ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) |
|
| 5 | 4 | simpli | |- QQ e. ( SubRing ` CCfld ) |
| 6 | 1 | subrgcrng | |- ( ( CCfld e. CRing /\ QQ e. ( SubRing ` CCfld ) ) -> Q e. CRing ) |
| 7 | 3 5 6 | mp2an | |- Q e. CRing |
| 8 | isfld | |- ( Q e. Field <-> ( Q e. DivRing /\ Q e. CRing ) ) |
|
| 9 | 2 7 8 | mpbir2an | |- Q e. Field |