fzopredsuc

Description: Join a predecessor and a successor to the beginning and the end of an open integer interval. This theorem holds even if N = M (then ( M ... N ) = { M } = ( { M } u. (/) ) u. { M } ) . (Contributed by AV, 14-Jul-2020)

		Ref	Expression
	Assertion	fzopredsuc	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = (\{M\} \cup (M + 1 ..^N)) \cup \{N\}$

Proof

Step	Hyp	Ref	Expression
1		unidm	$⊢ \{N\} \cup \{N\} = \{N\}$
2	1	eqcomi	$⊢ \{N\} = \{N\} \cup \{N\}$
3		oveq1	$⊢ M = N \to (M \dots N) = (N \dots N)$
4		fzsn	$⊢ N \in ℤ \to (N \dots N) = \{N\}$
5	3 4	sylan9eqr	$⊢ (N \in ℤ \land M = N) \to (M \dots N) = \{N\}$
6		sneq	$⊢ M = N \to \{M\} = \{N\}$
7		oveq1	$⊢ M = N \to M + 1 = N + 1$
8	7	oveq1d	$⊢ M = N \to (M + 1 ..^N) = (N + 1 ..^N)$
9	6 8	uneq12d	$⊢ M = N \to \{M\} \cup (M + 1 ..^N) = \{N\} \cup (N + 1 ..^N)$
10	9	uneq1d	$⊢ M = N \to (\{M\} \cup (M + 1 ..^N)) \cup \{N\} = (\{N\} \cup (N + 1 ..^N)) \cup \{N\}$
11		zre	$⊢ N \in ℤ \to N \in ℝ$
12	11	lep1d	$⊢ N \in ℤ \to N \leq N + 1$
13		peano2z	$⊢ N \in ℤ \to N + 1 \in ℤ$
14	13	zred	$⊢ N \in ℤ \to N + 1 \in ℝ$
15	11 14	lenltd	$⊢ N \in ℤ \to (N \leq N + 1 \leftrightarrow \neg N + 1 < N)$
16	12 15	mpbid	$⊢ N \in ℤ \to \neg N + 1 < N$
17		fzonlt0	$⊢ (N + 1 \in ℤ \land N \in ℤ) \to (\neg N + 1 < N \leftrightarrow (N + 1 ..^N) = \emptyset)$
18	13 17	mpancom	$⊢ N \in ℤ \to (\neg N + 1 < N \leftrightarrow (N + 1 ..^N) = \emptyset)$
19	16 18	mpbid	$⊢ N \in ℤ \to (N + 1 ..^N) = \emptyset$
20	19	uneq2d	$⊢ N \in ℤ \to \{N\} \cup (N + 1 ..^N) = \{N\} \cup \emptyset$
21		un0	$⊢ \{N\} \cup \emptyset = \{N\}$
22	20 21	eqtrdi	$⊢ N \in ℤ \to \{N\} \cup (N + 1 ..^N) = \{N\}$
23	22	uneq1d	$⊢ N \in ℤ \to (\{N\} \cup (N + 1 ..^N)) \cup \{N\} = \{N\} \cup \{N\}$
24	10 23	sylan9eqr	$⊢ (N \in ℤ \land M = N) \to (\{M\} \cup (M + 1 ..^N)) \cup \{N\} = \{N\} \cup \{N\}$
25	2 5 24	3eqtr4a	$⊢ (N \in ℤ \land M = N) \to (M \dots N) = (\{M\} \cup (M + 1 ..^N)) \cup \{N\}$
26	25	ex	$⊢ N \in ℤ \to (M = N \to (M \dots N) = (\{M\} \cup (M + 1 ..^N)) \cup \{N\})$
27		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
28	26 27	syl11	$⊢ M = N \to (N \in ℤ_{\geq M} \to (M \dots N) = (\{M\} \cup (M + 1 ..^N)) \cup \{N\})$
29		fzisfzounsn	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = (M ..^N) \cup \{N\}$
30	29	adantl	$⊢ (\neg M = N \land N \in ℤ_{\geq M}) \to (M \dots N) = (M ..^N) \cup \{N\}$
31		eluz2	$⊢ N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N \in ℤ \land M \leq N)$
32		simpl1	$⊢ ((M \in ℤ \land N \in ℤ \land M \leq N) \land \neg M = N) \to M \in ℤ$
33		simpl2	$⊢ ((M \in ℤ \land N \in ℤ \land M \leq N) \land \neg M = N) \to N \in ℤ$
34		nesym	$⊢ N \neq M \leftrightarrow \neg M = N$
35		zre	$⊢ M \in ℤ \to M \in ℝ$
36		ltlen	$⊢ (M \in ℝ \land N \in ℝ) \to (M < N \leftrightarrow (M \leq N \land N \neq M))$
37	35 11 36	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow (M \leq N \land N \neq M))$
38	37	biimprd	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \leq N \land N \neq M) \to M < N)$
39	38	exp4b	$⊢ M \in ℤ \to (N \in ℤ \to (M \leq N \to (N \neq M \to M < N)))$
40	39	3imp	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to (N \neq M \to M < N)$
41	34 40	syl5bir	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to (\neg M = N \to M < N)$
42	41	imp	$⊢ ((M \in ℤ \land N \in ℤ \land M \leq N) \land \neg M = N) \to M < N$
43	32 33 42	3jca	$⊢ ((M \in ℤ \land N \in ℤ \land M \leq N) \land \neg M = N) \to (M \in ℤ \land N \in ℤ \land M < N)$
44	43	ex	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to (\neg M = N \to (M \in ℤ \land N \in ℤ \land M < N))$
45	31 44	sylbi	$⊢ N \in ℤ_{\geq M} \to (\neg M = N \to (M \in ℤ \land N \in ℤ \land M < N))$
46	45	impcom	$⊢ (\neg M = N \land N \in ℤ_{\geq M}) \to (M \in ℤ \land N \in ℤ \land M < N)$
47		fzopred	$⊢ (M \in ℤ \land N \in ℤ \land M < N) \to (M ..^N) = \{M\} \cup (M + 1 ..^N)$
48	46 47	syl	$⊢ (\neg M = N \land N \in ℤ_{\geq M}) \to (M ..^N) = \{M\} \cup (M + 1 ..^N)$
49	48	uneq1d	$⊢ (\neg M = N \land N \in ℤ_{\geq M}) \to (M ..^N) \cup \{N\} = (\{M\} \cup (M + 1 ..^N)) \cup \{N\}$
50	30 49	eqtrd	$⊢ (\neg M = N \land N \in ℤ_{\geq M}) \to (M \dots N) = (\{M\} \cup (M + 1 ..^N)) \cup \{N\}$
51	50	ex	$⊢ \neg M = N \to (N \in ℤ_{\geq M} \to (M \dots N) = (\{M\} \cup (M + 1 ..^N)) \cup \{N\})$
52	28 51	pm2.61i	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = (\{M\} \cup (M + 1 ..^N)) \cup \{N\}$

Metamath Proof Explorer

Theorem fzopredsuc

Proof