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 ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
2 1 elin2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑥 ∈ ℙ )
3 prmuz2 ⊢ ( 𝑥 ∈ ℙ → 𝑥 ∈ ( ℤ≥ ‘ 2 ) )
4 2 3 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑥 ∈ ( ℤ≥ ‘ 2 ) )
5 prmz ⊢ ( 𝑥 ∈ ℙ → 𝑥 ∈ ℤ )
6 2 5 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑥 ∈ ℤ )
7 flcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
8 7 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
9 1 elin1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑥 ∈ ( 0 [,] 𝐴 ) )
10 0re ⊢ 0 ∈ ℝ
11 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℝ )
12 elicc2 ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) )
13 10 11 12 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑥 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) )
14 9 13 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴 ) )
15 14 simp3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑥 ≤ 𝐴 )
16 flge ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ ( ⌊ ‘ 𝐴 ) ) )
17 6 16 syldan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ ( ⌊ ‘ 𝐴 ) ) )
18 15 17 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑥 ≤ ( ⌊ ‘ 𝐴 ) )
19 eluz2 ⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑥 ) ↔ ( 𝑥 ∈ ℤ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ 𝑥 ≤ ( ⌊ ‘ 𝐴 ) ) )
20 6 8 18 19 syl3anbrc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑥 ) )
21 elfzuzb ⊢ ( 𝑥 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑥 ) ) )
22 4 20 21 sylanbrc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑥 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) )
23 22 2 elind ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑥 ∈ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
24 23 ex ⊢ ( 𝐴 ∈ ℝ → ( 𝑥 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → 𝑥 ∈ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) )
25 24 ssrdv ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
26 2z ⊢ 2 ∈ ℤ
27 fzval2 ⊢ ( ( 2 ∈ ℤ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℤ ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) = ( ( 2 [,] ( ⌊ ‘ 𝐴 ) ) ∩ ℤ ) )
28 26 7 27 sylancr ⊢ ( 𝐴 ∈ ℝ → ( 2 ... ( ⌊ ‘ 𝐴 ) ) = ( ( 2 [,] ( ⌊ ‘ 𝐴 ) ) ∩ ℤ ) )
29 inss1 ⊢ ( ( 2 [,] ( ⌊ ‘ 𝐴 ) ) ∩ ℤ ) ⊆ ( 2 [,] ( ⌊ ‘ 𝐴 ) )
30 10 a1i ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
31 id ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
32 0le2 ⊢ 0 ≤ 2
33 32 a1i ⊢ ( 𝐴 ∈ ℝ → 0 ≤ 2 )
34 flle ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
35 iccss ⊢ ( ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 0 ≤ 2 ∧ ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) ) → ( 2 [,] ( ⌊ ‘ 𝐴 ) ) ⊆ ( 0 [,] 𝐴 ) )
36 30 31 33 34 35 syl22anc ⊢ ( 𝐴 ∈ ℝ → ( 2 [,] ( ⌊ ‘ 𝐴 ) ) ⊆ ( 0 [,] 𝐴 ) )
37 29 36 sstrid ⊢ ( 𝐴 ∈ ℝ → ( ( 2 [,] ( ⌊ ‘ 𝐴 ) ) ∩ ℤ ) ⊆ ( 0 [,] 𝐴 ) )
38 28 37 eqsstrd ⊢ ( 𝐴 ∈ ℝ → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 0 [,] 𝐴 ) )
39 38 ssrind ⊢ ( 𝐴 ∈ ℝ → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
40 25 39 eqssd ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )