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 eqabcdv 
 |-  ( ( 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 ) ) )