Metamath Proof Explorer

Theorem divalglem6

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

Ref Expression
Hypotheses divalglem6.1 ⊢A∈ℕ
divalglem6.2 ⊢X∈0…A−1
divalglem6.3 ⊢K∈ℤ
Assertion divalglem6 ⊢K≠0→¬X+K⁢A∈0…A−1

Proof

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