Proof of Theorem modmuladd
Step | Hyp | Ref
| Expression |
1 | | zre 12323 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
2 | 1 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+)
→ 𝐴 ∈
ℝ) |
3 | | rpre 12738 |
. . . . . . . 8
⊢ (𝑀 ∈ ℝ+
→ 𝑀 ∈
ℝ) |
4 | 3 | adantl 482 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+)
→ 𝑀 ∈
ℝ) |
5 | | rpne0 12746 |
. . . . . . . 8
⊢ (𝑀 ∈ ℝ+
→ 𝑀 ≠
0) |
6 | 5 | adantl 482 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+)
→ 𝑀 ≠
0) |
7 | 2, 4, 6 | redivcld 11803 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+)
→ (𝐴 / 𝑀) ∈
ℝ) |
8 | 7 | flcld 13518 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝑀)) ∈
ℤ) |
9 | 8 | 3adant2 1130 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) →
(⌊‘(𝐴 / 𝑀)) ∈
ℤ) |
10 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑘 = (⌊‘(𝐴 / 𝑀)) → (𝑘 · 𝑀) = ((⌊‘(𝐴 / 𝑀)) · 𝑀)) |
11 | 10 | oveq1d 7290 |
. . . . . 6
⊢ (𝑘 = (⌊‘(𝐴 / 𝑀)) → ((𝑘 · 𝑀) + (𝐴 mod 𝑀)) = (((⌊‘(𝐴 / 𝑀)) · 𝑀) + (𝐴 mod 𝑀))) |
12 | 11 | eqeq2d 2749 |
. . . . 5
⊢ (𝑘 = (⌊‘(𝐴 / 𝑀)) → (𝐴 = ((𝑘 · 𝑀) + (𝐴 mod 𝑀)) ↔ 𝐴 = (((⌊‘(𝐴 / 𝑀)) · 𝑀) + (𝐴 mod 𝑀)))) |
13 | 12 | adantl 482 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) ∧ 𝑘 = (⌊‘(𝐴 / 𝑀))) → (𝐴 = ((𝑘 · 𝑀) + (𝐴 mod 𝑀)) ↔ 𝐴 = (((⌊‘(𝐴 / 𝑀)) · 𝑀) + (𝐴 mod 𝑀)))) |
14 | 1 | anim1i 615 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+)
→ (𝐴 ∈ ℝ
∧ 𝑀 ∈
ℝ+)) |
15 | 14 | 3adant2 1130 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) → (𝐴 ∈ ℝ ∧ 𝑀 ∈
ℝ+)) |
16 | | flpmodeq 13594 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+)
→ (((⌊‘(𝐴
/ 𝑀)) · 𝑀) + (𝐴 mod 𝑀)) = 𝐴) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) →
(((⌊‘(𝐴 / 𝑀)) · 𝑀) + (𝐴 mod 𝑀)) = 𝐴) |
18 | 17 | eqcomd 2744 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) → 𝐴 = (((⌊‘(𝐴 / 𝑀)) · 𝑀) + (𝐴 mod 𝑀))) |
19 | 9, 13, 18 | rspcedvd 3563 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) →
∃𝑘 ∈ ℤ
𝐴 = ((𝑘 · 𝑀) + (𝐴 mod 𝑀))) |
20 | | oveq2 7283 |
. . . . . 6
⊢ (𝐵 = (𝐴 mod 𝑀) → ((𝑘 · 𝑀) + 𝐵) = ((𝑘 · 𝑀) + (𝐴 mod 𝑀))) |
21 | 20 | eqeq2d 2749 |
. . . . 5
⊢ (𝐵 = (𝐴 mod 𝑀) → (𝐴 = ((𝑘 · 𝑀) + 𝐵) ↔ 𝐴 = ((𝑘 · 𝑀) + (𝐴 mod 𝑀)))) |
22 | 21 | eqcoms 2746 |
. . . 4
⊢ ((𝐴 mod 𝑀) = 𝐵 → (𝐴 = ((𝑘 · 𝑀) + 𝐵) ↔ 𝐴 = ((𝑘 · 𝑀) + (𝐴 mod 𝑀)))) |
23 | 22 | rexbidv 3226 |
. . 3
⊢ ((𝐴 mod 𝑀) = 𝐵 → (∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵) ↔ ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + (𝐴 mod 𝑀)))) |
24 | 19, 23 | syl5ibrcom 246 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵))) |
25 | | oveq1 7282 |
. . . 4
⊢ (𝐴 = ((𝑘 · 𝑀) + 𝐵) → (𝐴 mod 𝑀) = (((𝑘 · 𝑀) + 𝐵) mod 𝑀)) |
26 | | simpr 485 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈
ℤ) |
27 | | simpl3 1192 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) ∧ 𝑘 ∈ ℤ) → 𝑀 ∈
ℝ+) |
28 | | simpl2 1191 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) ∧ 𝑘 ∈ ℤ) → 𝐵 ∈ (0[,)𝑀)) |
29 | | muladdmodid 13631 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℝ+
∧ 𝐵 ∈ (0[,)𝑀)) → (((𝑘 · 𝑀) + 𝐵) mod 𝑀) = 𝐵) |
30 | 26, 27, 28, 29 | syl3anc 1370 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) ∧ 𝑘 ∈ ℤ) → (((𝑘 · 𝑀) + 𝐵) mod 𝑀) = 𝐵) |
31 | 25, 30 | sylan9eqr 2800 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) ∧ 𝑘 ∈ ℤ) ∧ 𝐴 = ((𝑘 · 𝑀) + 𝐵)) → (𝐴 mod 𝑀) = 𝐵) |
32 | 31 | rexlimdva2 3216 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) →
(∃𝑘 ∈ ℤ
𝐴 = ((𝑘 · 𝑀) + 𝐵) → (𝐴 mod 𝑀) = 𝐵)) |
33 | 24, 32 | impbid 211 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = 𝐵 ↔ ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵))) |