Proof of Theorem modqadd1
Step | Hyp | Ref
| Expression |
1 | | modqadd1.ab |
. 2
⊢ (𝜑 → (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) |
2 | | modqadd1.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℚ) |
3 | | modqadd1.dq |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℚ) |
4 | | modqadd1.dgt0 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝐷) |
5 | | modqval 10269 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝐷 ∈ ℚ ∧ 0 <
𝐷) → (𝐴 mod 𝐷) = (𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷))))) |
6 | 2, 3, 4, 5 | syl3anc 1233 |
. . . . . 6
⊢ (𝜑 → (𝐴 mod 𝐷) = (𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷))))) |
7 | | modqadd1.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℚ) |
8 | | modqval 10269 |
. . . . . . 7
⊢ ((𝐵 ∈ ℚ ∧ 𝐷 ∈ ℚ ∧ 0 <
𝐷) → (𝐵 mod 𝐷) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷))))) |
9 | 7, 3, 4, 8 | syl3anc 1233 |
. . . . . 6
⊢ (𝜑 → (𝐵 mod 𝐷) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷))))) |
10 | 6, 9 | eqeq12d 2185 |
. . . . 5
⊢ (𝜑 → ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) ↔ (𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))))) |
11 | | oveq1 5858 |
. . . . 5
⊢ ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = (𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) → ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶)) |
12 | 10, 11 | syl6bi 162 |
. . . 4
⊢ (𝜑 → ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) → ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶))) |
13 | | qcn 9582 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) |
14 | 2, 13 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
15 | | modqadd1.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℚ) |
16 | | qcn 9582 |
. . . . . . 7
⊢ (𝐶 ∈ ℚ → 𝐶 ∈
ℂ) |
17 | 15, 16 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
18 | | qcn 9582 |
. . . . . . . 8
⊢ (𝐷 ∈ ℚ → 𝐷 ∈
ℂ) |
19 | 3, 18 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℂ) |
20 | 4 | gt0ne0d 8420 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ≠ 0) |
21 | | qdivcl 9591 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℚ ∧ 𝐷 ∈ ℚ ∧ 𝐷 ≠ 0) → (𝐴 / 𝐷) ∈ ℚ) |
22 | 2, 3, 20, 21 | syl3anc 1233 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / 𝐷) ∈ ℚ) |
23 | 22 | flqcld 10222 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝐴 / 𝐷)) ∈ ℤ) |
24 | 23 | zcnd 9324 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝐴 / 𝐷)) ∈ ℂ) |
25 | 19, 24 | mulcld 7929 |
. . . . . 6
⊢ (𝜑 → (𝐷 · (⌊‘(𝐴 / 𝐷))) ∈ ℂ) |
26 | 14, 17, 25 | addsubd 8240 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶)) |
27 | | qcn 9582 |
. . . . . . 7
⊢ (𝐵 ∈ ℚ → 𝐵 ∈
ℂ) |
28 | 7, 27 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) |
29 | | qdivcl 9591 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℚ ∧ 𝐷 ∈ ℚ ∧ 𝐷 ≠ 0) → (𝐵 / 𝐷) ∈ ℚ) |
30 | 7, 3, 20, 29 | syl3anc 1233 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 / 𝐷) ∈ ℚ) |
31 | 30 | flqcld 10222 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝐵 / 𝐷)) ∈ ℤ) |
32 | 31 | zcnd 9324 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝐵 / 𝐷)) ∈ ℂ) |
33 | 19, 32 | mulcld 7929 |
. . . . . 6
⊢ (𝜑 → (𝐷 · (⌊‘(𝐵 / 𝐷))) ∈ ℂ) |
34 | 28, 17, 33 | addsubd 8240 |
. . . . 5
⊢ (𝜑 → ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶)) |
35 | 26, 34 | eqeq12d 2185 |
. . . 4
⊢ (𝜑 → (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) ↔ ((𝐴 − (𝐷 · (⌊‘(𝐴 / 𝐷)))) + 𝐶) = ((𝐵 − (𝐷 · (⌊‘(𝐵 / 𝐷)))) + 𝐶))) |
36 | 12, 35 | sylibrd 168 |
. . 3
⊢ (𝜑 → ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) → ((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))))) |
37 | | oveq1 5858 |
. . . 4
⊢ (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) → (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷)) |
38 | | qaddcl 9583 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝐶 ∈ ℚ) → (𝐴 + 𝐶) ∈ ℚ) |
39 | 2, 15, 38 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 𝐶) ∈ ℚ) |
40 | | modqcyc2 10305 |
. . . . . 6
⊢ ((((𝐴 + 𝐶) ∈ ℚ ∧ (⌊‘(𝐴 / 𝐷)) ∈ ℤ) ∧ (𝐷 ∈ ℚ ∧ 0 < 𝐷)) → (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = ((𝐴 + 𝐶) mod 𝐷)) |
41 | 39, 23, 3, 4, 40 | syl22anc 1234 |
. . . . 5
⊢ (𝜑 → (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = ((𝐴 + 𝐶) mod 𝐷)) |
42 | | qaddcl 9583 |
. . . . . . 7
⊢ ((𝐵 ∈ ℚ ∧ 𝐶 ∈ ℚ) → (𝐵 + 𝐶) ∈ ℚ) |
43 | 7, 15, 42 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → (𝐵 + 𝐶) ∈ ℚ) |
44 | | modqcyc2 10305 |
. . . . . 6
⊢ ((((𝐵 + 𝐶) ∈ ℚ ∧ (⌊‘(𝐵 / 𝐷)) ∈ ℤ) ∧ (𝐷 ∈ ℚ ∧ 0 < 𝐷)) → (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |
45 | 43, 31, 3, 4, 44 | syl22anc 1234 |
. . . . 5
⊢ (𝜑 → (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |
46 | 41, 45 | eqeq12d 2185 |
. . . 4
⊢ (𝜑 → ((((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) mod 𝐷) = (((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) mod 𝐷) ↔ ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))) |
47 | 37, 46 | syl5ib 153 |
. . 3
⊢ (𝜑 → (((𝐴 + 𝐶) − (𝐷 · (⌊‘(𝐴 / 𝐷)))) = ((𝐵 + 𝐶) − (𝐷 · (⌊‘(𝐵 / 𝐷)))) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))) |
48 | 36, 47 | syld 45 |
. 2
⊢ (𝜑 → ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))) |
49 | 1, 48 | mpd 13 |
1
⊢ (𝜑 → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |