This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzval2

Description: An alternative way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion fzval2 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 [,] 𝑁 ) ∩ ℤ ) )

Proof

Step Hyp Ref Expression
1 fzval ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) = { 𝑘 ∈ ℤ ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } )
2 zssre ⊢ ℤ ⊆ ℝ
3 ressxr ⊢ ℝ ⊆ ℝ*
4 2 3 sstri ⊢ ℤ ⊆ ℝ*
5 4 sseli ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ* )
6 4 sseli ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ* )
7 iccval ⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ) → ( 𝑀 [,] 𝑁 ) = { 𝑘 ∈ ℝ* ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } )
8 5 6 7 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 [,] 𝑁 ) = { 𝑘 ∈ ℝ* ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } )
9 8 ineq1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 [,] 𝑁 ) ∩ ℤ ) = ( { 𝑘 ∈ ℝ* ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } ∩ ℤ ) )
10 inrab2 ⊢ ( { 𝑘 ∈ ℝ* ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } ∩ ℤ ) = { 𝑘 ∈ ( ℝ* ∩ ℤ ) ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) }
11 sseqin2 ⊢ ( ℤ ⊆ ℝ* ↔ ( ℝ* ∩ ℤ ) = ℤ )
12 4 11 mpbi ⊢ ( ℝ* ∩ ℤ ) = ℤ
13 12 rabeqi ⊢ { 𝑘 ∈ ( ℝ* ∩ ℤ ) ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } = { 𝑘 ∈ ℤ ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) }
14 10 13 eqtri ⊢ ( { 𝑘 ∈ ℝ* ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } ∩ ℤ ) = { 𝑘 ∈ ℤ ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) }
15 9 14 eqtr2di ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → { 𝑘 ∈ ℤ ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } = ( ( 𝑀 [,] 𝑁 ) ∩ ℤ ) )
16 1 15 eqtrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 [,] 𝑁 ) ∩ ℤ ) )