Step |
Hyp |
Ref |
Expression |
1 |
|
rpcn |
⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ ) |
2 |
1
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ∈ ℂ ) |
3 |
|
recn |
⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ ) |
4 |
3
|
3ad2ant2 |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ∈ ℂ ) |
5 |
|
rpre |
⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ℝ ) |
6 |
5
|
adantl |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ ) |
7 |
|
refldivcl |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℝ ) |
8 |
6 7
|
remulcld |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ∈ ℝ ) |
9 |
8
|
recnd |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ∈ ℂ ) |
10 |
9
|
3adant1 |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ∈ ℂ ) |
11 |
2 4 10
|
subdid |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) = ( ( 𝐴 · 𝐵 ) − ( 𝐴 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) ) |
12 |
|
rpcnne0 |
⊢ ( 𝐶 ∈ ℝ+ → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) |
13 |
12
|
3ad2ant3 |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) |
14 |
|
rpcnne0 |
⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) |
15 |
14
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) |
16 |
|
divcan5 |
⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) = ( 𝐵 / 𝐶 ) ) |
17 |
4 13 15 16
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) = ( 𝐵 / 𝐶 ) ) |
18 |
17
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) = ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) |
19 |
18
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) = ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) |
20 |
|
rpcn |
⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ℂ ) |
21 |
20
|
3ad2ant3 |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℂ ) |
22 |
|
rerpdivcl |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 / 𝐶 ) ∈ ℝ ) |
23 |
|
reflcl |
⊢ ( ( 𝐵 / 𝐶 ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℝ ) |
24 |
23
|
recnd |
⊢ ( ( 𝐵 / 𝐶 ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℂ ) |
25 |
22 24
|
syl |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℂ ) |
26 |
25
|
3adant1 |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℂ ) |
27 |
2 21 26
|
mulassd |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) = ( 𝐴 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) |
28 |
19 27
|
eqtr2d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) = ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) ) |
29 |
28
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 · 𝐵 ) − ( 𝐴 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) = ( ( 𝐴 · 𝐵 ) − ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) ) ) |
30 |
11 29
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) = ( ( 𝐴 · 𝐵 ) − ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) ) ) |
31 |
|
modval |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) = ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) |
32 |
31
|
3adant1 |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) = ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) |
33 |
32
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐵 mod 𝐶 ) ) = ( 𝐴 · ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) ) |
34 |
|
rpre |
⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ ) |
35 |
|
remulcl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ ) |
36 |
34 35
|
sylan |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ ) |
37 |
36
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · 𝐵 ) ∈ ℝ ) |
38 |
|
rpmulcl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · 𝐶 ) ∈ ℝ+ ) |
39 |
|
modval |
⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ ( 𝐴 · 𝐶 ) ∈ ℝ+ ) → ( ( 𝐴 · 𝐵 ) mod ( 𝐴 · 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) − ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) ) ) |
40 |
37 38 39
|
3imp3i2an |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 · 𝐵 ) mod ( 𝐴 · 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) − ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) ) ) |
41 |
30 33 40
|
3eqtr4d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐵 mod 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) mod ( 𝐴 · 𝐶 ) ) ) |