Metamath Proof Explorer


Theorem shftuz

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

Ref Expression
Assertion shftuz
|- ( ( A e. ZZ /\ B e. ZZ ) -> { x e. CC | ( x - A ) e. ( ZZ>= ` B ) } = ( ZZ>= ` ( B + A ) ) )

Proof

Step Hyp Ref Expression
1 df-rab
 |-  { x e. CC | ( x - A ) e. ( ZZ>= ` B ) } = { x | ( x e. CC /\ ( x - A ) e. ( ZZ>= ` B ) ) }
2 simp2
 |-  ( ( A e. ZZ /\ x e. CC /\ ( x - A ) e. ( ZZ>= ` B ) ) -> x e. CC )
3 zcn
 |-  ( A e. ZZ -> A e. CC )
4 3 3ad2ant1
 |-  ( ( A e. ZZ /\ x e. CC /\ ( x - A ) e. ( ZZ>= ` B ) ) -> A e. CC )
5 2 4 npcand
 |-  ( ( A e. ZZ /\ x e. CC /\ ( x - A ) e. ( ZZ>= ` B ) ) -> ( ( x - A ) + A ) = x )
6 eluzadd
 |-  ( ( ( x - A ) e. ( ZZ>= ` B ) /\ A e. ZZ ) -> ( ( x - A ) + A ) e. ( ZZ>= ` ( B + A ) ) )
7 6 ancoms
 |-  ( ( A e. ZZ /\ ( x - A ) e. ( ZZ>= ` B ) ) -> ( ( x - A ) + A ) e. ( ZZ>= ` ( B + A ) ) )
8 7 3adant2
 |-  ( ( A e. ZZ /\ x e. CC /\ ( x - A ) e. ( ZZ>= ` B ) ) -> ( ( x - A ) + A ) e. ( ZZ>= ` ( B + A ) ) )
9 5 8 eqeltrrd
 |-  ( ( A e. ZZ /\ x e. CC /\ ( x - A ) e. ( ZZ>= ` B ) ) -> x e. ( ZZ>= ` ( B + A ) ) )
10 9 3expib
 |-  ( A e. ZZ -> ( ( x e. CC /\ ( x - A ) e. ( ZZ>= ` B ) ) -> x e. ( ZZ>= ` ( B + A ) ) ) )
11 10 adantr
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( x e. CC /\ ( x - A ) e. ( ZZ>= ` B ) ) -> x e. ( ZZ>= ` ( B + A ) ) ) )
12 eluzelcn
 |-  ( x e. ( ZZ>= ` ( B + A ) ) -> x e. CC )
13 12 a1i
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( x e. ( ZZ>= ` ( B + A ) ) -> x e. CC ) )
14 eluzsub
 |-  ( ( B e. ZZ /\ A e. ZZ /\ x e. ( ZZ>= ` ( B + A ) ) ) -> ( x - A ) e. ( ZZ>= ` B ) )
15 14 3expia
 |-  ( ( B e. ZZ /\ A e. ZZ ) -> ( x e. ( ZZ>= ` ( B + A ) ) -> ( x - A ) e. ( ZZ>= ` B ) ) )
16 15 ancoms
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( x e. ( ZZ>= ` ( B + A ) ) -> ( x - A ) e. ( ZZ>= ` B ) ) )
17 13 16 jcad
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( x e. ( ZZ>= ` ( B + A ) ) -> ( x e. CC /\ ( x - A ) e. ( ZZ>= ` B ) ) ) )
18 11 17 impbid
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( x e. CC /\ ( x - A ) e. ( ZZ>= ` B ) ) <-> x e. ( ZZ>= ` ( B + A ) ) ) )
19 18 abbi1dv
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> { x | ( x e. CC /\ ( x - A ) e. ( ZZ>= ` B ) ) } = ( ZZ>= ` ( B + A ) ) )
20 1 19 eqtrid
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> { x e. CC | ( x - A ) e. ( ZZ>= ` B ) } = ( ZZ>= ` ( B + A ) ) )