Metamath Proof Explorer

Theorem qsssubdrg

Description: The rational numbers are a subset of any subfield of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion qsssubdrg ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing → ℚ ⊆ R

Proof

Step Hyp Ref Expression
1 elq ⊢ z ∈ ℚ ↔ ∃ x ∈ ℤ ∃ y ∈ ℕ z = x y
2 drngring ⊢ ℂ fld ↾ 𝑠 R ∈ DivRing → ℂ fld ↾ 𝑠 R ∈ Ring
3 2 ad2antlr ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → ℂ fld ↾ 𝑠 R ∈ Ring
4 zsssubrg ⊢ R ∈ SubRing ⁡ ℂ fld → ℤ ⊆ R
5 4 ad2antrr ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → ℤ ⊆ R
6 eqid ⊢ ℂ fld ↾ 𝑠 R = ℂ fld ↾ 𝑠 R
7 6 subrgbas ⊢ R ∈ SubRing ⁡ ℂ fld → R = Base ℂ fld ↾ 𝑠 R
8 7 ad2antrr ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → R = Base ℂ fld ↾ 𝑠 R
9 5 8 sseqtrd ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → ℤ ⊆ Base ℂ fld ↾ 𝑠 R
10 simprl ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → x ∈ ℤ
11 9 10 sseldd ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → x ∈ Base ℂ fld ↾ 𝑠 R
12 nnz ⊢ y ∈ ℕ → y ∈ ℤ
13 12 ad2antll ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → y ∈ ℤ
14 9 13 sseldd ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → y ∈ Base ℂ fld ↾ 𝑠 R
15 nnne0 ⊢ y ∈ ℕ → y ≠ 0
16 15 ad2antll ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → y ≠ 0
17 cnfld0 ⊢ 0 = 0 ℂ fld
18 6 17 subrg0 ⊢ R ∈ SubRing ⁡ ℂ fld → 0 = 0 ℂ fld ↾ 𝑠 R
19 18 ad2antrr ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → 0 = 0 ℂ fld ↾ 𝑠 R
20 16 19 neeqtrd ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → y ≠ 0 ℂ fld ↾ 𝑠 R
21 eqid ⊢ Base ℂ fld ↾ 𝑠 R = Base ℂ fld ↾ 𝑠 R
22 eqid ⊢ Unit ⁡ ℂ fld ↾ 𝑠 R = Unit ⁡ ℂ fld ↾ 𝑠 R
23 eqid ⊢ 0 ℂ fld ↾ 𝑠 R = 0 ℂ fld ↾ 𝑠 R
24 21 22 23 drngunit ⊢ ℂ fld ↾ 𝑠 R ∈ DivRing → y ∈ Unit ⁡ ℂ fld ↾ 𝑠 R ↔ y ∈ Base ℂ fld ↾ 𝑠 R ∧ y ≠ 0 ℂ fld ↾ 𝑠 R
25 24 ad2antlr ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → y ∈ Unit ⁡ ℂ fld ↾ 𝑠 R ↔ y ∈ Base ℂ fld ↾ 𝑠 R ∧ y ≠ 0 ℂ fld ↾ 𝑠 R
26 14 20 25 mpbir2and ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → y ∈ Unit ⁡ ℂ fld ↾ 𝑠 R
27 eqid ⊢ / r ⁡ ℂ fld ↾ 𝑠 R = / r ⁡ ℂ fld ↾ 𝑠 R
28 21 22 27 dvrcl ⊢ ℂ fld ↾ 𝑠 R ∈ Ring ∧ x ∈ Base ℂ fld ↾ 𝑠 R ∧ y ∈ Unit ⁡ ℂ fld ↾ 𝑠 R → x / r ⁡ ℂ fld ↾ 𝑠 R y ∈ Base ℂ fld ↾ 𝑠 R
29 3 11 26 28 syl3anc ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → x / r ⁡ ℂ fld ↾ 𝑠 R y ∈ Base ℂ fld ↾ 𝑠 R
30 simpll ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → R ∈ SubRing ⁡ ℂ fld
31 5 10 sseldd ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → x ∈ R
32 cnflddiv ⊢ ÷ = / r ⁡ ℂ fld
33 6 32 22 27 subrgdv ⊢ R ∈ SubRing ⁡ ℂ fld ∧ x ∈ R ∧ y ∈ Unit ⁡ ℂ fld ↾ 𝑠 R → x y = x / r ⁡ ℂ fld ↾ 𝑠 R y
34 30 31 26 33 syl3anc ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → x y = x / r ⁡ ℂ fld ↾ 𝑠 R y
35 29 34 8 3eltr4d ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → x y ∈ R
36 eleq1 ⊢ z = x y → z ∈ R ↔ x y ∈ R
37 35 36 syl5ibrcom ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing ∧ x ∈ ℤ ∧ y ∈ ℕ → z = x y → z ∈ R
38 37 rexlimdvva ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing → ∃ x ∈ ℤ ∃ y ∈ ℕ z = x y → z ∈ R
39 1 38 syl5bi ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing → z ∈ ℚ → z ∈ R
40 39 ssrdv ⊢ R ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 R ∈ DivRing → ℚ ⊆ R