fzdifsuc2

Description: Remove a successor from the end of a finite set of sequential integers. Similar to fzdifsuc , but with a weaker condition. (Contributed by Glauco Siliprandi, 5-Apr-2020)

		Ref	Expression
	Assertion	fzdifsuc2	$⊢ N \in ℤ_{\geq (M - 1)} \to (M \dots N) = (M \dots N + 1) ∖ \{N + 1\}$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to N = M - 1$
2		zre	$⊢ M \in ℤ \to M \in ℝ$
3	2	ad2antlr	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to M \in ℝ$
4	3	ltm1d	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to M - 1 < M$
5	1 4	eqbrtrd	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to N < M$
6		simplr	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to M \in ℤ$
7		eluzelz	$⊢ N \in ℤ_{\geq (M - 1)} \to N \in ℤ$
8	7	ad2antrr	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to N \in ℤ$
9		fzn	$⊢ (M \in ℤ \land N \in ℤ) \to (N < M \leftrightarrow (M \dots N) = \emptyset)$
10	6 8 9	syl2anc	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to (N < M \leftrightarrow (M \dots N) = \emptyset)$
11	5 10	mpbid	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to (M \dots N) = \emptyset$
12		difid	$⊢ \{M\} ∖ \{M\} = \emptyset$
13	12	a1i	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to \{M\} ∖ \{M\} = \emptyset$
14	13	eqcomd	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to \emptyset = \{M\} ∖ \{M\}$
15		oveq1	$⊢ N = M - 1 \to N + 1 = M - 1 + 1$
16	15	adantl	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to N + 1 = M - 1 + 1$
17	2	recnd	$⊢ M \in ℤ \to M \in ℂ$
18	17	ad2antlr	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to M \in ℂ$
19		1cnd	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to 1 \in ℂ$
20	18 19	npcand	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to M - 1 + 1 = M$
21	16 20	eqtrd	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to N + 1 = M$
22	21	oveq2d	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to (M \dots N + 1) = (M \dots M)$
23		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
24	23	ad2antlr	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to (M \dots M) = \{M\}$
25	22 24	eqtr2d	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to \{M\} = (M \dots N + 1)$
26	21	eqcomd	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to M = N + 1$
27	26	sneqd	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to \{M\} = \{N + 1\}$
28	25 27	difeq12d	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to \{M\} ∖ \{M\} = (M \dots N + 1) ∖ \{N + 1\}$
29	11 14 28	3eqtrd	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land N = M - 1) \to (M \dots N) = (M \dots N + 1) ∖ \{N + 1\}$
30		simplr	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to M \in ℤ$
31	7	ad2antrr	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to N \in ℤ$
32	2	ad2antlr	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to M \in ℝ$
33		1red	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to 1 \in ℝ$
34	32 33	resubcld	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to M - 1 \in ℝ$
35	31	zred	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to N \in ℝ$
36		eluzle	$⊢ N \in ℤ_{\geq (M - 1)} \to M - 1 \leq N$
37	36	ad2antrr	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to M - 1 \leq N$
38		neqne	$⊢ \neg N = M - 1 \to N \neq M - 1$
39	38	adantl	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to N \neq M - 1$
40	34 35 37 39	leneltd	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to M - 1 < N$
41		zlem1lt	$⊢ (M \in ℤ \land N \in ℤ) \to (M \leq N \leftrightarrow M - 1 < N)$
42	30 31 41	syl2anc	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to (M \leq N \leftrightarrow M - 1 < N)$
43	40 42	mpbird	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to M \leq N$
44	30 31 43	3jca	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to (M \in ℤ \land N \in ℤ \land M \leq N)$
45		eluz2	$⊢ N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N \in ℤ \land M \leq N)$
46	44 45	sylibr	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to N \in ℤ_{\geq M}$
47		fzdifsuc	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = (M \dots N + 1) ∖ \{N + 1\}$
48	46 47	syl	$⊢ ((N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \land \neg N = M - 1) \to (M \dots N) = (M \dots N + 1) ∖ \{N + 1\}$
49	29 48	pm2.61dan	$⊢ (N \in ℤ_{\geq (M - 1)} \land M \in ℤ) \to (M \dots N) = (M \dots N + 1) ∖ \{N + 1\}$
50		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
51	50	con3i	$⊢ \neg M \in ℤ \to \neg N \in ℤ_{\geq M}$
52		fzn0	$⊢ (M \dots N) \neq \emptyset \leftrightarrow N \in ℤ_{\geq M}$
53	51 52	sylnibr	$⊢ \neg M \in ℤ \to \neg (M \dots N) \neq \emptyset$
54		nne	$⊢ \neg (M \dots N) \neq \emptyset \leftrightarrow (M \dots N) = \emptyset$
55	53 54	sylib	$⊢ \neg M \in ℤ \to (M \dots N) = \emptyset$
56		eluzel2	$⊢ N + 1 \in ℤ_{\geq M} \to M \in ℤ$
57	56	con3i	$⊢ \neg M \in ℤ \to \neg N + 1 \in ℤ_{\geq M}$
58		fzn0	$⊢ (M \dots N + 1) \neq \emptyset \leftrightarrow N + 1 \in ℤ_{\geq M}$
59	57 58	sylnibr	$⊢ \neg M \in ℤ \to \neg (M \dots N + 1) \neq \emptyset$
60		nne	$⊢ \neg (M \dots N + 1) \neq \emptyset \leftrightarrow (M \dots N + 1) = \emptyset$
61	59 60	sylib	$⊢ \neg M \in ℤ \to (M \dots N + 1) = \emptyset$
62	61	difeq1d	$⊢ \neg M \in ℤ \to (M \dots N + 1) ∖ \{N + 1\} = \emptyset ∖ \{N + 1\}$
63		0dif	$⊢ \emptyset ∖ \{N + 1\} = \emptyset$
64	63	a1i	$⊢ \neg M \in ℤ \to \emptyset ∖ \{N + 1\} = \emptyset$
65	62 64	eqtr2d	$⊢ \neg M \in ℤ \to \emptyset = (M \dots N + 1) ∖ \{N + 1\}$
66	55 65	eqtrd	$⊢ \neg M \in ℤ \to (M \dots N) = (M \dots N + 1) ∖ \{N + 1\}$
67	66	adantl	$⊢ (N \in ℤ_{\geq (M - 1)} \land \neg M \in ℤ) \to (M \dots N) = (M \dots N + 1) ∖ \{N + 1\}$
68	49 67	pm2.61dan	$⊢ N \in ℤ_{\geq (M - 1)} \to (M \dots N) = (M \dots N + 1) ∖ \{N + 1\}$

Metamath Proof Explorer

Theorem fzdifsuc2

Proof