Theorem znfi

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

	Ref	Expression
Hypotheses	zntos.y	|- Y = ( Z/nZ ` N )
	znhash.1	|- B = ( Base ` Y )
Assertion	znfi	|- ( N e. NN -> B e. Fin )

Proof

Step	Hyp	Ref	Expression
1		zntos.y	|- Y = ( Z/nZ ` N )
2		znhash.1	|- B = ( Base ` Y )
3	1 2	znhash	|- ( N e. NN -> ( # ` B ) = N )
4		nnnn0	|- ( N e. NN -> N e. NN0 )
5	3 4	eqeltrd	|- ( N e. NN -> ( # ` B ) e. NN0 )
6	2	fvexi	|- B e. _V
7		hashclb	|- ( B e. _V -> ( B e. Fin <-> ( # ` B ) e. NN0 ) )
8	6 7	ax-mp	|- ( B e. Fin <-> ( # ` B ) e. NN0 )
9	5 8	sylibr	|- ( N e. NN -> B e. Fin )