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