Proof of Theorem modmulnn
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnre 12273 | . . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 2 |  | reflcl 13836 | . . . . 5
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) | 
| 3 |  | remulcl 11240 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧
(⌊‘𝐴) ∈
ℝ) → (𝑁 ·
(⌊‘𝐴)) ∈
ℝ) | 
| 4 | 1, 2, 3 | syl2an 596 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) → (𝑁 · (⌊‘𝐴)) ∈
ℝ) | 
| 5 | 4 | 3adant3 1133 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · (⌊‘𝐴)) ∈
ℝ) | 
| 6 |  | remulcl 11240 | . . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑁 · 𝐴) ∈ ℝ) | 
| 7 | 1, 6 | sylan 580 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) → (𝑁 · 𝐴) ∈ ℝ) | 
| 8 |  | reflcl 13836 | . . . . 5
⊢ ((𝑁 · 𝐴) ∈ ℝ →
(⌊‘(𝑁 ·
𝐴)) ∈
ℝ) | 
| 9 | 7, 8 | syl 17 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) →
(⌊‘(𝑁 ·
𝐴)) ∈
ℝ) | 
| 10 | 9 | 3adant3 1133 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘(𝑁 ·
𝐴)) ∈
ℝ) | 
| 11 |  | nnmulcl 12290 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈ ℕ) | 
| 12 | 11 | nnred 12281 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈ ℝ) | 
| 13 | 12 | 3adant2 1132 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈ ℝ) | 
| 14 |  | nncn 12274 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 15 |  | nnne0 12300 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) | 
| 16 | 14, 15 | jca 511 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) | 
| 17 |  | nncn 12274 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) | 
| 18 |  | nnne0 12300 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) | 
| 19 | 17, 18 | jca 511 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0)) | 
| 20 |  | mulne0 11905 | . . . . . . . 8
⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0)) → (𝑁 · 𝑀) ≠ 0) | 
| 21 | 16, 19, 20 | syl2an 596 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ≠ 0) | 
| 22 | 21 | 3adant2 1132 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ≠ 0) | 
| 23 | 5, 13, 22 | redivcld 12095 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)) ∈ ℝ) | 
| 24 |  | reflcl 13836 | . . . . 5
⊢ (((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)) ∈ ℝ →
(⌊‘((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀))) ∈ ℝ) | 
| 25 | 23, 24 | syl 17 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀))) ∈ ℝ) | 
| 26 | 13, 25 | remulcld 11291 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) ∈ ℝ) | 
| 27 |  | nnnn0 12533 | . . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 28 |  | flmulnn0 13867 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℝ)
→ (𝑁 ·
(⌊‘𝐴)) ≤
(⌊‘(𝑁 ·
𝐴))) | 
| 29 | 27, 28 | sylan 580 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ) → (𝑁 · (⌊‘𝐴)) ≤ (⌊‘(𝑁 · 𝐴))) | 
| 30 | 29 | 3adant3 1133 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · (⌊‘𝐴)) ≤ (⌊‘(𝑁 · 𝐴))) | 
| 31 | 5, 10, 26, 30 | lesub1dd 11879 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀))))) ≤ ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) | 
| 32 | 11 | nnrpd 13075 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝑀) ∈
ℝ+) | 
| 33 |  | modval 13911 | . . 3
⊢ (((𝑁 · (⌊‘𝐴)) ∈ ℝ ∧ (𝑁 · 𝑀) ∈ ℝ+) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) = ((𝑁 · (⌊‘𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) | 
| 34 | 5, 32, 33 | 3imp3i2an 1346 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) = ((𝑁 · (⌊‘𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) | 
| 35 |  | modval 13911 | . . . 4
⊢
(((⌊‘(𝑁
· 𝐴)) ∈ ℝ
∧ (𝑁 · 𝑀) ∈ ℝ+)
→ ((⌊‘(𝑁
· 𝐴)) mod (𝑁 · 𝑀)) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀)))))) | 
| 36 | 10, 32, 35 | 3imp3i2an 1346 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
((⌊‘(𝑁 ·
𝐴)) mod (𝑁 · 𝑀)) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀)))))) | 
| 37 | 7 | 3adant3 1133 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → (𝑁 · 𝐴) ∈ ℝ) | 
| 38 |  | fldiv 13900 | . . . . . . 7
⊢ (((𝑁 · 𝐴) ∈ ℝ ∧ (𝑁 · 𝑀) ∈ ℕ) →
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · 𝐴) / (𝑁 · 𝑀)))) | 
| 39 | 37, 11, 38 | 3imp3i2an 1346 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · 𝐴) / (𝑁 · 𝑀)))) | 
| 40 |  | fldiv 13900 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑀)) = (⌊‘(𝐴 / 𝑀))) | 
| 41 | 40 | 3adant3 1133 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑀)) = (⌊‘(𝐴 / 𝑀))) | 
| 42 | 2 | recnd 11289 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℂ) | 
| 43 |  | divcan5 11969 | . . . . . . . . . 10
⊢
(((⌊‘𝐴)
∈ ℂ ∧ (𝑀
∈ ℂ ∧ 𝑀 ≠
0) ∧ (𝑁 ∈ ℂ
∧ 𝑁 ≠ 0)) →
((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀)) = ((⌊‘𝐴) / 𝑀)) | 
| 44 | 42, 19, 16, 43 | syl3an 1161 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)) = ((⌊‘𝐴) / 𝑀)) | 
| 45 | 44 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑁 ·
(⌊‘𝐴)) / (𝑁 · 𝑀))) = (⌊‘((⌊‘𝐴) / 𝑀))) | 
| 46 |  | recn 11245 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) | 
| 47 |  | divcan5 11969 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 ∈ ℂ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → ((𝑁 · 𝐴) / (𝑁 · 𝑀)) = (𝐴 / 𝑀)) | 
| 48 | 46, 19, 16, 47 | syl3an 1161 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝐴) / (𝑁 · 𝑀)) = (𝐴 / 𝑀)) | 
| 49 | 48 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑁 ·
𝐴) / (𝑁 · 𝑀))) = (⌊‘(𝐴 / 𝑀))) | 
| 50 | 41, 45, 49 | 3eqtr4rd 2788 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(⌊‘((𝑁 ·
𝐴) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) | 
| 51 | 50 | 3comr 1126 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((𝑁 ·
𝐴) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) | 
| 52 | 39, 51 | eqtrd 2777 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))) = (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))) | 
| 53 | 52 | oveq2d 7447 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀)))) = ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀))))) | 
| 54 | 53 | oveq2d 7447 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
((⌊‘(𝑁 ·
𝐴)) − ((𝑁 · 𝑀) ·
(⌊‘((⌊‘(𝑁 · 𝐴)) / (𝑁 · 𝑀))))) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) | 
| 55 | 36, 54 | eqtrd 2777 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) →
((⌊‘(𝑁 ·
𝐴)) mod (𝑁 · 𝑀)) = ((⌊‘(𝑁 · 𝐴)) − ((𝑁 · 𝑀) · (⌊‘((𝑁 · (⌊‘𝐴)) / (𝑁 · 𝑀)))))) | 
| 56 | 31, 34, 55 | 3brtr4d 5175 | 1
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) ≤ ((⌊‘(𝑁 · 𝐴)) mod (𝑁 · 𝑀))) |