Proof of Theorem modaddabs
| Step | Hyp | Ref
| Expression |
| 1 | | modcl 13913 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) ∈
ℝ) |
| 2 | 1 | recnd 11289 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) ∈
ℂ) |
| 3 | 2 | 3adant2 1132 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) ∈
ℂ) |
| 4 | | modcl 13913 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) ∈
ℝ) |
| 5 | 4 | recnd 11289 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) ∈
ℂ) |
| 6 | 5 | 3adant1 1131 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) ∈
ℂ) |
| 7 | 3, 6 | addcomd 11463 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) = ((𝐵 mod 𝐶) + (𝐴 mod 𝐶))) |
| 8 | 7 | oveq1d 7446 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) mod 𝐶) = (((𝐵 mod 𝐶) + (𝐴 mod 𝐶)) mod 𝐶)) |
| 9 | | simpl 482 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐵 ∈
ℝ) |
| 10 | 4, 9 | jca 511 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐵 mod 𝐶) ∈ ℝ ∧ 𝐵 ∈
ℝ)) |
| 11 | 10 | 3adant1 1131 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐵 mod 𝐶) ∈ ℝ ∧ 𝐵 ∈
ℝ)) |
| 12 | | simpr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℝ+) |
| 13 | 1, 12 | jca 511 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐶 ∈
ℝ+)) |
| 14 | 13 | 3adant2 1132 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐶 ∈
ℝ+)) |
| 15 | | modabs2 13945 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐵 mod 𝐶) mod 𝐶) = (𝐵 mod 𝐶)) |
| 16 | 15 | 3adant1 1131 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐵 mod 𝐶) mod 𝐶) = (𝐵 mod 𝐶)) |
| 17 | | modadd1 13948 |
. . . 4
⊢ ((((𝐵 mod 𝐶) ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐶 ∈ ℝ+) ∧ ((𝐵 mod 𝐶) mod 𝐶) = (𝐵 mod 𝐶)) → (((𝐵 mod 𝐶) + (𝐴 mod 𝐶)) mod 𝐶) = ((𝐵 + (𝐴 mod 𝐶)) mod 𝐶)) |
| 18 | 11, 14, 16, 17 | syl3anc 1373 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐵 mod 𝐶) + (𝐴 mod 𝐶)) mod 𝐶) = ((𝐵 + (𝐴 mod 𝐶)) mod 𝐶)) |
| 19 | | recn 11245 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
| 20 | 19 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
| 21 | 3, 20 | addcomd 11463 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) + 𝐵) = (𝐵 + (𝐴 mod 𝐶))) |
| 22 | 21 | oveq1d 7446 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 mod 𝐶) + 𝐵) mod 𝐶) = ((𝐵 + (𝐴 mod 𝐶)) mod 𝐶)) |
| 23 | 18, 22 | eqtr4d 2780 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐵 mod 𝐶) + (𝐴 mod 𝐶)) mod 𝐶) = (((𝐴 mod 𝐶) + 𝐵) mod 𝐶)) |
| 24 | | simpl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐴 ∈
ℝ) |
| 25 | 1, 24 | jca 511 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐴 ∈
ℝ)) |
| 26 | 25 | 3adant2 1132 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐴 ∈
ℝ)) |
| 27 | | 3simpc 1151 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+)) |
| 28 | | modabs2 13945 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) mod 𝐶) = (𝐴 mod 𝐶)) |
| 29 | 28 | 3adant2 1132 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) mod 𝐶) = (𝐴 mod 𝐶)) |
| 30 | | modadd1 13948 |
. . 3
⊢ ((((𝐴 mod 𝐶) ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) ∧ ((𝐴 mod 𝐶) mod 𝐶) = (𝐴 mod 𝐶)) → (((𝐴 mod 𝐶) + 𝐵) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶)) |
| 31 | 26, 27, 29, 30 | syl3anc 1373 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 mod 𝐶) + 𝐵) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶)) |
| 32 | 8, 23, 31 | 3eqtrd 2781 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶)) |