Metamath Proof Explorer

Theorem modvalr

Description: The value of the modulo operation (multiplication in reversed order). (Contributed by Alexander van der Vekens, 14-Apr-2018)

Ref Expression
Assertion modvalr ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}={A}-⌊\frac{{A}}{{B}}⌋{B}$

Proof

Step Hyp Ref Expression
1 modval ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}={A}-{B}⌊\frac{{A}}{{B}}⌋$
2 rpcn ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℂ$
3 2 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in ℂ$
4 rerpdivcl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \frac{{A}}{{B}}\in ℝ$
5 reflcl ${⊢}\frac{{A}}{{B}}\in ℝ\to ⌊\frac{{A}}{{B}}⌋\in ℝ$
6 5 recnd ${⊢}\frac{{A}}{{B}}\in ℝ\to ⌊\frac{{A}}{{B}}⌋\in ℂ$
7 4 6 syl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ⌊\frac{{A}}{{B}}⌋\in ℂ$
8 3 7 mulcomd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}⌊\frac{{A}}{{B}}⌋=⌊\frac{{A}}{{B}}⌋{B}$
9 8 oveq2d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}-{B}⌊\frac{{A}}{{B}}⌋={A}-⌊\frac{{A}}{{B}}⌋{B}$
10 1 9 eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{B}={A}-⌊\frac{{A}}{{B}}⌋{B}$