Proof of Theorem modqaddmulmod
Step | Hyp | Ref
| Expression |
1 | | simpl1 941 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → 𝐴 ∈
ℚ) |
2 | | qcn 8719 |
. . . . 5
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) |
3 | 1, 2 | syl 14 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → 𝐴 ∈
ℂ) |
4 | | simpl2 942 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → 𝐵 ∈
ℚ) |
5 | | simprl 497 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → 𝑀 ∈
ℚ) |
6 | | simprr 498 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → 0 < 𝑀) |
7 | 4, 5, 6 | modqcld 9330 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → (𝐵 mod 𝑀) ∈ ℚ) |
8 | | simpl3 943 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → 𝐶 ∈
ℤ) |
9 | | zq 8711 |
. . . . . . 7
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
ℚ) |
10 | 8, 9 | syl 14 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → 𝐶 ∈
ℚ) |
11 | | qmulcl 8722 |
. . . . . 6
⊢ (((𝐵 mod 𝑀) ∈ ℚ ∧ 𝐶 ∈ ℚ) → ((𝐵 mod 𝑀) · 𝐶) ∈ ℚ) |
12 | 7, 10, 11 | syl2anc 403 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → ((𝐵 mod 𝑀) · 𝐶) ∈ ℚ) |
13 | | qcn 8719 |
. . . . 5
⊢ (((𝐵 mod 𝑀) · 𝐶) ∈ ℚ → ((𝐵 mod 𝑀) · 𝐶) ∈ ℂ) |
14 | 12, 13 | syl 14 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → ((𝐵 mod 𝑀) · 𝐶) ∈ ℂ) |
15 | 3, 14 | addcomd 7259 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → (𝐴 + ((𝐵 mod 𝑀) · 𝐶)) = (((𝐵 mod 𝑀) · 𝐶) + 𝐴)) |
16 | 15 | oveq1d 5547 |
. 2
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → ((𝐴 + ((𝐵 mod 𝑀) · 𝐶)) mod 𝑀) = ((((𝐵 mod 𝑀) · 𝐶) + 𝐴) mod 𝑀)) |
17 | 9 | 3ad2ant3 961 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) → 𝐶 ∈
ℚ) |
18 | 17 | adantr 270 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → 𝐶 ∈
ℚ) |
19 | 7, 18, 11 | syl2anc 403 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → ((𝐵 mod 𝑀) · 𝐶) ∈ ℚ) |
20 | | qmulcl 8722 |
. . . . 5
⊢ ((𝐵 ∈ ℚ ∧ 𝐶 ∈ ℚ) → (𝐵 · 𝐶) ∈ ℚ) |
21 | 4, 18, 20 | syl2anc 403 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → (𝐵 · 𝐶) ∈ ℚ) |
22 | 21, 5, 6 | modqcld 9330 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → ((𝐵 · 𝐶) mod 𝑀) ∈ ℚ) |
23 | | modqmulmod 9391 |
. . . . 5
⊢ (((𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → (((𝐵 mod 𝑀) · 𝐶) mod 𝑀) = ((𝐵 · 𝐶) mod 𝑀)) |
24 | 23 | 3adantl1 1094 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → (((𝐵 mod 𝑀) · 𝐶) mod 𝑀) = ((𝐵 · 𝐶) mod 𝑀)) |
25 | | modqabs2 9360 |
. . . . 5
⊢ (((𝐵 · 𝐶) ∈ ℚ ∧ 𝑀 ∈ ℚ ∧ 0 < 𝑀) → (((𝐵 · 𝐶) mod 𝑀) mod 𝑀) = ((𝐵 · 𝐶) mod 𝑀)) |
26 | 21, 5, 6, 25 | syl3anc 1169 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → (((𝐵 · 𝐶) mod 𝑀) mod 𝑀) = ((𝐵 · 𝐶) mod 𝑀)) |
27 | 24, 26 | eqtr4d 2116 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → (((𝐵 mod 𝑀) · 𝐶) mod 𝑀) = (((𝐵 · 𝐶) mod 𝑀) mod 𝑀)) |
28 | 19, 22, 1, 5, 6, 27 | modqadd1 9363 |
. 2
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → ((((𝐵 mod 𝑀) · 𝐶) + 𝐴) mod 𝑀) = ((((𝐵 · 𝐶) mod 𝑀) + 𝐴) mod 𝑀)) |
29 | | modqaddmod 9365 |
. . . 4
⊢ ((((𝐵 · 𝐶) ∈ ℚ ∧ 𝐴 ∈ ℚ) ∧ (𝑀 ∈ ℚ ∧ 0 < 𝑀)) → ((((𝐵 · 𝐶) mod 𝑀) + 𝐴) mod 𝑀) = (((𝐵 · 𝐶) + 𝐴) mod 𝑀)) |
30 | 21, 1, 5, 6, 29 | syl22anc 1170 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → ((((𝐵 · 𝐶) mod 𝑀) + 𝐴) mod 𝑀) = (((𝐵 · 𝐶) + 𝐴) mod 𝑀)) |
31 | | qcn 8719 |
. . . . . 6
⊢ ((𝐵 · 𝐶) ∈ ℚ → (𝐵 · 𝐶) ∈ ℂ) |
32 | 21, 31 | syl 14 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → (𝐵 · 𝐶) ∈ ℂ) |
33 | 32, 3 | addcomd 7259 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → ((𝐵 · 𝐶) + 𝐴) = (𝐴 + (𝐵 · 𝐶))) |
34 | 33 | oveq1d 5547 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → (((𝐵 · 𝐶) + 𝐴) mod 𝑀) = ((𝐴 + (𝐵 · 𝐶)) mod 𝑀)) |
35 | 30, 34 | eqtrd 2113 |
. 2
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → ((((𝐵 · 𝐶) mod 𝑀) + 𝐴) mod 𝑀) = ((𝐴 + (𝐵 · 𝐶)) mod 𝑀)) |
36 | 16, 28, 35 | 3eqtrd 2117 |
1
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℤ) ∧ (𝑀 ∈ ℚ ∧ 0 <
𝑀)) → ((𝐴 + ((𝐵 mod 𝑀) · 𝐶)) mod 𝑀) = ((𝐴 + (𝐵 · 𝐶)) mod 𝑀)) |