This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ..^ 𝐶 ) )