Proof of Theorem divalglem6
Step | Hyp | Ref
| Expression |
1 | | divalglem6.3 |
. . . 4
⊢ 𝐾 ∈ ℤ |
2 | 1 | zrei 12068 |
. . 3
⊢ 𝐾 ∈ ℝ |
3 | | 0re 10721 |
. . 3
⊢ 0 ∈
ℝ |
4 | 2, 3 | lttri2i 10832 |
. 2
⊢ (𝐾 ≠ 0 ↔ (𝐾 < 0 ∨ 0 < 𝐾)) |
5 | | divalglem6.2 |
. . . . . . . . 9
⊢ 𝑋 ∈ (0...(𝐴 − 1)) |
6 | | 0z 12073 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
7 | | divalglem6.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ ℕ |
8 | 7 | nnzi 12087 |
. . . . . . . . . 10
⊢ 𝐴 ∈ ℤ |
9 | | elfzm11 13069 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ 𝐴
∈ ℤ) → (𝑋
∈ (0...(𝐴 − 1))
↔ (𝑋 ∈ ℤ
∧ 0 ≤ 𝑋 ∧ 𝑋 < 𝐴))) |
10 | 6, 8, 9 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑋 ∈ (0...(𝐴 − 1)) ↔ (𝑋 ∈ ℤ ∧ 0 ≤ 𝑋 ∧ 𝑋 < 𝐴)) |
11 | 5, 10 | mpbi 233 |
. . . . . . . 8
⊢ (𝑋 ∈ ℤ ∧ 0 ≤
𝑋 ∧ 𝑋 < 𝐴) |
12 | 11 | simp3i 1142 |
. . . . . . 7
⊢ 𝑋 < 𝐴 |
13 | 11 | simp1i 1140 |
. . . . . . . . 9
⊢ 𝑋 ∈ ℤ |
14 | 13 | zrei 12068 |
. . . . . . . 8
⊢ 𝑋 ∈ ℝ |
15 | 7 | nnrei 11725 |
. . . . . . . 8
⊢ 𝐴 ∈ ℝ |
16 | 2, 15 | remulcli 10735 |
. . . . . . . 8
⊢ (𝐾 · 𝐴) ∈ ℝ |
17 | 14, 15, 16 | ltadd1i 11272 |
. . . . . . 7
⊢ (𝑋 < 𝐴 ↔ (𝑋 + (𝐾 · 𝐴)) < (𝐴 + (𝐾 · 𝐴))) |
18 | 12, 17 | mpbi 233 |
. . . . . 6
⊢ (𝑋 + (𝐾 · 𝐴)) < (𝐴 + (𝐾 · 𝐴)) |
19 | 2 | renegcli 11025 |
. . . . . . . 8
⊢ -𝐾 ∈ ℝ |
20 | 7 | nnnn0i 11984 |
. . . . . . . . . 10
⊢ 𝐴 ∈
ℕ0 |
21 | 20 | nn0ge0i 12003 |
. . . . . . . . 9
⊢ 0 ≤
𝐴 |
22 | | lemulge12 11581 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ -𝐾 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 1 ≤ -𝐾)) → 𝐴 ≤ (-𝐾 · 𝐴)) |
23 | 22 | an4s 660 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (-𝐾 ∈ ℝ ∧ 1 ≤
-𝐾)) → 𝐴 ≤ (-𝐾 · 𝐴)) |
24 | 15, 21, 23 | mpanl12 702 |
. . . . . . . 8
⊢ ((-𝐾 ∈ ℝ ∧ 1 ≤
-𝐾) → 𝐴 ≤ (-𝐾 · 𝐴)) |
25 | 19, 24 | mpan 690 |
. . . . . . 7
⊢ (1 ≤
-𝐾 → 𝐴 ≤ (-𝐾 · 𝐴)) |
26 | | lt0neg1 11224 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℝ → (𝐾 < 0 ↔ 0 < -𝐾)) |
27 | 2, 26 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐾 < 0 ↔ 0 < -𝐾) |
28 | | znegcl 12098 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℤ → -𝐾 ∈
ℤ) |
29 | 1, 28 | ax-mp 5 |
. . . . . . . . . 10
⊢ -𝐾 ∈ ℤ |
30 | | zltp1le 12113 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ -𝐾
∈ ℤ) → (0 < -𝐾 ↔ (0 + 1) ≤ -𝐾)) |
31 | 6, 29, 30 | mp2an 692 |
. . . . . . . . 9
⊢ (0 <
-𝐾 ↔ (0 + 1) ≤
-𝐾) |
32 | | 0p1e1 11838 |
. . . . . . . . . 10
⊢ (0 + 1) =
1 |
33 | 32 | breq1i 5037 |
. . . . . . . . 9
⊢ ((0 + 1)
≤ -𝐾 ↔ 1 ≤
-𝐾) |
34 | 31, 33 | bitri 278 |
. . . . . . . 8
⊢ (0 <
-𝐾 ↔ 1 ≤ -𝐾) |
35 | 27, 34 | bitri 278 |
. . . . . . 7
⊢ (𝐾 < 0 ↔ 1 ≤ -𝐾) |
36 | 2 | recni 10733 |
. . . . . . . . . . . 12
⊢ 𝐾 ∈ ℂ |
37 | 15 | recni 10733 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈ ℂ |
38 | 36, 37 | mulneg1i 11164 |
. . . . . . . . . . 11
⊢ (-𝐾 · 𝐴) = -(𝐾 · 𝐴) |
39 | 38 | oveq2i 7181 |
. . . . . . . . . 10
⊢ (𝐴 − (-𝐾 · 𝐴)) = (𝐴 − -(𝐾 · 𝐴)) |
40 | 16 | recni 10733 |
. . . . . . . . . . 11
⊢ (𝐾 · 𝐴) ∈ ℂ |
41 | 37, 40 | subnegi 11043 |
. . . . . . . . . 10
⊢ (𝐴 − -(𝐾 · 𝐴)) = (𝐴 + (𝐾 · 𝐴)) |
42 | 39, 41 | eqtri 2761 |
. . . . . . . . 9
⊢ (𝐴 − (-𝐾 · 𝐴)) = (𝐴 + (𝐾 · 𝐴)) |
43 | 42 | breq1i 5037 |
. . . . . . . 8
⊢ ((𝐴 − (-𝐾 · 𝐴)) ≤ 0 ↔ (𝐴 + (𝐾 · 𝐴)) ≤ 0) |
44 | 19, 15 | remulcli 10735 |
. . . . . . . . 9
⊢ (-𝐾 · 𝐴) ∈ ℝ |
45 | | suble0 11232 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (-𝐾 · 𝐴) ∈ ℝ) → ((𝐴 − (-𝐾 · 𝐴)) ≤ 0 ↔ 𝐴 ≤ (-𝐾 · 𝐴))) |
46 | 15, 44, 45 | mp2an 692 |
. . . . . . . 8
⊢ ((𝐴 − (-𝐾 · 𝐴)) ≤ 0 ↔ 𝐴 ≤ (-𝐾 · 𝐴)) |
47 | 43, 46 | bitr3i 280 |
. . . . . . 7
⊢ ((𝐴 + (𝐾 · 𝐴)) ≤ 0 ↔ 𝐴 ≤ (-𝐾 · 𝐴)) |
48 | 25, 35, 47 | 3imtr4i 295 |
. . . . . 6
⊢ (𝐾 < 0 → (𝐴 + (𝐾 · 𝐴)) ≤ 0) |
49 | 14, 16 | readdcli 10734 |
. . . . . . 7
⊢ (𝑋 + (𝐾 · 𝐴)) ∈ ℝ |
50 | 15, 16 | readdcli 10734 |
. . . . . . 7
⊢ (𝐴 + (𝐾 · 𝐴)) ∈ ℝ |
51 | 49, 50, 3 | ltletri 10846 |
. . . . . 6
⊢ (((𝑋 + (𝐾 · 𝐴)) < (𝐴 + (𝐾 · 𝐴)) ∧ (𝐴 + (𝐾 · 𝐴)) ≤ 0) → (𝑋 + (𝐾 · 𝐴)) < 0) |
52 | 18, 48, 51 | sylancr 590 |
. . . . 5
⊢ (𝐾 < 0 → (𝑋 + (𝐾 · 𝐴)) < 0) |
53 | 49, 3 | ltnlei 10839 |
. . . . 5
⊢ ((𝑋 + (𝐾 · 𝐴)) < 0 ↔ ¬ 0 ≤ (𝑋 + (𝐾 · 𝐴))) |
54 | 52, 53 | sylib 221 |
. . . 4
⊢ (𝐾 < 0 → ¬ 0 ≤
(𝑋 + (𝐾 · 𝐴))) |
55 | | elfzle1 13001 |
. . . 4
⊢ ((𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1)) → 0 ≤ (𝑋 + (𝐾 · 𝐴))) |
56 | 54, 55 | nsyl 142 |
. . 3
⊢ (𝐾 < 0 → ¬ (𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1))) |
57 | | zltp1le 12113 |
. . . . . . . . 9
⊢ ((0
∈ ℤ ∧ 𝐾
∈ ℤ) → (0 < 𝐾 ↔ (0 + 1) ≤ 𝐾)) |
58 | 6, 1, 57 | mp2an 692 |
. . . . . . . 8
⊢ (0 <
𝐾 ↔ (0 + 1) ≤ 𝐾) |
59 | 32 | breq1i 5037 |
. . . . . . . 8
⊢ ((0 + 1)
≤ 𝐾 ↔ 1 ≤ 𝐾) |
60 | 58, 59 | bitri 278 |
. . . . . . 7
⊢ (0 <
𝐾 ↔ 1 ≤ 𝐾) |
61 | | lemulge12 11581 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐾 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 1 ≤ 𝐾)) → 𝐴 ≤ (𝐾 · 𝐴)) |
62 | 15, 2, 61 | mpanl12 702 |
. . . . . . . 8
⊢ ((0 ≤
𝐴 ∧ 1 ≤ 𝐾) → 𝐴 ≤ (𝐾 · 𝐴)) |
63 | 21, 62 | mpan 690 |
. . . . . . 7
⊢ (1 ≤
𝐾 → 𝐴 ≤ (𝐾 · 𝐴)) |
64 | 60, 63 | sylbi 220 |
. . . . . 6
⊢ (0 <
𝐾 → 𝐴 ≤ (𝐾 · 𝐴)) |
65 | 11 | simp2i 1141 |
. . . . . . 7
⊢ 0 ≤
𝑋 |
66 | | addge02 11229 |
. . . . . . . 8
⊢ (((𝐾 · 𝐴) ∈ ℝ ∧ 𝑋 ∈ ℝ) → (0 ≤ 𝑋 ↔ (𝐾 · 𝐴) ≤ (𝑋 + (𝐾 · 𝐴)))) |
67 | 16, 14, 66 | mp2an 692 |
. . . . . . 7
⊢ (0 ≤
𝑋 ↔ (𝐾 · 𝐴) ≤ (𝑋 + (𝐾 · 𝐴))) |
68 | 65, 67 | mpbi 233 |
. . . . . 6
⊢ (𝐾 · 𝐴) ≤ (𝑋 + (𝐾 · 𝐴)) |
69 | 15, 16, 49 | letri 10847 |
. . . . . 6
⊢ ((𝐴 ≤ (𝐾 · 𝐴) ∧ (𝐾 · 𝐴) ≤ (𝑋 + (𝐾 · 𝐴))) → 𝐴 ≤ (𝑋 + (𝐾 · 𝐴))) |
70 | 64, 68, 69 | sylancl 589 |
. . . . 5
⊢ (0 <
𝐾 → 𝐴 ≤ (𝑋 + (𝐾 · 𝐴))) |
71 | 15, 49 | lenlti 10838 |
. . . . 5
⊢ (𝐴 ≤ (𝑋 + (𝐾 · 𝐴)) ↔ ¬ (𝑋 + (𝐾 · 𝐴)) < 𝐴) |
72 | 70, 71 | sylib 221 |
. . . 4
⊢ (0 <
𝐾 → ¬ (𝑋 + (𝐾 · 𝐴)) < 𝐴) |
73 | | elfzm11 13069 |
. . . . . 6
⊢ ((0
∈ ℤ ∧ 𝐴
∈ ℤ) → ((𝑋
+ (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1)) ↔ ((𝑋 + (𝐾 · 𝐴)) ∈ ℤ ∧ 0 ≤ (𝑋 + (𝐾 · 𝐴)) ∧ (𝑋 + (𝐾 · 𝐴)) < 𝐴))) |
74 | 6, 8, 73 | mp2an 692 |
. . . . 5
⊢ ((𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1)) ↔ ((𝑋 + (𝐾 · 𝐴)) ∈ ℤ ∧ 0 ≤ (𝑋 + (𝐾 · 𝐴)) ∧ (𝑋 + (𝐾 · 𝐴)) < 𝐴)) |
75 | 74 | simp3bi 1148 |
. . . 4
⊢ ((𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1)) → (𝑋 + (𝐾 · 𝐴)) < 𝐴) |
76 | 72, 75 | nsyl 142 |
. . 3
⊢ (0 <
𝐾 → ¬ (𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1))) |
77 | 56, 76 | jaoi 856 |
. 2
⊢ ((𝐾 < 0 ∨ 0 < 𝐾) → ¬ (𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1))) |
78 | 4, 77 | sylbi 220 |
1
⊢ (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1))) |