Theorem aks4d1p9

Description: Show that the order is bound by the squared binary logarithm. (Contributed by metakunt, 14-Nov-2024)

	Ref	Expression
Hypotheses	aks4d1p9.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
	aks4d1p9.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
	aks4d1p9.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
	aks4d1p9.4	$$⊢R=sup\left(\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\},ℝ,<\right)$$
Assertion	aks4d1p9	$$⊢\phi \to {{\log }_{2}N}^2<{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p9.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
2		aks4d1p9.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
3		aks4d1p9.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
4		aks4d1p9.4	$$⊢R=sup\left(\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\},ℝ,<\right)$$
5		2re	$$⊢2\in ℝ$$
6	5	a1i	$$⊢\phi \to 2\in ℝ$$
7		2pos	$$⊢0<2$$
8	7	a1i	$$⊢\phi \to 0<2$$
9		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{Z}$$
10	1 9	syl	$$⊢\phi \to N\in \mathbb{Z}$$
11	10	zred	$$⊢\phi \to N\in ℝ$$
12		0red	$$⊢\phi \to 0\in ℝ$$
13		3re	$$⊢3\in ℝ$$
14	13	a1i	$$⊢\phi \to 3\in ℝ$$
15		3pos	$$⊢0<3$$
16	15	a1i	$$⊢\phi \to 0<3$$
17		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 3\le N$$
18	1 17	syl	$$⊢\phi \to 3\le N$$
19	12 14 11 16 18	ltletrd	$$⊢\phi \to 0<N$$
20		1red	$$⊢\phi \to 1\in ℝ$$
21		1lt2	$$⊢1<2$$
22	21	a1i	$$⊢\phi \to 1<2$$
23	20 22	ltned	$$⊢\phi \to 1\ne 2$$
24	23	necomd	$$⊢\phi \to 2\ne 1$$
25	6 8 11 19 24	relogbcld	$$⊢\phi \to {\log }_{2}N\in ℝ$$
26	25	resqcld	$$⊢\phi \to {{\log }_{2}N}^2\in ℝ$$
27	1 2 3 4	aks4d1p4	$$⊢\phi \to \left(R\in \left(1\dots B\right)\wedge \neg R\parallel A\right)$$
28	27	simpld	$$⊢\phi \to R\in \left(1\dots B\right)$$
29		elfznn	$$⊢R\in \left(1\dots B\right)\to R\in \mathbb{N}$$
30	28 29	syl	$$⊢\phi \to R\in \mathbb{N}$$
31	1 2 3 4	aks4d1p8	$$⊢\phi \to N\gcd R=1$$
32	30 10 31	3jca	$$⊢\phi \to \left(R\in \mathbb{N}\wedge N\in \mathbb{Z}\wedge N\gcd R=1\right)$$
33		odzcl	$$⊢\left(R\in \mathbb{N}\wedge N\in \mathbb{Z}\wedge N\gcd R=1\right)\to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\in \mathbb{N}$$
34	32 33	syl	$$⊢\phi \to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\in \mathbb{N}$$
35	34	nnzd	$$⊢\phi \to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\in \mathbb{Z}$$
36		flge	$$⊢\left({{\log }_{2}N}^2\in ℝ\wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\in \mathbb{Z}\right)\to \left({\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le {{\log }_{2}N}^2\leftrightarrow {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)$$
37	26 35 36	syl2anc	$$⊢\phi \to \left({\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le {{\log }_{2}N}^2\leftrightarrow {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)$$
38	37	biimpd	$$⊢\phi \to \left({\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le {{\log }_{2}N}^2\to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)$$
39	38	imp	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le {{\log }_{2}N}^2\right)\to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋$$
40	30	nnzd	$$⊢\phi \to R\in \mathbb{Z}$$
41	40	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to R\in \mathbb{Z}$$
42	10	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to N\in \mathbb{Z}$$
43	34	nnnn0d	$$⊢\phi \to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\in {\mathbb{N}}_0$$
44	43	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\in {\mathbb{N}}_0$$
45	42 44	zexpcld	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}\in \mathbb{Z}$$
46		1zzd	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to 1\in \mathbb{Z}$$
47	45 46	zsubcld	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}-1\in \mathbb{Z}$$
48	1 3	aks4d1lem1	$$⊢\phi \to \left(B\in \mathbb{N}\wedge 9<B\right)$$
49	48	simpld	$$⊢\phi \to B\in \mathbb{N}$$
50	49	nnred	$$⊢\phi \to B\in ℝ$$
51	49	nngt0d	$$⊢\phi \to 0<B$$
52	6 8 50 51 24	relogbcld	$$⊢\phi \to {\log }_{2}B\in ℝ$$
53	52	flcld	$$⊢\phi \to ⌊{\log }_{2}B⌋\in \mathbb{Z}$$
54		2cnd	$$⊢\phi \to 2\in ℂ$$
55	12 8	gtned	$$⊢\phi \to 2\ne 0$$
56	54 55 24	3jca	$$⊢\phi \to \left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)$$
57		logb1	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)\to {\log }_{2}1=0$$
58	56 57	syl	$$⊢\phi \to {\log }_{2}1=0$$
59		2z	$$⊢2\in \mathbb{Z}$$
60	59	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
61	6	leidd	$$⊢\phi \to 2\le 2$$
62		0lt1	$$⊢0<1$$
63	62	a1i	$$⊢\phi \to 0<1$$
64	49	nnge1d	$$⊢\phi \to 1\le B$$
65	60 61 20 63 50 51 64	logblebd	$$⊢\phi \to {\log }_{2}1\le {\log }_{2}B$$
66	58 65	eqbrtrrd	$$⊢\phi \to 0\le {\log }_{2}B$$
67		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
68		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)$$
69	52 67 68	syl2anc	$$⊢\phi \to \left(0\le {\log }_{2}B\leftrightarrow 0\le ⌊{\log }_{2}B⌋\right)$$
70	66 69	mpbid	$$⊢\phi \to 0\le ⌊{\log }_{2}B⌋$$
71	53 70	jca	$$⊢\phi \to \left(⌊{\log }_{2}B⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}B⌋\right)$$
72		elnn0z	$$⊢⌊{\log }_{2}B⌋\in {\mathbb{N}}_0\leftrightarrow \left(⌊{\log }_{2}B⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}B⌋\right)$$
73	71 72	sylibr	$$⊢\phi \to ⌊{\log }_{2}B⌋\in {\mathbb{N}}_0$$
74	10 73	zexpcld	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\in \mathbb{Z}$$
75		fzfid	$$⊢\phi \to \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\in \mathrm{Fin}$$
76	10	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N\in \mathbb{Z}$$
77		elfznn	$$⊢k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\to k\in \mathbb{N}$$
78	77	nnnn0d	$$⊢k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\to k\in {\mathbb{N}}_0$$
79	78	adantl	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in {\mathbb{N}}_0$$
80	76 79	zexpcld	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k\in \mathbb{Z}$$
81		1zzd	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\in \mathbb{Z}$$
82	80 81	zsubcld	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k-1\in \mathbb{Z}$$
83	75 82	fprodzcl	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in \mathbb{Z}$$
84	74 83	zmulcld	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in \mathbb{Z}$$
85	2	a1i	$$⊢\phi \to A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
86	85	eleq1d	$$⊢\phi \to \left(A\in \mathbb{Z}\leftrightarrow N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in \mathbb{Z}\right)$$
87	84 86	mpbird	$$⊢\phi \to A\in \mathbb{Z}$$
88	87	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to A\in \mathbb{Z}$$
89		iddvds	$$⊢{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\in \mathbb{Z}\to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\parallel {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
90	35 89	syl	$$⊢\phi \to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\parallel {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
91		odzdvds	$$⊢\left(\left(R\in \mathbb{N}\wedge N\in \mathbb{Z}\wedge N\gcd R=1\right)\wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\in {\mathbb{N}}_0\right)\to \left(R\parallel \left(N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}-1\right)\leftrightarrow {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\parallel {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\right)$$
92	32 43 91	syl2anc	$$⊢\phi \to \left(R\parallel \left(N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}-1\right)\leftrightarrow {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\parallel {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\right)$$
93	90 92	mpbird	$$⊢\phi \to R\parallel \left(N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}-1\right)$$
94	93	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to R\parallel \left(N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}-1\right)$$
95	73	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to ⌊{\log }_{2}B⌋\in {\mathbb{N}}_0$$
96	42 95	zexpcld	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to N^{⌊{\log }_{2}B⌋}\in \mathbb{Z}$$
97		fzfid	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\in \mathrm{Fin}$$
98	42	adantr	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N\in \mathbb{Z}$$
99	77	adantl	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in \mathbb{N}$$
100	99	nnnn0d	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in {\mathbb{N}}_0$$
101	98 100	zexpcld	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k\in \mathbb{Z}$$
102		1zzd	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\in \mathbb{Z}$$
103	101 102	zsubcld	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k-1\in \mathbb{Z}$$
104	97 103	fprodzcl	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in \mathbb{Z}$$
105		fveq2	$$⊢z={\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\to \left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(z\right)=\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left({\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\right)$$
106	105	breq1d	$$⊢z={\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\to \left(\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(z\right)\parallel \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(k\right)\leftrightarrow \left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left({\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\right)\parallel \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(k\right)\right)$$
107		ssidd	$$⊢\phi \to \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\subseteq \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)$$
108	10	adantr	$$⊢\left(\phi \wedge x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N\in \mathbb{Z}$$
109		elfznn	$$⊢x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\to x\in \mathbb{N}$$
110	109	adantl	$$⊢\left(\phi \wedge x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to x\in \mathbb{N}$$
111	110	nnnn0d	$$⊢\left(\phi \wedge x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to x\in {\mathbb{N}}_0$$
112	108 111	zexpcld	$$⊢\left(\phi \wedge x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^x\in \mathbb{Z}$$
113		1zzd	$$⊢\left(\phi \wedge x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\in \mathbb{Z}$$
114	112 113	zsubcld	$$⊢\left(\phi \wedge x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^x-1\in \mathbb{Z}$$
115	114	fmpttd	$$⊢\phi \to \left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right):\left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟶\mathbb{Z}$$
116	75 107 115	fprodfvdvdsd	$$⊢\phi \to \forall z\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(z\right)\parallel \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(k\right)$$
117	116	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to \forall z\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(z\right)\parallel \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(k\right)$$
118	25	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to {\log }_{2}N\in ℝ$$
119	118	resqcld	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to {{\log }_{2}N}^2\in ℝ$$
120	119	flcld	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to ⌊{{\log }_{2}N}^2⌋\in \mathbb{Z}$$
121	35	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\in \mathbb{Z}$$
122	34	nnge1d	$$⊢\phi \to 1\le {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
123	122	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to 1\le {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
124		simpr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋$$
125	46 120 121 123 124	elfzd	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)$$
126	106 117 125	rspcdva	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to \left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left({\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\right)\parallel \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(k\right)$$
127		eqidd	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to \left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)=\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)$$
128		simpr	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge x={\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\right)\to x={\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
129	128	oveq2d	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge x={\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\right)\to N^x=N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}$$
130	129	oveq1d	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge x={\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\right)\to N^x-1=N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}-1$$
131	127 130 125 47	fvmptd	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to \left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left({\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\right)=N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}-1$$
132		eqidd	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to \left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)=\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)$$
133		simpr	$$⊢\left(\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\wedge x=k\right)\to x=k$$
134	133	oveq2d	$$⊢\left(\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\wedge x=k\right)\to N^x=N^k$$
135	134	oveq1d	$$⊢\left(\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\wedge x=k\right)\to N^x-1=N^k-1$$
136		simpr	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)$$
137	132 135 136 103	fvmptd	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to \left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(k\right)=N^k-1$$
138	137	prodeq2dv	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(k\right)=\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
139	131 138	breq12d	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to \left(\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left({\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\right)\parallel \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(x\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)⟼N^x-1\right)\left(k\right)\leftrightarrow \left(N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}-1\right)\parallel \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\right)$$
140	126 139	mpbid	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to \left(N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}-1\right)\parallel \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
141	47 96 104 140	dvdsmultr2d	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to \left(N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}-1\right)\parallel N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
142	2	a1i	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
143	141 142	breqtrrd	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to \left(N^{{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)}-1\right)\parallel A$$
144	41 47 88 94 143	dvdstrd	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to R\parallel A$$
145	144	ex	$$⊢\phi \to \left({\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\to R\parallel A\right)$$
146	145	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le {{\log }_{2}N}^2\right)\to \left({\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\to R\parallel A\right)$$
147	146	imp	$$⊢\left(\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le {{\log }_{2}N}^2\right)\wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le ⌊{{\log }_{2}N}^2⌋\right)\to R\parallel A$$
148	39 147	mpdan	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le {{\log }_{2}N}^2\right)\to R\parallel A$$
149	27	simprd	$$⊢\phi \to \neg R\parallel A$$
150	149	adantr	$$⊢\left(\phi \wedge {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le {{\log }_{2}N}^2\right)\to \neg R\parallel A$$
151	148 150	pm2.65da	$$⊢\phi \to \neg {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le {{\log }_{2}N}^2$$
152	34	nnred	$$⊢\phi \to {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\in ℝ$$
153	26 152	ltnled	$$⊢\phi \to \left({{\log }_{2}N}^2<{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\leftrightarrow \neg {\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)\le {{\log }_{2}N}^2\right)$$
154	151 153	mpbird	$$⊢\phi \to {{\log }_{2}N}^2<{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$