Step | Hyp | Ref
| Expression |
1 | | simpr 109 |
. . . . . 6
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑖 ∈ ℤ) |
2 | 1 | adantr 271 |
. . . . 5
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝑖 ∈ ℤ) |
3 | | nn0cn 8781 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℂ) |
4 | 3 | 3ad2ant1 967 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝐴 ∈
ℂ) |
5 | 4 | ad2antrr 473 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝐴 ∈ ℂ) |
6 | | nn0z 8868 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℤ) |
7 | | zq 9210 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℚ) |
8 | 6, 7 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℚ) |
9 | 8 | 3ad2ant1 967 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝐴 ∈
ℚ) |
10 | 9 | adantr 271 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝐴 ∈ ℚ) |
11 | | simpl2 950 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝑀 ∈ ℚ) |
12 | | simpl3 951 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 0 < 𝑀) |
13 | 10, 11, 12 | modqcld 9884 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → (𝐴 mod 𝑀) ∈ ℚ) |
14 | | qcn 9218 |
. . . . . . . . . . . . 13
⊢ ((𝐴 mod 𝑀) ∈ ℚ → (𝐴 mod 𝑀) ∈ ℂ) |
15 | 13, 14 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → (𝐴 mod 𝑀) ∈ ℂ) |
16 | | eleq1 2157 |
. . . . . . . . . . . . 13
⊢ ((𝐴 mod 𝑀) = 𝐵 → ((𝐴 mod 𝑀) ∈ ℂ ↔ 𝐵 ∈ ℂ)) |
17 | 16 | adantl 272 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → ((𝐴 mod 𝑀) ∈ ℂ ↔ 𝐵 ∈ ℂ)) |
18 | 15, 17 | mpbid 146 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝐵 ∈ ℂ) |
19 | 18 | adantr 271 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝐵 ∈ ℂ) |
20 | | zcn 8853 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℂ) |
21 | 20 | adantl 272 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑖 ∈ ℂ) |
22 | | qcn 9218 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℚ → 𝑀 ∈
ℂ) |
23 | 11, 22 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝑀 ∈ ℂ) |
24 | 23 | adantr 271 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑀 ∈ ℂ) |
25 | 21, 24 | mulcld 7605 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝑖 · 𝑀) ∈ ℂ) |
26 | 5, 19, 25 | subadd2d 7909 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − 𝐵) = (𝑖 · 𝑀) ↔ ((𝑖 · 𝑀) + 𝐵) = 𝐴)) |
27 | | eqcom 2097 |
. . . . . . . . 9
⊢ (𝐴 = ((𝑖 · 𝑀) + 𝐵) ↔ ((𝑖 · 𝑀) + 𝐵) = 𝐴) |
28 | 26, 27 | syl6rbbr 198 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 = ((𝑖 · 𝑀) + 𝐵) ↔ (𝐴 − 𝐵) = (𝑖 · 𝑀))) |
29 | 4 | adantr 271 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → 𝐴 ∈ ℂ) |
30 | 29, 18 | subcld 7890 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → (𝐴 − 𝐵) ∈ ℂ) |
31 | 30 | adantr 271 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℂ) |
32 | | qre 9209 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℚ → 𝑀 ∈
ℝ) |
33 | 32 | 3ad2ant2 968 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝑀 ∈
ℝ) |
34 | 33 | ad2antrr 473 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑀 ∈ ℝ) |
35 | 12 | adantr 271 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 0 < 𝑀) |
36 | 34, 35 | gt0ap0d 8202 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑀 # 0) |
37 | 31, 21, 24, 36 | divmulap3d 8389 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (((𝐴 − 𝐵) / 𝑀) = 𝑖 ↔ (𝐴 − 𝐵) = (𝑖 · 𝑀))) |
38 | | oveq2 5698 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = (𝐴 mod 𝑀) → (𝐴 − 𝐵) = (𝐴 − (𝐴 mod 𝑀))) |
39 | 38 | oveq1d 5705 |
. . . . . . . . . . . . 13
⊢ (𝐵 = (𝐴 mod 𝑀) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
40 | 39 | eqcoms 2098 |
. . . . . . . . . . . 12
⊢ ((𝐴 mod 𝑀) = 𝐵 → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
41 | 40 | adantl 272 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
42 | 41 | adantr 271 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
43 | | modqdiffl 9891 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℚ ∧ 𝑀 ∈ ℚ ∧ 0 <
𝑀) → ((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
44 | 8, 43 | syl3an1 1214 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
45 | 44 | ad2antrr 473 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
46 | 42, 45 | eqtrd 2127 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − 𝐵) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
47 | 46 | eqeq1d 2103 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (((𝐴 − 𝐵) / 𝑀) = 𝑖 ↔ (⌊‘(𝐴 / 𝑀)) = 𝑖)) |
48 | 28, 37, 47 | 3bitr2d 215 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 = ((𝑖 · 𝑀) + 𝐵) ↔ (⌊‘(𝐴 / 𝑀)) = 𝑖)) |
49 | | qre 9209 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℝ) |
50 | 9, 49 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝐴 ∈
ℝ) |
51 | | nn0ge0 8796 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ0
→ 0 ≤ 𝐴) |
52 | 51 | 3ad2ant1 967 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
≤ 𝐴) |
53 | | simp3 948 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
< 𝑀) |
54 | | divge0 8431 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ (𝐴 / 𝑀)) |
55 | 50, 52, 33, 53, 54 | syl22anc 1182 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
≤ (𝐴 / 𝑀)) |
56 | | simp2 947 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝑀 ∈
ℚ) |
57 | 53 | gt0ne0d 8087 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
𝑀 ≠ 0) |
58 | | qdivcl 9227 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℚ ∧ 𝑀 ∈ ℚ ∧ 𝑀 ≠ 0) → (𝐴 / 𝑀) ∈ ℚ) |
59 | 9, 56, 57, 58 | syl3anc 1181 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
(𝐴 / 𝑀) ∈ ℚ) |
60 | | 0z 8859 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
61 | | flqge 9838 |
. . . . . . . . . . 11
⊢ (((𝐴 / 𝑀) ∈ ℚ ∧ 0 ∈ ℤ)
→ (0 ≤ (𝐴 / 𝑀) ↔ 0 ≤
(⌊‘(𝐴 / 𝑀)))) |
62 | 59, 60, 61 | sylancl 405 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → (0
≤ (𝐴 / 𝑀) ↔ 0 ≤ (⌊‘(𝐴 / 𝑀)))) |
63 | 55, 62 | mpbid 146 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) → 0
≤ (⌊‘(𝐴 /
𝑀))) |
64 | | breq2 3871 |
. . . . . . . . 9
⊢
((⌊‘(𝐴 /
𝑀)) = 𝑖 → (0 ≤ (⌊‘(𝐴 / 𝑀)) ↔ 0 ≤ 𝑖)) |
65 | 63, 64 | syl5ibcom 154 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((⌊‘(𝐴 / 𝑀)) = 𝑖 → 0 ≤ 𝑖)) |
66 | 65 | ad2antrr 473 |
. . . . . . 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 8861 |
. . . . 5
⊢ (𝑖 ∈ ℕ0
↔ (𝑖 ∈ ℤ
∧ 0 ≤ 𝑖)) |
70 | 2, 68, 69 | sylanbrc 409 |
. . . 4
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝑖 ∈ ℕ0) |
71 | | oveq1 5697 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → (𝑘 · 𝑀) = (𝑖 · 𝑀)) |
72 | 71 | oveq1d 5705 |
. . . . . 6
⊢ (𝑘 = 𝑖 → ((𝑘 · 𝑀) + 𝐵) = ((𝑖 · 𝑀) + 𝐵)) |
73 | 72 | eqeq2d 2106 |
. . . . 5
⊢ (𝑘 = 𝑖 → (𝐴 = ((𝑘 · 𝑀) + 𝐵) ↔ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
74 | 73 | adantl 272 |
. . . 4
⊢
((((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) ∧ 𝑘 = 𝑖) → (𝐴 = ((𝑘 · 𝑀) + 𝐵) ↔ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
75 | | simpr 109 |
. . . 4
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝐴 = ((𝑖 · 𝑀) + 𝐵)) |
76 | 70, 74, 75 | rspcedvd 2742 |
. . 3
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℚ ∧ 0 < 𝑀) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵)) |
77 | | modqmuladdim 9923 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℚ ∧ 0 <
𝑀) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
78 | 6, 77 | syl3an1 1214 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((𝐴 mod 𝑀) = 𝐵 → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
79 | 78 | imp 123 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) |
80 | 76, 79 | r19.29a 2525 |
. 2
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) ∧
(𝐴 mod 𝑀) = 𝐵) → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵)) |
81 | 80 | ex 114 |
1
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈ ℚ
∧ 0 < 𝑀) →
((𝐴 mod 𝑀) = 𝐵 → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵))) |