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

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