aks5lem8

Description: Lemma for aks5. Clean up the conclusion. (Contributed by metakunt, 9-Aug-2025)

	Ref	Expression
Hypotheses	aks5lem7.1	$⊢ φ \to \|{Base}_{K}\| \in ℕ$
	aks5lem7.2	$⊢ P = chr (K)$
	aks5lem7.3	$⊢ φ \to K \in Field$
	aks5lem7.4	$⊢ φ \to P \in ℙ$
	aks5lem7.5	$⊢ φ \to R \in ℕ$
	aks5lem7.6	$⊢ φ \to N \in ℤ_{\geq 3}$
	aks5lem7.7	$⊢ φ \to P ∥ N$
	aks5lem7.8	$⊢ φ \to N \gcd R = 1$
	aks5lem7.9	$⊢ A = ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
	aks5lem7.10	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
	aks5lem7.11	$⊢ φ \to R ∥ (\|{Base}_{K}\| - 1)$
	aks5lem7.12	$⊢ φ \to \forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
	aks5lem7.13	$⊢ φ \to \forall b \in (1 \dots A) b \gcd N = 1$
	aks5lem7.14	$⊢ S = {Poly}_{1} (ℤ / N ℤ)$
	aks5lem7.15	$⊢ L = RSpan (S) (\{(R \cdot_{{mulGrp}_{S}} X) -_{S} 1_{S}\})$
	aks5lem7.16	$⊢ X = {var}_{1} (ℤ / N ℤ)$
Assertion	aks5lem8	$⊢ φ \to \exists p \in ℙ \exists n \in ℕ N = p^{n}$

Proof

