aks6d1c7

	Ref	Expression
Hypotheses	aks6d1c7.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
	aks6d1c7.2	$⊢ P = chr (K)$
	aks6d1c7.3	$⊢ φ \to K \in Field$
	aks6d1c7.4	$⊢ φ \to P \in ℙ$
	aks6d1c7.5	$⊢ φ \to R \in ℕ$
	aks6d1c7.6	$⊢ φ \to N \in ℤ_{\geq 3}$
	aks6d1c7.7	$⊢ φ \to P ∥ N$
	aks6d1c7.8	$⊢ φ \to N \gcd R = 1$
	aks6d1c7.9	$⊢ A = ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
	aks6d1c7.10	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
	aks6d1c7.11	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
	aks6d1c7.12	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
	aks6d1c7.13	$⊢ φ \to \forall b \in (1 \dots A) b \gcd N = 1$
	aks6d1c7.14	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
Assertion	aks6d1c7	$⊢ φ \to N = P^{P pCnt N}$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c7.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
2		aks6d1c7.2	$⊢ P = chr (K)$
3		aks6d1c7.3	$⊢ φ \to K \in Field$
4		aks6d1c7.4	$⊢ φ \to P \in ℙ$
5		aks6d1c7.5	$⊢ φ \to R \in ℕ$
6		aks6d1c7.6	$⊢ φ \to N \in ℤ_{\geq 3}$
7		aks6d1c7.7	$⊢ φ \to P ∥ N$
8		aks6d1c7.8	$⊢ φ \to N \gcd R = 1$
9		aks6d1c7.9	$⊢ A = ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
10		aks6d1c7.10	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
11		aks6d1c7.11	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
12		aks6d1c7.12	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
13		aks6d1c7.13	$⊢ φ \to \forall b \in (1 \dots A) b \gcd N = 1$
14		aks6d1c7.14	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
15		simpr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to q = r$
16	7	ad2antrr	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to P ∥ N$
17		breq1	$⊢ s = P \to (s ∥ N \leftrightarrow P ∥ N)$
18		eqeq1	$⊢ s = P \to (s = r \leftrightarrow P = r)$
19	17 18	bibi12d	$⊢ s = P \to ((s ∥ N \leftrightarrow s = r) \leftrightarrow (P ∥ N \leftrightarrow P = r))$
20		nfv	$⊢ Ⅎ s (p ∥ N \leftrightarrow p = r)$
21		nfv	$⊢ Ⅎ p (s ∥ N \leftrightarrow s = r)$
22		breq1	$⊢ p = s \to (p ∥ N \leftrightarrow s ∥ N)$
23		equequ1	$⊢ p = s \to (p = r \leftrightarrow s = r)$
24	22 23	bibi12d	$⊢ p = s \to ((p ∥ N \leftrightarrow p = r) \leftrightarrow (s ∥ N \leftrightarrow s = r))$
25	20 21 24	cbvralw	$⊢ \forall p \in ℙ (p ∥ N \leftrightarrow p = r) \leftrightarrow \forall s \in ℙ (s ∥ N \leftrightarrow s = r)$
26	25	biimpi	$⊢ \forall p \in ℙ (p ∥ N \leftrightarrow p = r) \to \forall s \in ℙ (s ∥ N \leftrightarrow s = r)$
27	26	adantl	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to \forall s \in ℙ (s ∥ N \leftrightarrow s = r)$
28	4	ad2antrr	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to P \in ℙ$
29	19 27 28	rspcdva	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to (P ∥ N \leftrightarrow P = r)$
30	29	biimpd	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to (P ∥ N \to P = r)$
31	16 30	mpd	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to P = r$
32	31	ad2antrr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P = r$
33	32	eqcomd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to r = P$
34	15 33	eqtrd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to q = P$
35	34	oveq1d	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to q pCnt N = P pCnt N$
36		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
37	6 36	syl	$⊢ φ \to N \in ℤ$
38		0red	$⊢ φ \to 0 \in ℝ$
39		3re	$⊢ 3 \in ℝ$
40	39	a1i	$⊢ φ \to 3 \in ℝ$
41	37	zred	$⊢ φ \to N \in ℝ$
42		3pos	$⊢ 0 < 3$
43	42	a1i	$⊢ φ \to 0 < 3$
44		eluzle	$⊢ N \in ℤ_{\geq 3} \to 3 \leq N$
45	6 44	syl	$⊢ φ \to 3 \leq N$
46	38 40 41 43 45	ltletrd	$⊢ φ \to 0 < N$
47	37 46	jca	$⊢ φ \to (N \in ℤ \land 0 < N)$
48		elnnz	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N)$
49	47 48	sylibr	$⊢ φ \to N \in ℕ$
50		pcelnn	$⊢ (P \in ℙ \land N \in ℕ) \to (P pCnt N \in ℕ \leftrightarrow P ∥ N)$
51	4 49 50	syl2anc	$⊢ φ \to (P pCnt N \in ℕ \leftrightarrow P ∥ N)$
52	7 51	mpbird	$⊢ φ \to P pCnt N \in ℕ$
53	52	nncnd	$⊢ φ \to P pCnt N \in ℂ$
54	53	mulridd	$⊢ φ \to (P pCnt N) \cdot 1 = P pCnt N$
55	54	eqcomd	$⊢ φ \to P pCnt N = (P pCnt N) \cdot 1$
56		1nn0	$⊢ 1 \in ℕ_{0}$
57	56	a1i	$⊢ φ \to 1 \in ℕ_{0}$
58		pcidlem	$⊢ (P \in ℙ \land 1 \in ℕ_{0}) \to P pCnt P^{1} = 1$
59	4 57 58	syl2anc	$⊢ φ \to P pCnt P^{1} = 1$
60	59	eqcomd	$⊢ φ \to 1 = P pCnt P^{1}$
61		prmnn	$⊢ P \in ℙ \to P \in ℕ$
62	4 61	syl	$⊢ φ \to P \in ℕ$
63	62	nncnd	$⊢ φ \to P \in ℂ$
64	63	exp1d	$⊢ φ \to P^{1} = P$
65	64	oveq2d	$⊢ φ \to P pCnt P^{1} = P pCnt P$
66	60 65	eqtrd	$⊢ φ \to 1 = P pCnt P$
67	66	oveq2d	$⊢ φ \to (P pCnt N) \cdot 1 = (P pCnt N) (P pCnt P)$
68	55 67	eqtrd	$⊢ φ \to P pCnt N = (P pCnt N) (P pCnt P)$
69	68	adantr	$⊢ (φ \land r \in ℙ) \to P pCnt N = (P pCnt N) (P pCnt P)$
70	69	ad3antrrr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P pCnt N = (P pCnt N) (P pCnt P)$
71	28	ad2antrr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P \in ℙ$
72		nnq	$⊢ P \in ℕ \to P \in ℚ$
73	62 72	syl	$⊢ φ \to P \in ℚ$
74	62	nnne0d	$⊢ φ \to P \neq 0$
75	73 74	jca	$⊢ φ \to (P \in ℚ \land P \neq 0)$
76	75	adantr	$⊢ (φ \land r \in ℙ) \to (P \in ℚ \land P \neq 0)$
77	76	ad3antrrr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to (P \in ℚ \land P \neq 0)$
78	52	nnzd	$⊢ φ \to P pCnt N \in ℤ$
79	78	adantr	$⊢ (φ \land r \in ℙ) \to P pCnt N \in ℤ$
80	79	adantr	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to P pCnt N \in ℤ$
81	80	adantr	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to P pCnt N \in ℤ$
82	81	adantr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P pCnt N \in ℤ$
83		pcexp	$⊢ (P \in ℙ \land (P \in ℚ \land P \neq 0) \land P pCnt N \in ℤ) \to P pCnt P^{P pCnt N} = (P pCnt N) (P pCnt P)$
84	71 77 82 83	syl3anc	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P pCnt P^{P pCnt N} = (P pCnt N) (P pCnt P)$
85	84	eqcomd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to (P pCnt N) (P pCnt P) = P pCnt P^{P pCnt N}$
86	70 85	eqtrd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P pCnt N = P pCnt P^{P pCnt N}$
87	34	eqcomd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P = q$
88	87	oveq1d	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P pCnt P^{P pCnt N} = q pCnt P^{P pCnt N}$
89	86 88	eqtrd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P pCnt N = q pCnt P^{P pCnt N}$
90	35 89	eqtrd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to q pCnt N = q pCnt P^{P pCnt N}$
91		breq1	$⊢ s = q \to (s ∥ N \leftrightarrow q ∥ N)$
92		equequ1	$⊢ s = q \to (s = r \leftrightarrow q = r)$
93	91 92	bibi12d	$⊢ s = q \to ((s ∥ N \leftrightarrow s = r) \leftrightarrow (q ∥ N \leftrightarrow q = r))$
94	27	adantr	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to \forall s \in ℙ (s ∥ N \leftrightarrow s = r)$
95		simpr	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to q \in ℙ$
96	93 94 95	rspcdva	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to (q ∥ N \leftrightarrow q = r)$
97	96	bicomd	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to (q = r \leftrightarrow q ∥ N)$
98	97	notbid	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to (\neg q = r \leftrightarrow \neg q ∥ N)$
99	98	biimpa	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to \neg q ∥ N$
100	95	adantr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to q \in ℙ$
101	49	adantr	$⊢ (φ \land r \in ℙ) \to N \in ℕ$
102	101	ad3antrrr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to N \in ℕ$
103		pceq0	$⊢ (q \in ℙ \land N \in ℕ) \to (q pCnt N = 0 \leftrightarrow \neg q ∥ N)$
104	100 102 103	syl2anc	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to (q pCnt N = 0 \leftrightarrow \neg q ∥ N)$
105	99 104	mpbird	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to q pCnt N = 0$
106		neqne	$⊢ \neg q = r \to q \neq r$
107	106	adantl	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to q \neq r$
108	16	adantr	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to P ∥ N$
109	28	adantr	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to P \in ℙ$
110	19 94 109	rspcdva	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to (P ∥ N \leftrightarrow P = r)$
111	110	biimpd	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to (P ∥ N \to P = r)$
112	108 111	mpd	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to P = r$
113	112	adantr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to P = r$
114	113	eqcomd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to r = P$
115	107 114	neeqtrd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to q \neq P$
116	115	neneqd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to \neg q = P$
117		prmuz2	$⊢ q \in ℙ \to q \in ℤ_{\geq 2}$
118	117	adantl	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to q \in ℤ_{\geq 2}$
119	118	adantr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to q \in ℤ_{\geq 2}$
120	28	ad2antrr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to P \in ℙ$
121		dvdsprm	$⊢ (q \in ℤ_{\geq 2} \land P \in ℙ) \to (q ∥ P \leftrightarrow q = P)$
122	119 120 121	syl2anc	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to (q ∥ P \leftrightarrow q = P)$
123	116 122	mtbird	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to \neg q ∥ P$
124	62	ad4antr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to P \in ℕ$
125	124	nnzd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to P \in ℤ$
126	52	adantr	$⊢ (φ \land r \in ℙ) \to P pCnt N \in ℕ$
127	126	adantr	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to P pCnt N \in ℕ$
128	127	adantr	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to P pCnt N \in ℕ$
129	128	adantr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to P pCnt N \in ℕ$
130		prmdvdsexp	$⊢ (q \in ℙ \land P \in ℤ \land P pCnt N \in ℕ) \to (q ∥ P^{P pCnt N} \leftrightarrow q ∥ P)$
131	100 125 129 130	syl3anc	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to (q ∥ P^{P pCnt N} \leftrightarrow q ∥ P)$
132	123 131	mtbird	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to \neg q ∥ P^{P pCnt N}$
133	120 102	pccld	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to P pCnt N \in ℕ_{0}$
134	124 133	nnexpcld	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to P^{P pCnt N} \in ℕ$
135		pceq0	$⊢ (q \in ℙ \land P^{P pCnt N} \in ℕ) \to (q pCnt P^{P pCnt N} = 0 \leftrightarrow \neg q ∥ P^{P pCnt N})$
136	100 134 135	syl2anc	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to (q pCnt P^{P pCnt N} = 0 \leftrightarrow \neg q ∥ P^{P pCnt N})$
137	132 136	mpbird	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to q pCnt P^{P pCnt N} = 0$
138	137	eqcomd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to 0 = q pCnt P^{P pCnt N}$
139	105 138	eqtrd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to q pCnt N = q pCnt P^{P pCnt N}$
140	90 139	pm2.61dan	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to q pCnt N = q pCnt P^{P pCnt N}$
141	140	ralrimiva	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to \forall q \in ℙ q pCnt N = q pCnt P^{P pCnt N}$
142	1 2 3 4 5 6 7 8 9 10 11 12 13 14	aks6d1c7lem4	$⊢ φ \to \exists! p \in ℙ p ∥ N$
143		reu6	$⊢ \exists! p \in ℙ p ∥ N \leftrightarrow \exists r \in ℙ \forall p \in ℙ (p ∥ N \leftrightarrow p = r)$
144	142 143	sylib	$⊢ φ \to \exists r \in ℙ \forall p \in ℙ (p ∥ N \leftrightarrow p = r)$
145	141 144	r19.29a	$⊢ φ \to \forall q \in ℙ q pCnt N = q pCnt P^{P pCnt N}$
146	49	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
147	62	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
148	4 49	pccld	$⊢ φ \to P pCnt N \in ℕ_{0}$
149	147 148	nn0expcld	$⊢ φ \to P^{P pCnt N} \in ℕ_{0}$
150		pc11	$⊢ (N \in ℕ_{0} \land P^{P pCnt N} \in ℕ_{0}) \to (N = P^{P pCnt N} \leftrightarrow \forall q \in ℙ q pCnt N = q pCnt P^{P pCnt N})$
151	146 149 150	syl2anc	$⊢ φ \to (N = P^{P pCnt N} \leftrightarrow \forall q \in ℙ q pCnt N = q pCnt P^{P pCnt N})$
152	145 151	mpbird	$⊢ φ \to N = P^{P pCnt N}$

Metamath Proof Explorer

Theorem aks6d1c7

Proof