aks4d1p8

Description: Show that N and R are coprime for AKS existence theorem, with eliminated hypothesis. (Contributed by metakunt, 10-Nov-2024) (Proof sketch by Thierry Arnoux.)

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

Proof

Step	Hyp	Ref	Expression
1		aks4d1p8.1	$⊢ φ \to N \in ℤ_{\geq 3}$
2		aks4d1p8.2	$⊢ A = N^{⌊\log_{2} B⌋} \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1)$
3		aks4d1p8.3	$⊢ B = ⌈{\log_{2} N}^{5}⌉$
4		aks4d1p8.4	$⊢ R = sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <)$
5	4	a1i	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to R = sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <)$
6		ssrab2	$⊢ \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq (1 \dots B)$
7	6	a1i	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq (1 \dots B)$
8		elfznn	$⊢ o \in (1 \dots B) \to o \in ℕ$
9	8	adantl	$⊢ (φ \land o \in (1 \dots B)) \to o \in ℕ$
10	9	nnred	$⊢ (φ \land o \in (1 \dots B)) \to o \in ℝ$
11	10	ex	$⊢ φ \to (o \in (1 \dots B) \to o \in ℝ)$
12	11	ssrdv	$⊢ φ \to (1 \dots B) \subseteq ℝ$
13	7 12	sstrd	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
14	13	adantr	$⊢ (φ \land 1 < N \gcd R) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
15	14	adantr	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
16	15	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
17	16	adantr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
18		fzfid	$⊢ φ \to (1 \dots B) \in Fin$
19	18 7	ssfid	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin$
20	1 2 3	aks4d1p3	$⊢ φ \to \exists r \in (1 \dots B) \neg r ∥ A$
21		rabn0	$⊢ \{r \in (1 \dots B) \| \neg r ∥ A\} \neq \emptyset \leftrightarrow \exists r \in (1 \dots B) \neg r ∥ A$
22	20 21	sylibr	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \neq \emptyset$
23		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$
24	13 19 22 23	syl3anc	$⊢ φ \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$
25	24	adantr	$⊢ (φ \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$
26	25	adantr	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \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$
27	26	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \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$
28	27	adantr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \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$
29		breq1	$⊢ r = \frac{R}{p} \to (r ∥ A \leftrightarrow (\frac{R}{p}) ∥ A)$
30	29	notbid	$⊢ r = \frac{R}{p} \to (\neg r ∥ A \leftrightarrow \neg (\frac{R}{p}) ∥ A)$
31		1zzd	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to 1 \in ℤ$
32	3	a1i	$⊢ φ \to B = ⌈{\log_{2} N}^{5}⌉$
33		2re	$⊢ 2 \in ℝ$
34	33	a1i	$⊢ φ \to 2 \in ℝ$
35		2pos	$⊢ 0 < 2$
36	35	a1i	$⊢ φ \to 0 < 2$
37		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
38	1 37	syl	$⊢ φ \to N \in ℤ$
39	38	zred	$⊢ φ \to N \in ℝ$
40		0red	$⊢ φ \to 0 \in ℝ$
41		3re	$⊢ 3 \in ℝ$
42	41	a1i	$⊢ φ \to 3 \in ℝ$
43		3pos	$⊢ 0 < 3$
44	43	a1i	$⊢ φ \to 0 < 3$
45		eluzle	$⊢ N \in ℤ_{\geq 3} \to 3 \leq N$
46	1 45	syl	$⊢ φ \to 3 \leq N$
47	40 42 39 44 46	ltletrd	$⊢ φ \to 0 < N$
48		1red	$⊢ φ \to 1 \in ℝ$
49		1lt2	$⊢ 1 < 2$
50	49	a1i	$⊢ φ \to 1 < 2$
51	48 50	ltned	$⊢ φ \to 1 \neq 2$
52	51	necomd	$⊢ φ \to 2 \neq 1$
53	34 36 39 47 52	relogbcld	$⊢ φ \to \log_{2} N \in ℝ$
54		5nn0	$⊢ 5 \in ℕ_{0}$
55	54	a1i	$⊢ φ \to 5 \in ℕ_{0}$
56	53 55	reexpcld	$⊢ φ \to {\log_{2} N}^{5} \in ℝ$
57	56	ceilcld	$⊢ φ \to ⌈{\log_{2} N}^{5}⌉ \in ℤ$
58	32 57	eqeltrd	$⊢ φ \to B \in ℤ$
59	58	ad4antr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to B \in ℤ$
60		simplrl	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to p ∥ R$
61		prmnn	$⊢ p \in ℙ \to p \in ℕ$
62	61	adantl	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to p \in ℕ$
63	62	ad2antrr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to p \in ℕ$
64	63	nnzd	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to p \in ℤ$
65	62	nnne0d	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to p \neq 0$
66	65	ad2antrr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to p \neq 0$
67	1 2 3 4	aks4d1p4	$⊢ φ \to (R \in (1 \dots B) \land \neg R ∥ A)$
68	67	simpld	$⊢ φ \to R \in (1 \dots B)$
69		elfznn	$⊢ R \in (1 \dots B) \to R \in ℕ$
70	68 69	syl	$⊢ φ \to R \in ℕ$
71	70	ad4antr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land p ∥ R) \land \neg p ∥ N) \to R \in ℕ$
72	71	adantr	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land p ∥ R) \land \neg p ∥ N) \land (\frac{R}{N \gcd R}) ∥ A) \to R \in ℕ$
73	72	nnzd	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land p ∥ R) \land \neg p ∥ N) \land (\frac{R}{N \gcd R}) ∥ A) \to R \in ℤ$
74		anass	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land p ∥ R) \land \neg p ∥ N) \leftrightarrow (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N))$
75	74	anbi1i	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land p ∥ R) \land \neg p ∥ N) \land (\frac{R}{N \gcd R}) ∥ A) \leftrightarrow ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A)$
76	75	imbi1i	$⊢ ((((((φ \land 1 < N \gcd R) \land p \in ℙ) \land p ∥ R) \land \neg p ∥ N) \land (\frac{R}{N \gcd R}) ∥ A) \to R \in ℤ) \leftrightarrow (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to R \in ℤ)$
77	73 76	mpbi	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to R \in ℤ$
78		dvdsval2	$⊢ (p \in ℤ \land p \neq 0 \land R \in ℤ) \to (p ∥ R \leftrightarrow \frac{R}{p} \in ℤ)$
79	64 66 77 78	syl3anc	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to (p ∥ R \leftrightarrow \frac{R}{p} \in ℤ)$
80	60 79	mpbid	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \frac{R}{p} \in ℤ$
81	63	nncnd	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to p \in ℂ$
82	81	mulid2d	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to 1 p = p$
83	75 72	sylbir	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to R \in ℕ$
84	64 83	jca	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to (p \in ℤ \land R \in ℕ)$
85		dvdsle	$⊢ (p \in ℤ \land R \in ℕ) \to (p ∥ R \to p \leq R)$
86	85	imp	$⊢ ((p \in ℤ \land R \in ℕ) \land p ∥ R) \to p \leq R$
87	84 60 86	syl2anc	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to p \leq R$
88	82 87	eqbrtrd	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to 1 p \leq R$
89		1red	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to 1 \in ℝ$
90	70	nnred	$⊢ φ \to R \in ℝ$
91	90	adantr	$⊢ (φ \land 1 < N \gcd R) \to R \in ℝ$
92	91	adantr	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to R \in ℝ$
93	92	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to R \in ℝ$
94	93	adantr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to R \in ℝ$
95	63	nnrpd	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to p \in ℝ^{+}$
96	89 94 95	lemuldivd	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to (1 p \leq R \leftrightarrow 1 \leq \frac{R}{p})$
97	88 96	mpbid	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to 1 \leq \frac{R}{p}$
98	90	ad2antrr	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to R \in ℝ$
99	58	ad2antrr	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to B \in ℤ$
100	99	zred	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to B \in ℝ$
101	62	nnred	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to p \in ℝ$
102	100 101	remulcld	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to B p \in ℝ$
103		elfzle2	$⊢ R \in (1 \dots B) \to R \leq B$
104	68 103	syl	$⊢ φ \to R \leq B$
105	104	adantr	$⊢ (φ \land 1 < N \gcd R) \to R \leq B$
106	105	adantr	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to R \leq B$
107	58	zred	$⊢ φ \to B \in ℝ$
108		9re	$⊢ 9 \in ℝ$
109	108	a1i	$⊢ φ \to 9 \in ℝ$
110		9pos	$⊢ 0 < 9$
111	110	a1i	$⊢ φ \to 0 < 9$
112	32 107	eqeltrrd	$⊢ φ \to ⌈{\log_{2} N}^{5}⌉ \in ℝ$
113	39 46	3lexlogpow5ineq4	$⊢ φ \to 9 < {\log_{2} N}^{5}$
114	56	ceilged	$⊢ φ \to {\log_{2} N}^{5} \leq ⌈{\log_{2} N}^{5}⌉$
115	109 56 112 113 114	ltletrd	$⊢ φ \to 9 < ⌈{\log_{2} N}^{5}⌉$
116	115 32	breqtrrd	$⊢ φ \to 9 < B$
117	40 109 107 111 116	lttrd	$⊢ φ \to 0 < B$
118	40 107 117	ltled	$⊢ φ \to 0 \leq B$
119	118	adantr	$⊢ (φ \land 1 < N \gcd R) \to 0 \leq B$
120	119	adantr	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to 0 \leq B$
121	62	nnge1d	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to 1 \leq p$
122	100 101 120 121	lemulge11d	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to B \leq B p$
123	98 100 102 106 122	letrd	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to R \leq B p$
124	62	nnrpd	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to p \in ℝ^{+}$
125	98 100 124	ledivmul2d	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to (\frac{R}{p} \leq B \leftrightarrow R \leq B p)$
126	123 125	mpbird	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to \frac{R}{p} \leq B$
127	126	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \frac{R}{p} \leq B$
128	127	adantr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \frac{R}{p} \leq B$
129	31 59 80 97 128	elfzd	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \frac{R}{p} \in (1 \dots B)$
130	93	recnd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to R \in ℂ$
131	62	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p \in ℕ$
132	131	nnzd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p \in ℤ$
133		simplr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p \in ℙ$
134	71	anasss	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to R \in ℕ$
135	133 134	pccld	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p pCnt R \in ℕ_{0}$
136	132 135	zexpcld	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{p pCnt R} \in ℤ$
137	136	zcnd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{p pCnt R} \in ℂ$
138	131	nncnd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p \in ℂ$
139	65	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p \neq 0$
140	135	nn0zd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p pCnt R \in ℤ$
141	138 139 140	expne0d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{p pCnt R} \neq 0$
142	130 137 141	divcan1d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (\frac{R}{p^{p pCnt R}}) p^{p pCnt R} = R$
143	142	eqcomd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to R = (\frac{R}{p^{p pCnt R}}) p^{p pCnt R}$
144		pcdvds	$⊢ (p \in ℙ \land R \in ℕ) \to p^{p pCnt R} ∥ R$
145	133 134 144	syl2anc	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{p pCnt R} ∥ R$
146	134	nnzd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to R \in ℤ$
147		dvdsval2	$⊢ (p^{p pCnt R} \in ℤ \land p^{p pCnt R} \neq 0 \land R \in ℤ) \to (p^{p pCnt R} ∥ R \leftrightarrow \frac{R}{p^{p pCnt R}} \in ℤ)$
148	136 141 146 147	syl3anc	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (p^{p pCnt R} ∥ R \leftrightarrow \frac{R}{p^{p pCnt R}} \in ℤ)$
149	145 148	mpbid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \frac{R}{p^{p pCnt R}} \in ℤ$
150	38 47	jca	$⊢ φ \to (N \in ℤ \land 0 < N)$
151		elnnz	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N)$
152	151	a1i	$⊢ φ \to (N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N))$
153	150 152	mpbird	$⊢ φ \to N \in ℕ$
154	153	nnzd	$⊢ φ \to N \in ℤ$
155	34 36 107 117 52	relogbcld	$⊢ φ \to \log_{2} B \in ℝ$
156	155	flcld	$⊢ φ \to ⌊\log_{2} B⌋ \in ℤ$
157	34	recnd	$⊢ φ \to 2 \in ℂ$
158	40 36	gtned	$⊢ φ \to 2 \neq 0$
159		logb1	$⊢ (2 \in ℂ \land 2 \neq 0 \land 2 \neq 1) \to \log_{2} 1 = 0$
160	157 158 52 159	syl3anc	$⊢ φ \to \log_{2} 1 = 0$
161	160	eqcomd	$⊢ φ \to 0 = \log_{2} 1$
162		2z	$⊢ 2 \in ℤ$
163	162	a1i	$⊢ φ \to 2 \in ℤ$
164	34	leidd	$⊢ φ \to 2 \leq 2$
165		0lt1	$⊢ 0 < 1$
166	165	a1i	$⊢ φ \to 0 < 1$
167		1lt9	$⊢ 1 < 9$
168	167	a1i	$⊢ φ \to 1 < 9$
169	48 109 107 168 116	lttrd	$⊢ φ \to 1 < B$
170	48 107 169	ltled	$⊢ φ \to 1 \leq B$
171	163 164 48 166 107 117 170	logblebd	$⊢ φ \to \log_{2} 1 \leq \log_{2} B$
172	161 171	eqbrtrd	$⊢ φ \to 0 \leq \log_{2} B$
173		0zd	$⊢ φ \to 0 \in ℤ$
174		flge	$⊢ (\log_{2} B \in ℝ \land 0 \in ℤ) \to (0 \leq \log_{2} B \leftrightarrow 0 \leq ⌊\log_{2} B⌋)$
175	155 173 174	syl2anc	$⊢ φ \to (0 \leq \log_{2} B \leftrightarrow 0 \leq ⌊\log_{2} B⌋)$
176	172 175	mpbid	$⊢ φ \to 0 \leq ⌊\log_{2} B⌋$
177	156 176	jca	$⊢ φ \to (⌊\log_{2} B⌋ \in ℤ \land 0 \leq ⌊\log_{2} B⌋)$
178		elnn0z	$⊢ ⌊\log_{2} B⌋ \in ℕ_{0} \leftrightarrow (⌊\log_{2} B⌋ \in ℤ \land 0 \leq ⌊\log_{2} B⌋)$
179	178	a1i	$⊢ φ \to (⌊\log_{2} B⌋ \in ℕ_{0} \leftrightarrow (⌊\log_{2} B⌋ \in ℤ \land 0 \leq ⌊\log_{2} B⌋))$
180	177 179	mpbird	$⊢ φ \to ⌊\log_{2} B⌋ \in ℕ_{0}$
181	154 180	zexpcld	$⊢ φ \to N^{⌊\log_{2} B⌋} \in ℤ$
182		fzfid	$⊢ φ \to (1 \dots ⌊{\log_{2} N}^{2}⌋) \in Fin$
183	154	adantr	$⊢ (φ \land k \in (1 \dots ⌊{\log_{2} N}^{2}⌋)) \to N \in ℤ$
184		elfznn	$⊢ k \in (1 \dots ⌊{\log_{2} N}^{2}⌋) \to k \in ℕ$
185	184	adantl	$⊢ (φ \land k \in (1 \dots ⌊{\log_{2} N}^{2}⌋)) \to k \in ℕ$
186	185	nnnn0d	$⊢ (φ \land k \in (1 \dots ⌊{\log_{2} N}^{2}⌋)) \to k \in ℕ_{0}$
187	183 186	zexpcld	$⊢ (φ \land k \in (1 \dots ⌊{\log_{2} N}^{2}⌋)) \to N^{k} \in ℤ$
188		1zzd	$⊢ (φ \land k \in (1 \dots ⌊{\log_{2} N}^{2}⌋)) \to 1 \in ℤ$
189	187 188	zsubcld	$⊢ (φ \land k \in (1 \dots ⌊{\log_{2} N}^{2}⌋)) \to N^{k} - 1 \in ℤ$
190	182 189	fprodzcl	$⊢ φ \to \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1) \in ℤ$
191	181 190	zmulcld	$⊢ φ \to N^{⌊\log_{2} B⌋} \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1) \in ℤ$
192	2	a1i	$⊢ φ \to A = N^{⌊\log_{2} B⌋} \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1)$
193	192	eleq1d	$⊢ φ \to (A \in ℤ \leftrightarrow N^{⌊\log_{2} B⌋} \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1) \in ℤ)$
194	191 193	mpbird	$⊢ φ \to A \in ℤ$
195	194	ad3antrrr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to A \in ℤ$
196		simprl	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p ∥ R$
197	134 133 196	aks4d1p8d3	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (\frac{R}{p^{p pCnt R}}) \gcd p^{p pCnt R} = 1$
198	138	exp0d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{0} = 1$
199		pcelnn	$⊢ (p \in ℙ \land R \in ℕ) \to (p pCnt R \in ℕ \leftrightarrow p ∥ R)$
200	133 134 199	syl2anc	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (p pCnt R \in ℕ \leftrightarrow p ∥ R)$
201	196 200	mpbird	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p pCnt R \in ℕ$
202	201	nngt0d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 0 < p pCnt R$
203	101	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p \in ℝ$
204	173	ad3antrrr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 0 \in ℤ$
205		prmgt1	$⊢ p \in ℙ \to 1 < p$
206	205	adantl	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to 1 < p$
207	206	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 1 < p$
208	203 204 140 207	ltexp2d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (0 < p pCnt R \leftrightarrow p^{0} < p^{p pCnt R})$
209	202 208	mpbid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{0} < p^{p pCnt R}$
210	198 209	eqbrtrrd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 1 < p^{p pCnt R}$
211	136	zred	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{p pCnt R} \in ℝ$
212	70	nnrpd	$⊢ φ \to R \in ℝ^{+}$
213	212	adantr	$⊢ (φ \land 1 < N \gcd R) \to R \in ℝ^{+}$
214	213	adantr	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to R \in ℝ^{+}$
215	214	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to R \in ℝ^{+}$
216	211 215	ltmulgt11d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (1 < p^{p pCnt R} \leftrightarrow R < R p^{p pCnt R})$
217	210 216	mpbid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to R < R p^{p pCnt R}$
218	124	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p \in ℝ^{+}$
219	218 140	rpexpcld	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{p pCnt R} \in ℝ^{+}$
220	93 93 219	ltdivmul2d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (\frac{R}{p^{p pCnt R}} < R \leftrightarrow R < R p^{p pCnt R})$
221	217 220	mpbird	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \frac{R}{p^{p pCnt R}} < R$
222	93 211 141	redivcld	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \frac{R}{p^{p pCnt R}} \in ℝ$
223	222 93	ltnled	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (\frac{R}{p^{p pCnt R}} < R \leftrightarrow \neg R \leq \frac{R}{p^{p pCnt R}})$
224	221 223	mpbid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \neg R \leq \frac{R}{p^{p pCnt R}}$
225	4	a1i	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to R = sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <)$
226	225	breq1d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (R \leq \frac{R}{p^{p pCnt R}} \leftrightarrow sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{p^{p pCnt R}})$
227	226	notbid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (\neg R \leq \frac{R}{p^{p pCnt R}} \leftrightarrow \neg sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{p^{p pCnt R}})$
228	224 227	mpbid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \neg sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{p^{p pCnt R}}$
229		elfznn	$⊢ f \in (1 \dots B) \to f \in ℕ$
230	229	adantl	$⊢ (φ \land f \in (1 \dots B)) \to f \in ℕ$
231	230	nnred	$⊢ (φ \land f \in (1 \dots B)) \to f \in ℝ$
232	231	ex	$⊢ φ \to (f \in (1 \dots B) \to f \in ℝ)$
233	232	ssrdv	$⊢ φ \to (1 \dots B) \subseteq ℝ$
234	7 233	sstrd	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
235	234	adantr	$⊢ (φ \land 1 < N \gcd R) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
236	235	adantr	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
237	236	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
238	19	adantr	$⊢ (φ \land 1 < N \gcd R) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin$
239	238	adantr	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin$
240	239	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin$
241		infrefilb	$⊢ (\{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ \land \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin \land \frac{R}{p^{p pCnt R}} \in \{r \in (1 \dots B) \| \neg r ∥ A\}) \to sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{p^{p pCnt R}}$
242	241	3expa	$⊢ ((\{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ \land \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin) \land \frac{R}{p^{p pCnt R}} \in \{r \in (1 \dots B) \| \neg r ∥ A\}) \to sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{p^{p pCnt R}}$
243	242	ex	$⊢ (\{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ \land \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin) \to (\frac{R}{p^{p pCnt R}} \in \{r \in (1 \dots B) \| \neg r ∥ A\} \to sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{p^{p pCnt R}})$
244	243	con3d	$⊢ (\{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ \land \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin) \to (\neg sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{p^{p pCnt R}} \to \neg \frac{R}{p^{p pCnt R}} \in \{r \in (1 \dots B) \| \neg r ∥ A\})$
245	237 240 244	syl2anc	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (\neg sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{p^{p pCnt R}} \to \neg \frac{R}{p^{p pCnt R}} \in \{r \in (1 \dots B) \| \neg r ∥ A\})$
246	228 245	mpd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \neg \frac{R}{p^{p pCnt R}} \in \{r \in (1 \dots B) \| \neg r ∥ A\}$
247		1zzd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 1 \in ℤ$
248	99	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to B \in ℤ$
249	137	mulid2d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 1 p^{p pCnt R} = p^{p pCnt R}$
250		dvdsle	$⊢ (p^{p pCnt R} \in ℤ \land R \in ℕ) \to (p^{p pCnt R} ∥ R \to p^{p pCnt R} \leq R)$
251	136 134 250	syl2anc	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (p^{p pCnt R} ∥ R \to p^{p pCnt R} \leq R)$
252	145 251	mpd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{p pCnt R} \leq R$
253	249 252	eqbrtrd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 1 p^{p pCnt R} \leq R$
254	48	adantr	$⊢ (φ \land 1 < N \gcd R) \to 1 \in ℝ$
255	254	ad2antrr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 1 \in ℝ$
256	255 93 219	lemuldivd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (1 p^{p pCnt R} \leq R \leftrightarrow 1 \leq \frac{R}{p^{p pCnt R}})$
257	253 256	mpbid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 1 \leq \frac{R}{p^{p pCnt R}}$
258	100	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to B \in ℝ$
259	121	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 1 \leq p$
260	203 135 259	expge1d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 1 \leq p^{p pCnt R}$
261		nnledivrp	$⊢ (R \in ℕ \land p^{p pCnt R} \in ℝ^{+}) \to (1 \leq p^{p pCnt R} \leftrightarrow \frac{R}{p^{p pCnt R}} \leq R)$
262	134 219 261	syl2anc	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (1 \leq p^{p pCnt R} \leftrightarrow \frac{R}{p^{p pCnt R}} \leq R)$
263	260 262	mpbid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \frac{R}{p^{p pCnt R}} \leq R$
264	106	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to R \leq B$
265	222 93 258 263 264	letrd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \frac{R}{p^{p pCnt R}} \leq B$
266	247 248 149 257 265	elfzd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \frac{R}{p^{p pCnt R}} \in (1 \dots B)$
267		breq1	$⊢ r = \frac{R}{p^{p pCnt R}} \to (r ∥ A \leftrightarrow (\frac{R}{p^{p pCnt R}}) ∥ A)$
268	267	notbid	$⊢ r = \frac{R}{p^{p pCnt R}} \to (\neg r ∥ A \leftrightarrow \neg (\frac{R}{p^{p pCnt R}}) ∥ A)$
269	268	elrab3	$⊢ \frac{R}{p^{p pCnt R}} \in (1 \dots B) \to (\frac{R}{p^{p pCnt R}} \in \{r \in (1 \dots B) \| \neg r ∥ A\} \leftrightarrow \neg (\frac{R}{p^{p pCnt R}}) ∥ A)$
270	269	con2bid	$⊢ \frac{R}{p^{p pCnt R}} \in (1 \dots B) \to ((\frac{R}{p^{p pCnt R}}) ∥ A \leftrightarrow \neg \frac{R}{p^{p pCnt R}} \in \{r \in (1 \dots B) \| \neg r ∥ A\})$
271	266 270	syl	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to ((\frac{R}{p^{p pCnt R}}) ∥ A \leftrightarrow \neg \frac{R}{p^{p pCnt R}} \in \{r \in (1 \dots B) \| \neg r ∥ A\})$
272	246 271	mpbird	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (\frac{R}{p^{p pCnt R}}) ∥ A$
273	134	ad2antrr	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land q \in ℙ) \land (q ∥ N \land q ∥ R)) \to R \in ℕ$
274	153	adantr	$⊢ (φ \land 1 < N \gcd R) \to N \in ℕ$
275	274	adantr	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to N \in ℕ$
276	275	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land p ∥ R) \to N \in ℕ$
277	276	adantr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land p ∥ R) \land \neg p ∥ N) \to N \in ℕ$
278	74 277	sylbir	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to N \in ℕ$
279	278	ad2antrr	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land q \in ℙ) \land (q ∥ N \land q ∥ R)) \to N \in ℕ$
280	133	ad2antrr	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land q \in ℙ) \land (q ∥ N \land q ∥ R)) \to p \in ℙ$
281		simplr	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land q \in ℙ) \land (q ∥ N \land q ∥ R)) \to q \in ℙ$
282	196	ad2antrr	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land q \in ℙ) \land (q ∥ N \land q ∥ R)) \to p ∥ R$
283		simprr	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land q \in ℙ) \land (q ∥ N \land q ∥ R)) \to q ∥ R$
284		simplrr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land q \in ℙ) \to \neg p ∥ N$
285	284	adantr	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land q \in ℙ) \land (q ∥ N \land q ∥ R)) \to \neg p ∥ N$
286		simprl	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land q \in ℙ) \land (q ∥ N \land q ∥ R)) \to q ∥ N$
287	273 279 280 281 282 283 285 286	aks4d1p8d2	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land q \in ℙ) \land (q ∥ N \land q ∥ R)) \to p^{p pCnt R} < R$
288		simpr	$⊢ (φ \land 1 < N \gcd R) \to 1 < N \gcd R$
289	288	ad2antrr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 1 < N \gcd R$
290	255 289	ltned	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to 1 \neq N \gcd R$
291	290	necomd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to N \gcd R \neq 1$
292	278 134	prmdvdsncoprmbd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (\exists q \in ℙ (q ∥ N \land q ∥ R) \leftrightarrow N \gcd R \neq 1)$
293	292	bicomd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (N \gcd R \neq 1 \leftrightarrow \exists q \in ℙ (q ∥ N \land q ∥ R))$
294	293	biimpd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (N \gcd R \neq 1 \to \exists q \in ℙ (q ∥ N \land q ∥ R))$
295	291 294	mpd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \exists q \in ℙ (q ∥ N \land q ∥ R)$
296	287 295	r19.29a	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{p pCnt R} < R$
297	211 93	ltnled	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (p^{p pCnt R} < R \leftrightarrow \neg R \leq p^{p pCnt R})$
298	296 297	mpbid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \neg R \leq p^{p pCnt R}$
299	225	breq1d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (R \leq p^{p pCnt R} \leftrightarrow sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq p^{p pCnt R})$
300	299	notbid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (\neg R \leq p^{p pCnt R} \leftrightarrow \neg sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq p^{p pCnt R})$
301	298 300	mpbid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \neg sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq p^{p pCnt R}$
302		infrefilb	$⊢ (\{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ \land \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin \land p^{p pCnt R} \in \{r \in (1 \dots B) \| \neg r ∥ A\}) \to sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq p^{p pCnt R}$
303	302	3expa	$⊢ ((\{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ \land \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin) \land p^{p pCnt R} \in \{r \in (1 \dots B) \| \neg r ∥ A\}) \to sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq p^{p pCnt R}$
304	303	ex	$⊢ (\{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ \land \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin) \to (p^{p pCnt R} \in \{r \in (1 \dots B) \| \neg r ∥ A\} \to sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq p^{p pCnt R})$
305	304	con3d	$⊢ (\{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ \land \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin) \to (\neg sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq p^{p pCnt R} \to \neg p^{p pCnt R} \in \{r \in (1 \dots B) \| \neg r ∥ A\})$
306	237 240 305	syl2anc	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (\neg sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq p^{p pCnt R} \to \neg p^{p pCnt R} \in \{r \in (1 \dots B) \| \neg r ∥ A\})$
307	301 306	mpd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \neg p^{p pCnt R} \in \{r \in (1 \dots B) \| \neg r ∥ A\}$
308	211 93 258 252 264	letrd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{p pCnt R} \leq B$
309	247 248 136 260 308	elfzd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{p pCnt R} \in (1 \dots B)$
310		breq1	$⊢ r = p^{p pCnt R} \to (r ∥ A \leftrightarrow p^{p pCnt R} ∥ A)$
311	310	notbid	$⊢ r = p^{p pCnt R} \to (\neg r ∥ A \leftrightarrow \neg p^{p pCnt R} ∥ A)$
312	311	elrab3	$⊢ p^{p pCnt R} \in (1 \dots B) \to (p^{p pCnt R} \in \{r \in (1 \dots B) \| \neg r ∥ A\} \leftrightarrow \neg p^{p pCnt R} ∥ A)$
313	309 312	syl	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (p^{p pCnt R} \in \{r \in (1 \dots B) \| \neg r ∥ A\} \leftrightarrow \neg p^{p pCnt R} ∥ A)$
314	313	con2bid	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (p^{p pCnt R} ∥ A \leftrightarrow \neg p^{p pCnt R} \in \{r \in (1 \dots B) \| \neg r ∥ A\})$
315	307 314	mpbird	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to p^{p pCnt R} ∥ A$
316	149 136 195 197 272 315	coprmdvds2d	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to (\frac{R}{p^{p pCnt R}}) p^{p pCnt R} ∥ A$
317	143 316	eqbrtrd	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to R ∥ A$
318	317	adantr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to R ∥ A$
319	67	simprd	$⊢ φ \to \neg R ∥ A$
320	319	ad5antr	$⊢ (((((φ \land 1 < N \gcd R) \land p \in ℙ) \land p ∥ R) \land \neg p ∥ N) \land (\frac{R}{N \gcd R}) ∥ A) \to \neg R ∥ A$
321	75 320	sylbir	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \neg R ∥ A$
322	318 321	pm2.21dd	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \neg (\frac{R}{p}) ∥ A$
323	30 129 322	elrabd	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \frac{R}{p} \in \{r \in (1 \dots B) \| \neg r ∥ A\}$
324		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}{p} \in \{r \in (1 \dots B) \| \neg r ∥ A\}) \to sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{p}$
325	17 28 323 324	syl3anc	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to sup (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \leq \frac{R}{p}$
326	5 325	eqbrtrd	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to R \leq \frac{R}{p}$
327	207	adantr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to 1 < p$
328		1rp	$⊢ 1 \in ℝ^{+}$
329	328	a1i	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to 1 \in ℝ^{+}$
330	215	adantr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to R \in ℝ^{+}$
331	329 95 330	ltdiv2d	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to (1 < p \leftrightarrow \frac{R}{p} < \frac{R}{1})$
332	327 331	mpbid	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \frac{R}{p} < \frac{R}{1}$
333	130	adantr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to R \in ℂ$
334	333	div1d	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \frac{R}{1} = R$
335	332 334	breqtrd	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \frac{R}{p} < R$
336	98 101 65	redivcld	$⊢ ((φ \land 1 < N \gcd R) \land p \in ℙ) \to \frac{R}{p} \in ℝ$
337	336	adantr	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \frac{R}{p} \in ℝ$
338	337	adantr	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \frac{R}{p} \in ℝ$
339	338 94	ltnled	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to (\frac{R}{p} < R \leftrightarrow \neg R \leq \frac{R}{p})$
340	335 339	mpbid	$⊢ ((((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \land (\frac{R}{N \gcd R}) ∥ A) \to \neg R \leq \frac{R}{p}$
341	326 340	pm2.65da	$⊢ (((φ \land 1 < N \gcd R) \land p \in ℙ) \land (p ∥ R \land \neg p ∥ N)) \to \neg (\frac{R}{N \gcd R}) ∥ A$
342	1 2 3 4	aks4d1p7	$⊢ φ \to \exists p \in ℙ (p ∥ R \land \neg p ∥ N)$
343	342	adantr	$⊢ (φ \land 1 < N \gcd R) \to \exists p \in ℙ (p ∥ R \land \neg p ∥ N)$
344	341 343	r19.29a	$⊢ (φ \land 1 < N \gcd R) \to \neg (\frac{R}{N \gcd R}) ∥ A$
345	344	adantr	$⊢ ((φ \land 1 < N \gcd R) \land (\frac{R}{N \gcd R}) ∥ A) \to \neg (\frac{R}{N \gcd R}) ∥ A$
346	1 2 3 4 345	aks4d1p5	$⊢ φ \to N \gcd R = 1$

Metamath Proof Explorer

Theorem aks4d1p8

Proof