Metamath Proof Explorer

Theorem divalglem6

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

Ref Expression
Hypotheses divalglem6.1 
|- A e. NN
divalglem6.2 
|- X e. ( 0 ... ( A - 1 ) )
divalglem6.3 
|- K e. ZZ
Assertion divalglem6 
|- ( K =/= 0 -> -. ( X + ( K x. A ) ) e. ( 0 ... ( A - 1 ) ) )

Proof

Step Hyp Ref Expression
1 divalglem6.1 
 |-  A e. NN
2 divalglem6.2 
 |-  X e. ( 0 ... ( A - 1 ) )
3 divalglem6.3 
 |-  K e. ZZ
4 3 zrei 
 |-  K e. RR
5 0re 
 |-  0 e. RR
6 4 5 lttri2i 
 |-  ( K =/= 0 <-> ( K < 0 \/ 0 < K ) )
7 0z 
 |-  0 e. ZZ
8 1 nnzi 
 |-  A e. ZZ
9 elfzm11 
 |-  ( ( 0 e. ZZ /\ A e. ZZ ) -> ( X e. ( 0 ... ( A - 1 ) ) <-> ( X e. ZZ /\ 0 <_ X /\ X < A ) ) )
10 7 8 9 mp2an 
 |-  ( X e. ( 0 ... ( A - 1 ) ) <-> ( X e. ZZ /\ 0 <_ X /\ X < A ) )
11 2 10 mpbi 
 |-  ( X e. ZZ /\ 0 <_ X /\ X < A )
12 11 simp3i 
 |-  X < A
13 11 simp1i 
 |-  X e. ZZ
14 13 zrei 
 |-  X e. RR
15 1 nnrei 
 |-  A e. RR
16 4 15 remulcli 
 |-  ( K x. A ) e. RR
17 14 15 16 ltadd1i 
 |-  ( X < A <-> ( X + ( K x. A ) ) < ( A + ( K x. A ) ) )
18 12 17 mpbi 
 |-  ( X + ( K x. A ) ) < ( A + ( K x. A ) )
19 4 renegcli 
 |-  -u K e. RR
20 1 nnnn0i 
 |-  A e. NN0
21 20 nn0ge0i 
 |-  0 <_ A
22 lemulge12 
 |-  ( ( ( A e. RR /\ -u K e. RR ) /\ ( 0 <_ A /\ 1 <_ -u K ) ) -> A <_ ( -u K x. A ) )
23 22 an4s 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( -u K e. RR /\ 1 <_ -u K ) ) -> A <_ ( -u K x. A ) )
24 15 21 23 mpanl12 
 |-  ( ( -u K e. RR /\ 1 <_ -u K ) -> A <_ ( -u K x. A ) )
25 19 24 mpan 
 |-  ( 1 <_ -u K -> A <_ ( -u K x. A ) )
26 lt0neg1 
 |-  ( K e. RR -> ( K < 0 <-> 0 < -u K ) )
27 4 26 ax-mp 
 |-  ( K < 0 <-> 0 < -u K )
28 znegcl 
 |-  ( K e. ZZ -> -u K e. ZZ )
29 3 28 ax-mp 
 |-  -u K e. ZZ
30 zltp1le 
 |-  ( ( 0 e. ZZ /\ -u K e. ZZ ) -> ( 0 < -u K <-> ( 0 + 1 ) <_ -u K ) )
31 7 29 30 mp2an 
 |-  ( 0 < -u K <-> ( 0 + 1 ) <_ -u K )
32 0p1e1 
 |-  ( 0 + 1 ) = 1
33 32 breq1i 
 |-  ( ( 0 + 1 ) <_ -u K <-> 1 <_ -u K )
34 31 33 bitri 
 |-  ( 0 < -u K <-> 1 <_ -u K )
35 27 34 bitri 
 |-  ( K < 0 <-> 1 <_ -u K )
36 4 recni 
 |-  K e. CC
37 15 recni 
 |-  A e. CC
38 36 37 mulneg1i 
 |-  ( -u K x. A ) = -u ( K x. A )
39 38 oveq2i 
 |-  ( A - ( -u K x. A ) ) = ( A - -u ( K x. A ) )
40 16 recni 
 |-  ( K x. A ) e. CC
41 37 40 subnegi 
 |-  ( A - -u ( K x. A ) ) = ( A + ( K x. A ) )
42 39 41 eqtri 
 |-  ( A - ( -u K x. A ) ) = ( A + ( K x. A ) )
43 42 breq1i 
 |-  ( ( A - ( -u K x. A ) ) <_ 0 <-> ( A + ( K x. A ) ) <_ 0 )
44 19 15 remulcli 
 |-  ( -u K x. A ) e. RR
45 suble0 
 |-  ( ( A e. RR /\ ( -u K x. A ) e. RR ) -> ( ( A - ( -u K x. A ) ) <_ 0 <-> A <_ ( -u K x. A ) ) )
