Theorem addmodid

Description: The sum of a positive integer and a nonnegative integer less than the positive integer is equal to the nonnegative integer modulo the positive integer. (Contributed by Alexander van der Vekens, 30-Oct-2018) (Proof shortened by AV, 5-Jul-2020)

	Ref	Expression
Assertion	addmodid	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( ( M + A ) mod M ) = A )

Proof

Step	Hyp	Ref	Expression
1		nncn	|- ( M e. NN -> M e. CC )
2	1	mulid2d	|- ( M e. NN -> ( 1 x. M ) = M )
3	2	3ad2ant2	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( 1 x. M ) = M )
4	3	eqcomd	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> M = ( 1 x. M ) )
5	4	oveq1d	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( M + A ) = ( ( 1 x. M ) + A ) )
6	5	oveq1d	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( ( M + A ) mod M ) = ( ( ( 1 x. M ) + A ) mod M ) )
7		1zzd	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> 1 e. ZZ )
8		nnrp	|- ( M e. NN -> M e. RR+ )
9	8	3ad2ant2	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> M e. RR+ )
10		nn0re	|- ( A e. NN0 -> A e. RR )
11	10	rexrd	|- ( A e. NN0 -> A e. RR* )
12	11	3ad2ant1	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> A e. RR* )
13		nn0ge0	|- ( A e. NN0 -> 0 <_ A )
14	13	3ad2ant1	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> 0 <_ A )
15		simp3	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> A < M )
16		0xr	|- 0 e. RR*
17		nnre	|- ( M e. NN -> M e. RR )
18	17	rexrd	|- ( M e. NN -> M e. RR* )
19	18	3ad2ant2	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> M e. RR* )
20		elico1	|- ( ( 0 e. RR* /\ M e. RR* ) -> ( A e. ( 0 [,) M ) <-> ( A e. RR* /\ 0 <_ A /\ A < M ) ) )
21	16 19 20	sylancr	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( A e. ( 0 [,) M ) <-> ( A e. RR* /\ 0 <_ A /\ A < M ) ) )
22	12 14 15 21	mpbir3and	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> A e. ( 0 [,) M ) )
23		muladdmodid	|- ( ( 1 e. ZZ /\ M e. RR+ /\ A e. ( 0 [,) M ) ) -> ( ( ( 1 x. M ) + A ) mod M ) = A )
24	7 9 22 23	syl3anc	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( ( ( 1 x. M ) + A ) mod M ) = A )
25	6 24	eqtrd	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( ( M + A ) mod M ) = A )