Metamath Proof Explorer

Theorem divalglem6

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

Ref Expression
Hypotheses divalglem6.1 ⊢ 𝐴 ∈ ℕ
divalglem6.2 ⊢ 𝑋 ∈ ( 0 ... ( 𝐴 − 1 ) )
divalglem6.3 ⊢ 𝐾 ∈ ℤ
Assertion divalglem6 ( 𝐾 ≠ 0 → ¬ ( 𝑋 + ( 𝐾 · 𝐴 ) ) ∈ ( 0 ... ( 𝐴 − 1 ) ) )

Proof

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