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

Metamath Proof Explorer

Theorem fzosubel

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

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

Proof

Step Hyp Ref Expression
1 znegcl ⊢ ( 𝐷 ∈ ℤ → - 𝐷 ∈ ℤ )
2 fzoaddel ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ - 𝐷 ∈ ℤ ) → ( 𝐴 + - 𝐷 ) ∈ ( ( 𝐵 + - 𝐷 ) ..^ ( 𝐶 + - 𝐷 ) ) )
3 1 2 sylan2 ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐴 + - 𝐷 ) ∈ ( ( 𝐵 + - 𝐷 ) ..^ ( 𝐶 + - 𝐷 ) ) )
4 elfzoelz ⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐴 ∈ ℤ )
5 4 adantr ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐴 ∈ ℤ )
6 5 zcnd ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐴 ∈ ℂ )
7 simpr ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐷 ∈ ℤ )
8 7 zcnd ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐷 ∈ ℂ )
9 6 8 negsubd ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐴 + - 𝐷 ) = ( 𝐴 − 𝐷 ) )
10 elfzoel1 ⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐵 ∈ ℤ )
11 10 adantr ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐵 ∈ ℤ )
12 11 zcnd ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐵 ∈ ℂ )
13 12 8 negsubd ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐵 + - 𝐷 ) = ( 𝐵 − 𝐷 ) )
14 elfzoel2 ⊢ ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) → 𝐶 ∈ ℤ )
15 14 adantr ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐶 ∈ ℤ )
16 15 zcnd ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → 𝐶 ∈ ℂ )
17 16 8 negsubd ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐶 + - 𝐷 ) = ( 𝐶 − 𝐷 ) )
18 13 17 oveq12d ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( ( 𝐵 + - 𝐷 ) ..^ ( 𝐶 + - 𝐷 ) ) = ( ( 𝐵 − 𝐷 ) ..^ ( 𝐶 − 𝐷 ) ) )
19 3 9 18 3eltr3d ⊢ ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐴 − 𝐷 ) ∈ ( ( 𝐵 − 𝐷 ) ..^ ( 𝐶 − 𝐷 ) ) )