Proof of Theorem modadd1
Step | Hyp | Ref
| Expression |
1 | | modval 13579 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐴 mod 𝐷) = (𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷))))) |
2 | | modval 13579 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐵 mod 𝐷) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷))))) |
3 | 1, 2 | eqeqan12d 2752 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
∧ (𝐵 ∈ ℝ
∧ 𝐷 ∈
ℝ+)) → ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) ↔ (𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))))) |
4 | 3 | anandirs 676 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐷 ∈ ℝ+)
→ ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) ↔ (𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))))) |
5 | 4 | adantrl 713 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) ↔ (𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))))) |
6 | | oveq1 7275 |
. . . . 5
⊢ ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) → ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶)) |
7 | 5, 6 | syl6bi 252 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) → ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶))) |
8 | | recn 10949 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
9 | 8 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐴 ∈
ℂ) |
10 | | recn 10949 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) |
11 | 10 | ad2antrl 725 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐶 ∈
ℂ) |
12 | | rpcn 12728 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ℝ+
→ 𝐷 ∈
ℂ) |
13 | 12 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ 𝐷 ∈
ℂ) |
14 | | rerpdivcl 12748 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐴 / 𝐷) ∈
ℝ) |
15 | | reflcl 13504 |
. . . . . . . . . . 11
⊢ ((𝐴 / 𝐷) ∈ ℝ →
(⌊‘(𝐴 / 𝐷)) ∈
ℝ) |
16 | 15 | recnd 10991 |
. . . . . . . . . 10
⊢ ((𝐴 / 𝐷) ∈ ℝ →
(⌊‘(𝐴 / 𝐷)) ∈
ℂ) |
17 | 14, 16 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐷)) ∈
ℂ) |
18 | 13, 17 | mulcld 10983 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐷 ·
(⌊‘(𝐴 / 𝐷))) ∈
ℂ) |
19 | 18 | adantrl 713 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (𝐷 ·
(⌊‘(𝐴 / 𝐷))) ∈
ℂ) |
20 | 9, 11, 19 | addsubd 11341 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶)) |
21 | 20 | adantlr 712 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶)) |
22 | | recn 10949 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
23 | 22 | adantr 481 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐵 ∈
ℂ) |
24 | 10 | ad2antrl 725 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐶 ∈
ℂ) |
25 | 12 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ 𝐷 ∈
ℂ) |
26 | | rerpdivcl 12748 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐵 / 𝐷) ∈
ℝ) |
27 | | reflcl 13504 |
. . . . . . . . . . 11
⊢ ((𝐵 / 𝐷) ∈ ℝ →
(⌊‘(𝐵 / 𝐷)) ∈
ℝ) |
28 | 27 | recnd 10991 |
. . . . . . . . . 10
⊢ ((𝐵 / 𝐷) ∈ ℝ →
(⌊‘(𝐵 / 𝐷)) ∈
ℂ) |
29 | 26, 28 | syl 17 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐷)) ∈
ℂ) |
30 | 25, 29 | mulcld 10983 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐷 ·
(⌊‘(𝐵 / 𝐷))) ∈
ℂ) |
31 | 30 | adantrl 713 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (𝐷 ·
(⌊‘(𝐵 / 𝐷))) ∈
ℂ) |
32 | 23, 24, 31 | addsubd 11341 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶)) |
33 | 32 | adantll 711 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶)) |
34 | 21, 33 | eqeq12d 2754 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) ↔ ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶))) |
35 | 7, 34 | sylibrd 258 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) → ((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))))) |
36 | | oveq1 7275 |
. . . 4
⊢ (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) → (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷)) |
37 | | readdcl 10942 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) ∈ ℝ) |
38 | 37 | adantrr 714 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (𝐴 + 𝐶) ∈
ℝ) |
39 | | simprr 770 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐷 ∈
ℝ+) |
40 | 14 | flcld 13506 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐷)) ∈
ℤ) |
41 | 40 | adantrl 713 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (⌊‘(𝐴 /
𝐷)) ∈
ℤ) |
42 | | modcyc2 13615 |
. . . . . . 7
⊢ (((𝐴 + 𝐶) ∈ ℝ ∧ 𝐷 ∈ ℝ+ ∧
(⌊‘(𝐴 / 𝐷)) ∈ ℤ) →
(((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = ((𝐴 + 𝐶) mod 𝐷)) |
43 | 38, 39, 41, 42 | syl3anc 1370 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = ((𝐴 + 𝐶) mod 𝐷)) |
44 | 43 | adantlr 712 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = ((𝐴 + 𝐶) mod 𝐷)) |
45 | | readdcl 10942 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 + 𝐶) ∈ ℝ) |
46 | 45 | adantrr 714 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (𝐵 + 𝐶) ∈
ℝ) |
47 | | simprr 770 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐷 ∈
ℝ+) |
48 | 26 | flcld 13506 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐷)) ∈
ℤ) |
49 | 48 | adantrl 713 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (⌊‘(𝐵 /
𝐷)) ∈
ℤ) |
50 | | modcyc2 13615 |
. . . . . . 7
⊢ (((𝐵 + 𝐶) ∈ ℝ ∧ 𝐷 ∈ ℝ+ ∧
(⌊‘(𝐵 / 𝐷)) ∈ ℤ) →
(((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |
51 | 46, 47, 49, 50 | syl3anc 1370 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |
52 | 51 | adantll 711 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |
53 | 44, 52 | eqeq12d 2754 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷) ↔ ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))) |
54 | 36, 53 | syl5ib 243 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))) |
55 | 35, 54 | syld 47 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))) |
56 | 55 | 3impia 1116 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |