Proof of Theorem modaddabs
Step | Hyp | Ref
| Expression |
1 | | modcl 13603 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) ∈
ℝ) |
2 | 1 | recnd 11013 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) ∈
ℂ) |
3 | 2 | 3adant2 1130 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) ∈
ℂ) |
4 | | modcl 13603 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) ∈
ℝ) |
5 | 4 | recnd 11013 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) ∈
ℂ) |
6 | 5 | 3adant1 1129 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) ∈
ℂ) |
7 | 3, 6 | addcomd 11187 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) = ((𝐵 mod 𝐶) + (𝐴 mod 𝐶))) |
8 | 7 | oveq1d 7282 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) mod 𝐶) = (((𝐵 mod 𝐶) + (𝐴 mod 𝐶)) mod 𝐶)) |
9 | | simpl 483 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
10 | 4, 9 | jca 512 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐵 mod 𝐶) ∈ ℝ ∧ 𝐵 ∈
ℝ)) |
11 | 10 | 3adant1 1129 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐵 mod 𝐶) ∈ ℝ ∧ 𝐵 ∈
ℝ)) |
12 | | simpr 485 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℝ+) |
13 | 1, 12 | jca 512 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐶 ∈
ℝ+)) |
14 | 13 | 3adant2 1130 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐶 ∈
ℝ+)) |
15 | | modabs2 13635 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐵 mod 𝐶) mod 𝐶) = (𝐵 mod 𝐶)) |
16 | 15 | 3adant1 1129 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐵 mod 𝐶) mod 𝐶) = (𝐵 mod 𝐶)) |
17 | | modadd1 13638 |
. . . 4
⊢ ((((𝐵 mod 𝐶) ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐶 ∈ ℝ+) ∧ ((𝐵 mod 𝐶) mod 𝐶) = (𝐵 mod 𝐶)) → (((𝐵 mod 𝐶) + (𝐴 mod 𝐶)) mod 𝐶) = ((𝐵 + (𝐴 mod 𝐶)) mod 𝐶)) |
18 | 11, 14, 16, 17 | syl3anc 1370 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐵 mod 𝐶) + (𝐴 mod 𝐶)) mod 𝐶) = ((𝐵 + (𝐴 mod 𝐶)) mod 𝐶)) |
19 | | recn 10971 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
20 | 19 | 3ad2ant2 1133 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
21 | 3, 20 | addcomd 11187 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) + 𝐵) = (𝐵 + (𝐴 mod 𝐶))) |
22 | 21 | oveq1d 7282 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 mod 𝐶) + 𝐵) mod 𝐶) = ((𝐵 + (𝐴 mod 𝐶)) mod 𝐶)) |
23 | 18, 22 | eqtr4d 2781 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐵 mod 𝐶) + (𝐴 mod 𝐶)) mod 𝐶) = (((𝐴 mod 𝐶) + 𝐵) mod 𝐶)) |
24 | | simpl 483 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐴 ∈
ℝ) |
25 | 1, 24 | jca 512 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐴 ∈
ℝ)) |
26 | 25 | 3adant2 1130 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐴 ∈
ℝ)) |
27 | | 3simpc 1149 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+)) |
28 | | modabs2 13635 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) mod 𝐶) = (𝐴 mod 𝐶)) |
29 | 28 | 3adant2 1130 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) mod 𝐶) = (𝐴 mod 𝐶)) |
30 | | modadd1 13638 |
. . 3
⊢ ((((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) ∧ ((𝐴 mod 𝐶) mod 𝐶) = (𝐴 mod 𝐶)) → (((𝐴 mod 𝐶) + 𝐵) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶)) |
31 | 26, 27, 29, 30 | syl3anc 1370 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 mod 𝐶) + 𝐵) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶)) |
32 | 8, 23, 31 | 3eqtrd 2782 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶)) |