ppisval

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	ppisval	$⊢ A \in ℝ \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to x \in ([0, A] \cap ℙ)$
2	1	elin2d	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to x \in ℙ$
3		prmuz2	$⊢ x \in ℙ \to x \in ℤ_{\geq 2}$
4	2 3	syl	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to x \in ℤ_{\geq 2}$
5		prmz	$⊢ x \in ℙ \to x \in ℤ$
6	2 5	syl	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to x \in ℤ$
7		flcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℤ$
8	7	adantr	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to ⌊A⌋ \in ℤ$
9	1	elin1d	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to x \in [0, A]$
10		0re	$⊢ 0 \in ℝ$
11		simpl	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to A \in ℝ$
12		elicc2	$⊢ (0 \in ℝ \land A \in ℝ) \to (x \in [0, A] \leftrightarrow (x \in ℝ \land 0 \leq x \land x \leq A))$
13	10 11 12	sylancr	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to (x \in [0, A] \leftrightarrow (x \in ℝ \land 0 \leq x \land x \leq A))$
14	9 13	mpbid	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to (x \in ℝ \land 0 \leq x \land x \leq A)$
15	14	simp3d	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to x \leq A$
16		flge	$⊢ (A \in ℝ \land x \in ℤ) \to (x \leq A \leftrightarrow x \leq ⌊A⌋)$
17	6 16	syldan	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to (x \leq A \leftrightarrow x \leq ⌊A⌋)$
18	15 17	mpbid	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to x \leq ⌊A⌋$
19		eluz2	$⊢ ⌊A⌋ \in ℤ_{\geq x} \leftrightarrow (x \in ℤ \land ⌊A⌋ \in ℤ \land x \leq ⌊A⌋)$
20	6 8 18 19	syl3anbrc	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to ⌊A⌋ \in ℤ_{\geq x}$
21		elfzuzb	$⊢ x \in (2 \dots ⌊A⌋) \leftrightarrow (x \in ℤ_{\geq 2} \land ⌊A⌋ \in ℤ_{\geq x})$
22	4 20 21	sylanbrc	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to x \in (2 \dots ⌊A⌋)$
23	22 2	elind	$⊢ (A \in ℝ \land x \in ([0, A] \cap ℙ)) \to x \in ((2 \dots ⌊A⌋) \cap ℙ)$
24	23	ex	$⊢ A \in ℝ \to (x \in ([0, A] \cap ℙ) \to x \in ((2 \dots ⌊A⌋) \cap ℙ))$
25	24	ssrdv	$⊢ A \in ℝ \to [0, A] \cap ℙ \subseteq (2 \dots ⌊A⌋) \cap ℙ$
26		2z	$⊢ 2 \in ℤ$
27		fzval2	$⊢ (2 \in ℤ \land ⌊A⌋ \in ℤ) \to (2 \dots ⌊A⌋) = [2, ⌊A⌋] \cap ℤ$
28	26 7 27	sylancr	$⊢ A \in ℝ \to (2 \dots ⌊A⌋) = [2, ⌊A⌋] \cap ℤ$
29		inss1	$⊢ [2, ⌊A⌋] \cap ℤ \subseteq [2, ⌊A⌋]$
30	10	a1i	$⊢ A \in ℝ \to 0 \in ℝ$
31		id	$⊢ A \in ℝ \to A \in ℝ$
32		0le2	$⊢ 0 \leq 2$
33	32	a1i	$⊢ A \in ℝ \to 0 \leq 2$
34		flle	$⊢ A \in ℝ \to ⌊A⌋ \leq A$
35		iccss	$⊢ ((0 \in ℝ \land A \in ℝ) \land (0 \leq 2 \land ⌊A⌋ \leq A)) \to [2, ⌊A⌋] \subseteq [0, A]$
36	30 31 33 34 35	syl22anc	$⊢ A \in ℝ \to [2, ⌊A⌋] \subseteq [0, A]$
37	29 36	sstrid	$⊢ A \in ℝ \to [2, ⌊A⌋] \cap ℤ \subseteq [0, A]$
38	28 37	eqsstrd	$⊢ A \in ℝ \to (2 \dots ⌊A⌋) \subseteq [0, A]$
39	38	ssrind	$⊢ A \in ℝ \to (2 \dots ⌊A⌋) \cap ℙ \subseteq [0, A] \cap ℙ$
40	25 39	eqssd	$⊢ A \in ℝ \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$

Metamath Proof Explorer

Theorem ppisval

Proof