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

Metamath Proof Explorer

Theorem nelfzo

Description: An integer not being a member of a half-open finite set of integers. (Contributed by AV, 29-Apr-2020)

Ref Expression
Assertion nelfzo ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∉ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 < 𝑀 ∨ 𝑁 ≤ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 df-nel ⊢ ( 𝐾 ∉ ( 𝑀 ..^ 𝑁 ) ↔ ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) )
2 ianor ⊢ ( ¬ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ↔ ( ¬ 𝑀 ≤ 𝐾 ∨ ¬ 𝐾 < 𝑁 ) )
3 2 a1i ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ↔ ( ¬ 𝑀 ≤ 𝐾 ∨ ¬ 𝐾 < 𝑁 ) ) )
4 elfzo ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) )
5 4 notbid ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ¬ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) )
6 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
7 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
8 6 7 anim12i ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
9 8 3adant3 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
10 ltnle ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝐾 < 𝑀 ↔ ¬ 𝑀 ≤ 𝐾 ) )
11 9 10 syl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑀 ↔ ¬ 𝑀 ≤ 𝐾 ) )
12 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
13 6 12 anim12ci ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ ) )
14 13 3adant2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ ) )
15 lenlt ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑁 ≤ 𝐾 ↔ ¬ 𝐾 < 𝑁 ) )
16 14 15 syl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 𝐾 ↔ ¬ 𝐾 < 𝑁 ) )
17 11 16 orbi12d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 < 𝑀 ∨ 𝑁 ≤ 𝐾 ) ↔ ( ¬ 𝑀 ≤ 𝐾 ∨ ¬ 𝐾 < 𝑁 ) ) )
18 3 5 17 3bitr4d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 < 𝑀 ∨ 𝑁 ≤ 𝐾 ) ) )
19 1 18 bitrid ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∉ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 < 𝑀 ∨ 𝑁 ≤ 𝐾 ) ) )