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

Metamath Proof Explorer

Theorem shftuz

Description: A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013)

Ref Expression
Assertion shftuz ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) } = ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 df-rab ⊢ { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) } = { 𝑥 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) }
2 simp2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝑥 ∈ ℂ )
3 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
4 3 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝐴 ∈ ℂ )
5 2 4 npcand ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) = 𝑥 )
6 eluzadd ⊢ ( ( ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) )
7 6 ancoms ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) )
8 7 3adant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) → ( ( 𝑥 − 𝐴 ) + 𝐴 ) ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) )
9 5 8 eqeltrrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝑥 ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) )
10 9 3expib ⊢ ( 𝐴 ∈ ℤ → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝑥 ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) ) )
11 10 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝑥 ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) ) )
12 eluzelcn ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) → 𝑥 ∈ ℂ )
13 12 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) → 𝑥 ∈ ℂ ) )
14 eluzsub ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑥 ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) ) → ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) )
15 14 3expia ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) → ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) )
16 15 ancoms ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) → ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) )
17 13 16 jcad ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) → ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) ) )
18 11 17 impbid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) ↔ 𝑥 ∈ ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) ) )
19 18 eqabcdv ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { 𝑥 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) } = ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) )
20 1 19 eqtrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) } = ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) )