Metamath Proof Explorer

Theorem 1fldgenq

Description: The field of rational numbers QQ is generated by 1 in CCfld , that is, QQ is the prime field of CCfld . (Contributed by Thierry Arnoux, 15-Jan-2025)

Ref Expression
Assertion 1fldgenq ⊢ ℂ fld fldGen 1 = ℚ

Proof

Step Hyp Ref Expression
1 cnfldbas ⊢ ℂ = Base ℂ fld
2 cndrng ⊢ ℂ fld ∈ DivRing
3 2 a1i ⊢ ⊤ → ℂ fld ∈ DivRing
4 qsscn ⊢ ℚ ⊆ ℂ
5 4 a1i ⊢ ⊤ → ℚ ⊆ ℂ
6 1z ⊢ 1 ∈ ℤ
7 snssi ⊢ 1 ∈ ℤ → 1 ⊆ ℤ
8 6 7 ax-mp ⊢ 1 ⊆ ℤ
9 zssq ⊢ ℤ ⊆ ℚ
10 8 9 sstri ⊢ 1 ⊆ ℚ
11 10 a1i ⊢ ⊤ → 1 ⊆ ℚ
12 1 3 5 11 fldgenss ⊢ ⊤ → ℂ fld fldGen 1 ⊆ ℂ fld fldGen ℚ
13 qsubdrg ⊢ ℚ ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 ℚ ∈ DivRing
14 13 simpli ⊢ ℚ ∈ SubRing ⁡ ℂ fld
15 13 simpri ⊢ ℂ fld ↾ 𝑠 ℚ ∈ DivRing
16 issdrg ⊢ ℚ ∈ SubDRing ⁡ ℂ fld ↔ ℂ fld ∈ DivRing ∧ ℚ ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 ℚ ∈ DivRing
17 2 14 15 16 mpbir3an ⊢ ℚ ∈ SubDRing ⁡ ℂ fld
18 17 a1i ⊢ ⊤ → ℚ ∈ SubDRing ⁡ ℂ fld
19 1 3 18 fldgenidfld ⊢ ⊤ → ℂ fld fldGen ℚ = ℚ
20 12 19 sseqtrd ⊢ ⊤ → ℂ fld fldGen 1 ⊆ ℚ
21 elq ⊢ z ∈ ℚ ↔ ∃ p ∈ ℤ ∃ q ∈ ℕ z = p q
22 cnflddiv ⊢ ÷ = / r ⁡ ℂ fld
23 cnfld0 ⊢ 0 = 0 ℂ fld
24 11 4 sstrdi ⊢ ⊤ → 1 ⊆ ℂ
25 1 3 24 fldgensdrg ⊢ ⊤ → ℂ fld fldGen 1 ∈ SubDRing ⁡ ℂ fld
26 25 mptru ⊢ ℂ fld fldGen 1 ∈ SubDRing ⁡ ℂ fld
27 26 a1i ⊢ p ∈ ℤ ∧ q ∈ ℕ → ℂ fld fldGen 1 ∈ SubDRing ⁡ ℂ fld
28 ax-1cn ⊢ 1 ∈ ℂ
29 cnfldmulg ⊢ p ∈ ℤ ∧ 1 ∈ ℂ → p ⋅ ℂ fld 1 = p ⋅ 1
30 28 29 mpan2 ⊢ p ∈ ℤ → p ⋅ ℂ fld 1 = p ⋅ 1
31 zre ⊢ p ∈ ℤ → p ∈ ℝ
32 ax-1rid ⊢ p ∈ ℝ → p ⋅ 1 = p
33 31 32 syl ⊢ p ∈ ℤ → p ⋅ 1 = p
34 30 33 eqtrd ⊢ p ∈ ℤ → p ⋅ ℂ fld 1 = p
35 issdrg ⊢ ℂ fld fldGen 1 ∈ SubDRing ⁡ ℂ fld ↔ ℂ fld ∈ DivRing ∧ ℂ fld fldGen 1 ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 ℂ fld fldGen 1 ∈ DivRing
36 26 35 mpbi ⊢ ℂ fld ∈ DivRing ∧ ℂ fld fldGen 1 ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 ℂ fld fldGen 1 ∈ DivRing
37 36 simp2i ⊢ ℂ fld fldGen 1 ∈ SubRing ⁡ ℂ fld
38 subrgsubg ⊢ ℂ fld fldGen 1 ∈ SubRing ⁡ ℂ fld → ℂ fld fldGen 1 ∈ SubGrp ⁡ ℂ fld
39 37 38 ax-mp ⊢ ℂ fld fldGen 1 ∈ SubGrp ⁡ ℂ fld
40 1 3 24 fldgenssid ⊢ ⊤ → 1 ⊆ ℂ fld fldGen 1
41 1ex ⊢ 1 ∈ V
42 41 snss ⊢ 1 ∈ ℂ fld fldGen 1 ↔ 1 ⊆ ℂ fld fldGen 1
43 40 42 sylibr ⊢ ⊤ → 1 ∈ ℂ fld fldGen 1
44 43 mptru ⊢ 1 ∈ ℂ fld fldGen 1
45 eqid ⊢ ⋅ ℂ fld = ⋅ ℂ fld
46 45 subgmulgcl ⊢ ℂ fld fldGen 1 ∈ SubGrp ⁡ ℂ fld ∧ p ∈ ℤ ∧ 1 ∈ ℂ fld fldGen 1 → p ⋅ ℂ fld 1 ∈ ℂ fld fldGen 1
47 39 44 46 mp3an13 ⊢ p ∈ ℤ → p ⋅ ℂ fld 1 ∈ ℂ fld fldGen 1
48 34 47 eqeltrrd ⊢ p ∈ ℤ → p ∈ ℂ fld fldGen 1
49 48 adantr ⊢ p ∈ ℤ ∧ q ∈ ℕ → p ∈ ℂ fld fldGen 1
50 48 ssriv ⊢ ℤ ⊆ ℂ fld fldGen 1
51 nnz ⊢ q ∈ ℕ → q ∈ ℤ
52 51 adantl ⊢ p ∈ ℤ ∧ q ∈ ℕ → q ∈ ℤ
53 50 52 sselid ⊢ p ∈ ℤ ∧ q ∈ ℕ → q ∈ ℂ fld fldGen 1
54 nnne0 ⊢ q ∈ ℕ → q ≠ 0
55 54 adantl ⊢ p ∈ ℤ ∧ q ∈ ℕ → q ≠ 0
56 22 23 27 49 53 55 sdrgdvcl ⊢ p ∈ ℤ ∧ q ∈ ℕ → p q ∈ ℂ fld fldGen 1
57 eleq1 ⊢ z = p q → z ∈ ℂ fld fldGen 1 ↔ p q ∈ ℂ fld fldGen 1
58 56 57 syl5ibrcom ⊢ p ∈ ℤ ∧ q ∈ ℕ → z = p q → z ∈ ℂ fld fldGen 1
59 58 rexlimivv ⊢ ∃ p ∈ ℤ ∃ q ∈ ℕ z = p q → z ∈ ℂ fld fldGen 1
60 21 59 sylbi ⊢ z ∈ ℚ → z ∈ ℂ fld fldGen 1
61 60 ssriv ⊢ ℚ ⊆ ℂ fld fldGen 1
62 61 a1i ⊢ ⊤ → ℚ ⊆ ℂ fld fldGen 1
63 20 62 eqssd ⊢ ⊤ → ℂ fld fldGen 1 = ℚ
64 63 mptru ⊢ ℂ fld fldGen 1 = ℚ