Theorem fzosubel3

Description: Membership in a translated half-open integer range when the original range is zero-based. (Contributed by Stefan O'Rear, 15-Aug-2015)

	Ref	Expression
Assertion	fzosubel3	|- ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> ( A - B ) e. ( 0 ..^ D ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> A e. ( B ..^ ( B + D ) ) )
2		elfzoel1	|- ( A e. ( B ..^ ( B + D ) ) -> B e. ZZ )
3	2	adantr	|- ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> B e. ZZ )
4	3	zcnd	|- ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> B e. CC )
5	4	addid1d	|- ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> ( B + 0 ) = B )
6	5	oveq1d	|- ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> ( ( B + 0 ) ..^ ( B + D ) ) = ( B ..^ ( B + D ) ) )
7	1 6	eleqtrrd	|- ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> A e. ( ( B + 0 ) ..^ ( B + D ) ) )
8		0zd	|- ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> 0 e. ZZ )
9		simpr	|- ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> D e. ZZ )
10		fzosubel2	|- ( ( A e. ( ( B + 0 ) ..^ ( B + D ) ) /\ ( B e. ZZ /\ 0 e. ZZ /\ D e. ZZ ) ) -> ( A - B ) e. ( 0 ..^ D ) )
11	7 3 8 9 10	syl13anc	|- ( ( A e. ( B ..^ ( B + D ) ) /\ D e. ZZ ) -> ( A - B ) e. ( 0 ..^ D ) )