Metamath Proof Explorer

Theorem zringcyg

Description: The integers are a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 9-Jun-2019)

Ref Expression
Assertion zringcyg ⊢ ℤ ring ∈ CycGrp

Proof

Step Hyp Ref Expression
1 zringbas ⊢ ℤ = Base ℤ ring
2 eqid ⊢ ⋅ ℤ ring = ⋅ ℤ ring
3 zsubrg ⊢ ℤ ∈ SubRing ⁡ ℂ fld
4 subrgsubg ⊢ ℤ ∈ SubRing ⁡ ℂ fld → ℤ ∈ SubGrp ⁡ ℂ fld
5 3 4 ax-mp ⊢ ℤ ∈ SubGrp ⁡ ℂ fld
6 df-zring ⊢ ℤ ring = ℂ fld ↾ 𝑠 ℤ
7 6 subggrp ⊢ ℤ ∈ SubGrp ⁡ ℂ fld → ℤ ring ∈ Grp
8 5 7 mp1i ⊢ ⊤ → ℤ ring ∈ Grp
9 1zzd ⊢ ⊤ → 1 ∈ ℤ
10 ax-1cn ⊢ 1 ∈ ℂ
11 cnfldmulg ⊢ x ∈ ℤ ∧ 1 ∈ ℂ → x ⋅ ℂ fld 1 = x ⋅ 1
12 10 11 mpan2 ⊢ x ∈ ℤ → x ⋅ ℂ fld 1 = x ⋅ 1
13 1z ⊢ 1 ∈ ℤ
14 eqid ⊢ ⋅ ℂ fld = ⋅ ℂ fld
15 14 6 2 subgmulg ⊢ ℤ ∈ SubGrp ⁡ ℂ fld ∧ x ∈ ℤ ∧ 1 ∈ ℤ → x ⋅ ℂ fld 1 = x ⋅ ℤ ring 1
16 5 13 15 mp3an13 ⊢ x ∈ ℤ → x ⋅ ℂ fld 1 = x ⋅ ℤ ring 1
17 zcn ⊢ x ∈ ℤ → x ∈ ℂ
18 17 mulridd ⊢ x ∈ ℤ → x ⋅ 1 = x
19 12 16 18 3eqtr3rd ⊢ x ∈ ℤ → x = x ⋅ ℤ ring 1
20 oveq1 ⊢ z = x → z ⋅ ℤ ring 1 = x ⋅ ℤ ring 1
21 20 rspceeqv ⊢ x ∈ ℤ ∧ x = x ⋅ ℤ ring 1 → ∃ z ∈ ℤ x = z ⋅ ℤ ring 1
22 19 21 mpdan ⊢ x ∈ ℤ → ∃ z ∈ ℤ x = z ⋅ ℤ ring 1
23 22 adantl ⊢ ⊤ ∧ x ∈ ℤ → ∃ z ∈ ℤ x = z ⋅ ℤ ring 1
24 1 2 8 9 23 iscygd ⊢ ⊤ → ℤ ring ∈ CycGrp
25 24 mptru ⊢ ℤ ring ∈ CycGrp