aks4d1p4

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

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

Proof

Step	Hyp	Ref	Expression
1		aks4d1p4.1	$⊢ φ \to N \in ℤ_{\geq 3}$
2		aks4d1p4.2	$⊢ A = N^{⌊\log_{2} B⌋} \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1)$
3		aks4d1p4.3	$⊢ B = ⌈{\log_{2} N}^{5}⌉$
4		aks4d1p4.4	$⊢ R = inf (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <)$
5	4	a1i	$⊢ φ \to R = inf (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <)$
6		ltso	$⊢ < Or ℝ$
7	6	a1i	$⊢ φ \to < Or ℝ$
8		fzfid	$⊢ φ \to (1 \dots B) \in Fin$
9		ssrab2	$⊢ \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq (1 \dots B)$
10	9	a1i	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq (1 \dots B)$
11	8 10	ssfid	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin$
12	1 2 3	aks4d1p3	$⊢ φ \to \exists r \in (1 \dots B) \neg r ∥ A$
13		rabn0	$⊢ \{r \in (1 \dots B) \| \neg r ∥ A\} \neq \emptyset \leftrightarrow \exists r \in (1 \dots B) \neg r ∥ A$
14	12 13	sylibr	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \neq \emptyset$
15		elfznn	$⊢ o \in (1 \dots B) \to o \in ℕ$
16	15	adantl	$⊢ (φ \land o \in (1 \dots B)) \to o \in ℕ$
17	16	nnred	$⊢ (φ \land o \in (1 \dots B)) \to o \in ℝ$
18	17	ex	$⊢ φ \to (o \in (1 \dots B) \to o \in ℝ)$
19	18	ssrdv	$⊢ φ \to (1 \dots B) \subseteq ℝ$
20	10 19	sstrd	$⊢ φ \to \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ$
21	11 14 20	3jca	$⊢ φ \to (\{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin \land \{r \in (1 \dots B) \| \neg r ∥ A\} \neq \emptyset \land \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ)$
22		fiinfcl	$⊢ (< Or ℝ \land (\{r \in (1 \dots B) \| \neg r ∥ A\} \in Fin \land \{r \in (1 \dots B) \| \neg r ∥ A\} \neq \emptyset \land \{r \in (1 \dots B) \| \neg r ∥ A\} \subseteq ℝ)) \to inf (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \in \{r \in (1 \dots B) \| \neg r ∥ A\}$
23	7 21 22	syl2anc	$⊢ φ \to inf (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <) \in \{r \in (1 \dots B) \| \neg r ∥ A\}$
24	5 23	eqeltrd	$⊢ φ \to R \in \{r \in (1 \dots B) \| \neg r ∥ A\}$
25		breq1	$⊢ r = R \to (r ∥ A \leftrightarrow R ∥ A)$
26	25	notbid	$⊢ r = R \to (\neg r ∥ A \leftrightarrow \neg R ∥ A)$
27	26	elrab	$⊢ R \in \{r \in (1 \dots B) \| \neg r ∥ A\} \leftrightarrow (R \in (1 \dots B) \land \neg R ∥ A)$
28	24 27	sylib	$⊢ φ \to (R \in (1 \dots B) \land \neg R ∥ A)$

Metamath Proof Explorer

Theorem aks4d1p4

Proof