Step | Hyp | Ref
| Expression |
1 | | simpr 109 |
. . . . . 6
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑖 ∈ ℤ) |
2 | 1 | adantr 274 |
. . . . 5
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝑖 ∈ ℤ) |
3 | | eqcom 2172 |
. . . . . . . . 9
⊢ (𝐴 = ((𝑖 · 𝑀) + 𝐵) ↔ ((𝑖 · 𝑀) + 𝐵) = 𝐴) |
4 | | nn0cn 9145 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℂ) |
5 | 4 | 3ad2ant1 1013 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝐴 ∈
ℂ) |
6 | 5 | ad2antrr 485 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝐴 ∈ ℂ) |
7 | | nn0z 9232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℤ) |
8 | | zq 9585 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℚ) |
9 | 7, 8 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℚ) |
10 | 9 | 3ad2ant1 1013 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝐴 ∈
ℚ) |
11 | 10 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝐴 ∈ ℚ) |
12 | | simpl2 996 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝑀 ∈ ℚ) |
13 | | simpl3 997 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 0 < 𝑀) |
14 | 11, 12, 13 | modqcld 10284 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → (𝐴 mod 𝑀) ∈ ℚ) |
15 | | qcn 9593 |
. . . . . . . . . . . . 13
⊢ ((𝐴 mod 𝑀) ∈ ℚ → (𝐴 mod 𝑀) ∈ ℂ) |
16 | 14, 15 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → (𝐴 mod 𝑀) ∈ ℂ) |
17 | | eleq1 2233 |
. . . . . . . . . . . . 13
⊢ ((𝐴 mod 𝑀) = 𝐵 → ((𝐴 mod 𝑀) ∈ ℂ ↔ 𝐵 ∈ ℂ)) |
18 | 17 | adantl 275 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → ((𝐴 mod 𝑀) ∈ ℂ ↔ 𝐵 ∈ ℂ)) |
19 | 16, 18 | mpbid 146 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝐵 ∈ ℂ) |
20 | 19 | adantr 274 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝐵 ∈ ℂ) |
21 | | zcn 9217 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℂ) |
22 | 21 | adantl 275 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑖 ∈ ℂ) |
23 | | qcn 9593 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℚ → 𝑀 ∈
ℂ) |
24 | 12, 23 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝑀 ∈ ℂ) |
25 | 24 | adantr 274 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑀 ∈ ℂ) |
26 | 22, 25 | mulcld 7940 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝑖 · 𝑀) ∈ ℂ) |
27 | 6, 20, 26 | subadd2d 8249 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − 𝐵) = (𝑖 · 𝑀) ↔ ((𝑖 · 𝑀) + 𝐵) = 𝐴)) |
28 | 3, 27 | bitr4id 198 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 = ((𝑖 · 𝑀) + 𝐵) ↔ (𝐴 − 𝐵) = (𝑖 · 𝑀))) |
29 | 5 | adantr 274 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝐴 ∈ ℂ) |
30 | 29, 19 | subcld 8230 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → (𝐴 − 𝐵) ∈ ℂ) |
31 | 30 | adantr 274 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℂ) |
32 | | qre 9584 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℚ → 𝑀 ∈
ℝ) |
33 | 32 | 3ad2ant2 1014 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝑀 ∈
ℝ) |
34 | 33 | ad2antrr 485 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑀 ∈ ℝ) |
35 | 13 | adantr 274 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 0 < 𝑀) |
36 | 34, 35 | gt0ap0d 8548 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑀 # 0) |
37 | 31, 22, 25, 36 | divmulap3d 8742 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (((𝐴 − 𝐵) / 𝑀) = 𝑖 ↔ (𝐴 − 𝐵) = (𝑖 · 𝑀))) |
38 | | oveq2 5861 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = (𝐴 mod 𝑀) → (𝐴 − 𝐵) = (𝐴 − (𝐴 mod 𝑀))) |
39 | 38 | oveq1d 5868 |
. . . . . . . . . . . . 13
⊢ (𝐵 = (𝐴 mod 𝑀) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
40 | 39 | eqcoms 2173 |
. . . . . . . . . . . 12
⊢ ((𝐴 mod 𝑀) = 𝐵 → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
41 | 40 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
42 | 41 | adantr 274 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
43 | | modqdiffl 10291 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℚ ∧ 𝑀 ∈ ℚ ∧ 0 <
𝑀) → ((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
44 | 9, 43 | syl3an1 1266 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
45 | 44 | ad2antrr 485 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
46 | 42, 45 | eqtrd 2203 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − 𝐵) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
47 | 46 | eqeq1d 2179 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (((𝐴 − 𝐵) / 𝑀) = 𝑖 ↔ (⌊‘(𝐴 / 𝑀)) = 𝑖)) |
48 | 28, 37, 47 | 3bitr2d 215 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 = ((𝑖 · 𝑀) + 𝐵) ↔ (⌊‘(𝐴 / 𝑀)) = 𝑖)) |
49 | | qre 9584 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℝ) |
50 | 10, 49 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝐴 ∈
ℝ) |
51 | | nn0ge0 9160 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ0
→ 0 ≤ 𝐴) |
52 | 51 | 3ad2ant1 1013 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
≤ 𝐴) |
53 | | simp3 994 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
< 𝑀) |
54 | | divge0 8789 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ (𝐴 / 𝑀)) |
55 | 50, 52, 33, 53, 54 | syl22anc 1234 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
≤ (𝐴 / 𝑀)) |
56 | | simp2 993 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝑀 ∈
ℚ) |
57 | 53 | gt0ne0d 8431 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝑀 ≠ 0) |
58 | | qdivcl 9602 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℚ ∧ 𝑀 ∈ ℚ ∧ 𝑀 ≠ 0) → (𝐴 / 𝑀) ∈ ℚ) |
59 | 10, 56, 57, 58 | syl3anc 1233 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
(𝐴 / 𝑀) ∈ ℚ) |
60 | | 0z 9223 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
61 | | flqge 10238 |
. . . . . . . . . . 11
⊢ (((𝐴 / 𝑀) ∈ ℚ ∧ 0 ∈ ℤ)
→ (0 ≤ (𝐴 / 𝑀) ↔ 0 ≤
(⌊‘(𝐴 / 𝑀)))) |
62 | 59, 60, 61 | sylancl 411 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → (0
≤ (𝐴 / 𝑀) ↔ 0 ≤ (⌊‘(𝐴 / 𝑀)))) |
63 | 55, 62 | mpbid 146 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
≤ (⌊‘(𝐴 /
𝑀))) |
64 | | breq2 3993 |
. . . . . . . . 9
⊢
((⌊‘(𝐴 /
𝑀)) = 𝑖 → (0 ≤ (⌊‘(𝐴 / 𝑀)) ↔ 0 ≤ 𝑖)) |
65 | 63, 64 | syl5ibcom 154 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((⌊‘(𝐴 / 𝑀)) = 𝑖 → 0 ≤ 𝑖)) |
66 | 65 | ad2antrr 485 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) →
((⌊‘(𝐴 / 𝑀)) = 𝑖 → 0 ≤ 𝑖)) |
67 | 48, 66 | sylbid 149 |
. . . . . 6
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 = ((𝑖 · 𝑀) + 𝐵) → 0 ≤ 𝑖)) |
68 | 67 | imp 123 |
. . . . 5
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 0 ≤ 𝑖) |
69 | | elnn0z 9225 |
. . . . 5
⊢ (𝑖 ∈ ℕ0
↔ (𝑖 ∈ ℤ
∧ 0 ≤ 𝑖)) |
70 | 2, 68, 69 | sylanbrc 415 |
. . . 4
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝑖 ∈ ℕ0) |
71 | | oveq1 5860 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → (𝑘 · 𝑀) = (𝑖 · 𝑀)) |
72 | 71 | oveq1d 5868 |
. . . . . 6
⊢ (𝑘 = 𝑖 → ((𝑘 · 𝑀) + 𝐵) = ((𝑖 · 𝑀) + 𝐵)) |
73 | 72 | eqeq2d 2182 |
. . . . 5
⊢ (𝑘 = 𝑖 → (𝐴 = ((𝑘 · 𝑀) + 𝐵) ↔ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
74 | 73 | adantl 275 |
. . . 4
⊢
((((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) ∧ 𝑘 = 𝑖) → (𝐴 = ((𝑘 · 𝑀) + 𝐵) ↔ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
75 | | simpr 109 |
. . . 4
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝐴 = ((𝑖 · 𝑀) + 𝐵)) |
76 | 70, 74, 75 | rspcedvd 2840 |
. . 3
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵)) |
77 | | modqmuladdim 10323 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℚ ∧ 0 <
𝑀) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
78 | 7, 77 | syl3an1 1266 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((𝐴 mod 𝑀) = 𝐵 → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
79 | 78 | imp 123 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) |
80 | 76, 79 | r19.29a 2613 |
. 2
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵)) |
81 | 80 | ex 114 |
1
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((𝐴 mod 𝑀) = 𝐵 → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵))) |