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		elin	$⊢ x \in ((M \dots ⌊A⌋) \cap ℙ) \leftrightarrow (x \in (M \dots ⌊A⌋) \land x \in ℙ)$
7	6	bilani	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to (x \in (M \dots ⌊A⌋) \land x \in ℙ)$
8	7	simprd	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to x \in ℙ$
9		prmuz2	$⊢ x \in ℙ \to x \in ℤ_{\geq 2}$
10	8 9	syl	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to x \in ℤ_{\geq 2}$
11	7	simpld	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to x \in (M \dots ⌊A⌋)$
12		elfzuz3	$⊢ x \in (M \dots ⌊A⌋) \to ⌊A⌋ \in ℤ_{\geq x}$
13	11 12	syl	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to ⌊A⌋ \in ℤ_{\geq x}$
14		elfzuzb	$⊢ x \in (2 \dots ⌊A⌋) \leftrightarrow (x \in ℤ_{\geq 2} \land ⌊A⌋ \in ℤ_{\geq x})$
15	10 13 14	sylanbrc	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to x \in (2 \dots ⌊A⌋)$
16	15 8	elind	$⊢ ((A \in ℝ \land 2 \in ℤ_{\geq M}) \land x \in ((M \dots ⌊A⌋) \cap ℙ)) \to x \in ((2 \dots ⌊A⌋) \cap ℙ)$
17	5 16	eqelssd	$⊢ (A \in ℝ \land 2 \in ℤ_{\geq M}) \to (2 \dots ⌊A⌋) \cap ℙ = (M \dots ⌊A⌋) \cap ℙ$
18	2 17	eqtrd	$⊢ (A \in ℝ \land 2 \in ℤ_{\geq M}) \to [0, A] \cap ℙ = (M \dots ⌊A⌋) \cap ℙ$