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	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∉ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 < 𝑀 ∨ 𝑁 ≤ 𝐾 ) ) )