| Step | Hyp | Ref
| Expression |
| 1 | | cnfldbas 21368 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
| 2 | | cndrng 21411 |
. . . . . 6
⊢
ℂfld ∈ DivRing |
| 3 | 2 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℂfld ∈ DivRing) |
| 4 | | qsscn 13002 |
. . . . . 6
⊢ ℚ
⊆ ℂ |
| 5 | 4 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℚ ⊆ ℂ) |
| 6 | | 1z 12647 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
| 7 | | snssi 4808 |
. . . . . . . 8
⊢ (1 ∈
ℤ → {1} ⊆ ℤ) |
| 8 | 6, 7 | ax-mp 5 |
. . . . . . 7
⊢ {1}
⊆ ℤ |
| 9 | | zssq 12998 |
. . . . . . 7
⊢ ℤ
⊆ ℚ |
| 10 | 8, 9 | sstri 3993 |
. . . . . 6
⊢ {1}
⊆ ℚ |
| 11 | 10 | a1i 11 |
. . . . 5
⊢ (⊤
→ {1} ⊆ ℚ) |
| 12 | 1, 3, 5, 11 | fldgenss 33318 |
. . . 4
⊢ (⊤
→ (ℂfld fldGen {1}) ⊆ (ℂfld fldGen
ℚ)) |
| 13 | | qsubdrg 21437 |
. . . . . . . 8
⊢ (ℚ
∈ (SubRing‘ℂfld) ∧ (ℂfld
↾s ℚ) ∈ DivRing) |
| 14 | 13 | simpli 483 |
. . . . . . 7
⊢ ℚ
∈ (SubRing‘ℂfld) |
| 15 | 13 | simpri 485 |
. . . . . . 7
⊢
(ℂfld ↾s ℚ) ∈
DivRing |
| 16 | | issdrg 20789 |
. . . . . . 7
⊢ (ℚ
∈ (SubDRing‘ℂfld) ↔ (ℂfld
∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld) ∧
(ℂfld ↾s ℚ) ∈
DivRing)) |
| 17 | 2, 14, 15, 16 | mpbir3an 1342 |
. . . . . 6
⊢ ℚ
∈ (SubDRing‘ℂfld) |
| 18 | 17 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℚ ∈ (SubDRing‘ℂfld)) |
| 19 | 1, 3, 18 | fldgenidfld 33319 |
. . . 4
⊢ (⊤
→ (ℂfld fldGen ℚ) = ℚ) |
| 20 | 12, 19 | sseqtrd 4020 |
. . 3
⊢ (⊤
→ (ℂfld fldGen {1}) ⊆ ℚ) |
| 21 | | elq 12992 |
. . . . . 6
⊢ (𝑧 ∈ ℚ ↔
∃𝑝 ∈ ℤ
∃𝑞 ∈ ℕ
𝑧 = (𝑝 / 𝑞)) |
| 22 | | cnflddiv 21413 |
. . . . . . . . 9
⊢ / =
(/r‘ℂfld) |
| 23 | | cnfld0 21405 |
. . . . . . . . 9
⊢ 0 =
(0g‘ℂfld) |
| 24 | 11, 4 | sstrdi 3996 |
. . . . . . . . . . . 12
⊢ (⊤
→ {1} ⊆ ℂ) |
| 25 | 1, 3, 24 | fldgensdrg 33316 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂfld fldGen {1}) ∈
(SubDRing‘ℂfld)) |
| 26 | 25 | mptru 1547 |
. . . . . . . . . 10
⊢
(ℂfld fldGen {1}) ∈
(SubDRing‘ℂfld) |
| 27 | 26 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) →
(ℂfld fldGen {1}) ∈
(SubDRing‘ℂfld)) |
| 28 | | ax-1cn 11213 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
| 29 | | cnfldmulg 21416 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℤ ∧ 1 ∈
ℂ) → (𝑝(.g‘ℂfld)1)
= (𝑝 ·
1)) |
| 30 | 28, 29 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℤ → (𝑝(.g‘ℂfld)1)
= (𝑝 ·
1)) |
| 31 | | zre 12617 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℤ → 𝑝 ∈
ℝ) |
| 32 | | ax-1rid 11225 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℝ → (𝑝 · 1) = 𝑝) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℤ → (𝑝 · 1) = 𝑝) |
| 34 | 30, 33 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℤ → (𝑝(.g‘ℂfld)1)
= 𝑝) |
| 35 | | issdrg 20789 |
. . . . . . . . . . . . . . 15
⊢
((ℂfld fldGen {1}) ∈
(SubDRing‘ℂfld) ↔ (ℂfld ∈
DivRing ∧ (ℂfld fldGen {1}) ∈
(SubRing‘ℂfld) ∧ (ℂfld
↾s (ℂfld fldGen {1})) ∈
DivRing)) |
| 36 | 26, 35 | mpbi 230 |
. . . . . . . . . . . . . 14
⊢
(ℂfld ∈ DivRing ∧ (ℂfld
fldGen {1}) ∈ (SubRing‘ℂfld) ∧
(ℂfld ↾s (ℂfld fldGen {1}))
∈ DivRing) |
| 37 | 36 | simp2i 1141 |
. . . . . . . . . . . . 13
⊢
(ℂfld fldGen {1}) ∈
(SubRing‘ℂfld) |
| 38 | | subrgsubg 20577 |
. . . . . . . . . . . . 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 33315 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ {1} ⊆ (ℂfld fldGen {1})) |
| 41 | | 1ex 11257 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
| 42 | 41 | snss 4785 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
(ℂfld fldGen {1}) ↔ {1} ⊆ (ℂfld
fldGen {1})) |
| 43 | 40, 42 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 1 ∈ (ℂfld fldGen {1})) |
| 44 | 43 | mptru 1547 |
. . . . . . . . . . . 12
⊢ 1 ∈
(ℂfld fldGen {1}) |
| 45 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(.g‘ℂfld) =
(.g‘ℂfld) |
| 46 | 45 | subgmulgcl 19157 |
. . . . . . . . . . . 12
⊢
(((ℂfld fldGen {1}) ∈
(SubGrp‘ℂfld) ∧ 𝑝 ∈ ℤ ∧ 1 ∈
(ℂfld fldGen {1})) → (𝑝(.g‘ℂfld)1)
∈ (ℂfld fldGen {1})) |
| 47 | 39, 44, 46 | mp3an13 1454 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℤ → (𝑝(.g‘ℂfld)1)
∈ (ℂfld fldGen {1})) |
| 48 | 34, 47 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℤ → 𝑝 ∈ (ℂfld
fldGen {1})) |
| 49 | 48 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → 𝑝 ∈ (ℂfld
fldGen {1})) |
| 50 | 48 | ssriv 3987 |
. . . . . . . . . 10
⊢ ℤ
⊆ (ℂfld fldGen {1}) |
| 51 | | nnz 12634 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ ℕ → 𝑞 ∈
ℤ) |
| 52 | 51 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → 𝑞 ∈
ℤ) |
| 53 | 50, 52 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → 𝑞 ∈ (ℂfld
fldGen {1})) |
| 54 | | nnne0 12300 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℕ → 𝑞 ≠ 0) |
| 55 | 54 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → 𝑞 ≠ 0) |
| 56 | 22, 23, 27, 49, 53, 55 | sdrgdvcl 33301 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ (ℂfld fldGen
{1})) |
| 57 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑧 = (𝑝 / 𝑞) → (𝑧 ∈ (ℂfld fldGen {1})
↔ (𝑝 / 𝑞) ∈ (ℂfld
fldGen {1}))) |
| 58 | 56, 57 | syl5ibrcom 247 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑧 = (𝑝 / 𝑞) → 𝑧 ∈ (ℂfld fldGen
{1}))) |
| 59 | 58 | rexlimivv 3201 |
. . . . . 6
⊢
(∃𝑝 ∈
ℤ ∃𝑞 ∈
ℕ 𝑧 = (𝑝 / 𝑞) → 𝑧 ∈ (ℂfld fldGen
{1})) |
| 60 | 21, 59 | sylbi 217 |
. . . . 5
⊢ (𝑧 ∈ ℚ → 𝑧 ∈ (ℂfld
fldGen {1})) |
| 61 | 60 | ssriv 3987 |
. . . 4
⊢ ℚ
⊆ (ℂfld fldGen {1}) |
| 62 | 61 | a1i 11 |
. . 3
⊢ (⊤
→ ℚ ⊆ (ℂfld fldGen {1})) |
| 63 | 20, 62 | eqssd 4001 |
. 2
⊢ (⊤
→ (ℂfld fldGen {1}) = ℚ) |
| 64 | 63 | mptru 1547 |
1
⊢
(ℂfld fldGen {1}) = ℚ |