Step | Hyp | Ref
| Expression |
1 | | nn0z 11277 |
. . . . 5
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℤ) |
2 | | modmuladdim 12575 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+)
→ ((𝐴 mod 𝑀) = 𝐵 → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
3 | 1, 2 | sylan 487 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
4 | 3 | imp 444 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) → ∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) |
5 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑖 ∈ ℤ) |
6 | 5 | adantr 480 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝑖 ∈ ℤ) |
7 | | nn0cn 11179 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℂ) |
8 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → 𝐴 ∈ ℂ) |
9 | 8 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝐴 ∈ ℂ) |
10 | | nn0re 11178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) |
11 | | modcl 12534 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+)
→ (𝐴 mod 𝑀) ∈
ℝ) |
12 | 10, 11 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → (𝐴 mod 𝑀) ∈ ℝ) |
13 | 12 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → (𝐴 mod 𝑀) ∈ ℂ) |
14 | 13 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) → (𝐴 mod 𝑀) ∈ ℂ) |
15 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 mod 𝑀) = 𝐵 → ((𝐴 mod 𝑀) ∈ ℂ ↔ 𝐵 ∈ ℂ)) |
16 | 15 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) → ((𝐴 mod 𝑀) ∈ ℂ ↔ 𝐵 ∈ ℂ)) |
17 | 14, 16 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) → 𝐵 ∈ ℂ) |
18 | 17 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝐵 ∈ ℂ) |
19 | | zcn 11259 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℂ) |
20 | 19 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑖 ∈ ℂ) |
21 | | rpcn 11717 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℝ+
→ 𝑀 ∈
ℂ) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → 𝑀 ∈ ℂ) |
23 | 22 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → 𝑀 ∈ ℂ) |
24 | 20, 23 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝑖 · 𝑀) ∈ ℂ) |
25 | 9, 18, 24 | subadd2d 10290 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − 𝐵) = (𝑖 · 𝑀) ↔ ((𝑖 · 𝑀) + 𝐵) = 𝐴)) |
26 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ (𝐴 = ((𝑖 · 𝑀) + 𝐵) ↔ ((𝑖 · 𝑀) + 𝐵) = 𝐴) |
27 | 25, 26 | syl6rbbr 278 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 = ((𝑖 · 𝑀) + 𝐵) ↔ (𝐴 − 𝐵) = (𝑖 · 𝑀))) |
28 | 7 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) → 𝐴 ∈ ℂ) |
29 | 28, 17 | subcld 10271 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) → (𝐴 − 𝐵) ∈ ℂ) |
30 | 29 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℂ) |
31 | | rpcnne0 11726 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℝ+
→ (𝑀 ∈ ℂ
∧ 𝑀 ≠
0)) |
32 | 31 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0)) |
33 | 32 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0)) |
34 | | divmul3 10569 |
. . . . . . . . . . 11
⊢ (((𝐴 − 𝐵) ∈ ℂ ∧ 𝑖 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0)) → (((𝐴 − 𝐵) / 𝑀) = 𝑖 ↔ (𝐴 − 𝐵) = (𝑖 · 𝑀))) |
35 | 30, 20, 33, 34 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (((𝐴 − 𝐵) / 𝑀) = 𝑖 ↔ (𝐴 − 𝐵) = (𝑖 · 𝑀))) |
36 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 = (𝐴 mod 𝑀) → (𝐴 − 𝐵) = (𝐴 − (𝐴 mod 𝑀))) |
37 | 36 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 = (𝐴 mod 𝑀) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
38 | 37 | eqcoms 2618 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 mod 𝑀) = 𝐵 → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
39 | 38 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
40 | 39 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − 𝐵) / 𝑀) = ((𝐴 − (𝐴 mod 𝑀)) / 𝑀)) |
41 | | moddiffl 12543 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+)
→ ((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
42 | 10, 41 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → ((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
43 | 42 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − (𝐴 mod 𝑀)) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
44 | 40, 43 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → ((𝐴 − 𝐵) / 𝑀) = (⌊‘(𝐴 / 𝑀))) |
45 | 44 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (((𝐴 − 𝐵) / 𝑀) = 𝑖 ↔ (⌊‘(𝐴 / 𝑀)) = 𝑖)) |
46 | 27, 35, 45 | 3bitr2d 295 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 = ((𝑖 · 𝑀) + 𝐵) ↔ (⌊‘(𝐴 / 𝑀)) = 𝑖)) |
47 | | nn0ge0 11195 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ0
→ 0 ≤ 𝐴) |
48 | 10, 47 | jca 553 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ0
→ (𝐴 ∈ ℝ
∧ 0 ≤ 𝐴)) |
49 | | rpregt0 11722 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℝ+
→ (𝑀 ∈ ℝ
∧ 0 < 𝑀)) |
50 | | divge0 10771 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ (𝐴 / 𝑀)) |
51 | 48, 49, 50 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → 0 ≤ (𝐴 / 𝑀)) |
52 | 10 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → 𝐴 ∈ ℝ) |
53 | | rpre 11715 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℝ+
→ 𝑀 ∈
ℝ) |
54 | 53 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → 𝑀 ∈ ℝ) |
55 | | rpne0 11724 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℝ+
→ 𝑀 ≠
0) |
56 | 55 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → 𝑀 ≠ 0) |
57 | 52, 54, 56 | redivcld 10732 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → (𝐴 / 𝑀) ∈ ℝ) |
58 | | 0z 11265 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℤ |
59 | | flge 12468 |
. . . . . . . . . . . . 13
⊢ (((𝐴 / 𝑀) ∈ ℝ ∧ 0 ∈ ℤ)
→ (0 ≤ (𝐴 / 𝑀) ↔ 0 ≤
(⌊‘(𝐴 / 𝑀)))) |
60 | 57, 58, 59 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → (0 ≤ (𝐴 / 𝑀) ↔ 0 ≤ (⌊‘(𝐴 / 𝑀)))) |
61 | 51, 60 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → 0 ≤ (⌊‘(𝐴 / 𝑀))) |
62 | | breq2 4587 |
. . . . . . . . . . 11
⊢
((⌊‘(𝐴 /
𝑀)) = 𝑖 → (0 ≤ (⌊‘(𝐴 / 𝑀)) ↔ 0 ≤ 𝑖)) |
63 | 61, 62 | syl5ibcom 234 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → ((⌊‘(𝐴 / 𝑀)) = 𝑖 → 0 ≤ 𝑖)) |
64 | 63 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) →
((⌊‘(𝐴 / 𝑀)) = 𝑖 → 0 ≤ 𝑖)) |
65 | 46, 64 | sylbid 229 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 = ((𝑖 · 𝑀) + 𝐵) → 0 ≤ 𝑖)) |
66 | 65 | imp 444 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 0 ≤ 𝑖) |
67 | | elnn0z 11267 |
. . . . . . 7
⊢ (𝑖 ∈ ℕ0
↔ (𝑖 ∈ ℤ
∧ 0 ≤ 𝑖)) |
68 | 6, 66, 67 | sylanbrc 695 |
. . . . . 6
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝑖 ∈ ℕ0) |
69 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = 𝑖 → (𝑘 · 𝑀) = (𝑖 · 𝑀)) |
70 | 69 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → ((𝑘 · 𝑀) + 𝐵) = ((𝑖 · 𝑀) + 𝐵)) |
71 | 70 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → (𝐴 = ((𝑘 · 𝑀) + 𝐵) ↔ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
72 | 71 | adantl 481 |
. . . . . 6
⊢
((((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) ∧ 𝑘 = 𝑖) → (𝐴 = ((𝑘 · 𝑀) + 𝐵) ↔ 𝐴 = ((𝑖 · 𝑀) + 𝐵))) |
73 | | simpr 476 |
. . . . . 6
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → 𝐴 = ((𝑖 · 𝑀) + 𝐵)) |
74 | 68, 72, 73 | rspcedvd 3289 |
. . . . 5
⊢
(((((𝐴 ∈
ℕ0 ∧ 𝑀
∈ ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) ∧ 𝐴 = ((𝑖 · 𝑀) + 𝐵)) → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵)) |
75 | 74 | ex 449 |
. . . 4
⊢ ((((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) ∧ 𝑖 ∈ ℤ) → (𝐴 = ((𝑖 · 𝑀) + 𝐵) → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵))) |
76 | 75 | rexlimdva 3013 |
. . 3
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) → (∃𝑖 ∈ ℤ 𝐴 = ((𝑖 · 𝑀) + 𝐵) → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵))) |
77 | 4, 76 | mpd 15 |
. 2
⊢ (((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) ∧ (𝐴 mod 𝑀) = 𝐵) → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵)) |
78 | 77 | ex 449 |
1
⊢ ((𝐴 ∈ ℕ0
∧ 𝑀 ∈
ℝ+) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵))) |