Metamath Proof Explorer


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 ) ... 𝑁 ) ) ) )