Theorem fzosubel

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

	Ref	Expression
Assertion	fzosubel	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐴 − 𝐷 ) ∈ ( ( 𝐵 − 𝐷 ) ..^ ( 𝐶 − 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		znegcl	⊢ ( 𝐷 ∈ ℤ → - 𝐷 ∈ ℤ )
2		fzoaddel	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ - 𝐷 ∈ ℤ ) → ( 𝐴 + - 𝐷 ) ∈ ( ( 𝐵 + - 𝐷 ) ..^ ( 𝐶 + - 𝐷 ) ) )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐴 + - 𝐷 ) ∈ ( ( 𝐵 + - 𝐷 ) ..^ ( 𝐶 + - 𝐷 ) ) )
4		elfzoelz	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐴 ∈ ℤ )
5	4	adantr	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐴 ∈ ℤ )
6	5	zcnd	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐴 ∈ ℂ )
7		simpr	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐷 ∈ ℤ )
8	7	zcnd	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐷 ∈ ℂ )
9	6 8	negsubd	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐴 + - 𝐷 ) = ( 𝐴 − 𝐷 ) )
10		elfzoel1	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐵 ∈ ℤ )
11	10	adantr	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐵 ∈ ℤ )
12	11	zcnd	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐵 ∈ ℂ )
13	12 8	negsubd	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐵 + - 𝐷 ) = ( 𝐵 − 𝐷 ) )
14		elfzoel2	⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐶 ∈ ℤ )
15	14	adantr	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐶 ∈ ℤ )
16	15	zcnd	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐶 ∈ ℂ )
17	16 8	negsubd	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐶 + - 𝐷 ) = ( 𝐶 − 𝐷 ) )
18	13 17	oveq12d	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( ( 𝐵 + - 𝐷 ) ..^ ( 𝐶 + - 𝐷 ) ) = ( ( 𝐵 − 𝐷 ) ..^ ( 𝐶 − 𝐷 ) ) )
19	3 9 18	3eltr3d	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐴 − 𝐷 ) ∈ ( ( 𝐵 − 𝐷 ) ..^ ( 𝐶 − 𝐷 ) ) )