elfzolborelfzop1

Description: An element of a half-open integer interval is either equal to the left bound of the interval or an element of a half-open integer interval with a lower bound increased by 1. (Contributed by AV, 2-Jun-2020)

		Ref	Expression
	Assertion	elfzolborelfzop1	$⊢ K \in (M ..^N) \to (K = M \lor K \in (M + 1 ..^N))$

Proof

Step	Hyp	Ref	Expression
1		elfzo2	$⊢ K \in (M ..^N) \leftrightarrow (K \in ℤ_{\geq M} \land N \in ℤ \land K < N)$
2		eluz2	$⊢ K \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land K \in ℤ \land M \leq K)$
3		zre	$⊢ M \in ℤ \to M \in ℝ$
4		zre	$⊢ K \in ℤ \to K \in ℝ$
5		leloe	$⊢ (M \in ℝ \land K \in ℝ) \to (M \leq K \leftrightarrow (M < K \lor M = K))$
6	3 4 5	syl2an	$⊢ (M \in ℤ \land K \in ℤ) \to (M \leq K \leftrightarrow (M < K \lor M = K))$
7		peano2z	$⊢ M \in ℤ \to M + 1 \in ℤ$
8	7	adantr	$⊢ (M \in ℤ \land K \in ℤ) \to M + 1 \in ℤ$
9	8	ad2antrl	$⊢ (M < K \land ((M \in ℤ \land K \in ℤ) \land N \in ℤ)) \to M + 1 \in ℤ$
10		simprlr	$⊢ (M < K \land ((M \in ℤ \land K \in ℤ) \land N \in ℤ)) \to K \in ℤ$
11		simpl	$⊢ (M < K \land ((M \in ℤ \land K \in ℤ) \land N \in ℤ)) \to M < K$
12		zltp1le	$⊢ (M \in ℤ \land K \in ℤ) \to (M < K \leftrightarrow M + 1 \leq K)$
13	12	ad2antrl	$⊢ (M < K \land ((M \in ℤ \land K \in ℤ) \land N \in ℤ)) \to (M < K \leftrightarrow M + 1 \leq K)$
14	11 13	mpbid	$⊢ (M < K \land ((M \in ℤ \land K \in ℤ) \land N \in ℤ)) \to M + 1 \leq K$
15	9 10 14	3jca	$⊢ (M < K \land ((M \in ℤ \land K \in ℤ) \land N \in ℤ)) \to (M + 1 \in ℤ \land K \in ℤ \land M + 1 \leq K)$
16	15	adantr	$⊢ ((M < K \land ((M \in ℤ \land K \in ℤ) \land N \in ℤ)) \land K < N) \to (M + 1 \in ℤ \land K \in ℤ \land M + 1 \leq K)$
17		simplrr	$⊢ ((M < K \land ((M \in ℤ \land K \in ℤ) \land N \in ℤ)) \land K < N) \to N \in ℤ$
18		simpr	$⊢ ((M < K \land ((M \in ℤ \land K \in ℤ) \land N \in ℤ)) \land K < N) \to K < N$
19		elfzo2	$⊢ K \in (M + 1 ..^N) \leftrightarrow (K \in ℤ_{\geq (M + 1)} \land N \in ℤ \land K < N)$
20		eluz2	$⊢ K \in ℤ_{\geq (M + 1)} \leftrightarrow (M + 1 \in ℤ \land K \in ℤ \land M + 1 \leq K)$
21	20	3anbi1i	$⊢ (K \in ℤ_{\geq (M + 1)} \land N \in ℤ \land K < N) \leftrightarrow ((M + 1 \in ℤ \land K \in ℤ \land M + 1 \leq K) \land N \in ℤ \land K < N)$
22	19 21	bitri	$⊢ K \in (M + 1 ..^N) \leftrightarrow ((M + 1 \in ℤ \land K \in ℤ \land M + 1 \leq K) \land N \in ℤ \land K < N)$
23	16 17 18 22	syl3anbrc	$⊢ ((M < K \land ((M \in ℤ \land K \in ℤ) \land N \in ℤ)) \land K < N) \to K \in (M + 1 ..^N)$
24	23	olcd	$⊢ ((M < K \land ((M \in ℤ \land K \in ℤ) \land N \in ℤ)) \land K < N) \to (K = M \lor K \in (M + 1 ..^N))$
25	24	exp31	$⊢ M < K \to (((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to (K < N \to (K = M \lor K \in (M + 1 ..^N))))$
26		orc	$⊢ K = M \to (K = M \lor K \in (M + 1 ..^N))$
27	26	eqcoms	$⊢ M = K \to (K = M \lor K \in (M + 1 ..^N))$
28	27	2a1d	$⊢ M = K \to (((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to (K < N \to (K = M \lor K \in (M + 1 ..^N))))$
29	25 28	jaoi	$⊢ (M < K \lor M = K) \to (((M \in ℤ \land K \in ℤ) \land N \in ℤ) \to (K < N \to (K = M \lor K \in (M + 1 ..^N))))$
30	29	expd	$⊢ (M < K \lor M = K) \to ((M \in ℤ \land K \in ℤ) \to (N \in ℤ \to (K < N \to (K = M \lor K \in (M + 1 ..^N)))))$
31	30	com12	$⊢ (M \in ℤ \land K \in ℤ) \to ((M < K \lor M = K) \to (N \in ℤ \to (K < N \to (K = M \lor K \in (M + 1 ..^N)))))$
32	6 31	sylbid	$⊢ (M \in ℤ \land K \in ℤ) \to (M \leq K \to (N \in ℤ \to (K < N \to (K = M \lor K \in (M + 1 ..^N)))))$
33	32	3impia	$⊢ (M \in ℤ \land K \in ℤ \land M \leq K) \to (N \in ℤ \to (K < N \to (K = M \lor K \in (M + 1 ..^N))))$
34	2 33	sylbi	$⊢ K \in ℤ_{\geq M} \to (N \in ℤ \to (K < N \to (K = M \lor K \in (M + 1 ..^N))))$
35	34	3imp	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ \land K < N) \to (K = M \lor K \in (M + 1 ..^N))$
36	1 35	sylbi	$⊢ K \in (M ..^N) \to (K = M \lor K \in (M + 1 ..^N))$

Metamath Proof Explorer

Theorem elfzolborelfzop1

Proof