Theorem znfi

Description: The Z/nZ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	zntos.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
	znhash.1	$$⊢B={\mathrm{Base}}_Y$$
Assertion	znfi	$$⊢N\in \mathbb{N}\to B\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		zntos.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
2		znhash.1	$$⊢B={\mathrm{Base}}_Y$$
3	1 2	znhash	$$⊢N\in \mathbb{N}\to \left|B\right|=N$$
4		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
5	3 4	eqeltrd	$$⊢N\in \mathbb{N}\to \left|B\right|\in {\mathbb{N}}_0$$
6	2	fvexi	$$⊢B\in \mathrm{V}$$
7		hashclb	$$⊢B\in \mathrm{V}\to \left(B\in \mathrm{Fin}\leftrightarrow \left|B\right|\in {\mathbb{N}}_0\right)$$
8	6 7	ax-mp	$$⊢B\in \mathrm{Fin}\leftrightarrow \left|B\right|\in {\mathbb{N}}_0$$
9	5 8	sylibr	$$⊢N\in \mathbb{N}\to B\in \mathrm{Fin}$$