Theorem fzoend

Description: The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015)

	Ref	Expression
Assertion	fzoend	|- ( A e. ( A ..^ B ) -> ( B - 1 ) e. ( A ..^ B ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( A e. ( A ..^ B ) -> A e. ( A ..^ B ) )
2		elfzoel2	|- ( A e. ( A ..^ B ) -> B e. ZZ )
3		fzoval	|- ( B e. ZZ -> ( A ..^ B ) = ( A ... ( B - 1 ) ) )
4	2 3	syl	|- ( A e. ( A ..^ B ) -> ( A ..^ B ) = ( A ... ( B - 1 ) ) )
5	1 4	eleqtrd	|- ( A e. ( A ..^ B ) -> A e. ( A ... ( B - 1 ) ) )
6		elfzuz3	|- ( A e. ( A ... ( B - 1 ) ) -> ( B - 1 ) e. ( ZZ>= ` A ) )
7	5 6	syl	|- ( A e. ( A ..^ B ) -> ( B - 1 ) e. ( ZZ>= ` A ) )
8		eluzfz2	|- ( ( B - 1 ) e. ( ZZ>= ` A ) -> ( B - 1 ) e. ( A ... ( B - 1 ) ) )
9	7 8	syl	|- ( A e. ( A ..^ B ) -> ( B - 1 ) e. ( A ... ( B - 1 ) ) )
10	9 4	eleqtrrd	|- ( A e. ( A ..^ B ) -> ( B - 1 ) e. ( A ..^ B ) )