Proof of Theorem modqdi
Step | Hyp | Ref
| Expression |
1 | | simp1l 1016 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 𝐴 ∈ ℚ) |
2 | | qcn 9586 |
. . . . 5
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) |
3 | 1, 2 | syl 14 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 𝐴 ∈ ℂ) |
4 | | simp2 993 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 𝐵 ∈ ℚ) |
5 | | qcn 9586 |
. . . . 5
⊢ (𝐵 ∈ ℚ → 𝐵 ∈
ℂ) |
6 | 4, 5 | syl 14 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 𝐵 ∈ ℂ) |
7 | | simp3l 1020 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 𝐶 ∈ ℚ) |
8 | | simp3r 1021 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 0 < 𝐶) |
9 | 8 | gt0ne0d 8424 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 𝐶 ≠ 0) |
10 | | qdivcl 9595 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℚ ∧ 𝐶 ∈ ℚ ∧ 𝐶 ≠ 0) → (𝐵 / 𝐶) ∈ ℚ) |
11 | 4, 7, 9, 10 | syl3anc 1233 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (𝐵 / 𝐶) ∈ ℚ) |
12 | 11 | flqcld 10226 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (⌊‘(𝐵 / 𝐶)) ∈ ℤ) |
13 | | zq 9578 |
. . . . . . 7
⊢
((⌊‘(𝐵 /
𝐶)) ∈ ℤ →
(⌊‘(𝐵 / 𝐶)) ∈
ℚ) |
14 | 12, 13 | syl 14 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (⌊‘(𝐵 / 𝐶)) ∈ ℚ) |
15 | | qmulcl 9589 |
. . . . . 6
⊢ ((𝐶 ∈ ℚ ∧
(⌊‘(𝐵 / 𝐶)) ∈ ℚ) → (𝐶 · (⌊‘(𝐵 / 𝐶))) ∈ ℚ) |
16 | 7, 14, 15 | syl2anc 409 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (𝐶 · (⌊‘(𝐵 / 𝐶))) ∈ ℚ) |
17 | | qcn 9586 |
. . . . 5
⊢ ((𝐶 · (⌊‘(𝐵 / 𝐶))) ∈ ℚ → (𝐶 · (⌊‘(𝐵 / 𝐶))) ∈ ℂ) |
18 | 16, 17 | syl 14 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (𝐶 · (⌊‘(𝐵 / 𝐶))) ∈ ℂ) |
19 | 3, 6, 18 | subdid 8326 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (𝐴 · (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) = ((𝐴 · 𝐵) − (𝐴 · (𝐶 · (⌊‘(𝐵 / 𝐶)))))) |
20 | | qcn 9586 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℚ → 𝐶 ∈
ℂ) |
21 | 7, 20 | syl 14 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 𝐶 ∈ ℂ) |
22 | | qre 9577 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℚ → 𝐶 ∈
ℝ) |
23 | 7, 22 | syl 14 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 𝐶 ∈ ℝ) |
24 | 23, 8 | gt0ap0d 8541 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 𝐶 # 0) |
25 | | qre 9577 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℝ) |
26 | 1, 25 | syl 14 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 𝐴 ∈ ℝ) |
27 | | simp1r 1017 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 0 < 𝐴) |
28 | 26, 27 | gt0ap0d 8541 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 𝐴 # 0) |
29 | 6, 21, 3, 24, 28 | divcanap5d 8727 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → ((𝐴 · 𝐵) / (𝐴 · 𝐶)) = (𝐵 / 𝐶)) |
30 | 29 | fveq2d 5498 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶))) = (⌊‘(𝐵 / 𝐶))) |
31 | 30 | oveq2d 5867 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶)))) = ((𝐴 · 𝐶) · (⌊‘(𝐵 / 𝐶)))) |
32 | 12 | zcnd 9328 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (⌊‘(𝐵 / 𝐶)) ∈ ℂ) |
33 | 3, 21, 32 | mulassd 7936 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) · (⌊‘(𝐵 / 𝐶))) = (𝐴 · (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
34 | 31, 33 | eqtr2d 2204 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (𝐴 · (𝐶 · (⌊‘(𝐵 / 𝐶)))) = ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶))))) |
35 | 34 | oveq2d 5867 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → ((𝐴 · 𝐵) − (𝐴 · (𝐶 · (⌊‘(𝐵 / 𝐶))))) = ((𝐴 · 𝐵) − ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶)))))) |
36 | 19, 35 | eqtrd 2203 |
. 2
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (𝐴 · (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) = ((𝐴 · 𝐵) − ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶)))))) |
37 | | modqval 10273 |
. . . 4
⊢ ((𝐵 ∈ ℚ ∧ 𝐶 ∈ ℚ ∧ 0 <
𝐶) → (𝐵 mod 𝐶) = (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
38 | 4, 7, 8, 37 | syl3anc 1233 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (𝐵 mod 𝐶) = (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
39 | 38 | oveq2d 5867 |
. 2
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (𝐴 · (𝐵 mod 𝐶)) = (𝐴 · (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶)))))) |
40 | | qmulcl 9589 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ) |
41 | 1, 4, 40 | syl2anc 409 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (𝐴 · 𝐵) ∈ ℚ) |
42 | | qmulcl 9589 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝐶 ∈ ℚ) → (𝐴 · 𝐶) ∈ ℚ) |
43 | 1, 7, 42 | syl2anc 409 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (𝐴 · 𝐶) ∈ ℚ) |
44 | 26, 23, 27, 8 | mulgt0d 8035 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → 0 < (𝐴 · 𝐶)) |
45 | | modqval 10273 |
. . 3
⊢ (((𝐴 · 𝐵) ∈ ℚ ∧ (𝐴 · 𝐶) ∈ ℚ ∧ 0 < (𝐴 · 𝐶)) → ((𝐴 · 𝐵) mod (𝐴 · 𝐶)) = ((𝐴 · 𝐵) − ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶)))))) |
46 | 41, 43, 44, 45 | syl3anc 1233 |
. 2
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → ((𝐴 · 𝐵) mod (𝐴 · 𝐶)) = ((𝐴 · 𝐵) − ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶)))))) |
47 | 36, 39, 46 | 3eqtr4d 2213 |
1
⊢ (((𝐴 ∈ ℚ ∧ 0 <
𝐴) ∧ 𝐵 ∈ ℚ ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (𝐴 · (𝐵 mod 𝐶)) = ((𝐴 · 𝐵) mod (𝐴 · 𝐶))) |