Step	Hyp	Ref	Expression
1		aks5lem7.1	$⊢ φ \to \|{Base}_{K}\| \in ℕ$
2		aks5lem7.2	$⊢ P = chr (K)$
3		aks5lem7.3	$⊢ φ \to K \in Field$
4		aks5lem7.4	$⊢ φ \to P \in ℙ$
5		aks5lem7.5	$⊢ φ \to R \in ℕ$
6		aks5lem7.6	$⊢ φ \to N \in ℤ_{\geq 3}$
7		aks5lem7.7	$⊢ φ \to P ∥ N$
8		aks5lem7.8	$⊢ φ \to N \gcd R = 1$
9		aks5lem7.9	$⊢ A = ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
10		aks5lem7.10	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
11		aks5lem7.11	$⊢ φ \to R ∥ (\|{Base}_{K}\| - 1)$
12		aks5lem7.12	$⊢ φ \to \forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
13		aks5lem7.13	$⊢ φ \to \forall b \in (1 \dots A) b \gcd N = 1$
14		aks5lem7.14	$⊢ S = {Poly}_{1} (ℤ / N ℤ)$
15		aks5lem7.15	$⊢ L = RSpan (S) (\{(R \cdot_{{mulGrp}_{S}} X) -_{S} 1_{S}\})$
16		aks5lem7.16	$⊢ X = {var}_{1} (ℤ / N ℤ)$
17		simpr	$⊢ (φ \land p = P) \to p = P$
18	17	oveq1d	$⊢ (φ \land p = P) \to p^{n} = P^{n}$
19	18	eqeq2d	$⊢ (φ \land p = P) \to (N = p^{n} \leftrightarrow N = P^{n})$
20	19	rexbidv	$⊢ (φ \land p = P) \to (\exists n \in ℕ N = p^{n} \leftrightarrow \exists n \in ℕ N = P^{n})$
21	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	aks5lem7	$⊢ φ \to N = P^{P pCnt N}$
22		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
23	6 22	syl	$⊢ φ \to N \in ℤ$
24		0red	$⊢ φ \to 0 \in ℝ$
25		3re	$⊢ 3 \in ℝ$
26	25	a1i	$⊢ φ \to 3 \in ℝ$
27	23	zred	$⊢ φ \to N \in ℝ$
28		3pos	$⊢ 0 < 3$
29	28	a1i	$⊢ φ \to 0 < 3$
30		eluzle	$⊢ N \in ℤ_{\geq 3} \to 3 \leq N$
31	6 30	syl	$⊢ φ \to 3 \leq N$
32	24 26 27 29 31	ltletrd	$⊢ φ \to 0 < N$
33	23 32	jca	$⊢ φ \to (N \in ℤ \land 0 < N)$
34		elnnz	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N)$
35	33 34	sylibr	$⊢ φ \to N \in ℕ$
36		pcprmpw	$⊢ (P \in ℙ \land N \in ℕ) \to (\exists n \in ℕ_{0} N = P^{n} \leftrightarrow N = P^{P pCnt N})$
37	4 35 36	syl2anc	$⊢ φ \to (\exists n \in ℕ_{0} N = P^{n} \leftrightarrow N = P^{P pCnt N})$
38	21 37	mpbird	$⊢ φ \to \exists n \in ℕ_{0} N = P^{n}$
39		simprl	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to n \in ℕ_{0}$
40	39	nn0zd	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to n \in ℤ$
41		simpr	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land 0 < n) \to 0 < n$
42	39	nn0red	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to n \in ℝ$
43		0red	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to 0 \in ℝ$
44	42 43	lenltd	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to (n \leq 0 \leftrightarrow \neg 0 < n)$
45	44	bicomd	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to (\neg 0 < n \leftrightarrow n \leq 0)$
46	45	biimpd	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to (\neg 0 < n \to n \leq 0)$
47	46	imp	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land \neg 0 < n) \to n \leq 0$
48		simpr	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n \leq 0) \to n \leq 0$
49	39	adantr	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n \leq 0) \to n \in ℕ_{0}$
50		nn0le0eq0	$⊢ n \in ℕ_{0} \to (n \leq 0 \leftrightarrow n = 0)$
51	50	bicomd	$⊢ n \in ℕ_{0} \to (n = 0 \leftrightarrow n \leq 0)$
52	49 51	syl	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n \leq 0) \to (n = 0 \leftrightarrow n \leq 0)$
53	48 52	mpbird	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n \leq 0) \to n = 0$
54		simplrr	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to N = P^{n}$
55		simpr	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to n = 0$
56	55	oveq2d	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to P^{n} = P^{0}$
57	4	ad2antrr	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to P \in ℙ$
58		prmnn	$⊢ P \in ℙ \to P \in ℕ$
59	57 58	syl	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to P \in ℕ$
60	59	nncnd	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to P \in ℂ$
61	60	exp0d	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to P^{0} = 1$
62	56 61	eqtrd	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to P^{n} = 1$
63	54 62	eqtrd	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to N = 1$
64		1red	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to 1 \in ℝ$
65		1red	$⊢ φ \to 1 \in ℝ$
66	35	nnred	$⊢ φ \to N \in ℝ$
67		1lt3	$⊢ 1 < 3$
68	67	a1i	$⊢ φ \to 1 < 3$
69	65 26 66 68 31	ltletrd	$⊢ φ \to 1 < N$
70	69	adantr	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to 1 < N$
71	70	adantr	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to 1 < N$
72	64 71	ltned	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to 1 \neq N$
73	72	necomd	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to N \neq 1$
74	73	neneqd	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to \neg N = 1$
75	63 74	pm2.21dd	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n = 0) \to 0 < n$
76	75	ex	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to (n = 0 \to 0 < n)$
77	76	adantr	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n \leq 0) \to (n = 0 \to 0 < n)$
78	53 77	mpd	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land n \leq 0) \to 0 < n$
79	78	ex	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to (n \leq 0 \to 0 < n)$
80	79	adantr	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land \neg 0 < n) \to (n \leq 0 \to 0 < n)$
81	47 80	mpd	$⊢ ((φ \land (n \in ℕ_{0} \land N = P^{n})) \land \neg 0 < n) \to 0 < n$
82	41 81	pm2.61dan	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to 0 < n$
83	40 82	jca	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to (n \in ℤ \land 0 < n)$
84		elnnz	$⊢ n \in ℕ \leftrightarrow (n \in ℤ \land 0 < n)$
85	83 84	sylibr	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to n \in ℕ$
86		simprr	$⊢ (φ \land (n \in ℕ_{0} \land N = P^{n})) \to N = P^{n}$
87	38 85 86	reximssdv	$⊢ φ \to \exists n \in ℕ N = P^{n}$
88	4 20 87	rspcedvd	$⊢ φ \to \exists p \in ℙ \exists n \in ℕ N = p^{n}$

Metamath Proof Explorer

Theorem aks5lem8

Proof