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 [,] 𝐴 ) ∩ ℙ ) = ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )