prmgaplem3

		Ref	Expression
	Hypothesis	prmgaplem3.a	$⊢ A = \{p \in ℙ \| p < N\}$
	Assertion	prmgaplem3	$⊢ N \in ℤ_{\geq 3} \to \exists x \in A \forall y \in A y \leq x$

Proof

Step	Hyp	Ref	Expression
1		prmgaplem3.a	$⊢ A = \{p \in ℙ \| p < N\}$
2		ssrab2	$⊢ \{p \in ℙ \| p < N\} \subseteq ℙ$
3	2	a1i	$⊢ N \in ℤ_{\geq 3} \to \{p \in ℙ \| p < N\} \subseteq ℙ$
4		prmssnn	$⊢ ℙ \subseteq ℕ$
5		nnssre	$⊢ ℕ \subseteq ℝ$
6	4 5	sstri	$⊢ ℙ \subseteq ℝ$
7	3 6	sstrdi	$⊢ N \in ℤ_{\geq 3} \to \{p \in ℙ \| p < N\} \subseteq ℝ$
8		fzofi	$⊢ (0 ..^N) \in Fin$
9		breq1	$⊢ p = i \to (p < N \leftrightarrow i < N)$
10	9	elrab	$⊢ i \in \{p \in ℙ \| p < N\} \leftrightarrow (i \in ℙ \land i < N)$
11		prmnn	$⊢ i \in ℙ \to i \in ℕ$
12	11	nnnn0d	$⊢ i \in ℙ \to i \in ℕ_{0}$
13	12	ad2antrl	$⊢ (N \in ℤ_{\geq 3} \land (i \in ℙ \land i < N)) \to i \in ℕ_{0}$
14		eluzge3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
15	14	adantr	$⊢ (N \in ℤ_{\geq 3} \land (i \in ℙ \land i < N)) \to N \in ℕ$
16		simprr	$⊢ (N \in ℤ_{\geq 3} \land (i \in ℙ \land i < N)) \to i < N$
17		elfzo0	$⊢ i \in (0 ..^N) \leftrightarrow (i \in ℕ_{0} \land N \in ℕ \land i < N)$
18	13 15 16 17	syl3anbrc	$⊢ (N \in ℤ_{\geq 3} \land (i \in ℙ \land i < N)) \to i \in (0 ..^N)$
19	18	ex	$⊢ N \in ℤ_{\geq 3} \to ((i \in ℙ \land i < N) \to i \in (0 ..^N))$
20	10 19	biimtrid	$⊢ N \in ℤ_{\geq 3} \to (i \in \{p \in ℙ \| p < N\} \to i \in (0 ..^N))$
21	20	ssrdv	$⊢ N \in ℤ_{\geq 3} \to \{p \in ℙ \| p < N\} \subseteq (0 ..^N)$
22		ssfi	$⊢ ((0 ..^N) \in Fin \land \{p \in ℙ \| p < N\} \subseteq (0 ..^N)) \to \{p \in ℙ \| p < N\} \in Fin$
23	8 21 22	sylancr	$⊢ N \in ℤ_{\geq 3} \to \{p \in ℙ \| p < N\} \in Fin$
24		breq1	$⊢ p = 2 \to (p < N \leftrightarrow 2 < N)$
25		2prm	$⊢ 2 \in ℙ$
26	25	a1i	$⊢ N \in ℤ_{\geq 3} \to 2 \in ℙ$
27		eluz2	$⊢ N \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land N \in ℤ \land 3 \leq N)$
28		df-3	$⊢ 3 = 2 + 1$
29	28	breq1i	$⊢ 3 \leq N \leftrightarrow 2 + 1 \leq N$
30		2z	$⊢ 2 \in ℤ$
31		zltp1le	$⊢ (2 \in ℤ \land N \in ℤ) \to (2 < N \leftrightarrow 2 + 1 \leq N)$
32	30 31	mpan	$⊢ N \in ℤ \to (2 < N \leftrightarrow 2 + 1 \leq N)$
33	32	biimprd	$⊢ N \in ℤ \to (2 + 1 \leq N \to 2 < N)$
34	29 33	biimtrid	$⊢ N \in ℤ \to (3 \leq N \to 2 < N)$
35	34	imp	$⊢ (N \in ℤ \land 3 \leq N) \to 2 < N$
36	35	3adant1	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to 2 < N$
37	27 36	sylbi	$⊢ N \in ℤ_{\geq 3} \to 2 < N$
38	24 26 37	elrabd	$⊢ N \in ℤ_{\geq 3} \to 2 \in \{p \in ℙ \| p < N\}$
39	38	ne0d	$⊢ N \in ℤ_{\geq 3} \to \{p \in ℙ \| p < N\} \neq \emptyset$
40		sseq1	$⊢ A = \{p \in ℙ \| p < N\} \to (A \subseteq ℝ \leftrightarrow \{p \in ℙ \| p < N\} \subseteq ℝ)$
41		eleq1	$⊢ A = \{p \in ℙ \| p < N\} \to (A \in Fin \leftrightarrow \{p \in ℙ \| p < N\} \in Fin)$
42		neeq1	$⊢ A = \{p \in ℙ \| p < N\} \to (A \neq \emptyset \leftrightarrow \{p \in ℙ \| p < N\} \neq \emptyset)$
43	40 41 42	3anbi123d	$⊢ A = \{p \in ℙ \| p < N\} \to ((A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \leftrightarrow (\{p \in ℙ \| p < N\} \subseteq ℝ \land \{p \in ℙ \| p < N\} \in Fin \land \{p \in ℙ \| p < N\} \neq \emptyset))$
44	1 43	ax-mp	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \leftrightarrow (\{p \in ℙ \| p < N\} \subseteq ℝ \land \{p \in ℙ \| p < N\} \in Fin \land \{p \in ℙ \| p < N\} \neq \emptyset)$
45	7 23 39 44	syl3anbrc	$⊢ N \in ℤ_{\geq 3} \to (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset)$
46		fimaxre	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A y \leq x$
47	45 46	syl	$⊢ N \in ℤ_{\geq 3} \to \exists x \in A \forall y \in A y \leq x$

Metamath Proof Explorer

Theorem prmgaplem3

Proof