Step | Hyp | Ref
| Expression |
1 | | cnfldbas 20800 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
2 | | cndrng 20826 |
. . . . . 6
⊢
ℂfld ∈ DivRing |
3 | 2 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℂfld ∈ DivRing) |
4 | | qsscn 12885 |
. . . . . 6
⊢ ℚ
⊆ ℂ |
5 | 4 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℚ ⊆ ℂ) |
6 | | 1z 12533 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
7 | | snssi 4768 |
. . . . . . . 8
⊢ (1 ∈
ℤ → {1} ⊆ ℤ) |
8 | 6, 7 | ax-mp 5 |
. . . . . . 7
⊢ {1}
⊆ ℤ |
9 | | zssq 12881 |
. . . . . . 7
⊢ ℤ
⊆ ℚ |
10 | 8, 9 | sstri 3953 |
. . . . . 6
⊢ {1}
⊆ ℚ |
11 | 10 | a1i 11 |
. . . . 5
⊢ (⊤
→ {1} ⊆ ℚ) |
12 | 1, 3, 5, 11 | fldgenss 32084 |
. . . 4
⊢ (⊤
→ (ℂfld fldGen {1}) ⊆ (ℂfld fldGen
ℚ)) |
13 | | qsubdrg 20849 |
. . . . . . . 8
⊢ (ℚ
∈ (SubRing‘ℂfld) ∧ (ℂfld
↾s ℚ) ∈ DivRing) |
14 | 13 | simpli 484 |
. . . . . . 7
⊢ ℚ
∈ (SubRing‘ℂfld) |
15 | 13 | simpri 486 |
. . . . . . 7
⊢
(ℂfld ↾s ℚ) ∈
DivRing |
16 | | issdrg 20261 |
. . . . . . 7
⊢ (ℚ
∈ (SubDRing‘ℂfld) ↔ (ℂfld
∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld) ∧
(ℂfld ↾s ℚ) ∈
DivRing)) |
17 | 2, 14, 15, 16 | mpbir3an 1341 |
. . . . . 6
⊢ ℚ
∈ (SubDRing‘ℂfld) |
18 | 17 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℚ ∈ (SubDRing‘ℂfld)) |
19 | 1, 3, 18 | fldgenidfld 32085 |
. . . 4
⊢ (⊤
→ (ℂfld fldGen ℚ) = ℚ) |
20 | 12, 19 | sseqtrd 3984 |
. . 3
⊢ (⊤
→ (ℂfld fldGen {1}) ⊆ ℚ) |
21 | | elq 12875 |
. . . . . 6
⊢ (𝑧 ∈ ℚ ↔
∃𝑝 ∈ ℤ
∃𝑞 ∈ ℕ
𝑧 = (𝑝 / 𝑞)) |
22 | | cnflddiv 20827 |
. . . . . . . . 9
⊢ / =
(/r‘ℂfld) |
23 | | cnfld0 20821 |
. . . . . . . . 9
⊢ 0 =
(0g‘ℂfld) |
24 | 11, 4 | sstrdi 3956 |
. . . . . . . . . . . 12
⊢ (⊤
→ {1} ⊆ ℂ) |
25 | 1, 3, 24 | fldgensdrg 32083 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂfld fldGen {1}) ∈
(SubDRing‘ℂfld)) |
26 | 25 | mptru 1548 |
. . . . . . . . . 10
⊢
(ℂfld fldGen {1}) ∈
(SubDRing‘ℂfld) |
27 | 26 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) →
(ℂfld fldGen {1}) ∈
(SubDRing‘ℂfld)) |
28 | | ax-1cn 11109 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
29 | | cnfldmulg 20829 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℤ ∧ 1 ∈
ℂ) → (𝑝(.g‘ℂfld)1)
= (𝑝 ·
1)) |
30 | 28, 29 | mpan2 689 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℤ → (𝑝(.g‘ℂfld)1)
= (𝑝 ·
1)) |
31 | | zre 12503 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℤ → 𝑝 ∈
ℝ) |
32 | | ax-1rid 11121 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℝ → (𝑝 · 1) = 𝑝) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℤ → (𝑝 · 1) = 𝑝) |
34 | 30, 33 | eqtrd 2776 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℤ → (𝑝(.g‘ℂfld)1)
= 𝑝) |
35 | | issdrg 20261 |
. . . . . . . . . . . . . . 15
⊢
((ℂfld fldGen {1}) ∈
(SubDRing‘ℂfld) ↔ (ℂfld ∈
DivRing ∧ (ℂfld fldGen {1}) ∈
(SubRing‘ℂfld) ∧ (ℂfld
↾s (ℂfld fldGen {1})) ∈
DivRing)) |
36 | 26, 35 | mpbi 229 |
. . . . . . . . . . . . . 14
⊢
(ℂfld ∈ DivRing ∧ (ℂfld
fldGen {1}) ∈ (SubRing‘ℂfld) ∧
(ℂfld ↾s (ℂfld fldGen {1}))
∈ DivRing) |
37 | 36 | simp2i 1140 |
. . . . . . . . . . . . 13
⊢
(ℂfld fldGen {1}) ∈
(SubRing‘ℂfld) |
38 | | subrgsubg 20228 |
. . . . . . . . . . . . 13
⊢
((ℂfld fldGen {1}) ∈
(SubRing‘ℂfld) → (ℂfld fldGen {1})
∈ (SubGrp‘ℂfld)) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(ℂfld fldGen {1}) ∈
(SubGrp‘ℂfld) |
40 | 1, 3, 24 | fldgenssid 32082 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ {1} ⊆ (ℂfld fldGen {1})) |
41 | | 1ex 11151 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
42 | 41 | snss 4746 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
(ℂfld fldGen {1}) ↔ {1} ⊆ (ℂfld
fldGen {1})) |
43 | 40, 42 | sylibr 233 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 1 ∈ (ℂfld fldGen {1})) |
44 | 43 | mptru 1548 |
. . . . . . . . . . . 12
⊢ 1 ∈
(ℂfld fldGen {1}) |
45 | | eqid 2736 |
. . . . . . . . . . . . 13
⊢
(.g‘ℂfld) =
(.g‘ℂfld) |
46 | 45 | subgmulgcl 18941 |
. . . . . . . . . . . 12
⊢
(((ℂfld fldGen {1}) ∈
(SubGrp‘ℂfld) ∧ 𝑝 ∈ ℤ ∧ 1 ∈
(ℂfld fldGen {1})) → (𝑝(.g‘ℂfld)1)
∈ (ℂfld fldGen {1})) |
47 | 39, 44, 46 | mp3an13 1452 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℤ → (𝑝(.g‘ℂfld)1)
∈ (ℂfld fldGen {1})) |
48 | 34, 47 | eqeltrrd 2839 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℤ → 𝑝 ∈ (ℂfld
fldGen {1})) |
49 | 48 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → 𝑝 ∈ (ℂfld
fldGen {1})) |
50 | 48 | ssriv 3948 |
. . . . . . . . . 10
⊢ ℤ
⊆ (ℂfld fldGen {1}) |
51 | | nnz 12520 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ ℕ → 𝑞 ∈
ℤ) |
52 | 51 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → 𝑞 ∈
ℤ) |
53 | 50, 52 | sselid 3942 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → 𝑞 ∈ (ℂfld
fldGen {1})) |
54 | | nnne0 12187 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℕ → 𝑞 ≠ 0) |
55 | 54 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → 𝑞 ≠ 0) |
56 | 22, 23, 27, 49, 53, 55 | sdrgdvcl 32076 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ (ℂfld fldGen
{1})) |
57 | | eleq1 2825 |
. . . . . . . 8
⊢ (𝑧 = (𝑝 / 𝑞) → (𝑧 ∈ (ℂfld fldGen {1})
↔ (𝑝 / 𝑞) ∈ (ℂfld
fldGen {1}))) |
58 | 56, 57 | syl5ibrcom 246 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑧 = (𝑝 / 𝑞) → 𝑧 ∈ (ℂfld fldGen
{1}))) |
59 | 58 | rexlimivv 3196 |
. . . . . 6
⊢
(∃𝑝 ∈
ℤ ∃𝑞 ∈
ℕ 𝑧 = (𝑝 / 𝑞) → 𝑧 ∈ (ℂfld fldGen
{1})) |
60 | 21, 59 | sylbi 216 |
. . . . 5
⊢ (𝑧 ∈ ℚ → 𝑧 ∈ (ℂfld
fldGen {1})) |
61 | 60 | ssriv 3948 |
. . . 4
⊢ ℚ
⊆ (ℂfld fldGen {1}) |
62 | 61 | a1i 11 |
. . 3
⊢ (⊤
→ ℚ ⊆ (ℂfld fldGen {1})) |
63 | 20, 62 | eqssd 3961 |
. 2
⊢ (⊤
→ (ℂfld fldGen {1}) = ℚ) |
64 | 63 | mptru 1548 |
1
⊢
(ℂfld fldGen {1}) = ℚ |