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

Metamath Proof Explorer

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