Proof of Theorem modmulnn
Step | Hyp | Ref
| Expression |
1 | | nnre 10904 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
2 | | reflcl 12459 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
3 | | remulcl 9900 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧
(⌊‘𝐴) ∈
ℝ) → (𝑁 ·
(⌊‘𝐴)) ∈
ℝ) |
4 | 1, 2, 3 | syl2an 493 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) → (𝑁 · (⌊‘𝐴)) ∈
ℝ) |
5 | 4 | 3adant3 1074 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · (⌊‘𝐴)) ∈
ℝ) |
6 | | remulcl 9900 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑁 · 𝐴) ∈ ℝ) |
7 | 1, 6 | sylan 487 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) → (𝑁 · 𝐴) ∈ ℝ) |
8 | | reflcl 12459 |
. . . . 5
⊢ ((𝑁 · 𝐴) ∈ ℝ →
(⌊‘(𝑁 ·
𝐴)) ∈
ℝ) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) →
(⌊‘(𝑁 ·
𝐴)) ∈
ℝ) |
10 | 9 | 3adant3 1074 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘(𝑁 ·
𝐴)) ∈
ℝ) |
11 | | nnmulcl 10920 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈ ℕ) |
12 | 11 | nnred 10912 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈ ℝ) |
13 | 12 | 3adant2 1073 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈ ℝ) |
14 | | nncn 10905 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
15 | | nnne0 10930 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
16 | 14, 15 | jca 553 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
17 | | nncn 10905 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
18 | | nnne0 10930 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) |
19 | 17, 18 | jca 553 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0)) |
20 | | mulne0 10548 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0)) → (𝑁 · 𝑀) ≠ 0) |
21 | 16, 19, 20 | syl2an 493 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ≠ 0) |
22 | 21 | 3adant2 1073 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ≠ 0) |
23 | 5, 13, 22 | redivcld 10732 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)) ∈ ℝ) |
24 | | reflcl 12459 |
. . . . 5
⊢ (((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)) ∈ ℝ →
(⌊‘((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀))) ∈ ℝ) |
25 | 23, 24 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀))) ∈ ℝ) |
26 | 13, 25 | remulcld 9949 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) ∈ ℝ) |
27 | | nnnn0 11176 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
28 | | flmulnn0 12490 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℝ)
→ (𝑁 ·
(⌊‘𝐴)) ≤
(⌊‘(𝑁 ·
𝐴))) |
29 | 27, 28 | sylan 487 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) → (𝑁 · (⌊‘𝐴)) ≤ (⌊‘(𝑁 · 𝐴))) |
30 | 29 | 3adant3 1074 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · (⌊‘𝐴)) ≤ (⌊‘(𝑁 · 𝐴))) |
31 | 5, 10, 26, 30 | lesub1dd 10522 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀))))) ≤ ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) |
32 | 11 | nnrpd 11746 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈
ℝ+) |
33 | 32 | 3adant2 1073 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈
ℝ+) |
34 | | modval 12532 |
. . 3
⊢ (((𝑁 · (⌊‘𝐴)) ∈ ℝ ∧ (𝑁 · 𝑀) ∈ ℝ+) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) = ((𝑁 · (⌊‘𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) |
35 | 5, 33, 34 | syl2anc 691 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) = ((𝑁 · (⌊‘𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) |
36 | | modval 12532 |
. . . 4
⊢
(((⌊‘(𝑁
· 𝐴)) ∈ ℝ
∧ (𝑁 · 𝑀) ∈ ℝ+)
→ ((⌊‘(𝑁
· 𝐴)) mod (𝑁 · 𝑀)) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀)))))) |
37 | 10, 33, 36 | syl2anc 691 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
((⌊‘(𝑁 ·
𝐴)) mod (𝑁 · 𝑀)) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀)))))) |
38 | 7 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝐴) ∈ ℝ) |
39 | 11 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈ ℕ) |
40 | | fldiv 12521 |
. . . . . . 7
⊢ (((𝑁 · 𝐴) ∈ ℝ ∧ (𝑁 · 𝑀) ∈ ℕ) →
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · 𝐴) / (𝑁 · 𝑀)))) |
41 | 38, 39, 40 | syl2anc 691 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · 𝐴) / (𝑁 · 𝑀)))) |
42 | | fldiv 12521 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑀)) = (⌊‘(𝐴 / 𝑀))) |
43 | 42 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑀)) = (⌊‘(𝐴 / 𝑀))) |
44 | 2 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℂ) |
45 | | divcan5 10606 |
. . . . . . . . . 10
⊢
(((⌊‘𝐴)
∈ ℂ ∧ (𝑀
∈ ℂ ∧ 𝑀 ≠
0) ∧ (𝑁 ∈ ℂ
∧ 𝑁 ≠ 0)) →
((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀)) = ((⌊‘𝐴) / 𝑀)) |
46 | 44, 19, 16, 45 | syl3an 1360 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)) = ((⌊‘𝐴) / 𝑀)) |
47 | 46 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀))) = (⌊‘((⌊‘𝐴) / 𝑀))) |
48 | | recn 9905 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
49 | | divcan5 10606 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → ((𝑁 · 𝐴) / (𝑁 · 𝑀)) = (𝐴 / 𝑀)) |
50 | 48, 19, 16, 49 | syl3an 1360 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝐴) / (𝑁 · 𝑀)) = (𝐴 / 𝑀)) |
51 | 50 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑁 ·
𝐴) / (𝑁 · 𝑀))) = (⌊‘(𝐴 / 𝑀))) |
52 | 43, 47, 51 | 3eqtr4rd 2655 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑁 ·
𝐴) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) |
53 | 52 | 3comr 1265 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((𝑁 ·
𝐴) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) |
54 | 41, 53 | eqtrd 2644 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) |
55 | 54 | oveq2d 6565 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀)))) = ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀))))) |
56 | 55 | oveq2d 6565 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
((⌊‘(𝑁 ·
𝐴)) − ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))))) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) |
57 | 37, 56 | eqtrd 2644 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
((⌊‘(𝑁 ·
𝐴)) mod (𝑁 · 𝑀)) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) |
58 | 31, 35, 57 | 3brtr4d 4615 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) ≤ ((⌊‘(𝑁 · 𝐴)) mod (𝑁 · 𝑀))) |