Step | Hyp | Ref
| Expression |
1 | | simpr 109 |
. . . . . 6
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑖 ∈ ℤ) |
2 | 1 | adantr 274 |
. . . . 5
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝑖 ∈ ℤ) |
3 | | eqcom 2159 |
. . . . . . . . 9
⊢ (𝐴 = ((𝑖 · 𝑀) + 𝐵) ↔ ((𝑖 · 𝑀) + 𝐵) = 𝐴) |
4 | | nn0cn 9105 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℂ) |
5 | 4 | 3ad2ant1 1003 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝐴 ∈
ℂ) |
6 | 5 | ad2antrr 480 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝐴 ∈ ℂ) |
7 | | nn0z 9192 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℤ) |
8 | | zq 9541 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℚ) |
9 | 7, 8 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℚ) |
10 | 9 | 3ad2ant1 1003 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝐴 ∈
ℚ) |
11 | 10 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝐴 ∈ ℚ) |
12 | | simpl2 986 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝑀 ∈ ℚ) |
13 | | simpl3 987 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 0 < 𝑀) |
14 | 11, 12, 13 | modqcld 10236 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → (𝐴 mod 𝑀) ∈ ℚ) |
15 | | qcn 9549 |
. . . . . . . . . . . . 13
⊢ ((𝐴 mod 𝑀) ∈ ℚ → (𝐴 mod 𝑀) ∈ ℂ) |
16 | 14, 15 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → (𝐴 mod 𝑀) ∈ ℂ) |
17 | | eleq1 2220 |
. . . . . . . . . . . . 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 9177 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℂ) |
22 | 21 | adantl 275 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑖 ∈ ℂ) |
23 | | qcn 9549 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℚ → 𝑀 ∈
ℂ) |
24 | 12, 23 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝑀 ∈ ℂ) |
25 | 24 | adantr 274 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑀 ∈ ℂ) |
26 | 22, 25 | mulcld 7900 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝑖 · 𝑀) ∈ ℂ) |
27 | 6, 20, 26 | subadd2d 8209 |
. . . . . . . . 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 8190 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → (𝐴 − 𝐵) ∈ ℂ) |
31 | 30 | adantr 274 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℂ) |
32 | | qre 9540 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℚ → 𝑀 ∈
ℝ) |
33 | 32 | 3ad2ant2 1004 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝑀 ∈
ℝ) |
34 | 33 | ad2antrr 480 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑀 ∈ ℝ) |
35 | 13 | adantr 274 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 0 < 𝑀) |
36 | 34, 35 | gt0ap0d 8508 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑀 # 0) |
37 | 31, 22, 25, 36 | divmulap3d 8702 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (((𝐴 − 𝐵) / 𝑀) = 𝑖 ↔ (𝐴 − 𝐵) = (𝑖 · 𝑀))) |
38 | | oveq2 5834 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = (𝐴 mod 𝑀) → (𝐴 − 𝐵) = (𝐴 − (𝐴 mod 𝑀))) |
39 | 38 | oveq1d 5841 |
. . . . . . . . . . . . 13
⊢ (𝐵 = (𝐴 mod 𝑀) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
40 | 39 | eqcoms 2160 |
. . . . . . . . . . . 12
⊢ ((𝐴 mod 𝑀) = 𝐵 → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
41 | 40 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
42 | 41 | adantr 274 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
43 | | modqdiffl 10243 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℚ ∧ 𝑀 ∈ ℚ ∧ 0 <
𝑀) → ((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
44 | 9, 43 | syl3an1 1253 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
45 | 44 | ad2antrr 480 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
46 | 42, 45 | eqtrd 2190 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − 𝐵) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
47 | 46 | eqeq1d 2166 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (((𝐴 − 𝐵) / 𝑀) = 𝑖 ↔ (⌊‘(𝐴 / 𝑀)) = 𝑖)) |
48 | 28, 37, 47 | 3bitr2d 215 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 = ((𝑖 · 𝑀) + 𝐵) ↔ (⌊‘(𝐴 / 𝑀)) = 𝑖)) |
49 | | qre 9540 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℝ) |
50 | 10, 49 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝐴 ∈
ℝ) |
51 | | nn0ge0 9120 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ0
→ 0 ≤ 𝐴) |
52 | 51 | 3ad2ant1 1003 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
≤ 𝐴) |
53 | | simp3 984 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
< 𝑀) |
54 | | divge0 8749 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ (𝐴 / 𝑀)) |
55 | 50, 52, 33, 53, 54 | syl22anc 1221 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
≤ (𝐴 / 𝑀)) |
56 | | simp2 983 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝑀 ∈
ℚ) |
57 | 53 | gt0ne0d 8391 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝑀 ≠ 0) |
58 | | qdivcl 9558 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℚ ∧ 𝑀 ∈ ℚ ∧ 𝑀 ≠ 0) → (𝐴 / 𝑀) ∈ ℚ) |
59 | 10, 56, 57, 58 | syl3anc 1220 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
(𝐴 / 𝑀) ∈ ℚ) |
60 | | 0z 9183 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
61 | | flqge 10190 |
. . . . . . . . . . 11
⊢ (((𝐴 / 𝑀) ∈ ℚ ∧ 0 ∈ ℤ)
→ (0 ≤ (𝐴 / 𝑀) ↔ 0 ≤
(⌊‘(𝐴 / 𝑀)))) |
62 | 59, 60, 61 | sylancl 410 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → (0
≤ (𝐴 / 𝑀) ↔ 0 ≤ (⌊‘(𝐴 / 𝑀)))) |
63 | 55, 62 | mpbid 146 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
≤ (⌊‘(𝐴 /
𝑀))) |
64 | | breq2 3971 |
. . . . . . . . 9
⊢
((⌊‘(𝐴 /
𝑀)) = 𝑖 → (0 ≤ (⌊‘(𝐴 / 𝑀)) ↔ 0 ≤ 𝑖)) |
65 | 63, 64 | syl5ibcom 154 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((⌊‘(𝐴 / 𝑀)) = 𝑖 → 0 ≤ 𝑖)) |
66 | 65 | ad2antrr 480 |
. . . . . . 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 9185 |
. . . . 5
⊢ (𝑖 ∈ ℕ0
↔ (𝑖 ∈ ℤ
∧ 0 ≤ 𝑖)) |
70 | 2, 68, 69 | sylanbrc 414 |
. . . 4
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝑖 ∈ ℕ0) |
71 | | oveq1 5833 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → (𝑘 · 𝑀) = (𝑖 · 𝑀)) |
72 | 71 | oveq1d 5841 |
. . . . . 6
⊢ (𝑘 = 𝑖 → ((𝑘 · 𝑀) + 𝐵) = ((𝑖 · 𝑀) + 𝐵)) |
73 | 72 | eqeq2d 2169 |
. . . . 5
⊢ (𝑘 = 𝑖 → (𝐴 = ((𝑘 · 𝑀) + 𝐵) ↔ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
74 | 73 | adantl 275 |
. . . 4
⊢
((((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) ∧ 𝑘 = 𝑖) → (𝐴 = ((𝑘 · 𝑀) + 𝐵) ↔ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
75 | | simpr 109 |
. . . 4
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝐴 = ((𝑖 · 𝑀) + 𝐵)) |
76 | 70, 74, 75 | rspcedvd 2822 |
. . 3
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵)) |
77 | | modqmuladdim 10275 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℚ ∧ 0 <
𝑀) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
78 | 7, 77 | syl3an1 1253 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((𝐴 mod 𝑀) = 𝐵 → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
79 | 78 | imp 123 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) |
80 | 76, 79 | r19.29a 2600 |
. 2
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵)) |
81 | 80 | ex 114 |
1
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((𝐴 mod 𝑀) = 𝐵 → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵))) |