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

Proof

Step Hyp Ref Expression
1 ppisval ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
3 fzss1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) )
4 3 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) )
5 4 ssrind ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
6 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
7 elin ⊢ ( 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ↔ ( 𝑥 ∈ ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑥 ∈ ℙ ) )
8 6 7 sylib ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( 𝑥 ∈ ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑥 ∈ ℙ ) )
9 8 simprd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑥 ∈ ℙ )
10 prmuz2 ⊢ ( 𝑥 ∈ ℙ → 𝑥 ∈ ( ℤ≥ ‘ 2 ) )
11 9 10 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑥 ∈ ( ℤ≥ ‘ 2 ) )
12 8 simpld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑥 ∈ ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) )
13 elfzuz3 ⊢ ( 𝑥 ∈ ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑥 ) )
14 12 13 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑥 ) )
15 elfzuzb ⊢ ( 𝑥 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑥 ) ) )
16 11 14 15 sylanbrc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑥 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) )
17 16 9 elind ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑥 ∈ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
18 5 17 eqelssd ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
19 2 18 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )