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	⊢ ( .g ‘ ℤring ) = ( .g ‘ ℤring )
3		zsubrg	⊢ ℤ ∈ ( SubRing ‘ ℂfld )
4		subrgsubg	⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubGrp ‘ ℂfld ) )
5	3 4	ax-mp	⊢ ℤ ∈ ( SubGrp ‘ ℂfld )
6		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
7	6	subggrp	⊢ ( ℤ ∈ ( SubGrp ‘ ℂfld ) → ℤring ∈ Grp )
8	5 7	mp1i	⊢ ( ⊤ → ℤring ∈ Grp )
9		1zzd	⊢ ( ⊤ → 1 ∈ ℤ )
10		ax-1cn	⊢ 1 ∈ ℂ
11		cnfldmulg	⊢ ( ( 𝑥 ∈ ℤ ∧ 1 ∈ ℂ ) → ( 𝑥 ( .g ‘ ℂfld ) 1 ) = ( 𝑥 · 1 ) )
12	10 11	mpan2	⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ( .g ‘ ℂfld ) 1 ) = ( 𝑥 · 1 ) )
13		1z	⊢ 1 ∈ ℤ
14		eqid	⊢ ( .g ‘ ℂfld ) = ( .g ‘ ℂfld )
15	14 6 2	subgmulg	⊢ ( ( ℤ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑥 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑥 ( .g ‘ ℂfld ) 1 ) = ( 𝑥 ( .g ‘ ℤring ) 1 ) )
16	5 13 15	mp3an13	⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ( .g ‘ ℂfld ) 1 ) = ( 𝑥 ( .g ‘ ℤring ) 1 ) )
17		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
18	17	mulid1d	⊢ ( 𝑥 ∈ ℤ → ( 𝑥 · 1 ) = 𝑥 )
19	12 16 18	3eqtr3rd	⊢ ( 𝑥 ∈ ℤ → 𝑥 = ( 𝑥 ( .g ‘ ℤring ) 1 ) )
20		oveq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ( .g ‘ ℤring ) 1 ) = ( 𝑥 ( .g ‘ ℤring ) 1 ) )
21	20	rspceeqv	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑥 = ( 𝑥 ( .g ‘ ℤring ) 1 ) ) → ∃ 𝑧 ∈ ℤ 𝑥 = ( 𝑧 ( .g ‘ ℤring ) 1 ) )
22	19 21	mpdan	⊢ ( 𝑥 ∈ ℤ → ∃ 𝑧 ∈ ℤ 𝑥 = ( 𝑧 ( .g ‘ ℤring ) 1 ) )
23	22	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℤ ) → ∃ 𝑧 ∈ ℤ 𝑥 = ( 𝑧 ( .g ‘ ℤring ) 1 ) )
24	1 2 8 9 23	iscygd	⊢ ( ⊤ → ℤring ∈ CycGrp )
25	24	mptru	⊢ ℤring ∈ CycGrp