Step |
Hyp |
Ref |
Expression |
1 |
|
nnre |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ ) |
2 |
|
reflcl |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ ) |
3 |
|
remulcl |
⊢ ( ( 𝑁 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ) |
4 |
1 2 3
|
syl2an |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ) |
5 |
4
|
3adant3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ) |
6 |
|
remulcl |
⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · 𝐴 ) ∈ ℝ ) |
7 |
1 6
|
sylan |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · 𝐴 ) ∈ ℝ ) |
8 |
|
reflcl |
⊢ ( ( 𝑁 · 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ∈ ℝ ) |
9 |
7 8
|
syl |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ) → ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ∈ ℝ ) |
10 |
9
|
3adant3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ∈ ℝ ) |
11 |
|
nnmulcl |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ∈ ℕ ) |
12 |
11
|
nnred |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ∈ ℝ ) |
13 |
12
|
3adant2 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ∈ ℝ ) |
14 |
|
nncn |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ ) |
15 |
|
nnne0 |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 ) |
16 |
14 15
|
jca |
⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) |
17 |
|
nncn |
⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ ) |
18 |
|
nnne0 |
⊢ ( 𝑀 ∈ ℕ → 𝑀 ≠ 0 ) |
19 |
17 18
|
jca |
⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ) |
20 |
|
mulne0 |
⊢ ( ( ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ∧ ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ) → ( 𝑁 · 𝑀 ) ≠ 0 ) |
21 |
16 19 20
|
syl2an |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ≠ 0 ) |
22 |
21
|
3adant2 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ≠ 0 ) |
23 |
5 13 22
|
redivcld |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ∈ ℝ ) |
24 |
|
reflcl |
⊢ ( ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ∈ ℝ → ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ∈ ℝ ) |
25 |
23 24
|
syl |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ∈ ℝ ) |
26 |
13 25
|
remulcld |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ∈ ℝ ) |
27 |
|
nnnn0 |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 ) |
28 |
|
flmulnn0 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ) |
29 |
27 28
|
sylan |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ) |
30 |
29
|
3adant3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ) |
31 |
5 10 26 30
|
lesub1dd |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) ≤ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) ) |
32 |
11
|
nnrpd |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝑀 ) ∈ ℝ+ ) |
33 |
|
modval |
⊢ ( ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝑁 · 𝑀 ) ∈ ℝ+ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) = ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) ) |
34 |
5 32 33
|
3imp3i2an |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) = ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) ) |
35 |
|
modval |
⊢ ( ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ∈ ℝ ∧ ( 𝑁 · 𝑀 ) ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) = ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) ) |
36 |
10 32 35
|
3imp3i2an |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) = ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) ) |
37 |
7
|
3adant3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( 𝑁 · 𝐴 ) ∈ ℝ ) |
38 |
|
fldiv |
⊢ ( ( ( 𝑁 · 𝐴 ) ∈ ℝ ∧ ( 𝑁 · 𝑀 ) ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) ) ) |
39 |
37 11 38
|
3imp3i2an |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) ) ) |
40 |
|
fldiv |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑀 ) ) = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) ) |
41 |
40
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑀 ) ) = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) ) |
42 |
2
|
recnd |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℂ ) |
43 |
|
divcan5 |
⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) = ( ( ⌊ ‘ 𝐴 ) / 𝑀 ) ) |
44 |
42 19 16 43
|
syl3an |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) = ( ( ⌊ ‘ 𝐴 ) / 𝑀 ) ) |
45 |
44
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( ⌊ ‘ 𝐴 ) / 𝑀 ) ) ) |
46 |
|
recn |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) |
47 |
|
divcan5 |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) = ( 𝐴 / 𝑀 ) ) |
48 |
46 19 16 47
|
syl3an |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) = ( 𝐴 / 𝑀 ) ) |
49 |
48
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) ) |
50 |
41 45 49
|
3eqtr4rd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) |
51 |
50
|
3comr |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑁 · 𝐴 ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) |
52 |
39 51
|
eqtrd |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) = ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) |
53 |
52
|
oveq2d |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) = ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) |
54 |
53
|
oveq2d |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) ) |
55 |
36 54
|
eqtrd |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) = ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) − ( ( 𝑁 · 𝑀 ) · ( ⌊ ‘ ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) / ( 𝑁 · 𝑀 ) ) ) ) ) ) |
56 |
31 34 55
|
3brtr4d |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) ≤ ( ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) mod ( 𝑁 · 𝑀 ) ) ) |