Theorem fzosubel2

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

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

Proof

Step	Hyp	Ref	Expression
1		fzosubel	⊢ ( ( 𝐴 ∈ ( ( 𝐵 + 𝐶 ) ..^ ( 𝐵 + 𝐷 ) ) ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ( ( ( 𝐵 + 𝐶 ) − 𝐵 ) ..^ ( ( 𝐵 + 𝐷 ) − 𝐵 ) ) )
2	1	3ad2antr1	⊢ ( ( 𝐴 ∈ ( ( 𝐵 + 𝐶 ) ..^ ( 𝐵 + 𝐷 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( 𝐴 − 𝐵 ) ∈ ( ( ( 𝐵 + 𝐶 ) − 𝐵 ) ..^ ( ( 𝐵 + 𝐷 ) − 𝐵 ) ) )
3		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
4		zcn	⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
5		zcn	⊢ ( 𝐷 ∈ ℤ → 𝐷 ∈ ℂ )
6		pncan2	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 + 𝐶 ) − 𝐵 ) = 𝐶 )
7	6	3adant3	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐵 + 𝐶 ) − 𝐵 ) = 𝐶 )
8		pncan2	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐵 + 𝐷 ) − 𝐵 ) = 𝐷 )
9	8	3adant2	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐵 + 𝐷 ) − 𝐵 ) = 𝐷 )
10	7 9	oveq12d	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( ( 𝐵 + 𝐶 ) − 𝐵 ) ..^ ( ( 𝐵 + 𝐷 ) − 𝐵 ) ) = ( 𝐶 ..^ 𝐷 ) )
11	3 4 5 10	syl3an	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ( ( 𝐵 + 𝐶 ) − 𝐵 ) ..^ ( ( 𝐵 + 𝐷 ) − 𝐵 ) ) = ( 𝐶 ..^ 𝐷 ) )
12	11	adantl	⊢ ( ( 𝐴 ∈ ( ( 𝐵 + 𝐶 ) ..^ ( 𝐵 + 𝐷 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( ( 𝐵 + 𝐶 ) − 𝐵 ) ..^ ( ( 𝐵 + 𝐷 ) − 𝐵 ) ) = ( 𝐶 ..^ 𝐷 ) )
13	2 12	eleqtrd	⊢ ( ( 𝐴 ∈ ( ( 𝐵 + 𝐶 ) ..^ ( 𝐵 + 𝐷 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( 𝐴 − 𝐵 ) ∈ ( 𝐶 ..^ 𝐷 ) )