Theorem aks6d1c2p1

Description: In the AKS-theorem the subset defined by E takes values in the positive integers. (Contributed by metakunt, 7-Jan-2025)

	Ref	Expression
Hypotheses	aks6d1c2p1.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	aks6d1c2p1.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	aks6d1c2p1.3	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
	aks6d1c2p1.4	⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
Assertion	aks6d1c2p1	⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ )

Proof

Step	Hyp	Ref	Expression
1		aks6d1c2p1.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		aks6d1c2p1.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3		aks6d1c2p1.3	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
4		aks6d1c2p1.4	⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
5		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
6	2 5	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
7	6	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ℕ0 × ℕ0 ) ) → 𝑃 ∈ ℕ )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ℕ0 × ℕ0 ) ) → 𝑎 ∈ ( ℕ0 × ℕ0 ) )
9		xp1st	⊢ ( 𝑎 ∈ ( ℕ0 × ℕ0 ) → ( 1st ‘ 𝑎 ) ∈ ℕ0 )
10	8 9	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ℕ0 × ℕ0 ) ) → ( 1st ‘ 𝑎 ) ∈ ℕ0 )
11	7 10	nnexpcld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑃 ↑ ( 1st ‘ 𝑎 ) ) ∈ ℕ )
12	1 6	jca	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℕ ) )
13		nndivdvds	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℕ ) → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℕ ) )
14	12 13	syl	⊢ ( 𝜑 → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℕ ) )
15	3 14	mpbid	⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∈ ℕ )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑁 / 𝑃 ) ∈ ℕ )
17		xp2nd	⊢ ( 𝑎 ∈ ( ℕ0 × ℕ0 ) → ( 2nd ‘ 𝑎 ) ∈ ℕ0 )
18	8 17	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ℕ0 × ℕ0 ) ) → ( 2nd ‘ 𝑎 ) ∈ ℕ0 )
19	16 18	nnexpcld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑎 ) ) ∈ ℕ )
20	11 19	nnmulcld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑎 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑎 ) ) ) ∈ ℕ )
21		vex	⊢ 𝑘 ∈ V
22		vex	⊢ 𝑙 ∈ V
23	21 22	op1std	⊢ ( 𝑎 = ⟨ 𝑘 , 𝑙 ⟩ → ( 1st ‘ 𝑎 ) = 𝑘 )
24	23	oveq2d	⊢ ( 𝑎 = ⟨ 𝑘 , 𝑙 ⟩ → ( 𝑃 ↑ ( 1st ‘ 𝑎 ) ) = ( 𝑃 ↑ 𝑘 ) )
25	21 22	op2ndd	⊢ ( 𝑎 = ⟨ 𝑘 , 𝑙 ⟩ → ( 2nd ‘ 𝑎 ) = 𝑙 )
26	25	oveq2d	⊢ ( 𝑎 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑎 ) ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) )
27	24 26	oveq12d	⊢ ( 𝑎 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑃 ↑ ( 1st ‘ 𝑎 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑎 ) ) ) = ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
28	27	mpompt	⊢ ( 𝑎 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑎 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑎 ) ) ) ) = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
29	28	eqcomi	⊢ ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) = ( 𝑎 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑎 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑎 ) ) ) )
30	4 29	eqtri	⊢ 𝐸 = ( 𝑎 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑎 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑎 ) ) ) )
31	20 30	fmptd	⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ )