This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mullidd 
 |-  ( 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 )