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		elin	⊢ ( 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ↔ ( 𝑥 ∈ ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑥 ∈ ℙ ) )
7	6	bilani	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( 𝑥 ∈ ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑥 ∈ ℙ ) )
8	7	simprd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑥 ∈ ℙ )
9		prmuz2	⊢ ( 𝑥 ∈ ℙ → 𝑥 ∈ ( ℤ≥ ‘ 2 ) )
10	8 9	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑥 ∈ ( ℤ≥ ‘ 2 ) )
11	7	simpld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑥 ∈ ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) )
12		elfzuz3	⊢ ( 𝑥 ∈ ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑥 ) )
13	11 12	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑥 ) )
14		elfzuzb	⊢ ( 𝑥 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑥 ) ) )
15	10 13 14	sylanbrc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑥 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) )
16	15 8	elind	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑥 ∈ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
17	5 16	eqelssd	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
18	2 17	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 𝑀 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )