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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 [,] 𝑁 ) ∩ ℤ ) )