fzp1disj

Description: ( M ... ( N + 1 ) ) is the disjoint union of ( M ... N ) with { ( N + 1 ) } . (Contributed by Mario Carneiro, 7-Mar-2014)

		Ref	Expression
	Assertion	fzp1disj	$⊢ (M \dots N) \cap \{N + 1\} = \emptyset$

Step	Hyp	Ref	Expression
1		elfzle2	$⊢ N + 1 \in (M \dots N) \to N + 1 \leq N$
2		elfzel2	$⊢ N + 1 \in (M \dots N) \to N \in ℤ$
3	2	zred	$⊢ N + 1 \in (M \dots N) \to N \in ℝ$
4		ltp1	$⊢ N \in ℝ \to N < N + 1$
5		peano2re	$⊢ N \in ℝ \to N + 1 \in ℝ$
6		ltnle	$⊢ (N \in ℝ \land N + 1 \in ℝ) \to (N < N + 1 \leftrightarrow \neg N + 1 \leq N)$
7	5 6	mpdan	$⊢ N \in ℝ \to (N < N + 1 \leftrightarrow \neg N + 1 \leq N)$
8	4 7	mpbid	$⊢ N \in ℝ \to \neg N + 1 \leq N$
9	3 8	syl	$⊢ N + 1 \in (M \dots N) \to \neg N + 1 \leq N$
10	1 9	pm2.65i	$⊢ \neg N + 1 \in (M \dots N)$
11		disjsn	$⊢ (M \dots N) \cap \{N + 1\} = \emptyset \leftrightarrow \neg N + 1 \in (M \dots N)$
12	10 11	mpbir	$⊢ (M \dots N) \cap \{N + 1\} = \emptyset$

Metamath Proof Explorer