Theorem aks4d1p3

Description: There exists a small enough number such that it does not divide A . (Contributed by metakunt, 27-Oct-2024)

	Ref	Expression
Hypotheses	aks4d1p3.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
	aks4d1p3.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
	aks4d1p3.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
Assertion	aks4d1p3	$$⊢\phi \to \exists r\in \left(1\dots B\right)\neg r\parallel A$$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p3.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
2		aks4d1p3.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
3		aks4d1p3.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
4	1 2 3	aks4d1p1	$$⊢\phi \to A<2^B$$
5	4	adantr	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to A<2^B$$
6		2re	$$⊢2\in ℝ$$
7	6	a1i	$$⊢\phi \to 2\in ℝ$$
8	3	a1i	$$⊢\phi \to B=⌈{{\log }_{2}N}^5⌉$$
9		2pos	$$⊢0<2$$
10	9	a1i	$$⊢\phi \to 0<2$$
11		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{Z}$$
12	1 11	syl	$$⊢\phi \to N\in \mathbb{Z}$$
13	12	zred	$$⊢\phi \to N\in ℝ$$
14		0red	$$⊢\phi \to 0\in ℝ$$
15		3re	$$⊢3\in ℝ$$
16	15	a1i	$$⊢\phi \to 3\in ℝ$$
17		3pos	$$⊢0<3$$
18	17	a1i	$$⊢\phi \to 0<3$$
19		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 3\le N$$
20	1 19	syl	$$⊢\phi \to 3\le N$$
21	14 16 13 18 20	ltletrd	$$⊢\phi \to 0<N$$
22		1red	$$⊢\phi \to 1\in ℝ$$
23		1lt2	$$⊢1<2$$
24	23	a1i	$$⊢\phi \to 1<2$$
25	22 24	ltned	$$⊢\phi \to 1\ne 2$$
26	25	necomd	$$⊢\phi \to 2\ne 1$$
27	7 10 13 21 26	relogbcld	$$⊢\phi \to {\log }_{2}N\in ℝ$$
28		5nn0	$$⊢5\in {\mathbb{N}}_0$$
29	28	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
30	27 29	reexpcld	$$⊢\phi \to {{\log }_{2}N}^5\in ℝ$$
31		ceilcl	$$⊢{{\log }_{2}N}^5\in ℝ\to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
32	30 31	syl	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
33	8 32	eqeltrd	$$⊢\phi \to B\in \mathbb{Z}$$
34	32	zred	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in ℝ$$
35	8 34	eqeltrd	$$⊢\phi \to B\in ℝ$$
36		7re	$$⊢7\in ℝ$$
37	36	a1i	$$⊢\phi \to 7\in ℝ$$
38		7pos	$$⊢0<7$$
39	38	a1i	$$⊢\phi \to 0<7$$
40	13 20	3lexlogpow5ineq3	$$⊢\phi \to 7<{{\log }_{2}N}^5$$
41	14 37 30 39 40	lttrd	$$⊢\phi \to 0<{{\log }_{2}N}^5$$
42		ceilge	$$⊢{{\log }_{2}N}^5\in ℝ\to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
43	30 42	syl	$$⊢\phi \to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
44	14 30 34 41 43	ltletrd	$$⊢\phi \to 0<⌈{{\log }_{2}N}^5⌉$$
45	44 8	breqtrrd	$$⊢\phi \to 0<B$$
46	14 35 45	ltled	$$⊢\phi \to 0\le B$$
47	33 46	jca	$$⊢\phi \to \left(B\in \mathbb{Z}\wedge 0\le B\right)$$
48		elnn0z	$$⊢B\in {\mathbb{N}}_0\leftrightarrow \left(B\in \mathbb{Z}\wedge 0\le B\right)$$
49	47 48	sylibr	$$⊢\phi \to B\in {\mathbb{N}}_0$$
50	7 49	reexpcld	$$⊢\phi \to 2^B\in ℝ$$
51	50	adantr	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to 2^B\in ℝ$$
52		elfznn	$$⊢q\in \left(1\dots B\right)\to q\in \mathbb{N}$$
53	52	adantl	$$⊢\left(\phi \wedge q\in \left(1\dots B\right)\right)\to q\in \mathbb{N}$$
54	53	nnzd	$$⊢\left(\phi \wedge q\in \left(1\dots B\right)\right)\to q\in \mathbb{Z}$$
55	54	ex	$$⊢\phi \to \left(q\in \left(1\dots B\right)\to q\in \mathbb{Z}\right)$$
56	55	ssrdv	$$⊢\phi \to \left(1\dots B\right)\subseteq \mathbb{Z}$$
57		fzfid	$$⊢\phi \to \left(1\dots B\right)\in \mathrm{Fin}$$
58		lcmfcl	$$⊢\left(\left(1\dots B\right)\subseteq \mathbb{Z}\wedge \left(1\dots B\right)\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\in {\mathbb{N}}_0$$
59	56 57 58	syl2anc	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\in {\mathbb{N}}_0$$
60	59	nn0red	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\in ℝ$$
61	60	adantr	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\in ℝ$$
62	2	a1i	$$⊢\phi \to A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
63		elnnz	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in \mathbb{Z}\wedge 0<N\right)$$
64	12 21 63	sylanbrc	$$⊢\phi \to N\in \mathbb{N}$$
65	7 10 35 45 26	relogbcld	$$⊢\phi \to {\log }_{2}B\in ℝ$$
66	65	flcld	$$⊢\phi \to ⌊{\log }_{2}B⌋\in \mathbb{Z}$$
67	7 10 7 10 26	relogbcld	$$⊢\phi \to {\log }_{2}2\in ℝ$$
68		0le1	$$⊢0\le 1$$
69	68	a1i	$$⊢\phi \to 0\le 1$$
70	7	recnd	$$⊢\phi \to 2\in ℂ$$
71	14 10	gtned	$$⊢\phi \to 2\ne 0$$
72		logbid1	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)\to {\log }_{2}2=1$$
73	70 71 26 72	syl3anc	$$⊢\phi \to {\log }_{2}2=1$$
74	73	eqcomd	$$⊢\phi \to 1={\log }_{2}2$$
75	69 74	breqtrd	$$⊢\phi \to 0\le {\log }_{2}2$$
76		2z	$$⊢2\in \mathbb{Z}$$
77	76	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
78	7	leidd	$$⊢\phi \to 2\le 2$$
79		2lt7	$$⊢2<7$$
80	79	a1i	$$⊢\phi \to 2<7$$
81	7 37 80	ltled	$$⊢\phi \to 2\le 7$$
82	37 30 34 40 43	ltletrd	$$⊢\phi \to 7<⌈{{\log }_{2}N}^5⌉$$
83	82 8	breqtrrd	$$⊢\phi \to 7<B$$
84	37 35 83	ltled	$$⊢\phi \to 7\le B$$
85	7 37 35 81 84	letrd	$$⊢\phi \to 2\le B$$
86	77 78 7 10 35 45 85	logblebd	$$⊢\phi \to {\log }_{2}2\le {\log }_{2}B$$
87	14 67 65 75 86	letrd	$$⊢\phi \to 0\le {\log }_{2}B$$
88		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
89		flge	$$⊢\left({\log }_{2}B\in ℝ\wedge 0\in \mathbb{Z}\right)\to \left(0\le {\log }_{2}B\leftrightarrow 0\le ⌊{\log }_{2}B⌋\right)$$
90	65 88 89	syl2anc	$$⊢\phi \to \left(0\le {\log }_{2}B\leftrightarrow 0\le ⌊{\log }_{2}B⌋\right)$$
91	87 90	mpbid	$$⊢\phi \to 0\le ⌊{\log }_{2}B⌋$$
92	66 91	jca	$$⊢\phi \to \left(⌊{\log }_{2}B⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}B⌋\right)$$
93		elnn0z	$$⊢⌊{\log }_{2}B⌋\in {\mathbb{N}}_0\leftrightarrow \left(⌊{\log }_{2}B⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}B⌋\right)$$
94	92 93	sylibr	$$⊢\phi \to ⌊{\log }_{2}B⌋\in {\mathbb{N}}_0$$
95	64 94	nnexpcld	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\in \mathbb{N}$$
96		fzfid	$$⊢\phi \to \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\in \mathrm{Fin}$$
97	12	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N\in \mathbb{Z}$$
98		elfznn	$$⊢k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\to k\in \mathbb{N}$$
99	98	adantl	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in \mathbb{N}$$
100	99	nnnn0d	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in {\mathbb{N}}_0$$
101		zexpcl	$$⊢\left(N\in \mathbb{Z}\wedge k\in {\mathbb{N}}_0\right)\to N^k\in \mathbb{Z}$$
102	97 100 101	syl2anc	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k\in \mathbb{Z}$$
103		1zzd	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\in \mathbb{Z}$$
104	102 103	zsubcld	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k-1\in \mathbb{Z}$$
105		1cnd	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\in ℂ$$
106	105	addid1d	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1+0=1$$
107	22	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\in ℝ$$
108		1nn0	$$⊢1\in {\mathbb{N}}_0$$
109	108	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
110	13 109	reexpcld	$$⊢\phi \to N^1\in ℝ$$
111	110	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^1\in ℝ$$
112	102	zred	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k\in ℝ$$
113		1lt3	$$⊢1<3$$
114	113	a1i	$$⊢\phi \to 1<3$$
115	22 16 13 114 20	ltletrd	$$⊢\phi \to 1<N$$
116	13	recnd	$$⊢\phi \to N\in ℂ$$
117	116	exp1d	$$⊢\phi \to N^1=N$$
118	117	eqcomd	$$⊢\phi \to N=N^1$$
119	115 118	breqtrd	$$⊢\phi \to 1<N^1$$
120	119	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1<N^1$$
121	13	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N\in ℝ$$
122	64	nnge1d	$$⊢\phi \to 1\le N$$
123	122	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\le N$$
124		elfzuz	$$⊢k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\to k\in {\mathbb{Z}}_{\ge 1}$$
125	124	adantl	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in {\mathbb{Z}}_{\ge 1}$$
126	121 123 125	leexp2ad	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^1\le N^k$$
127	107 111 112 120 126	ltletrd	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1<N^k$$
128	106 127	eqbrtrd	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1+0<N^k$$
129	14	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 0\in ℝ$$
130	107 129 112	ltaddsub2d	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to \left(1+0<N^k\leftrightarrow 0<N^k-1\right)$$
131	128 130	mpbid	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 0<N^k-1$$
132	104 131	jca	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to \left(N^k-1\in \mathbb{Z}\wedge 0<N^k-1\right)$$
133		elnnz	$$⊢N^k-1\in \mathbb{N}\leftrightarrow \left(N^k-1\in \mathbb{Z}\wedge 0<N^k-1\right)$$
134	132 133	sylibr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k-1\in \mathbb{N}$$
135	96 134	fprodnncl	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in \mathbb{N}$$
136	95 135	nnmulcld	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in \mathbb{N}$$
137	62 136	eqeltrd	$$⊢\phi \to A\in \mathbb{N}$$
138	137	nnred	$$⊢\phi \to A\in ℝ$$
139	138	adantr	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to A\in ℝ$$
140	1 2 3	aks4d1p2	$$⊢\phi \to 2^B\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)$$
141	140	adantr	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to 2^B\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)$$
142	137	nnzd	$$⊢\phi \to A\in \mathbb{Z}$$
143	142	adantr	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to A\in \mathbb{Z}$$
144	56	adantr	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \left(1\dots B\right)\subseteq \mathbb{Z}$$
145		fzfid	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \left(1\dots B\right)\in \mathrm{Fin}$$
146		lcmfdvdsb	$$⊢\left(A\in \mathbb{Z}\wedge \left(1\dots B\right)\subseteq \mathbb{Z}\wedge \left(1\dots B\right)\in \mathrm{Fin}\right)\to \left(\forall r\in \left(1\dots B\right)r\parallel A\leftrightarrow \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\parallel A\right)$$
147	143 144 145 146	syl3anc	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \left(\forall r\in \left(1\dots B\right)r\parallel A\leftrightarrow \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\parallel A\right)$$
148	147	biimpd	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \left(\forall r\in \left(1\dots B\right)r\parallel A\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\parallel A\right)$$
149	148	syldbl2	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\parallel A$$
150	59	nn0zd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\in \mathbb{Z}$$
151	150	adantr	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\in \mathbb{Z}$$
152	137	adantr	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to A\in \mathbb{N}$$
153		dvdsle	$$⊢\left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\in \mathbb{Z}\wedge A\in \mathbb{N}\right)\to \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\parallel A\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\le A\right)$$
154	151 152 153	syl2anc	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\parallel A\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\le A\right)$$
155	149 154	mpd	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots B\right)\right)\le A$$
156	51 61 139 141 155	letrd	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to 2^B\le A$$
157	51 139	lenltd	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \left(2^B\le A\leftrightarrow \neg A<2^B\right)$$
158	156 157	mpbid	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \neg A<2^B$$
159	5 158	pm2.21dd	$$⊢\left(\phi \wedge \forall r\in \left(1\dots B\right)r\parallel A\right)\to \neg \forall r\in \left(1\dots B\right)r\parallel A$$
160		simpr	$$⊢\left(\phi \wedge \neg \forall r\in \left(1\dots B\right)r\parallel A\right)\to \neg \forall r\in \left(1\dots B\right)r\parallel A$$
161	159 160	pm2.61dan	$$⊢\phi \to \neg \forall r\in \left(1\dots B\right)r\parallel A$$
162		rexnal	$$⊢\exists r\in \left(1\dots B\right)\neg r\parallel A\leftrightarrow \neg \forall r\in \left(1\dots B\right)r\parallel A$$
163	161 162	sylibr	$$⊢\phi \to \exists r\in \left(1\dots B\right)\neg r\parallel A$$