Metamath Proof Explorer

Theorem shftuz

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

Ref Expression
Assertion shftuz ⊢ A ∈ ℤ ∧ B ∈ ℤ → x ∈ ℂ | x − A ∈ ℤ ≥ B = ℤ ≥ B + A

Proof

Step Hyp Ref Expression
1 df-rab ⊢ x ∈ ℂ | x − A ∈ ℤ ≥ B = x | x ∈ ℂ ∧ x − A ∈ ℤ ≥ B
2 simp2 ⊢ A ∈ ℤ ∧ x ∈ ℂ ∧ x − A ∈ ℤ ≥ B → x ∈ ℂ
3 zcn ⊢ A ∈ ℤ → A ∈ ℂ
4 3 3ad2ant1 ⊢ A ∈ ℤ ∧ x ∈ ℂ ∧ x − A ∈ ℤ ≥ B → A ∈ ℂ
5 2 4 npcand ⊢ A ∈ ℤ ∧ x ∈ ℂ ∧ x − A ∈ ℤ ≥ B → x - A + A = x
6 eluzadd ⊢ x − A ∈ ℤ ≥ B ∧ A ∈ ℤ → x - A + A ∈ ℤ ≥ B + A
7 6 ancoms ⊢ A ∈ ℤ ∧ x − A ∈ ℤ ≥ B → x - A + A ∈ ℤ ≥ B + A
8 7 3adant2 ⊢ A ∈ ℤ ∧ x ∈ ℂ ∧ x − A ∈ ℤ ≥ B → x - A + A ∈ ℤ ≥ B + A
9 5 8 eqeltrrd ⊢ A ∈ ℤ ∧ x ∈ ℂ ∧ x − A ∈ ℤ ≥ B → x ∈ ℤ ≥ B + A
10 9 3expib ⊢ A ∈ ℤ → x ∈ ℂ ∧ x − A ∈ ℤ ≥ B → x ∈ ℤ ≥ B + A
11 10 adantr ⊢ A ∈ ℤ ∧ B ∈ ℤ → x ∈ ℂ ∧ x − A ∈ ℤ ≥ B → x ∈ ℤ ≥ B + A
12 eluzelcn ⊢ x ∈ ℤ ≥ B + A → x ∈ ℂ
13 12 a1i ⊢ A ∈ ℤ ∧ B ∈ ℤ → x ∈ ℤ ≥ B + A → x ∈ ℂ
14 eluzsub ⊢ B ∈ ℤ ∧ A ∈ ℤ ∧ x ∈ ℤ ≥ B + A → x − A ∈ ℤ ≥ B
15 14 3expia ⊢ B ∈ ℤ ∧ A ∈ ℤ → x ∈ ℤ ≥ B + A → x − A ∈ ℤ ≥ B
16 15 ancoms ⊢ A ∈ ℤ ∧ B ∈ ℤ → x ∈ ℤ ≥ B + A → x − A ∈ ℤ ≥ B
17 13 16 jcad ⊢ A ∈ ℤ ∧ B ∈ ℤ → x ∈ ℤ ≥ B + A → x ∈ ℂ ∧ x − A ∈ ℤ ≥ B
18 11 17 impbid ⊢ A ∈ ℤ ∧ B ∈ ℤ → x ∈ ℂ ∧ x − A ∈ ℤ ≥ B ↔ x ∈ ℤ ≥ B + A
19 18 abbi1dv ⊢ A ∈ ℤ ∧ B ∈ ℤ → x | x ∈ ℂ ∧ x − A ∈ ℤ ≥ B = ℤ ≥ B + A
20 1 19 syl5eq ⊢ A ∈ ℤ ∧ B ∈ ℤ → x ∈ ℂ | x − A ∈ ℤ ≥ B = ℤ ≥ B + A