Proof of Theorem modadd1
| Step | Hyp | Ref
| Expression |
| 1 | | modval 13911 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐴 mod 𝐷) = (𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷))))) |
| 2 | | modval 13911 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐵 mod 𝐷) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷))))) |
| 3 | 1, 2 | eqeqan12d 2751 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
∧ (𝐵 ∈ ℝ
∧ 𝐷 ∈
ℝ+)) → ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) ↔ (𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))))) |
| 4 | 3 | anandirs 679 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐷 ∈ ℝ+)
→ ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) ↔ (𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))))) |
| 5 | 4 | adantrl 716 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) ↔ (𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))))) |
| 6 | | oveq1 7438 |
. . . . 5
⊢ ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) → ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶)) |
| 7 | 5, 6 | biimtrdi 253 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) → ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶))) |
| 8 | | recn 11245 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐴 ∈
ℂ) |
| 10 | | recn 11245 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) |
| 11 | 10 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐶 ∈
ℂ) |
| 12 | | rpcn 13045 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ℝ+
→ 𝐷 ∈
ℂ) |
| 13 | 12 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ 𝐷 ∈
ℂ) |
| 14 | | rerpdivcl 13065 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐴 / 𝐷) ∈
ℝ) |
| 15 | | reflcl 13836 |
. . . . . . . . . . 11
⊢ ((𝐴 / 𝐷) ∈ ℝ →
(⌊‘(𝐴 / 𝐷)) ∈
ℝ) |
| 16 | 15 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝐴 / 𝐷) ∈ ℝ →
(⌊‘(𝐴 / 𝐷)) ∈
ℂ) |
| 17 | 14, 16 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐷)) ∈
ℂ) |
| 18 | 13, 17 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐷 ·
(⌊‘(𝐴 / 𝐷))) ∈
ℂ) |
| 19 | 18 | adantrl 716 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (𝐷 ·
(⌊‘(𝐴 / 𝐷))) ∈
ℂ) |
| 20 | 9, 11, 19 | addsubd 11641 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶)) |
| 21 | 20 | adantlr 715 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶)) |
| 22 | | recn 11245 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
| 23 | 22 | adantr 480 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐵 ∈
ℂ) |
| 24 | 10 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐶 ∈
ℂ) |
| 25 | 12 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ 𝐷 ∈
ℂ) |
| 26 | | rerpdivcl 13065 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐵 / 𝐷) ∈
ℝ) |
| 27 | | reflcl 13836 |
. . . . . . . . . . 11
⊢ ((𝐵 / 𝐷) ∈ ℝ →
(⌊‘(𝐵 / 𝐷)) ∈
ℝ) |
| 28 | 27 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝐵 / 𝐷) ∈ ℝ →
(⌊‘(𝐵 / 𝐷)) ∈
ℂ) |
| 29 | 26, 28 | syl 17 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐷)) ∈
ℂ) |
| 30 | 25, 29 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (𝐷 ·
(⌊‘(𝐵 / 𝐷))) ∈
ℂ) |
| 31 | 30 | adantrl 716 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (𝐷 ·
(⌊‘(𝐵 / 𝐷))) ∈
ℂ) |
| 32 | 23, 24, 31 | addsubd 11641 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶)) |
| 33 | 32 | adantll 714 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶)) |
| 34 | 21, 33 | eqeq12d 2753 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) ↔ ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶))) |
| 35 | 7, 34 | sylibrd 259 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) → ((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))))) |
| 36 | | oveq1 7438 |
. . . 4
⊢ (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) → (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷)) |
| 37 | | readdcl 11238 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) ∈ ℝ) |
| 38 | 37 | adantrr 717 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (𝐴 + 𝐶) ∈
ℝ) |
| 39 | | simprr 773 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐷 ∈
ℝ+) |
| 40 | 14 | flcld 13838 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐷)) ∈
ℤ) |
| 41 | 40 | adantrl 716 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (⌊‘(𝐴 /
𝐷)) ∈
ℤ) |
| 42 | | modcyc2 13947 |
. . . . . . 7
⊢ (((𝐴 + 𝐶) ∈ ℝ ∧ 𝐷 ∈ ℝ+ ∧
(⌊‘(𝐴 / 𝐷)) ∈ ℤ) →
(((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = ((𝐴 + 𝐶) mod 𝐷)) |
| 43 | 38, 39, 41, 42 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = ((𝐴 + 𝐶) mod 𝐷)) |
| 44 | 43 | adantlr 715 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = ((𝐴 + 𝐶) mod 𝐷)) |
| 45 | | readdcl 11238 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 + 𝐶) ∈ ℝ) |
| 46 | 45 | adantrr 717 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (𝐵 + 𝐶) ∈
ℝ) |
| 47 | | simprr 773 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ 𝐷 ∈
ℝ+) |
| 48 | 26 | flcld 13838 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐷)) ∈
ℤ) |
| 49 | 48 | adantrl 716 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (⌊‘(𝐵 /
𝐷)) ∈
ℤ) |
| 50 | | modcyc2 13947 |
. . . . . . 7
⊢ (((𝐵 + 𝐶) ∈ ℝ ∧ 𝐷 ∈ ℝ+ ∧
(⌊‘(𝐵 / 𝐷)) ∈ ℤ) →
(((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |
| 51 | 46, 47, 49, 50 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |
| 52 | 51 | adantll 714 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |
| 53 | 44, 52 | eqeq12d 2753 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷) ↔ ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))) |
| 54 | 36, 53 | imbitrid 244 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))) |
| 55 | 35, 54 | syld 47 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+))
→ ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))) |
| 56 | 55 | 3impia 1118 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+)
∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |