aks4d1p9

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

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

Proof

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

Metamath Proof Explorer

Theorem aks4d1p9

Proof