Theorem hashscontpowcl

Description: Closure of E for https://www3.nd.edu/%7eandyp/notes/AKS.pdf Theorem 6.1. (Contributed by metakunt, 28-Apr-2025)

	Ref	Expression
Hypotheses	hashscontpowcl.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	hashscontpowcl.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	hashscontpowcl.3	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
	hashscontpowcl.4	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	hashscontpowcl.5	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
	hashscontpowcl.6	⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
	hashscontpowcl.7	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
	hashscontpowcl.8	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑅 )
Assertion	hashscontpowcl	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		hashscontpowcl.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		hashscontpowcl.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3		hashscontpowcl.3	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
4		hashscontpowcl.4	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
5		hashscontpowcl.5	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
6		hashscontpowcl.6	⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
7		hashscontpowcl.7	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
8		hashscontpowcl.8	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑅 )
9		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
10	8 9	znfi	⊢ ( 𝑅 ∈ ℕ → ( Base ‘ 𝑌 ) ∈ Fin )
11	4 10	syl	⊢ ( 𝜑 → ( Base ‘ 𝑌 ) ∈ Fin )
12	4	nnnn0d	⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
13	8	zncrng	⊢ ( 𝑅 ∈ ℕ0 → 𝑌 ∈ CRing )
14	12 13	syl	⊢ ( 𝜑 → 𝑌 ∈ CRing )
15		crngring	⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
16	14 15	syl	⊢ ( 𝜑 → 𝑌 ∈ Ring )
17	7	zrhrhm	⊢ ( 𝑌 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
18		zringbas	⊢ ℤ = ( Base ‘ ℤring )
19	18 9	rhmf	⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑌 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
20		fimass	⊢ ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) → ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ⊆ ( Base ‘ 𝑌 ) )
21	16 17 19 20	4syl	⊢ ( 𝜑 → ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ⊆ ( Base ‘ 𝑌 ) )
22	11 21	ssfid	⊢ ( 𝜑 → ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ Fin )
23		hashcl	⊢ ( ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ Fin → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 )
24	22 23	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 )