Metamath Proof Explorer

Theorem divalglem7

Description: Lemma for divalg . (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Hypotheses divalglem7.1 
|- D e. ZZ
divalglem7.2 
|- D =/= 0
Assertion divalglem7 
|- ( ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) /\ K e. ZZ ) -> ( K =/= 0 -> -. ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 divalglem7.1 
 |-  D e. ZZ
2 divalglem7.2 
 |-  D =/= 0
3 oveq1 
 |-  ( X = if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) -> ( X + ( K x. ( abs ` D ) ) ) = ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( K x. ( abs ` D ) ) ) )
4 3 eleq1d 
 |-  ( X = if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) -> ( ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) <-> ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
5 4 notbid 
 |-  ( X = if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) -> ( -. ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) <-> -. ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
6 5 imbi2d 
 |-  ( X = if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) -> ( ( K =/= 0 -> -. ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) <-> ( K =/= 0 -> -. ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) ) )
7 neeq1 
 |-  ( K = if ( K e. ZZ , K , 0 ) -> ( K =/= 0 <-> if ( K e. ZZ , K , 0 ) =/= 0 ) )
8 oveq1 
 |-  ( K = if ( K e. ZZ , K , 0 ) -> ( K x. ( abs ` D ) ) = ( if ( K e. ZZ , K , 0 ) x. ( abs ` D ) ) )
9 8 oveq2d 
 |-  ( K = if ( K e. ZZ , K , 0 ) -> ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( K x. ( abs ` D ) ) ) = ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( if ( K e. ZZ , K , 0 ) x. ( abs ` D ) ) ) )
10 9 eleq1d 
 |-  ( K = if ( K e. ZZ , K , 0 ) -> ( ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) <-> ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( if ( K e. ZZ , K , 0 ) x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
11 10 notbid 
 |-  ( K = if ( K e. ZZ , K , 0 ) -> ( -. ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) <-> -. ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( if ( K e. ZZ , K , 0 ) x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
12 7 11 imbi12d 
 |-  ( K = if ( K e. ZZ , K , 0 ) -> ( ( K =/= 0 -> -. ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) <-> ( if ( K e. ZZ , K , 0 ) =/= 0 -> -. ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( if ( K e. ZZ , K , 0 ) x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) ) )
13 nnabscl 
 |-  ( ( D e. ZZ /\ D =/= 0 ) -> ( abs ` D ) e. NN )
14 1 2 13 mp2an 
 |-  ( abs ` D ) e. NN
15 0z 
 |-  0 e. ZZ
16 0le0 
 |-  0 <_ 0
17 14 nngt0i 
 |-  0 < ( abs ` D )
18 14 nnzi 
 |-  ( abs ` D ) e. ZZ
19 elfzm11 
 |-  ( ( 0 e. ZZ /\ ( abs ` D ) e. ZZ ) -> ( 0 e. ( 0 ... ( ( abs ` D ) - 1 ) ) <-> ( 0 e. ZZ /\ 0 <_ 0 /\ 0 < ( abs ` D ) ) ) )
20 15 18 19 mp2an 
 |-  ( 0 e. ( 0 ... ( ( abs ` D ) - 1 ) ) <-> ( 0 e. ZZ /\ 0 <_ 0 /\ 0 < ( abs ` D ) ) )
21 15 16 17 20 mpbir3an 
 |-  0 e. ( 0 ... ( ( abs ` D ) - 1 ) )
22 21 elimel 
 |-  if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) e. ( 0 ... ( ( abs ` D ) - 1 ) )
23 15 elimel 
 |-  if ( K e. ZZ , K , 0 ) e. ZZ
24 14 22 23 divalglem6 
 |-  ( if ( K e. ZZ , K , 0 ) =/= 0 -> -. ( if ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) , X , 0 ) + ( if ( K e. ZZ , K , 0 ) x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) )
25 6 12 24 dedth2h 
 |-  ( ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) /\ K e. ZZ ) -> ( K =/= 0 -> -. ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )