Theorem fzosubel

Description: Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015)

	Ref	Expression
Assertion	fzosubel	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A - D ) e. ( ( B - D ) ..^ ( C - D ) ) )

Proof

Step	Hyp	Ref	Expression
1		znegcl	|- ( D e. ZZ -> -u D e. ZZ )
2		fzoaddel	|- ( ( A e. ( B ..^ C ) /\ -u D e. ZZ ) -> ( A + -u D ) e. ( ( B + -u D ) ..^ ( C + -u D ) ) )
3	1 2	sylan2	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A + -u D ) e. ( ( B + -u D ) ..^ ( C + -u D ) ) )
4		elfzoelz	|- ( A e. ( B ..^ C ) -> A e. ZZ )
5	4	adantr	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> A e. ZZ )
6	5	zcnd	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> A e. CC )
7		simpr	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> D e. ZZ )
8	7	zcnd	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> D e. CC )
9	6 8	negsubd	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A + -u D ) = ( A - D ) )
10		elfzoel1	|- ( A e. ( B ..^ C ) -> B e. ZZ )
11	10	adantr	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> B e. ZZ )
12	11	zcnd	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> B e. CC )
13	12 8	negsubd	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( B + -u D ) = ( B - D ) )
14		elfzoel2	|- ( A e. ( B ..^ C ) -> C e. ZZ )
15	14	adantr	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> C e. ZZ )
16	15	zcnd	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> C e. CC )
17	16 8	negsubd	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( C + -u D ) = ( C - D ) )
18	13 17	oveq12d	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( ( B + -u D ) ..^ ( C + -u D ) ) = ( ( B - D ) ..^ ( C - D ) ) )
19	3 9 18	3eltr3d	|- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) -> ( A - D ) e. ( ( B - D ) ..^ ( C - D ) ) )