Theorem elfzp12

Description: Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010)

	Ref	Expression
Assertion	elfzp12	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ V )
2	1	anim2i	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ V ) )
3		elfvex	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ V )
4		eleq1	⊢ ( 𝐾 = 𝑀 → ( 𝐾 ∈ V ↔ 𝑀 ∈ V ) )
5	3 4	syl5ibrcom	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 = 𝑀 → 𝐾 ∈ V ) )
6	5	imdistani	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 = 𝑀 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ V ) )
7		elex	⊢ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝐾 ∈ V )
8	7	anim2i	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ V ) )
9	6 8	jaodan	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ V ) )
10		fzpred	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
11	10	eleq2d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝐾 ∈ ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
12		elun	⊢ ( 𝐾 ∈ ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ↔ ( 𝐾 ∈ { 𝑀 } ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
13	11 12	bitrdi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 ∈ { 𝑀 } ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
14		elsng	⊢ ( 𝐾 ∈ V → ( 𝐾 ∈ { 𝑀 } ↔ 𝐾 = 𝑀 ) )
15	14	orbi1d	⊢ ( 𝐾 ∈ V → ( ( 𝐾 ∈ { 𝑀 } ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ↔ ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
16	13 15	sylan9bb	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ V ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
17	2 9 16	pm5.21nd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )