fzofzp1

Description: If a point is in a half-open range, the next point is in the closed range. (Contributed by Stefan O'Rear, 23-Aug-2015)

		Ref	Expression
	Assertion	fzofzp1	$⊢ C \in (A ..^B) \to C + 1 \in (A \dots B)$

Step	Hyp	Ref	Expression
1		elfzoel1	$⊢ C \in (A ..^B) \to A \in ℤ$
2		uzid	$⊢ A \in ℤ \to A \in ℤ_{\geq A}$
3		peano2uz	$⊢ A \in ℤ_{\geq A} \to A + 1 \in ℤ_{\geq A}$
4		fzoss1	$⊢ A + 1 \in ℤ_{\geq A} \to (A + 1 ..^B + 1) \subseteq (A ..^B + 1)$
5	1 2 3 4	4syl	$⊢ C \in (A ..^B) \to (A + 1 ..^B + 1) \subseteq (A ..^B + 1)$
6		1z	$⊢ 1 \in ℤ$
7		fzoaddel	$⊢ (C \in (A ..^B) \land 1 \in ℤ) \to C + 1 \in (A + 1 ..^B + 1)$
8	6 7	mpan2	$⊢ C \in (A ..^B) \to C + 1 \in (A + 1 ..^B + 1)$
9	5 8	sseldd	$⊢ C \in (A ..^B) \to C + 1 \in (A ..^B + 1)$
10		elfzoel2	$⊢ C \in (A ..^B) \to B \in ℤ$
11		fzval3	$⊢ B \in ℤ \to (A \dots B) = (A ..^B + 1)$
12	10 11	syl	$⊢ C \in (A ..^B) \to (A \dots B) = (A ..^B + 1)$
13	9 12	eleqtrrd	$⊢ C \in (A ..^B) \to C + 1 \in (A \dots B)$

Metamath Proof Explorer