fzone1

Description: Elementhood in a half-open interval, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024)

		Ref	Expression
	Assertion	fzone1	$⊢ (K \in (M ..^N) \land K \neq M) \to K \in (M + 1 ..^N)$

Step	Hyp	Ref	Expression
1		elfzofz	$⊢ K \in (M ..^N) \to K \in (M \dots N)$
2	1	adantr	$⊢ (K \in (M ..^N) \land K \neq M) \to K \in (M \dots N)$
3		elfzlmr	$⊢ K \in (M \dots N) \to (K = M \lor K \in (M + 1 ..^N) \lor K = N)$
4	2 3	syl	$⊢ (K \in (M ..^N) \land K \neq M) \to (K = M \lor K \in (M + 1 ..^N) \lor K = N)$
5		df-3or	$⊢ (K = M \lor K \in (M + 1 ..^N) \lor K = N) \leftrightarrow ((K = M \lor K \in (M + 1 ..^N)) \lor K = N)$
6	4 5	sylib	$⊢ (K \in (M ..^N) \land K \neq M) \to ((K = M \lor K \in (M + 1 ..^N)) \lor K = N)$
7	2	elfzelzd	$⊢ (K \in (M ..^N) \land K \neq M) \to K \in ℤ$
8	7	zred	$⊢ (K \in (M ..^N) \land K \neq M) \to K \in ℝ$
9		elfzolt2	$⊢ K \in (M ..^N) \to K < N$
10	9	adantr	$⊢ (K \in (M ..^N) \land K \neq M) \to K < N$
11	8 10	ltned	$⊢ (K \in (M ..^N) \land K \neq M) \to K \neq N$
12	11	neneqd	$⊢ (K \in (M ..^N) \land K \neq M) \to \neg K = N$
13	6 12	olcnd	$⊢ (K \in (M ..^N) \land K \neq M) \to (K = M \lor K \in (M + 1 ..^N))$
14		simpr	$⊢ (K \in (M ..^N) \land K \neq M) \to K \neq M$
15	14	neneqd	$⊢ (K \in (M ..^N) \land K \neq M) \to \neg K = M$
16	13 15	orcnd	$⊢ (K \in (M ..^N) \land K \neq M) \to K \in (M + 1 ..^N)$

Metamath Proof Explorer