aks4d1p5

Description: Show that N and R are coprime for AKS existence theorem. Precondition will be eliminated in further theorem. (Contributed by metakunt, 30-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		aks4d1p5.1	$⊢ φ \to N \in ℤ_{\geq 3}$
2		aks4d1p5.2	$⊢ A = N^{⌊\log_{2} B⌋} \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1)$
3		aks4d1p5.3	$⊢ B = ⌈{\log_{2} N}^{5}⌉$
4		aks4d1p5.4	$⊢ R = inf (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <)$
5		aks4d1p5.5	$⊢ ((φ \land 1 < N \gcd R) \land (\frac{R}{N \gcd R}) ∥ A) \to \neg (\frac{R}{N \gcd R}) ∥ A$
6		simpr	$⊢ ((φ \land 1 < N \gcd R) \land R \leq \frac{R}{N \gcd R}) \to R \leq \frac{R}{N \gcd R}$
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	nnred	$⊢ φ \to R \in ℝ$
12		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
13	1 12	syl	$⊢ φ \to N \in ℤ$
14		0red	$⊢ φ \to 0 \in ℝ$
15		3re	$⊢ 3 \in ℝ$
16	15	a1i	$⊢ φ \to 3 \in ℝ$
17	13	zred	$⊢ φ \to N \in ℝ$
18		3pos	$⊢ 0 < 3$
19	18	a1i	$⊢ φ \to 0 < 3$
20		eluzle	$⊢ N \in ℤ_{\geq 3} \to 3 \leq N$
21	1 20	syl	$⊢ φ \to 3 \leq N$
22	14 16 17 19 21	ltletrd	$⊢ φ \to 0 < N$
23	13 22	jca	$⊢ φ \to (N \in ℤ \land 0 < N)$
24		elnnz	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N)$
25	23 24	sylibr	$⊢ φ \to N \in ℕ$
26		gcdnncl	$⊢ (N \in ℕ \land R \in ℕ) \to N \gcd R \in ℕ$
27	25 10 26	syl2anc	$⊢ φ \to N \gcd R \in ℕ$
28	27	nnred	$⊢ φ \to N \gcd R \in ℝ$
29	27	nnne0d	$⊢ φ \to N \gcd R \neq 0$
30	11 28 29	redivcld	$⊢ φ \to \frac{R}{N \gcd R} \in ℝ$
31	30	adantr	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{N \gcd R} \in ℝ$
32	11	adantr	$⊢ (φ \land 1 < N \gcd R) \to R \in ℝ$
33	31 32	ltnled	$⊢ (φ \land 1 < N \gcd R) \to (\frac{R}{N \gcd R} < R \leftrightarrow \neg R \leq \frac{R}{N \gcd R})$
34	33	biimprd	$⊢ (φ \land 1 < N \gcd R) \to (\neg R \leq \frac{R}{N \gcd R} \to \frac{R}{N \gcd R} < R)$
35	34	imp	$⊢ ((φ \land 1 < N \gcd R) \land \neg R \leq \frac{R}{N \gcd R}) \to \frac{R}{N \gcd R} < R$
36	4	a1i	$⊢ (φ \land 1 < N \gcd R) \to R = inf (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <)$
37		ssrab2	$⊢ \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq (1 \dots B)$
38	37	a1i	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq (1 \dots B)$
39		elfznn	$⊢ o \in (1 \dots B) \to o \in ℕ$
40	39	adantl	$⊢ (φ \land o \in (1 \dots B)) \to o \in ℕ$
41	40	nnred	$⊢ (φ \land o \in (1 \dots B)) \to o \in ℝ$
42	41	ex	$⊢ φ \to (o \in (1 \dots B) \to o \in ℝ)$
43	42	ssrdv	$⊢ φ \to (1 \dots B) \subseteq ℝ$
44	38 43	sstrd	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
45	44	adantr	$⊢ (φ \land 1 < N \gcd R) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
46		fzfid	$⊢ φ \to (1 \dots B) \in Fin$
47	46 38	ssfid	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin$
48	47	adantr	$⊢ (φ \land 1 < N \gcd R) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin$
49	1 2 3	aks4d1p3	$⊢ φ \to \exists r \in (1 \dots B) \neg r ∥ A$
50		rabn0	$⊢ \{r \in (1 \dots B) \| \neg r ∥ A\} \neq \emptyset \leftrightarrow \exists r \in (1 \dots B) \neg r ∥ A$
51	49 50	sylibr	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \neq \emptyset$
52	51	adantr	$⊢ (φ \land 1 < N \gcd R) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \neq \emptyset$
53		fiminre	$⊢ (\{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ \land \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin \land \{r \in (1 \dots B) \| \neg r ∥ A\} \neq \emptyset) \to \exists x \in \{r \in (1 \dots B) \| \neg r ∥ A\} \forall y \in \{r \in (1 \dots B) \| \neg r ∥ A\} x \leq y$
54	45 48 52 53	syl3anc	$⊢ (φ \land 1 < N \gcd R) \to \exists x \in \{r \in (1 \dots B) \| \neg r ∥ A\} \forall y \in \{r \in (1 \dots B) \| \neg r ∥ A\} x \leq y$
55		breq1	$⊢ r = \frac{R}{N \gcd R} \to (r ∥ A \leftrightarrow (\frac{R}{N \gcd R}) ∥ A)$
56	55	notbid	$⊢ r = \frac{R}{N \gcd R} \to (\neg r ∥ A \leftrightarrow \neg (\frac{R}{N \gcd R}) ∥ A)$
57		1zzd	$⊢ (φ \land 1 < N \gcd R) \to 1 \in ℤ$
58	3	a1i	$⊢ φ \to B = ⌈{\log_{2} N}^{5}⌉$
59		2re	$⊢ 2 \in ℝ$
60	59	a1i	$⊢ φ \to 2 \in ℝ$
61		2pos	$⊢ 0 < 2$
62	61	a1i	$⊢ φ \to 0 < 2$
63		1red	$⊢ φ \to 1 \in ℝ$
64		1lt2	$⊢ 1 < 2$
65	64	a1i	$⊢ φ \to 1 < 2$
66	63 65	ltned	$⊢ φ \to 1 \neq 2$
67	66	necomd	$⊢ φ \to 2 \neq 1$
68	60 62 17 22 67	relogbcld	$⊢ φ \to \log_{2} N \in ℝ$
69		5nn0	$⊢ 5 \in ℕ_{0}$
70	69	a1i	$⊢ φ \to 5 \in ℕ_{0}$
71	68 70	reexpcld	$⊢ φ \to {\log_{2} N}^{5} \in ℝ$
72		ceilcl	$⊢ {\log_{2} N}^{5} \in ℝ \to ⌈{\log_{2} N}^{5}⌉ \in ℤ$
73	71 72	syl	$⊢ φ \to ⌈{\log_{2} N}^{5}⌉ \in ℤ$
74	58 73	eqeltrd	$⊢ φ \to B \in ℤ$
75	74	adantr	$⊢ (φ \land 1 < N \gcd R) \to B \in ℤ$
76	25	nnzd	$⊢ φ \to N \in ℤ$
77		divgcdnnr	$⊢ (R \in ℕ \land N \in ℤ) \to \frac{R}{N \gcd R} \in ℕ$
78	10 76 77	syl2anc	$⊢ φ \to \frac{R}{N \gcd R} \in ℕ$
79	78	adantr	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{N \gcd R} \in ℕ$
80	79	nnzd	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{N \gcd R} \in ℤ$
81	79	nnge1d	$⊢ (φ \land 1 < N \gcd R) \to 1 \leq \frac{R}{N \gcd R}$
82	75	zred	$⊢ (φ \land 1 < N \gcd R) \to B \in ℝ$
83	10	nnrpd	$⊢ φ \to R \in ℝ^{+}$
84	83	adantr	$⊢ (φ \land 1 < N \gcd R) \to R \in ℝ^{+}$
85	27	nnrpd	$⊢ φ \to N \gcd R \in ℝ^{+}$
86	85	adantr	$⊢ (φ \land 1 < N \gcd R) \to N \gcd R \in ℝ^{+}$
87	32	recnd	$⊢ (φ \land 1 < N \gcd R) \to R \in ℂ$
88	84	rpne0d	$⊢ (φ \land 1 < N \gcd R) \to R \neq 0$
89	87 88	dividd	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{R} = 1$
90		simpr	$⊢ (φ \land 1 < N \gcd R) \to 1 < N \gcd R$
91	89 90	eqbrtrd	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{R} < N \gcd R$
92	32 84 86 91	ltdiv23d	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{N \gcd R} < R$
93	31 32 92	ltled	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{N \gcd R} \leq R$
94		elfzle2	$⊢ R \in (1 \dots B) \to R \leq B$
95	8 94	syl	$⊢ φ \to R \leq B$
96	95	adantr	$⊢ (φ \land 1 < N \gcd R) \to R \leq B$
97	31 32 82 93 96	letrd	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{N \gcd R} \leq B$
98	57 75 80 81 97	elfzd	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{N \gcd R} \in (1 \dots B)$
99		simpr	$⊢ ((φ \land 1 < N \gcd R) \land \neg (\frac{R}{N \gcd R}) ∥ A) \to \neg (\frac{R}{N \gcd R}) ∥ A$
100		exmidd	$⊢ (φ \land 1 < N \gcd R) \to ((\frac{R}{N \gcd R}) ∥ A \lor \neg (\frac{R}{N \gcd R}) ∥ A)$
101	5 99 100	mpjaodan	$⊢ (φ \land 1 < N \gcd R) \to \neg (\frac{R}{N \gcd R}) ∥ A$
102	56 98 101	elrabd	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{N \gcd R} \in \{r \in (1 \dots B) \| \neg r ∥ A\}$
103		lbinfle	$⊢ (\{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ \land \exists x \in \{r \in (1 \dots B) \| \neg r ∥ A\} \forall y \in \{r \in (1 \dots B) \| \neg r ∥ A\} x \leq y \land \frac{R}{N \gcd R} \in \{r \in (1 \dots B) \| \neg r ∥ A\}) \to inf (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{N \gcd R}$
104	45 54 102 103	syl3anc	$⊢ (φ \land 1 < N \gcd R) \to inf (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{N \gcd R}$
105	36 104	eqbrtrd	$⊢ (φ \land 1 < N \gcd R) \to R \leq \frac{R}{N \gcd R}$
106	32 31	lenltd	$⊢ (φ \land 1 < N \gcd R) \to (R \leq \frac{R}{N \gcd R} \leftrightarrow \neg \frac{R}{N \gcd R} < R)$
107	105 106	mpbid	$⊢ (φ \land 1 < N \gcd R) \to \neg \frac{R}{N \gcd R} < R$
108	107	adantr	$⊢ ((φ \land 1 < N \gcd R) \land \neg R \leq \frac{R}{N \gcd R}) \to \neg \frac{R}{N \gcd R} < R$
109	35 108	pm2.21dd	$⊢ ((φ \land 1 < N \gcd R) \land \neg R \leq \frac{R}{N \gcd R}) \to R \leq \frac{R}{N \gcd R}$
110	6 109	pm2.61dan	$⊢ (φ \land 1 < N \gcd R) \to R \leq \frac{R}{N \gcd R}$
111	83	rpred	$⊢ φ \to R \in ℝ$
112	111	adantr	$⊢ (φ \land 1 < N \gcd R) \to R \in ℝ$
113	92 107	pm2.21dd	$⊢ (φ \land 1 < N \gcd R) \to N \gcd R \in ℕ$
114	113	nnrpd	$⊢ (φ \land 1 < N \gcd R) \to N \gcd R \in ℝ^{+}$
115	112	recnd	$⊢ (φ \land 1 < N \gcd R) \to R \in ℂ$
116	115 88	dividd	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{R} = 1$
117	116 90	eqbrtrd	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{R} < N \gcd R$
118	112 84 114 117	ltdiv23d	$⊢ (φ \land 1 < N \gcd R) \to \frac{R}{N \gcd R} < R$
119	78	nnred	$⊢ φ \to \frac{R}{N \gcd R} \in ℝ$
120	119 111	ltnled	$⊢ φ \to (\frac{R}{N \gcd R} < R \leftrightarrow \neg R \leq \frac{R}{N \gcd R})$
121	120	adantr	$⊢ (φ \land 1 < N \gcd R) \to (\frac{R}{N \gcd R} < R \leftrightarrow \neg R \leq \frac{R}{N \gcd R})$
122	118 121	mpbid	$⊢ (φ \land 1 < N \gcd R) \to \neg R \leq \frac{R}{N \gcd R}$
123	110 122	pm2.21dd	$⊢ (φ \land 1 < N \gcd R) \to N \gcd R = 1$
124		simpr	$⊢ ((φ \land \neg 1 < N \gcd R) \land N \gcd R = 1) \to N \gcd R = 1$
125	27	adantr	$⊢ (φ \land \neg 1 < N \gcd R) \to N \gcd R \in ℕ$
126	125	nnred	$⊢ (φ \land \neg 1 < N \gcd R) \to N \gcd R \in ℝ$
127	126	adantr	$⊢ ((φ \land \neg 1 < N \gcd R) \land N \gcd R \in ℤ_{\geq 2}) \to N \gcd R \in ℝ$
128	59	a1i	$⊢ ((φ \land \neg 1 < N \gcd R) \land N \gcd R \in ℤ_{\geq 2}) \to 2 \in ℝ$
129		1red	$⊢ ((φ \land \neg 1 < N \gcd R) \land N \gcd R \in ℤ_{\geq 2}) \to 1 \in ℝ$
130	28 63	lenltd	$⊢ φ \to (N \gcd R \leq 1 \leftrightarrow \neg 1 < N \gcd R)$
131	130	biimprd	$⊢ φ \to (\neg 1 < N \gcd R \to N \gcd R \leq 1)$
132	131	imp	$⊢ (φ \land \neg 1 < N \gcd R) \to N \gcd R \leq 1$
133	132	adantr	$⊢ ((φ \land \neg 1 < N \gcd R) \land N \gcd R \in ℤ_{\geq 2}) \to N \gcd R \leq 1$
134	64	a1i	$⊢ ((φ \land \neg 1 < N \gcd R) \land N \gcd R \in ℤ_{\geq 2}) \to 1 < 2$
135	127 129 128 133 134	lelttrd	$⊢ ((φ \land \neg 1 < N \gcd R) \land N \gcd R \in ℤ_{\geq 2}) \to N \gcd R < 2$
136		eluzle	$⊢ N \gcd R \in ℤ_{\geq 2} \to 2 \leq N \gcd R$
137	136	adantl	$⊢ ((φ \land \neg 1 < N \gcd R) \land N \gcd R \in ℤ_{\geq 2}) \to 2 \leq N \gcd R$
138	127 128 127 135 137	ltletrd	$⊢ ((φ \land \neg 1 < N \gcd R) \land N \gcd R \in ℤ_{\geq 2}) \to N \gcd R < N \gcd R$
139	127	ltnrd	$⊢ ((φ \land \neg 1 < N \gcd R) \land N \gcd R \in ℤ_{\geq 2}) \to \neg N \gcd R < N \gcd R$
140	138 139	pm2.21dd	$⊢ ((φ \land \neg 1 < N \gcd R) \land N \gcd R \in ℤ_{\geq 2}) \to N \gcd R = 1$
141		elnn1uz2	$⊢ N \gcd R \in ℕ \leftrightarrow (N \gcd R = 1 \lor N \gcd R \in ℤ_{\geq 2})$
142	125 141	sylib	$⊢ (φ \land \neg 1 < N \gcd R) \to (N \gcd R = 1 \lor N \gcd R \in ℤ_{\geq 2})$
143	124 140 142	mpjaodan	$⊢ (φ \land \neg 1 < N \gcd R) \to N \gcd R = 1$
144	123 143	pm2.61dan	$⊢ φ \to N \gcd R = 1$

Metamath Proof Explorer

Theorem aks4d1p5

Proof