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

Metamath Proof Explorer

Theorem elfzo2

Description: Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion elfzo2 ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )

Proof

Step Hyp Ref Expression
1 an4 ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) ↔ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≤ 𝐾 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
2 df-3an ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ↔ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) )
3 2 anbi1i ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) ↔ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) )
4 eluz2 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) )
5 3ancoma ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) )
6 df-3an ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) ↔ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≤ 𝐾 ) )
7 4 5 6 3bitri ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≤ 𝐾 ) )
8 7 anbi1i ⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) ↔ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≤ 𝐾 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
9 1 3 8 3bitr4i ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
10 elfzoelz ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ℤ )
11 elfzoel1 ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℤ )
12 elfzoel2 ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
13 10 11 12 3jca ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
14 elfzo ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) )
15 13 14 biadanii ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) )
16 3anass ⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
17 9 15 16 3bitr4i ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )