Theorem znfi

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

	Ref	Expression
Hypotheses	zntos.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	znhash.1	⊢ 𝐵 = ( Base ‘ 𝑌 )
Assertion	znfi	⊢ ( 𝑁 ∈ ℕ → 𝐵 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		zntos.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2		znhash.1	⊢ 𝐵 = ( Base ‘ 𝑌 )
3	1 2	znhash	⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝐵 ) = 𝑁 )
4		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
5	3 4	eqeltrd	⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
6	2	fvexi	⊢ 𝐵 ∈ V
7		hashclb	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) )
8	6 7	ax-mp	⊢ ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
9	5 8	sylibr	⊢ ( 𝑁 ∈ ℕ → 𝐵 ∈ Fin )