# Metamath Proof Explorer

## Theorem 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 \left[0,{A}\right]\cap ℙ=\left(2\dots ⌊{A}⌋\right)\cap ℙ$

### Proof

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