Theorem modabs2

Description: Absorption law for modulo. (Contributed by NM, 29-Dec-2008)

	Ref	Expression
Assertion	modabs2	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(A\mathrm{mod}B\right)\mathrm{mod}B=A\mathrm{mod}B$$

Proof

Step	Hyp	Ref	Expression
1		rpre	$$⊢B\in {ℝ}^{+}\to B\in ℝ$$
2	1	leidd	$$⊢B\in {ℝ}^{+}\to B\le B$$
3	2	adantl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\le B$$
4		modabs	$$⊢\left(\left(A\in ℝ\wedge B\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\wedge B\le B\right)\to \left(A\mathrm{mod}B\right)\mathrm{mod}B=A\mathrm{mod}B$$
5	4	ex	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(B\le B\to \left(A\mathrm{mod}B\right)\mathrm{mod}B=A\mathrm{mod}B\right)$$
6	5	3anidm23	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(B\le B\to \left(A\mathrm{mod}B\right)\mathrm{mod}B=A\mathrm{mod}B\right)$$
7	3 6	mpd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(A\mathrm{mod}B\right)\mathrm{mod}B=A\mathrm{mod}B$$