# Metamath Proof Explorer

## Theorem shftuz

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

Ref Expression
Assertion shftuz ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left\{{x}\in ℂ|{x}-{A}\in {ℤ}_{\ge {B}}\right\}={ℤ}_{\ge \left({B}+{A}\right)}$

### Proof

Step Hyp Ref Expression
1 df-rab ${⊢}\left\{{x}\in ℂ|{x}-{A}\in {ℤ}_{\ge {B}}\right\}=\left\{{x}|\left({x}\in ℂ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)\right\}$
2 simp2 ${⊢}\left({A}\in ℤ\wedge {x}\in ℂ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)\to {x}\in ℂ$
3 zcn ${⊢}{A}\in ℤ\to {A}\in ℂ$
4 3 3ad2ant1 ${⊢}\left({A}\in ℤ\wedge {x}\in ℂ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)\to {A}\in ℂ$
5 2 4 npcand ${⊢}\left({A}\in ℤ\wedge {x}\in ℂ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)\to {x}-{A}+{A}={x}$
6 eluzadd ${⊢}\left({x}-{A}\in {ℤ}_{\ge {B}}\wedge {A}\in ℤ\right)\to {x}-{A}+{A}\in {ℤ}_{\ge \left({B}+{A}\right)}$
7 6 ancoms ${⊢}\left({A}\in ℤ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)\to {x}-{A}+{A}\in {ℤ}_{\ge \left({B}+{A}\right)}$
8 7 3adant2 ${⊢}\left({A}\in ℤ\wedge {x}\in ℂ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)\to {x}-{A}+{A}\in {ℤ}_{\ge \left({B}+{A}\right)}$
9 5 8 eqeltrrd ${⊢}\left({A}\in ℤ\wedge {x}\in ℂ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)\to {x}\in {ℤ}_{\ge \left({B}+{A}\right)}$
10 9 3expib ${⊢}{A}\in ℤ\to \left(\left({x}\in ℂ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)\to {x}\in {ℤ}_{\ge \left({B}+{A}\right)}\right)$
11 10 adantr ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left({x}\in ℂ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)\to {x}\in {ℤ}_{\ge \left({B}+{A}\right)}\right)$
12 eluzelcn ${⊢}{x}\in {ℤ}_{\ge \left({B}+{A}\right)}\to {x}\in ℂ$
13 12 a1i ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left({x}\in {ℤ}_{\ge \left({B}+{A}\right)}\to {x}\in ℂ\right)$
14 eluzsub ${⊢}\left({B}\in ℤ\wedge {A}\in ℤ\wedge {x}\in {ℤ}_{\ge \left({B}+{A}\right)}\right)\to {x}-{A}\in {ℤ}_{\ge {B}}$
15 14 3expia ${⊢}\left({B}\in ℤ\wedge {A}\in ℤ\right)\to \left({x}\in {ℤ}_{\ge \left({B}+{A}\right)}\to {x}-{A}\in {ℤ}_{\ge {B}}\right)$
16 15 ancoms ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left({x}\in {ℤ}_{\ge \left({B}+{A}\right)}\to {x}-{A}\in {ℤ}_{\ge {B}}\right)$
17 13 16 jcad ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left({x}\in {ℤ}_{\ge \left({B}+{A}\right)}\to \left({x}\in ℂ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)\right)$
18 11 17 impbid ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left({x}\in ℂ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)↔{x}\in {ℤ}_{\ge \left({B}+{A}\right)}\right)$
19 18 abbi1dv ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left\{{x}|\left({x}\in ℂ\wedge {x}-{A}\in {ℤ}_{\ge {B}}\right)\right\}={ℤ}_{\ge \left({B}+{A}\right)}$
20 1 19 syl5eq ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left\{{x}\in ℂ|{x}-{A}\in {ℤ}_{\ge {B}}\right\}={ℤ}_{\ge \left({B}+{A}\right)}$