aks4d1p7d1

Description: Technical step in AKS lemma 4.1. (Contributed by metakunt, 31-Oct-2024)

	Ref	Expression
Hypotheses	aks4d1p7d1.1	$⊢ φ \to N \in ℤ_{\geq 3}$
	aks4d1p7d1.2	$⊢ A = N^{⌊\log_{2} B⌋} \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1)$
	aks4d1p7d1.3	$⊢ B = ⌈{\log_{2} N}^{5}⌉$
	aks4d1p7d1.4	$⊢ R = inf (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <)$
	aks4d1p7d1.5	$⊢ φ \to \forall p \in ℙ (p ∥ R \to p ∥ N)$
Assertion	aks4d1p7d1	$⊢ φ \to R ∥ N^{⌊\log_{2} B⌋}$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p7d1.1	$⊢ φ \to N \in ℤ_{\geq 3}$
2		aks4d1p7d1.2	$⊢ A = N^{⌊\log_{2} B⌋} \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1)$
3		aks4d1p7d1.3	$⊢ B = ⌈{\log_{2} N}^{5}⌉$
4		aks4d1p7d1.4	$⊢ R = inf (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <)$
5		aks4d1p7d1.5	$⊢ φ \to \forall p \in ℙ (p ∥ R \to p ∥ N)$
6		simp2	$⊢ (φ \land p \in ℙ \land p ∥ R) \to p \in ℙ$
7	1 2 3 4	aks4d1p4	$⊢ φ \to (R \in (1 \dots B) \land \neg R ∥ A)$
8	7	simpld	$⊢ φ \to R \in (1 \dots B)$
9		elfznn	$⊢ R \in (1 \dots B) \to R \in ℕ$
10	8 9	syl	$⊢ φ \to R \in ℕ$
11	10	3ad2ant1	$⊢ (φ \land p \in ℙ \land p ∥ R) \to R \in ℕ$
12	6 11	pccld	$⊢ (φ \land p \in ℙ \land p ∥ R) \to p pCnt R \in ℕ_{0}$
13	12	3expa	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p pCnt R \in ℕ_{0}$
14	13	nn0red	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p pCnt R \in ℝ$
15		2re	$⊢ 2 \in ℝ$
16	15	a1i	$⊢ φ \to 2 \in ℝ$
17		2pos	$⊢ 0 < 2$
18	17	a1i	$⊢ φ \to 0 < 2$
19	3	a1i	$⊢ φ \to B = ⌈{\log_{2} N}^{5}⌉$
20		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
21	1 20	syl	$⊢ φ \to N \in ℤ$
22	21	zred	$⊢ φ \to N \in ℝ$
23		0red	$⊢ φ \to 0 \in ℝ$
24		3re	$⊢ 3 \in ℝ$
25	24	a1i	$⊢ φ \to 3 \in ℝ$
26		3pos	$⊢ 0 < 3$
27	26	a1i	$⊢ φ \to 0 < 3$
28		eluzle	$⊢ N \in ℤ_{\geq 3} \to 3 \leq N$
29	1 28	syl	$⊢ φ \to 3 \leq N$
30	23 25 22 27 29	ltletrd	$⊢ φ \to 0 < N$
31		1red	$⊢ φ \to 1 \in ℝ$
32		1lt2	$⊢ 1 < 2$
33	32	a1i	$⊢ φ \to 1 < 2$
34	31 33	ltned	$⊢ φ \to 1 \neq 2$
35	34	necomd	$⊢ φ \to 2 \neq 1$
36	16 18 22 30 35	relogbcld	$⊢ φ \to \log_{2} N \in ℝ$
37		5nn0	$⊢ 5 \in ℕ_{0}$
38	37	a1i	$⊢ φ \to 5 \in ℕ_{0}$
39	36 38	reexpcld	$⊢ φ \to {\log_{2} N}^{5} \in ℝ$
40		ceilcl	$⊢ {\log_{2} N}^{5} \in ℝ \to ⌈{\log_{2} N}^{5}⌉ \in ℤ$
41	39 40	syl	$⊢ φ \to ⌈{\log_{2} N}^{5}⌉ \in ℤ$
42	41	zred	$⊢ φ \to ⌈{\log_{2} N}^{5}⌉ \in ℝ$
43	19 42	eqeltrd	$⊢ φ \to B \in ℝ$
44		9re	$⊢ 9 \in ℝ$
45	44	a1i	$⊢ φ \to 9 \in ℝ$
46		9pos	$⊢ 0 < 9$
47	46	a1i	$⊢ φ \to 0 < 9$
48	22 29	3lexlogpow5ineq4	$⊢ φ \to 9 < {\log_{2} N}^{5}$
49	23 45 39 47 48	lttrd	$⊢ φ \to 0 < {\log_{2} N}^{5}$
50		ceilge	$⊢ {\log_{2} N}^{5} \in ℝ \to {\log_{2} N}^{5} \leq ⌈{\log_{2} N}^{5}⌉$
51	39 50	syl	$⊢ φ \to {\log_{2} N}^{5} \leq ⌈{\log_{2} N}^{5}⌉$
52	23 39 42 49 51	ltletrd	$⊢ φ \to 0 < ⌈{\log_{2} N}^{5}⌉$
53	52 19	breqtrrd	$⊢ φ \to 0 < B$
54	16 18 43 53 35	relogbcld	$⊢ φ \to \log_{2} B \in ℝ$
55	54	flcld	$⊢ φ \to ⌊\log_{2} B⌋ \in ℤ$
56	55	zred	$⊢ φ \to ⌊\log_{2} B⌋ \in ℝ$
57	56	ad2antrr	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to ⌊\log_{2} B⌋ \in ℝ$
58		simplr	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p \in ℙ$
59	21 30	jca	$⊢ φ \to (N \in ℤ \land 0 < N)$
60		elnnz	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N)$
61	59 60	sylibr	$⊢ φ \to N \in ℕ$
62	61	ad2antrr	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to N \in ℕ$
63		1cnd	$⊢ φ \to 1 \in ℂ$
64	63	addlidd	$⊢ φ \to 0 + 1 = 1$
65	16	recnd	$⊢ φ \to 2 \in ℂ$
66	23 18	gtned	$⊢ φ \to 2 \neq 0$
67		logbid1	$⊢ (2 \in ℂ \land 2 \neq 0 \land 2 \neq 1) \to \log_{2} 2 = 1$
68	65 66 35 67	syl3anc	$⊢ φ \to \log_{2} 2 = 1$
69	68	eqcomd	$⊢ φ \to 1 = \log_{2} 2$
70	64 69	eqtrd	$⊢ φ \to 0 + 1 = \log_{2} 2$
71		2z	$⊢ 2 \in ℤ$
72	71	a1i	$⊢ φ \to 2 \in ℤ$
73	16	leidd	$⊢ φ \to 2 \leq 2$
74		2lt9	$⊢ 2 < 9$
75	74	a1i	$⊢ φ \to 2 < 9$
76	16 45 75	ltled	$⊢ φ \to 2 \leq 9$
77	45 39 42 48 51	ltletrd	$⊢ φ \to 9 < ⌈{\log_{2} N}^{5}⌉$
78	77 19	breqtrrd	$⊢ φ \to 9 < B$
79	45 43 78	ltled	$⊢ φ \to 9 \leq B$
80	16 45 43 76 79	letrd	$⊢ φ \to 2 \leq B$
81	72 73 16 18 43 53 80	logblebd	$⊢ φ \to \log_{2} 2 \leq \log_{2} B$
82	70 81	eqbrtrd	$⊢ φ \to 0 + 1 \leq \log_{2} B$
83		0zd	$⊢ φ \to 0 \in ℤ$
84	83	peano2zd	$⊢ φ \to 0 + 1 \in ℤ$
85		flge	$⊢ (\log_{2} B \in ℝ \land 0 + 1 \in ℤ) \to (0 + 1 \leq \log_{2} B \leftrightarrow 0 + 1 \leq ⌊\log_{2} B⌋)$
86	54 84 85	syl2anc	$⊢ φ \to (0 + 1 \leq \log_{2} B \leftrightarrow 0 + 1 \leq ⌊\log_{2} B⌋)$
87	82 86	mpbid	$⊢ φ \to 0 + 1 \leq ⌊\log_{2} B⌋$
88	83 55	zltp1led	$⊢ φ \to (0 < ⌊\log_{2} B⌋ \leftrightarrow 0 + 1 \leq ⌊\log_{2} B⌋)$
89	87 88	mpbird	$⊢ φ \to 0 < ⌊\log_{2} B⌋$
90	55 89	jca	$⊢ φ \to (⌊\log_{2} B⌋ \in ℤ \land 0 < ⌊\log_{2} B⌋)$
91		elnnz	$⊢ ⌊\log_{2} B⌋ \in ℕ \leftrightarrow (⌊\log_{2} B⌋ \in ℤ \land 0 < ⌊\log_{2} B⌋)$
92	90 91	sylibr	$⊢ φ \to ⌊\log_{2} B⌋ \in ℕ$
93	92	nnnn0d	$⊢ φ \to ⌊\log_{2} B⌋ \in ℕ_{0}$
94	93	ad2antrr	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to ⌊\log_{2} B⌋ \in ℕ_{0}$
95	62 94	nnexpcld	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to N^{⌊\log_{2} B⌋} \in ℕ$
96	58 95	pccld	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p pCnt N^{⌊\log_{2} B⌋} \in ℕ_{0}$
97	96	nn0red	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p pCnt N^{⌊\log_{2} B⌋} \in ℝ$
98	1	3ad2ant1	$⊢ (φ \land p \in ℙ \land p ∥ R) \to N \in ℤ_{\geq 3}$
99		simp3	$⊢ (φ \land p \in ℙ \land p ∥ R) \to p ∥ R$
100		eqid	$⊢ p pCnt R = p pCnt R$
101	98 2 3 4 6 99 100	aks4d1p6	$⊢ (φ \land p \in ℙ \land p ∥ R) \to p pCnt R \leq ⌊\log_{2} B⌋$
102	101	3expa	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p pCnt R \leq ⌊\log_{2} B⌋$
103	58 62	pccld	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p pCnt N \in ℕ_{0}$
104	103	nn0red	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p pCnt N \in ℝ$
105	23 56 89	ltled	$⊢ φ \to 0 \leq ⌊\log_{2} B⌋$
106	105	adantr	$⊢ (φ \land p \in ℙ) \to 0 \leq ⌊\log_{2} B⌋$
107	106	adantr	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to 0 \leq ⌊\log_{2} B⌋$
108		rsp	$⊢ \forall p \in ℙ (p ∥ R \to p ∥ N) \to (p \in ℙ \to (p ∥ R \to p ∥ N))$
109	5 108	syl	$⊢ φ \to (p \in ℙ \to (p ∥ R \to p ∥ N))$
110	109	imp	$⊢ (φ \land p \in ℙ) \to (p ∥ R \to p ∥ N)$
111	110	imp	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p ∥ N$
112	61	adantr	$⊢ (φ \land p \in ℙ) \to N \in ℕ$
113	112	adantr	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to N \in ℕ$
114		pcelnn	$⊢ (p \in ℙ \land N \in ℕ) \to (p pCnt N \in ℕ \leftrightarrow p ∥ N)$
115	58 113 114	syl2anc	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to (p pCnt N \in ℕ \leftrightarrow p ∥ N)$
116	111 115	mpbird	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p pCnt N \in ℕ$
117		nnge1	$⊢ p pCnt N \in ℕ \to 1 \leq p pCnt N$
118	116 117	syl	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to 1 \leq p pCnt N$
119	57 104 107 118	lemulge11d	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to ⌊\log_{2} B⌋ \leq ⌊\log_{2} B⌋ (p pCnt N)$
120		zq	$⊢ N \in ℤ \to N \in ℚ$
121	21 120	syl	$⊢ φ \to N \in ℚ$
122	61	nnne0d	$⊢ φ \to N \neq 0$
123	121 122	jca	$⊢ φ \to (N \in ℚ \land N \neq 0)$
124	123	adantr	$⊢ (φ \land p \in ℙ) \to (N \in ℚ \land N \neq 0)$
125	124	adantr	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to (N \in ℚ \land N \neq 0)$
126	55	adantr	$⊢ (φ \land p \in ℙ) \to ⌊\log_{2} B⌋ \in ℤ$
127	126	adantr	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to ⌊\log_{2} B⌋ \in ℤ$
128		pcexp	$⊢ (p \in ℙ \land (N \in ℚ \land N \neq 0) \land ⌊\log_{2} B⌋ \in ℤ) \to p pCnt N^{⌊\log_{2} B⌋} = ⌊\log_{2} B⌋ (p pCnt N)$
129	58 125 127 128	syl3anc	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p pCnt N^{⌊\log_{2} B⌋} = ⌊\log_{2} B⌋ (p pCnt N)$
130	119 129	breqtrrd	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to ⌊\log_{2} B⌋ \leq p pCnt N^{⌊\log_{2} B⌋}$
131	14 57 97 102 130	letrd	$⊢ ((φ \land p \in ℙ) \land p ∥ R) \to p pCnt R \leq p pCnt N^{⌊\log_{2} B⌋}$
132		simpr	$⊢ ((φ \land p \in ℙ) \land \neg p ∥ R) \to \neg p ∥ R$
133		simplr	$⊢ ((φ \land p \in ℙ) \land \neg p ∥ R) \to p \in ℙ$
134	10	adantr	$⊢ (φ \land p \in ℙ) \to R \in ℕ$
135	134	adantr	$⊢ ((φ \land p \in ℙ) \land \neg p ∥ R) \to R \in ℕ$
136		pceq0	$⊢ (p \in ℙ \land R \in ℕ) \to (p pCnt R = 0 \leftrightarrow \neg p ∥ R)$
137	133 135 136	syl2anc	$⊢ ((φ \land p \in ℙ) \land \neg p ∥ R) \to (p pCnt R = 0 \leftrightarrow \neg p ∥ R)$
138	132 137	mpbird	$⊢ ((φ \land p \in ℙ) \land \neg p ∥ R) \to p pCnt R = 0$
139	112	adantr	$⊢ ((φ \land p \in ℙ) \land \neg p ∥ R) \to N \in ℕ$
140	93	adantr	$⊢ (φ \land p \in ℙ) \to ⌊\log_{2} B⌋ \in ℕ_{0}$
141	140	adantr	$⊢ ((φ \land p \in ℙ) \land \neg p ∥ R) \to ⌊\log_{2} B⌋ \in ℕ_{0}$
142	139 141	nnexpcld	$⊢ ((φ \land p \in ℙ) \land \neg p ∥ R) \to N^{⌊\log_{2} B⌋} \in ℕ$
143	133 142	pccld	$⊢ ((φ \land p \in ℙ) \land \neg p ∥ R) \to p pCnt N^{⌊\log_{2} B⌋} \in ℕ_{0}$
144	143	nn0ge0d	$⊢ ((φ \land p \in ℙ) \land \neg p ∥ R) \to 0 \leq p pCnt N^{⌊\log_{2} B⌋}$
145	138 144	eqbrtrd	$⊢ ((φ \land p \in ℙ) \land \neg p ∥ R) \to p pCnt R \leq p pCnt N^{⌊\log_{2} B⌋}$
146	131 145	pm2.61dan	$⊢ (φ \land p \in ℙ) \to p pCnt R \leq p pCnt N^{⌊\log_{2} B⌋}$
147	146	ralrimiva	$⊢ φ \to \forall p \in ℙ p pCnt R \leq p pCnt N^{⌊\log_{2} B⌋}$
148	8	elfzelzd	$⊢ φ \to R \in ℤ$
149	21 93	zexpcld	$⊢ φ \to N^{⌊\log_{2} B⌋} \in ℤ$
150		pc2dvds	$⊢ (R \in ℤ \land N^{⌊\log_{2} B⌋} \in ℤ) \to (R ∥ N^{⌊\log_{2} B⌋} \leftrightarrow \forall p \in ℙ p pCnt R \leq p pCnt N^{⌊\log_{2} B⌋})$
151	148 149 150	syl2anc	$⊢ φ \to (R ∥ N^{⌊\log_{2} B⌋} \leftrightarrow \forall p \in ℙ p pCnt R \leq p pCnt N^{⌊\log_{2} B⌋})$
152	147 151	mpbird	$⊢ φ \to R ∥ N^{⌊\log_{2} B⌋}$

Metamath Proof Explorer

Theorem aks4d1p7d1

Proof