Proof of Theorem modmulnn
Step | Hyp | Ref
| Expression |
1 | | nnre 11027 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
2 | | reflcl 12597 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
3 | | remulcl 10021 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧
(⌊‘𝐴) ∈
ℝ) → (𝑁 ·
(⌊‘𝐴)) ∈
ℝ) |
4 | 1, 2, 3 | syl2an 494 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) → (𝑁 · (⌊‘𝐴)) ∈
ℝ) |
5 | 4 | 3adant3 1081 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · (⌊‘𝐴)) ∈
ℝ) |
6 | | remulcl 10021 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑁 · 𝐴) ∈ ℝ) |
7 | 1, 6 | sylan 488 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) → (𝑁 · 𝐴) ∈ ℝ) |
8 | | reflcl 12597 |
. . . . 5
⊢ ((𝑁 · 𝐴) ∈ ℝ →
(⌊‘(𝑁 ·
𝐴)) ∈
ℝ) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) →
(⌊‘(𝑁 ·
𝐴)) ∈
ℝ) |
10 | 9 | 3adant3 1081 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘(𝑁 ·
𝐴)) ∈
ℝ) |
11 | | nnmulcl 11043 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈ ℕ) |
12 | 11 | nnred 11035 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈ ℝ) |
13 | 12 | 3adant2 1080 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈ ℝ) |
14 | | nncn 11028 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
15 | | nnne0 11053 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
16 | 14, 15 | jca 554 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
17 | | nncn 11028 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
18 | | nnne0 11053 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) |
19 | 17, 18 | jca 554 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0)) |
20 | | mulne0 10669 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0)) → (𝑁 · 𝑀) ≠ 0) |
21 | 16, 19, 20 | syl2an 494 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ≠ 0) |
22 | 21 | 3adant2 1080 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ≠ 0) |
23 | 5, 13, 22 | redivcld 10853 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)) ∈ ℝ) |
24 | | reflcl 12597 |
. . . . 5
⊢ (((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)) ∈ ℝ →
(⌊‘((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀))) ∈ ℝ) |
25 | 23, 24 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀))) ∈ ℝ) |
26 | 13, 25 | remulcld 10070 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) ∈ ℝ) |
27 | | nnnn0 11299 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
28 | | flmulnn0 12628 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℝ)
→ (𝑁 ·
(⌊‘𝐴)) ≤
(⌊‘(𝑁 ·
𝐴))) |
29 | 27, 28 | sylan 488 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) → (𝑁 · (⌊‘𝐴)) ≤ (⌊‘(𝑁 · 𝐴))) |
30 | 29 | 3adant3 1081 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · (⌊‘𝐴)) ≤ (⌊‘(𝑁 · 𝐴))) |
31 | 5, 10, 26, 30 | lesub1dd 10643 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀))))) ≤ ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) |
32 | 11 | nnrpd 11870 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈
ℝ+) |
33 | 32 | 3adant2 1080 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈
ℝ+) |
34 | | modval 12670 |
. . 3
⊢ (((𝑁 · (⌊‘𝐴)) ∈ ℝ ∧ (𝑁 · 𝑀) ∈ ℝ+) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) = ((𝑁 · (⌊‘𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) |
35 | 5, 33, 34 | syl2anc 693 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) = ((𝑁 · (⌊‘𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) |
36 | | modval 12670 |
. . . 4
⊢
(((⌊‘(𝑁
· 𝐴)) ∈ ℝ
∧ (𝑁 · 𝑀) ∈ ℝ+)
→ ((⌊‘(𝑁
· 𝐴)) mod (𝑁 · 𝑀)) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀)))))) |
37 | 10, 33, 36 | syl2anc 693 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
((⌊‘(𝑁 ·
𝐴)) mod (𝑁 · 𝑀)) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀)))))) |
38 | 7 | 3adant3 1081 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝐴) ∈ ℝ) |
39 | 11 | 3adant2 1080 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈ ℕ) |
40 | | fldiv 12659 |
. . . . . . 7
⊢ (((𝑁 · 𝐴) ∈ ℝ ∧ (𝑁 · 𝑀) ∈ ℕ) →
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · 𝐴) / (𝑁 · 𝑀)))) |
41 | 38, 39, 40 | syl2anc 693 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · 𝐴) / (𝑁 · 𝑀)))) |
42 | | fldiv 12659 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑀)) = (⌊‘(𝐴 / 𝑀))) |
43 | 42 | 3adant3 1081 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑀)) = (⌊‘(𝐴 / 𝑀))) |
44 | 2 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℂ) |
45 | | divcan5 10727 |
. . . . . . . . . 10
⊢
(((⌊‘𝐴)
∈ ℂ ∧ (𝑀
∈ ℂ ∧ 𝑀 ≠
0) ∧ (𝑁 ∈ ℂ
∧ 𝑁 ≠ 0)) →
((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀)) = ((⌊‘𝐴) / 𝑀)) |
46 | 44, 19, 16, 45 | syl3an 1368 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)) = ((⌊‘𝐴) / 𝑀)) |
47 | 46 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀))) = (⌊‘((⌊‘𝐴) / 𝑀))) |
48 | | recn 10026 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
49 | | divcan5 10727 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → ((𝑁 · 𝐴) / (𝑁 · 𝑀)) = (𝐴 / 𝑀)) |
50 | 48, 19, 16, 49 | syl3an 1368 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝐴) / (𝑁 · 𝑀)) = (𝐴 / 𝑀)) |
51 | 50 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑁 ·
𝐴) / (𝑁 · 𝑀))) = (⌊‘(𝐴 / 𝑀))) |
52 | 43, 47, 51 | 3eqtr4rd 2667 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑁 ·
𝐴) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) |
53 | 52 | 3comr 1273 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((𝑁 ·
𝐴) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) |
54 | 41, 53 | eqtrd 2656 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) |
55 | 54 | oveq2d 6666 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀)))) = ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀))))) |
56 | 55 | oveq2d 6666 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
((⌊‘(𝑁 ·
𝐴)) − ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))))) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) |
57 | 37, 56 | eqtrd 2656 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
((⌊‘(𝑁 ·
𝐴)) mod (𝑁 · 𝑀)) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) |
58 | 31, 35, 57 | 3brtr4d 4685 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) ≤ ((⌊‘(𝑁 · 𝐴)) mod (𝑁 · 𝑀))) |