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	abbi1dv	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { 𝑥 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) ) } = ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) )
20	1 19	eqtrid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝐴 ) ∈ ( ℤ≥ ‘ 𝐵 ) } = ( ℤ≥ ‘ ( 𝐵 + 𝐴 ) ) )