Metamath Proof Explorer

Theorem ppisval2

Description: The set of primes less than A expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014)

		Ref	Expression
	Assertion	ppisval2	$⊢ (A \in ℝ \land 2 \in ℤ_{\geq M}) \to [0, A] \cap ℙ = (M \dots ⌊A⌋) \cap ℙ$

Proof

Step	Hyp	Ref	Expression
1		ppisval	$⊢ A \in ℝ \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
2	1	adantr	$⊢ (A \in ℝ \land 2 \in ℤ_{\geq M}) \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
3		fzss1	$⊢ 2 \in ℤ_{\geq M} \to (2 \dots ⌊A⌋) \subseteq (M \dots ⌊A⌋)$
4	3	adantl	$⊢ (A \in ℝ \land 2 \in ℤ_{\geq M}) \to (2 \dots ⌊A⌋) \subseteq (M \dots ⌊A⌋)$
5	4	ssrind	$⊢ (A \in ℝ \land 2 \in ℤ_{\geq M}) \to (2 \dots ⌊A⌋) \cap ℙ \subseteq (M \dots ⌊A⌋) \cap ℙ$
6		simpr	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to x \in ((M \dots ⌊A⌋) \cap ℙ)$
7		elin	$⊢ x \in ((M \dots ⌊A⌋) \cap ℙ) \leftrightarrow (x \in (M \dots ⌊A⌋) \land x \in ℙ)$
8	6 7	sylib	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to (x \in (M \dots ⌊A⌋) \land x \in ℙ)$
9	8	simprd	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to x \in ℙ$
10		prmuz2	$⊢ x \in ℙ \to x \in ℤ_{\geq 2}$
11	9 10	syl	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to x \in ℤ_{\geq 2}$
12	8	simpld	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to x \in (M \dots ⌊A⌋)$
13		elfzuz3	$⊢ x \in (M \dots ⌊A⌋) \to ⌊A⌋ \in ℤ_{\geq x}$
14	12 13	syl	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to ⌊A⌋ \in ℤ_{\geq x}$
15		elfzuzb	$⊢ x \in (2 \dots ⌊A⌋) \leftrightarrow (x \in ℤ_{\geq 2} \land ⌊A⌋ \in ℤ_{\geq x})$
16	11 14 15	sylanbrc	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to x \in (2 \dots ⌊A⌋)$
17	16 9	elind	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to x \in ((2 \dots ⌊A⌋) \cap ℙ)$
18	5 17	eqelssd	$⊢ (A \in ℝ \land 2 \in ℤ_{\geq M}) \to (2 \dots ⌊A⌋) \cap ℙ = (M \dots ⌊A⌋) \cap ℙ$
19	2 18	eqtrd	$⊢ (A \in ℝ \land 2 \in ℤ_{\geq M}) \to [0, A] \cap ℙ = (M \dots ⌊A⌋) \cap ℙ$