46 15 44 45 mp2an 
 |-  ( ( A - ( -u K x. A ) ) <_ 0 <-> A <_ ( -u K x. A ) )
47 43 46 bitr3i 
 |-  ( ( A + ( K x. A ) ) <_ 0 <-> A <_ ( -u K x. A ) )
48 25 35 47 3imtr4i 
 |-  ( K < 0 -> ( A + ( K x. A ) ) <_ 0 )
49 14 16 readdcli 
 |-  ( X + ( K x. A ) ) e. RR
50 15 16 readdcli 
 |-  ( A + ( K x. A ) ) e. RR
51 49 50 5 ltletri 
 |-  ( ( ( X + ( K x. A ) ) < ( A + ( K x. A ) ) /\ ( A + ( K x. A ) ) <_ 0 ) -> ( X + ( K x. A ) ) < 0 )
52 18 48 51 sylancr 
 |-  ( K < 0 -> ( X + ( K x. A ) ) < 0 )
53 49 5 ltnlei 
 |-  ( ( X + ( K x. A ) ) < 0 <-> -. 0 <_ ( X + ( K x. A ) ) )
54 52 53 sylib 
 |-  ( K < 0 -> -. 0 <_ ( X + ( K x. A ) ) )
55 elfzle1 
 |-  ( ( X + ( K x. A ) ) e. ( 0 ... ( A - 1 ) ) -> 0 <_ ( X + ( K x. A ) ) )
56 54 55 nsyl 
 |-  ( K < 0 -> -. ( X + ( K x. A ) ) e. ( 0 ... ( A - 1 ) ) )
57 zltp1le 
 |-  ( ( 0 e. ZZ /\ K e. ZZ ) -> ( 0 < K <-> ( 0 + 1 ) <_ K ) )
58 7 3 57 mp2an 
 |-  ( 0 < K <-> ( 0 + 1 ) <_ K )
59 32 breq1i 
 |-  ( ( 0 + 1 ) <_ K <-> 1 <_ K )
60 58 59 bitri 
 |-  ( 0 < K <-> 1 <_ K )
61 lemulge12 
 |-  ( ( ( A e. RR /\ K e. RR ) /\ ( 0 <_ A /\ 1 <_ K ) ) -> A <_ ( K x. A ) )
62 15 4 61 mpanl12 
 |-  ( ( 0 <_ A /\ 1 <_ K ) -> A <_ ( K x. A ) )
63 21 62 mpan 
 |-  ( 1 <_ K -> A <_ ( K x. A ) )
64 60 63 sylbi 
 |-  ( 0 < K -> A <_ ( K x. A ) )
65 11 simp2i 
 |-  0 <_ X
66 addge02 
 |-  ( ( ( K x. A ) e. RR /\ X e. RR ) -> ( 0 <_ X <-> ( K x. A ) <_ ( X + ( K x. A ) ) ) )
67 16 14 66 mp2an 
 |-  ( 0 <_ X <-> ( K x. A ) <_ ( X + ( K x. A ) ) )
68 65 67 mpbi 
 |-  ( K x. A ) <_ ( X + ( K x. A ) )
69 15 16 49 letri 
 |-  ( ( A <_ ( K x. A ) /\ ( K x. A ) <_ ( X + ( K x. A ) ) ) -> A <_ ( X + ( K x. A ) ) )
70 64 68 69 sylancl 
 |-  ( 0 < K -> A <_ ( X + ( K x. A ) ) )
71 15 49 lenlti 
 |-  ( A <_ ( X + ( K x. A ) ) <-> -. ( X + ( K x. A ) ) < A )
72 70 71 sylib 
 |-  ( 0 < K -> -. ( X + ( K x. A ) ) < A )
73 elfzm11 
 |-  ( ( 0 e. ZZ /\ A e. ZZ ) -> ( ( X + ( K x. A ) ) e. ( 0 ... ( A - 1 ) ) <-> ( ( X + ( K x. A ) ) e. ZZ /\ 0 <_ ( X + ( K x. A ) ) /\ ( X + ( K x. A ) ) < A ) ) )
74 7 8 73 mp2an 
 |-  ( ( X + ( K x. A ) ) e. ( 0 ... ( A - 1 ) ) <-> ( ( X + ( K x. A ) ) e. ZZ /\ 0 <_ ( X + ( K x. A ) ) /\ ( X + ( K x. A ) ) < A ) )
75 74 simp3bi 
 |-  ( ( X + ( K x. A ) ) e. ( 0 ... ( A - 1 ) ) -> ( X + ( K x. A ) ) < A )
76 72 75 nsyl 
 |-  ( 0 < K -> -. ( X + ( K x. A ) ) e. ( 0 ... ( A - 1 ) ) )
77 56 76 jaoi 
 |-  ( ( K < 0 \/ 0 < K ) -> -. ( X + ( K x. A ) ) e. ( 0 ... ( A - 1 ) ) )
78 6 77 sylbi 
 |-  ( K =/= 0 -> -. ( X + ( K x. A ) ) e. ( 0 ... ( A - 1 ) ) )