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

Metamath Proof Explorer

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 addlid ⊢ ( 𝐶 ∈ ℂ → ( 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 ..^ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 + 𝐶 ) ∈ ( 𝐶 ..^ 𝐵 ) )