Proof of Theorem modaddmodlo
Step | Hyp | Ref
| Expression |
1 | | elfzoelz 12470 |
. . . . . . . 8
⊢ (𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀))) → 𝐵 ∈ ℤ) |
2 | 1 | zred 11482 |
. . . . . . 7
⊢ (𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀))) → 𝐵 ∈ ℝ) |
3 | 2 | adantr 481 |
. . . . . 6
⊢ ((𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀))) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → 𝐵 ∈ ℝ) |
4 | | zmodcl 12690 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) ∈
ℕ0) |
5 | 4 | nn0red 11352 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐴 mod 𝑀) ∈ ℝ) |
6 | 5 | adantl 482 |
. . . . . 6
⊢ ((𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀))) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐴 mod 𝑀) ∈ ℝ) |
7 | 3, 6 | readdcld 10069 |
. . . . 5
⊢ ((𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀))) ∧ (𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ)) → (𝐵 + (𝐴 mod 𝑀)) ∈ ℝ) |
8 | 7 | ancoms 469 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → (𝐵 + (𝐴 mod 𝑀)) ∈ ℝ) |
9 | | nnrp 11842 |
. . . . 5
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ+) |
10 | 9 | ad2antlr 763 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → 𝑀 ∈
ℝ+) |
11 | 2 | adantl 482 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → 𝐵 ∈ ℝ) |
12 | 5 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → (𝐴 mod 𝑀) ∈ ℝ) |
13 | | elfzole1 12478 |
. . . . . 6
⊢ (𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀))) → 0 ≤ 𝐵) |
14 | 13 | adantl 482 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → 0 ≤ 𝐵) |
15 | 4 | nn0ge0d 11354 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 0 ≤
(𝐴 mod 𝑀)) |
16 | 15 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → 0 ≤ (𝐴 mod 𝑀)) |
17 | 11, 12, 14, 16 | addge0d 10603 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → 0 ≤ (𝐵 + (𝐴 mod 𝑀))) |
18 | | elfzolt2 12479 |
. . . . . 6
⊢ (𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀))) → 𝐵 < (𝑀 − (𝐴 mod 𝑀))) |
19 | 18 | adantl 482 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → 𝐵 < (𝑀 − (𝐴 mod 𝑀))) |
20 | | nnre 11027 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
21 | 20 | ad2antlr 763 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → 𝑀 ∈ ℝ) |
22 | 11, 12, 21 | ltaddsubd 10627 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → ((𝐵 + (𝐴 mod 𝑀)) < 𝑀 ↔ 𝐵 < (𝑀 − (𝐴 mod 𝑀)))) |
23 | 19, 22 | mpbird 247 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → (𝐵 + (𝐴 mod 𝑀)) < 𝑀) |
24 | | modid 12695 |
. . . 4
⊢ ((((𝐵 + (𝐴 mod 𝑀)) ∈ ℝ ∧ 𝑀 ∈ ℝ+) ∧ (0 ≤
(𝐵 + (𝐴 mod 𝑀)) ∧ (𝐵 + (𝐴 mod 𝑀)) < 𝑀)) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = (𝐵 + (𝐴 mod 𝑀))) |
25 | 8, 10, 17, 23, 24 | syl22anc 1327 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = (𝐵 + (𝐴 mod 𝑀))) |
26 | | zre 11381 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
27 | 26 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝐴 ∈
ℝ) |
28 | 27 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → 𝐴 ∈ ℝ) |
29 | | modadd2mod 12720 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+)
→ ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + 𝐴) mod 𝑀)) |
30 | 28, 11, 10, 29 | syl3anc 1326 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + 𝐴) mod 𝑀)) |
31 | 25, 30 | eqtr3d 2658 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ 𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀)))) → (𝐵 + (𝐴 mod 𝑀)) = ((𝐵 + 𝐴) mod 𝑀)) |
32 | 31 | ex 450 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀))) → (𝐵 + (𝐴 mod 𝑀)) = ((𝐵 + 𝐴) mod 𝑀))) |