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	bilani	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to \forall s \in ℙ (s ∥ N \leftrightarrow s = r)$
27	4	ad2antrr	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to P \in ℙ$
28	19 26 27	rspcdva	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to (P ∥ N \leftrightarrow P = r)$
29	28	biimpd	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to (P ∥ N \to P = r)$
30	16 29	mpd	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to P = r$
31	30	ad2antrr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P = r$
32	31	eqcomd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to r = P$
33	15 32	eqtrd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to q = P$
34	33	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$
35		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
36	6 35	syl	$⊢ φ \to N \in ℤ$
37		0red	$⊢ φ \to 0 \in ℝ$
38		3re	$⊢ 3 \in ℝ$
39	38	a1i	$⊢ φ \to 3 \in ℝ$
40	36	zred	$⊢ φ \to N \in ℝ$
41		3pos	$⊢ 0 < 3$
42	41	a1i	$⊢ φ \to 0 < 3$
43		eluzle	$⊢ N \in ℤ_{\geq 3} \to 3 \leq N$
44	6 43	syl	$⊢ φ \to 3 \leq N$
45	37 39 40 42 44	ltletrd	$⊢ φ \to 0 < N$
46	36 45	jca	$⊢ φ \to (N \in ℤ \land 0 < N)$
47		elnnz	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N)$
48	46 47	sylibr	$⊢ φ \to N \in ℕ$
49		pcelnn	$⊢ (P \in ℙ \land N \in ℕ) \to (P pCnt N \in ℕ \leftrightarrow P ∥ N)$
50	4 48 49	syl2anc	$⊢ φ \to (P pCnt N \in ℕ \leftrightarrow P ∥ N)$
51	7 50	mpbird	$⊢ φ \to P pCnt N \in ℕ$
52	51	nncnd	$⊢ φ \to P pCnt N \in ℂ$
53	52	mulridd	$⊢ φ \to (P pCnt N) \cdot 1 = P pCnt N$
54	53	eqcomd	$⊢ φ \to P pCnt N = (P pCnt N) \cdot 1$
55		1nn0	$⊢ 1 \in ℕ_{0}$
56	55	a1i	$⊢ φ \to 1 \in ℕ_{0}$
57		pcidlem	$⊢ (P \in ℙ \land 1 \in ℕ_{0}) \to P pCnt P^{1} = 1$
58	4 56 57	syl2anc	$⊢ φ \to P pCnt P^{1} = 1$
59	58	eqcomd	$⊢ φ \to 1 = P pCnt P^{1}$
60		prmnn	$⊢ P \in ℙ \to P \in ℕ$
61	4 60	syl	$⊢ φ \to P \in ℕ$
62	61	nncnd	$⊢ φ \to P \in ℂ$
63	62	exp1d	$⊢ φ \to P^{1} = P$
64	63	oveq2d	$⊢ φ \to P pCnt P^{1} = P pCnt P$
65	59 64	eqtrd	$⊢ φ \to 1 = P pCnt P$
66	65	oveq2d	$⊢ φ \to (P pCnt N) \cdot 1 = (P pCnt N) (P pCnt P)$
67	54 66	eqtrd	$⊢ φ \to P pCnt N = (P pCnt N) (P pCnt P)$
68	67	adantr	$⊢ (φ \land r \in ℙ) \to P pCnt N = (P pCnt N) (P pCnt P)$
69	68	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)$
70	27	ad2antrr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P \in ℙ$
71		nnq	$⊢ P \in ℕ \to P \in ℚ$
72	61 71	syl	$⊢ φ \to P \in ℚ$
73	61	nnne0d	$⊢ φ \to P \neq 0$
74	72 73	jca	$⊢ φ \to (P \in ℚ \land P \neq 0)$
75	74	adantr	$⊢ (φ \land r \in ℙ) \to (P \in ℚ \land P \neq 0)$
76	75	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)$
77	51	nnzd	$⊢ φ \to P pCnt N \in ℤ$
78	77	adantr	$⊢ (φ \land r \in ℙ) \to P pCnt N \in ℤ$
79	78	adantr	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to P pCnt N \in ℤ$
80	79	adantr	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to P pCnt N \in ℤ$
81	80	adantr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P pCnt N \in ℤ$
82		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)$
83	70 76 81 82	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)$
84	83	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}$
85	69 84	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}$
86	33	eqcomd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land q = r) \to P = q$
87	86	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}$
88	85 87	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}$
89	34 88	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}$
90		breq1	$⊢ s = q \to (s ∥ N \leftrightarrow q ∥ N)$
91		equequ1	$⊢ s = q \to (s = r \leftrightarrow q = r)$
92	90 91	bibi12d	$⊢ s = q \to ((s ∥ N \leftrightarrow s = r) \leftrightarrow (q ∥ N \leftrightarrow q = r))$
93	26	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)$
94		simpr	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to q \in ℙ$
95	92 93 94	rspcdva	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to (q ∥ N \leftrightarrow q = r)$
96	95	bicomd	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to (q = r \leftrightarrow q ∥ N)$
97	96	notbid	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to (\neg q = r \leftrightarrow \neg q ∥ N)$
98	97	biimpa	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to \neg q ∥ N$
99	94	adantr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to q \in ℙ$
100	48	adantr	$⊢ (φ \land r \in ℙ) \to N \in ℕ$
101	100	ad3antrrr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to N \in ℕ$
102		pceq0	$⊢ (q \in ℙ \land N \in ℕ) \to (q pCnt N = 0 \leftrightarrow \neg q ∥ N)$
103	99 101 102	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)$
104	98 103	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$
105		neqne	$⊢ \neg q = r \to q \neq r$
106	105	adantl	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to q \neq r$
107	16	adantr	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to P ∥ N$
108	27	adantr	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to P \in ℙ$
109	19 93 108	rspcdva	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to (P ∥ N \leftrightarrow P = r)$
110	109	biimpd	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to (P ∥ N \to P = r)$
111	107 110	mpd	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to P = r$
112	111	adantr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to P = r$
113	112	eqcomd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to r = P$
114	106 113	neeqtrd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to q \neq P$
115	114	neneqd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to \neg q = P$
116		prmuz2	$⊢ q \in ℙ \to q \in ℤ_{\geq 2}$
117	116	adantl	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to q \in ℤ_{\geq 2}$
118	117	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}$
119	27	ad2antrr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to P \in ℙ$
120		dvdsprm	$⊢ (q \in ℤ_{\geq 2} \land P \in ℙ) \to (q ∥ P \leftrightarrow q = P)$
121	118 119 120	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)$
122	115 121	mtbird	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to \neg q ∥ P$
123	61	ad4antr	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to P \in ℕ$
124	123	nnzd	$⊢ ((((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \land \neg q = r) \to P \in ℤ$
125	51	adantr	$⊢ (φ \land r \in ℙ) \to P pCnt N \in ℕ$
126	125	adantr	$⊢ ((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \to P pCnt N \in ℕ$
127	126	adantr	$⊢ (((φ \land r \in ℙ) \land \forall p \in ℙ (p ∥ N \leftrightarrow p = r)) \land q \in ℙ) \to P pCnt N \in ℕ$
128	127	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 ℕ$
129		prmdvdsexp	$⊢ (q \in ℙ \land P \in ℤ \land P pCnt N \in ℕ) \to (q ∥ P^{P pCnt N} \leftrightarrow q ∥ P)$
130	99 124 128 129	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)$
131	122 130	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}$
132	119 101	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}$
133	123 132	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 ℕ$
134		pceq0	$⊢ (q \in ℙ \land P^{P pCnt N} \in ℕ) \to (q pCnt P^{P pCnt N} = 0 \leftrightarrow \neg q ∥ P^{P pCnt N})$
135	99 133 134	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})$
136	131 135	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$
137	136	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}$
138	104 137	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}$
139	89 138	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}$
140	139	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}$
141	1 2 3 4 5 6 7 8 9 10 11 12 13 14	aks6d1c7lem4	$⊢ φ \to \exists! p \in ℙ p ∥ N$
142		reu6	$⊢ \exists! p \in ℙ p ∥ N \leftrightarrow \exists r \in ℙ \forall p \in ℙ (p ∥ N \leftrightarrow p = r)$
143	141 142	sylib	$⊢ φ \to \exists r \in ℙ \forall p \in ℙ (p ∥ N \leftrightarrow p = r)$
144	140 143	r19.29a	$⊢ φ \to \forall q \in ℙ q pCnt N = q pCnt P^{P pCnt N}$
145	48	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
146	61	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
147	4 48	pccld	$⊢ φ \to P pCnt N \in ℕ_{0}$
148	146 147	nn0expcld	$⊢ φ \to P^{P pCnt N} \in ℕ_{0}$
149		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})$
150	145 148 149	syl2anc	$⊢ φ \to (N = P^{P pCnt N} \leftrightarrow \forall q \in ℙ q pCnt N = q pCnt P^{P pCnt N})$
151	144 150	mpbird	$⊢ φ \to N = P^{P pCnt N}$

Metamath Proof Explorer

Theorem aks6d1c7

Proof