Theorem fzoaddel2

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

	Ref	Expression
Assertion	fzoaddel2	⊢ ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 + 𝐶 ) ∈ ( 𝐶 ..^ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fzoaddel	⊢ ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 − 𝐶 ) ) ∧ 𝐶 ∈ ℤ ) → ( 𝐴 + 𝐶 ) ∈ ( ( 0 + 𝐶 ) ..^ ( ( 𝐵 − 𝐶 ) + 𝐶 ) ) )
2	1	3adant2	⊢ ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 + 𝐶 ) ∈ ( ( 0 + 𝐶 ) ..^ ( ( 𝐵 − 𝐶 ) + 𝐶 ) ) )
3		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
4		zcn	⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
5		addid2	⊢ ( 𝐶 ∈ ℂ → ( 0 + 𝐶 ) = 𝐶 )
6	5	adantl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 0 + 𝐶 ) = 𝐶 )
7		npcan	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) + 𝐶 ) = 𝐵 )
8	6 7	oveq12d	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 0 + 𝐶 ) ..^ ( ( 𝐵 − 𝐶 ) + 𝐶 ) ) = ( 𝐶 ..^ 𝐵 ) )
9	3 4 8	syl2an	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 0 + 𝐶 ) ..^ ( ( 𝐵 − 𝐶 ) + 𝐶 ) ) = ( 𝐶 ..^ 𝐵 ) )
10	9	3adant1	⊢ ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 0 + 𝐶 ) ..^ ( ( 𝐵 − 𝐶 ) + 𝐶 ) ) = ( 𝐶 ..^ 𝐵 ) )
11	2 10	eleqtrd	⊢ ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 + 𝐶 ) ∈ ( 𝐶 ..^ 𝐵 ) )