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