Theorem fzocatel

Description: Translate membership in a half-open integer range. (Contributed by Thierry Arnoux, 28-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		simplr	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) )
2		fzospliti	⊢ ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ ( 0 ..^ 𝐵 ) ∨ 𝐴 ∈ ( 𝐵 ..^ ( 𝐵 + 𝐶 ) ) ) )
3	2	ad2ant2r	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴 ∈ ( 0 ..^ 𝐵 ) ∨ 𝐴 ∈ ( 𝐵 ..^ ( 𝐵 + 𝐶 ) ) ) )
4	3	ord	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) → 𝐴 ∈ ( 𝐵 ..^ ( 𝐵 + 𝐶 ) ) ) )
5	1 4	mpd	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝐴 ∈ ( 𝐵 ..^ ( 𝐵 + 𝐶 ) ) )
6		simprl	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝐵 ∈ ℤ )
7		fzosubel	⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ ( 𝐵 + 𝐶 ) ) ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ( ( 𝐵 − 𝐵 ) ..^ ( ( 𝐵 + 𝐶 ) − 𝐵 ) ) )
8	5 6 7	syl2anc	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴 − 𝐵 ) ∈ ( ( 𝐵 − 𝐵 ) ..^ ( ( 𝐵 + 𝐶 ) − 𝐵 ) ) )
9		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
10	9	subidd	⊢ ( 𝐵 ∈ ℤ → ( 𝐵 − 𝐵 ) = 0 )
11	6 10	syl	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐵 − 𝐵 ) = 0 )
12	6	zcnd	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
13		simprr	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝐶 ∈ ℤ )
14	13	zcnd	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝐶 ∈ ℂ )
15	12 14	pncan2d	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ( 𝐵 + 𝐶 ) − 𝐵 ) = 𝐶 )
16	11 15	oveq12d	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ( 𝐵 − 𝐵 ) ..^ ( ( 𝐵 + 𝐶 ) − 𝐵 ) ) = ( 0 ..^ 𝐶 ) )
17	8 16	eleqtrd	⊢ ( ( ( 𝐴 ∈ ( 0 ..^ ( 𝐵 + 𝐶 ) ) ∧ ¬ 𝐴 ∈ ( 0 ..^ 𝐵 ) ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴 − 𝐵 ) ∈ ( 0 ..^ 𝐶 ) )