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	$$⊢\phi \to N\in \mathbb{N}$$
	aks6d1c2p1.2	$$⊢\phi \to P\in \mathbb{P}$$
	aks6d1c2p1.3	$$⊢\phi \to P\parallel N$$
	aks6d1c2p1.4	$$⊢E=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
Assertion	aks6d1c2p1	$$⊢\phi \to E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶\mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c2p1.1	$$⊢\phi \to N\in \mathbb{N}$$
2		aks6d1c2p1.2	$$⊢\phi \to P\in \mathbb{P}$$
3		aks6d1c2p1.3	$$⊢\phi \to P\parallel N$$
4		aks6d1c2p1.4	$$⊢E=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
5		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
6	2 5	syl	$$⊢\phi \to P\in \mathbb{N}$$
7	6	adantr	$$⊢\left(\phi \wedge a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\right)\to P\in \mathbb{N}$$
8		simpr	$$⊢\left(\phi \wedge a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\right)\to a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
9		xp1st	$$⊢a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to 1^{st}\left(a\right)\in {\mathbb{N}}_0$$
10	8 9	syl	$$⊢\left(\phi \wedge a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\right)\to 1^{st}\left(a\right)\in {\mathbb{N}}_0$$
11	7 10	nnexpcld	$$⊢\left(\phi \wedge a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\right)\to P^{1^{st}\left(a\right)}\in \mathbb{N}$$
12	1 6	jca	$$⊢\phi \to \left(N\in \mathbb{N}\wedge P\in \mathbb{N}\right)$$
13		nndivdvds	$$⊢\left(N\in \mathbb{N}\wedge P\in \mathbb{N}\right)\to \left(P\parallel N\leftrightarrow \frac{N}{P}\in \mathbb{N}\right)$$
14	12 13	syl	$$⊢\phi \to \left(P\parallel N\leftrightarrow \frac{N}{P}\in \mathbb{N}\right)$$
15	3 14	mpbid	$$⊢\phi \to \frac{N}{P}\in \mathbb{N}$$
16	15	adantr	$$⊢\left(\phi \wedge a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\right)\to \frac{N}{P}\in \mathbb{N}$$
17		xp2nd	$$⊢a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to 2^{nd}\left(a\right)\in {\mathbb{N}}_0$$
18	8 17	syl	$$⊢\left(\phi \wedge a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\right)\to 2^{nd}\left(a\right)\in {\mathbb{N}}_0$$
19	16 18	nnexpcld	$$⊢\left(\phi \wedge a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\right)\to {\left(\frac{N}{P}\right)}^{2^{nd}\left(a\right)}\in \mathbb{N}$$
20	11 19	nnmulcld	$$⊢\left(\phi \wedge a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\right)\to P^{1^{st}\left(a\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(a\right)}\in \mathbb{N}$$
21		vex	$$⊢k\in \mathrm{V}$$
22		vex	$$⊢l\in \mathrm{V}$$
23	21 22	op1std	$$⊢a=⟨k,l⟩\to 1^{st}\left(a\right)=k$$
24	23	oveq2d	$$⊢a=⟨k,l⟩\to P^{1^{st}\left(a\right)}=P^k$$
25	21 22	op2ndd	$$⊢a=⟨k,l⟩\to 2^{nd}\left(a\right)=l$$
26	25	oveq2d	$$⊢a=⟨k,l⟩\to {\left(\frac{N}{P}\right)}^{2^{nd}\left(a\right)}={\left(\frac{N}{P}\right)}^l$$
27	24 26	oveq12d	$$⊢a=⟨k,l⟩\to P^{1^{st}\left(a\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(a\right)}=P^k{\left(\frac{N}{P}\right)}^l$$
28	27	mpompt	$$⊢\left(a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)⟼P^{1^{st}\left(a\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(a\right)}\right)=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
29	28	eqcomi	$$⊢\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)=\left(a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)⟼P^{1^{st}\left(a\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(a\right)}\right)$$
30	4 29	eqtri	$$⊢E=\left(a\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)⟼P^{1^{st}\left(a\right)}{\left(\frac{N}{P}\right)}^{2^{nd}\left(a\right)}\right)$$
31	20 30	fmptd	$$⊢\phi \to E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶\mathbb{N}$$