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 ) ) )