prmgaplem4

		Ref	Expression
	Hypothesis	prmgaplem4.a	$⊢ A = \{p \in ℙ \| (N < p \land p \leq P)\}$
	Assertion	prmgaplem4	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to \exists x \in A \forall y \in A x \leq y$

Proof

Step	Hyp	Ref	Expression
1		prmgaplem4.a	$⊢ A = \{p \in ℙ \| (N < p \land p \leq P)\}$
2		ssrab2	$⊢ \{p \in ℙ \| (N < p \land p \leq P)\} \subseteq ℙ$
3	2	a1i	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to \{p \in ℙ \| (N < p \land p \leq P)\} \subseteq ℙ$
4		prmssnn	$⊢ ℙ \subseteq ℕ$
5		nnssre	$⊢ ℕ \subseteq ℝ$
6	4 5	sstri	$⊢ ℙ \subseteq ℝ$
7	3 6	sstrdi	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to \{p \in ℙ \| (N < p \land p \leq P)\} \subseteq ℝ$
8		fzfid	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to (N \dots P) \in Fin$
9		breq2	$⊢ p = i \to (N < p \leftrightarrow N < i)$
10		breq1	$⊢ p = i \to (p \leq P \leftrightarrow i \leq P)$
11	9 10	anbi12d	$⊢ p = i \to ((N < p \land p \leq P) \leftrightarrow (N < i \land i \leq P))$
12	11	elrab	$⊢ i \in \{p \in ℙ \| (N < p \land p \leq P)\} \leftrightarrow (i \in ℙ \land (N < i \land i \leq P))$
13		nnz	$⊢ N \in ℕ \to N \in ℤ$
14		prmz	$⊢ P \in ℙ \to P \in ℤ$
15	13 14	anim12i	$⊢ (N \in ℕ \land P \in ℙ) \to (N \in ℤ \land P \in ℤ)$
16	15	3adant3	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to (N \in ℤ \land P \in ℤ)$
17		prmz	$⊢ i \in ℙ \to i \in ℤ$
18	17	adantr	$⊢ (i \in ℙ \land (N < i \land i \leq P)) \to i \in ℤ$
19	16 18	anim12i	$⊢ ((N \in ℕ \land P \in ℙ \land N < P) \land (i \in ℙ \land (N < i \land i \leq P))) \to ((N \in ℤ \land P \in ℤ) \land i \in ℤ)$
20		df-3an	$⊢ (N \in ℤ \land P \in ℤ \land i \in ℤ) \leftrightarrow ((N \in ℤ \land P \in ℤ) \land i \in ℤ)$
21	19 20	sylibr	$⊢ ((N \in ℕ \land P \in ℙ \land N < P) \land (i \in ℙ \land (N < i \land i \leq P))) \to (N \in ℤ \land P \in ℤ \land i \in ℤ)$
22		nnre	$⊢ N \in ℕ \to N \in ℝ$
23	22	adantr	$⊢ (N \in ℕ \land P \in ℙ) \to N \in ℝ$
24	6	sseli	$⊢ i \in ℙ \to i \in ℝ$
25		ltle	$⊢ (N \in ℝ \land i \in ℝ) \to (N < i \to N \leq i)$
26	23 24 25	syl2an	$⊢ ((N \in ℕ \land P \in ℙ) \land i \in ℙ) \to (N < i \to N \leq i)$
27	26	anim1d	$⊢ ((N \in ℕ \land P \in ℙ) \land i \in ℙ) \to ((N < i \land i \leq P) \to (N \leq i \land i \leq P))$
28	27	ex	$⊢ (N \in ℕ \land P \in ℙ) \to (i \in ℙ \to ((N < i \land i \leq P) \to (N \leq i \land i \leq P)))$
29	28	3adant3	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to (i \in ℙ \to ((N < i \land i \leq P) \to (N \leq i \land i \leq P)))$
30	29	imp32	$⊢ ((N \in ℕ \land P \in ℙ \land N < P) \land (i \in ℙ \land (N < i \land i \leq P))) \to (N \leq i \land i \leq P)$
31		elfz2	$⊢ i \in (N \dots P) \leftrightarrow ((N \in ℤ \land P \in ℤ \land i \in ℤ) \land (N \leq i \land i \leq P))$
32	21 30 31	sylanbrc	$⊢ ((N \in ℕ \land P \in ℙ \land N < P) \land (i \in ℙ \land (N < i \land i \leq P))) \to i \in (N \dots P)$
33	32	ex	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to ((i \in ℙ \land (N < i \land i \leq P)) \to i \in (N \dots P))$
34	12 33	syl5bi	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to (i \in \{p \in ℙ \| (N < p \land p \leq P)\} \to i \in (N \dots P))$
35	34	ssrdv	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to \{p \in ℙ \| (N < p \land p \leq P)\} \subseteq (N \dots P)$
36	8 35	ssfid	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to \{p \in ℙ \| (N < p \land p \leq P)\} \in Fin$
37		breq2	$⊢ p = P \to (N < p \leftrightarrow N < P)$
38		breq1	$⊢ p = P \to (p \leq P \leftrightarrow P \leq P)$
39	37 38	anbi12d	$⊢ p = P \to ((N < p \land p \leq P) \leftrightarrow (N < P \land P \leq P))$
40		simp2	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to P \in ℙ$
41		prmnn	$⊢ P \in ℙ \to P \in ℕ$
42	41	nnred	$⊢ P \in ℙ \to P \in ℝ$
43	42	leidd	$⊢ P \in ℙ \to P \leq P$
44	43	anim1ci	$⊢ (P \in ℙ \land N < P) \to (N < P \land P \leq P)$
45	44	3adant1	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to (N < P \land P \leq P)$
46	39 40 45	elrabd	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to P \in \{p \in ℙ \| (N < p \land p \leq P)\}$
47	46	ne0d	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to \{p \in ℙ \| (N < p \land p \leq P)\} \neq \emptyset$
48		sseq1	$⊢ A = \{p \in ℙ \| (N < p \land p \leq P)\} \to (A \subseteq ℝ \leftrightarrow \{p \in ℙ \| (N < p \land p \leq P)\} \subseteq ℝ)$
49		eleq1	$⊢ A = \{p \in ℙ \| (N < p \land p \leq P)\} \to (A \in Fin \leftrightarrow \{p \in ℙ \| (N < p \land p \leq P)\} \in Fin)$
50		neeq1	$⊢ A = \{p \in ℙ \| (N < p \land p \leq P)\} \to (A \neq \emptyset \leftrightarrow \{p \in ℙ \| (N < p \land p \leq P)\} \neq \emptyset)$
51	48 49 50	3anbi123d	$⊢ A = \{p \in ℙ \| (N < p \land p \leq P)\} \to ((A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \leftrightarrow (\{p \in ℙ \| (N < p \land p \leq P)\} \subseteq ℝ \land \{p \in ℙ \| (N < p \land p \leq P)\} \in Fin \land \{p \in ℙ \| (N < p \land p \leq P)\} \neq \emptyset))$
52	1 51	ax-mp	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \leftrightarrow (\{p \in ℙ \| (N < p \land p \leq P)\} \subseteq ℝ \land \{p \in ℙ \| (N < p \land p \leq P)\} \in Fin \land \{p \in ℙ \| (N < p \land p \leq P)\} \neq \emptyset)$
53	7 36 47 52	syl3anbrc	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset)$
54		fiminre	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A x \leq y$
55	53 54	syl	$⊢ (N \in ℕ \land P \in ℙ \land N < P) \to \exists x \in A \forall y \in A x \leq y$

Metamath Proof Explorer

Theorem prmgaplem4

Proof