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} \in CycGrp$

Step	Hyp	Ref	Expression
1		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
2		eqid	$⊢ \cdot_{ℤ_{ring}} = \cdot_{ℤ_{ring}}$
3		zsubrg	$⊢ ℤ \in SubRing (ℂ_{fld})$
4		subrgsubg	$⊢ ℤ \in SubRing (ℂ_{fld}) \to ℤ \in SubGrp (ℂ_{fld})$
5	3 4	ax-mp	$⊢ ℤ \in SubGrp (ℂ_{fld})$
6		df-zring	$⊢ ℤ_{ring} = ℂ_{fld} ↾_{𝑠} ℤ$
7	6	subggrp	$⊢ ℤ \in SubGrp (ℂ_{fld}) \to ℤ_{ring} \in Grp$
8	5 7	mp1i	$⊢ ⊤ \to ℤ_{ring} \in Grp$
9		1zzd	$⊢ ⊤ \to 1 \in ℤ$
10		ax-1cn	$⊢ 1 \in ℂ$
11		cnfldmulg	$⊢ (x \in ℤ \land 1 \in ℂ) \to x \cdot_{ℂ_{fld}} 1 = x \cdot 1$
12	10 11	mpan2	$⊢ x \in ℤ \to x \cdot_{ℂ_{fld}} 1 = x \cdot 1$
13		1z	$⊢ 1 \in ℤ$
14		eqid	$⊢ \cdot_{ℂ_{fld}} = \cdot_{ℂ_{fld}}$
15	14 6 2	subgmulg	$⊢ (ℤ \in SubGrp (ℂ_{fld}) \land x \in ℤ \land 1 \in ℤ) \to x \cdot_{ℂ_{fld}} 1 = x \cdot_{ℤ_{ring}} 1$
16	5 13 15	mp3an13	$⊢ x \in ℤ \to x \cdot_{ℂ_{fld}} 1 = x \cdot_{ℤ_{ring}} 1$
17		zcn	$⊢ x \in ℤ \to x \in ℂ$
18	17	mulridd	$⊢ x \in ℤ \to x \cdot 1 = x$
19	12 16 18	3eqtr3rd	$⊢ x \in ℤ \to x = x \cdot_{ℤ_{ring}} 1$
20		oveq1	$⊢ z = x \to z \cdot_{ℤ_{ring}} 1 = x \cdot_{ℤ_{ring}} 1$
21	20	rspceeqv	$⊢ (x \in ℤ \land x = x \cdot_{ℤ_{ring}} 1) \to \exists z \in ℤ x = z \cdot_{ℤ_{ring}} 1$
22	19 21	mpdan	$⊢ x \in ℤ \to \exists z \in ℤ x = z \cdot_{ℤ_{ring}} 1$
23	22	adantl	$⊢ (⊤ \land x \in ℤ) \to \exists z \in ℤ x = z \cdot_{ℤ_{ring}} 1$
24	1 2 8 9 23	iscygd	$⊢ ⊤ \to ℤ_{ring} \in CycGrp$
25	24	mptru	$⊢ ℤ_{ring} \in CycGrp$

Metamath Proof Explorer