fzm1

Description: Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	fzm1	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \leftrightarrow (K \in (M \dots N - 1) \lor K = N))$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ N = M \to (N \dots N) = (M \dots N)$
2	1	eleq2d	$⊢ N = M \to (K \in (N \dots N) \leftrightarrow K \in (M \dots N))$
3		elfz1eq	$⊢ K \in (N \dots N) \to K = N$
4	2 3	syl6bir	$⊢ N = M \to (K \in (M \dots N) \to K = N)$
5		olc	$⊢ K = N \to (K \in (M \dots N - 1) \lor K = N)$
6	4 5	syl6	$⊢ N = M \to (K \in (M \dots N) \to (K \in (M \dots N - 1) \lor K = N))$
7	6	adantl	$⊢ (N \in ℤ_{\geq M} \land N = M) \to (K \in (M \dots N) \to (K \in (M \dots N - 1) \lor K = N))$
8		noel	$⊢ \neg K \in \emptyset$
9		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
10	9	adantr	$⊢ (N \in ℤ_{\geq M} \land N = M) \to N \in ℤ$
11	10	zred	$⊢ (N \in ℤ_{\geq M} \land N = M) \to N \in ℝ$
12	11	ltm1d	$⊢ (N \in ℤ_{\geq M} \land N = M) \to N - 1 < N$
13		breq2	$⊢ N = M \to (N - 1 < N \leftrightarrow N - 1 < M)$
14	13	adantl	$⊢ (N \in ℤ_{\geq M} \land N = M) \to (N - 1 < N \leftrightarrow N - 1 < M)$
15	12 14	mpbid	$⊢ (N \in ℤ_{\geq M} \land N = M) \to N - 1 < M$
16		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
17		1zzd	$⊢ (N \in ℤ_{\geq M} \land N = M) \to 1 \in ℤ$
18	10 17	zsubcld	$⊢ (N \in ℤ_{\geq M} \land N = M) \to N - 1 \in ℤ$
19		fzn	$⊢ (M \in ℤ \land N - 1 \in ℤ) \to (N - 1 < M \leftrightarrow (M \dots N - 1) = \emptyset)$
20	16 18 19	syl2an2r	$⊢ (N \in ℤ_{\geq M} \land N = M) \to (N - 1 < M \leftrightarrow (M \dots N - 1) = \emptyset)$
21	15 20	mpbid	$⊢ (N \in ℤ_{\geq M} \land N = M) \to (M \dots N - 1) = \emptyset$
22	21	eleq2d	$⊢ (N \in ℤ_{\geq M} \land N = M) \to (K \in (M \dots N - 1) \leftrightarrow K \in \emptyset)$
23	8 22	mtbiri	$⊢ (N \in ℤ_{\geq M} \land N = M) \to \neg K \in (M \dots N - 1)$
24	23	pm2.21d	$⊢ (N \in ℤ_{\geq M} \land N = M) \to (K \in (M \dots N - 1) \to K \in (M \dots N))$
25		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
26	25	ad2antrr	$⊢ ((N \in ℤ_{\geq M} \land N = M) \land K = N) \to N \in (M \dots N)$
27		eleq1	$⊢ K = N \to (K \in (M \dots N) \leftrightarrow N \in (M \dots N))$
28	27	adantl	$⊢ ((N \in ℤ_{\geq M} \land N = M) \land K = N) \to (K \in (M \dots N) \leftrightarrow N \in (M \dots N))$
29	26 28	mpbird	$⊢ ((N \in ℤ_{\geq M} \land N = M) \land K = N) \to K \in (M \dots N)$
30	29	ex	$⊢ (N \in ℤ_{\geq M} \land N = M) \to (K = N \to K \in (M \dots N))$
31	24 30	jaod	$⊢ (N \in ℤ_{\geq M} \land N = M) \to ((K \in (M \dots N - 1) \lor K = N) \to K \in (M \dots N))$
32	7 31	impbid	$⊢ (N \in ℤ_{\geq M} \land N = M) \to (K \in (M \dots N) \leftrightarrow (K \in (M \dots N - 1) \lor K = N))$
33		elfzp1	$⊢ N - 1 \in ℤ_{\geq M} \to (K \in (M \dots N - 1 + 1) \leftrightarrow (K \in (M \dots N - 1) \lor K = N - 1 + 1))$
34	33	adantl	$⊢ (N \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq M}) \to (K \in (M \dots N - 1 + 1) \leftrightarrow (K \in (M \dots N - 1) \lor K = N - 1 + 1))$
35	9	adantr	$⊢ (N \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq M}) \to N \in ℤ$
36	35	zcnd	$⊢ (N \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq M}) \to N \in ℂ$
37		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
38	36 37	syl	$⊢ (N \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq M}) \to N - 1 + 1 = N$
39	38	oveq2d	$⊢ (N \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq M}) \to (M \dots N - 1 + 1) = (M \dots N)$
40	39	eleq2d	$⊢ (N \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq M}) \to (K \in (M \dots N - 1 + 1) \leftrightarrow K \in (M \dots N))$
41	38	eqeq2d	$⊢ (N \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq M}) \to (K = N - 1 + 1 \leftrightarrow K = N)$
42	41	orbi2d	$⊢ (N \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq M}) \to ((K \in (M \dots N - 1) \lor K = N - 1 + 1) \leftrightarrow (K \in (M \dots N - 1) \lor K = N))$
43	34 40 42	3bitr3d	$⊢ (N \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq M}) \to (K \in (M \dots N) \leftrightarrow (K \in (M \dots N - 1) \lor K = N))$
44		uzm1	$⊢ N \in ℤ_{\geq M} \to (N = M \lor N - 1 \in ℤ_{\geq M})$
45	32 43 44	mpjaodan	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \leftrightarrow (K \in (M \dots N - 1) \lor K = N))$

Metamath Proof Explorer

Theorem fzm1

Proof