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