Description: The field of rational numbers is a field. (Contributed by Thierry Arnoux, 19-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | qfld.1 | ⊢ 𝑄 = ( ℂfld ↾s ℚ ) | |
| Assertion | qfld | ⊢ 𝑄 ∈ Field |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | qfld.1 | ⊢ 𝑄 = ( ℂfld ↾s ℚ ) | |
| 2 | 1 | qdrng | ⊢ 𝑄 ∈ DivRing |
| 3 | cncrng | ⊢ ℂfld ∈ CRing | |
| 4 | qsubdrg | ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing ) | |
| 5 | 4 | simpli | ⊢ ℚ ∈ ( SubRing ‘ ℂfld ) |
| 6 | 1 | subrgcrng | ⊢ ( ( ℂfld ∈ CRing ∧ ℚ ∈ ( SubRing ‘ ℂfld ) ) → 𝑄 ∈ CRing ) |
| 7 | 3 5 6 | mp2an | ⊢ 𝑄 ∈ CRing |
| 8 | isfld | ⊢ ( 𝑄 ∈ Field ↔ ( 𝑄 ∈ DivRing ∧ 𝑄 ∈ CRing ) ) | |
| 9 | 2 7 8 | mpbir2an | ⊢ 𝑄 ∈ Field |