Metamath Proof Explorer

Theorem modmuladd

Description: Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021)

Ref Expression
Assertion modmuladd 
|- ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) -> ( ( A mod M ) = B <-> E. k e. ZZ A = ( ( k x. M ) + B ) ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( A e. ZZ -> A e. RR )
2 1 adantr 
 |-  ( ( A e. ZZ /\ M e. RR+ ) -> A e. RR )
3 rpre 
 |-  ( M e. RR+ -> M e. RR )
4 3 adantl 
 |-  ( ( A e. ZZ /\ M e. RR+ ) -> M e. RR )
5 rpne0 
 |-  ( M e. RR+ -> M =/= 0 )
6 5 adantl 
 |-  ( ( A e. ZZ /\ M e. RR+ ) -> M =/= 0 )
7 2 4 6 redivcld 
 |-  ( ( A e. ZZ /\ M e. RR+ ) -> ( A / M ) e. RR )
8 7 flcld 
 |-  ( ( A e. ZZ /\ M e. RR+ ) -> ( |_ ` ( A / M ) ) e. ZZ )
9 8 3adant2 
 |-  ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) -> ( |_ ` ( A / M ) ) e. ZZ )
10 oveq1 
 |-  ( k = ( |_ ` ( A / M ) ) -> ( k x. M ) = ( ( |_ ` ( A / M ) ) x. M ) )
11 10 oveq1d 
 |-  ( k = ( |_ ` ( A / M ) ) -> ( ( k x. M ) + ( A mod M ) ) = ( ( ( |_ ` ( A / M ) ) x. M ) + ( A mod M ) ) )
12 11 eqeq2d 
 |-  ( k = ( |_ ` ( A / M ) ) -> ( A = ( ( k x. M ) + ( A mod M ) ) <-> A = ( ( ( |_ ` ( A / M ) ) x. M ) + ( A mod M ) ) ) )
13 12 adantl 
 |-  ( ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) /\ k = ( |_ ` ( A / M ) ) ) -> ( A = ( ( k x. M ) + ( A mod M ) ) <-> A = ( ( ( |_ ` ( A / M ) ) x. M ) + ( A mod M ) ) ) )
14 1 anim1i 
 |-  ( ( A e. ZZ /\ M e. RR+ ) -> ( A e. RR /\ M e. RR+ ) )
15 14 3adant2 
 |-  ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) -> ( A e. RR /\ M e. RR+ ) )
16 flpmodeq 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( ( ( |_ ` ( A / M ) ) x. M ) + ( A mod M ) ) = A )
17 15 16 syl 
 |-  ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) -> ( ( ( |_ ` ( A / M ) ) x. M ) + ( A mod M ) ) = A )
18 17 eqcomd 
 |-  ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) -> A = ( ( ( |_ ` ( A / M ) ) x. M ) + ( A mod M ) ) )
19 9 13 18 rspcedvd 
 |-  ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) -> E. k e. ZZ A = ( ( k x. M ) + ( A mod M ) ) )
20 oveq2 
 |-  ( B = ( A mod M ) -> ( ( k x. M ) + B ) = ( ( k x. M ) + ( A mod M ) ) )
21 20 eqeq2d 
 |-  ( B = ( A mod M ) -> ( A = ( ( k x. M ) + B ) <-> A = ( ( k x. M ) + ( A mod M ) ) ) )
22 21 eqcoms 
 |-  ( ( A mod M ) = B -> ( A = ( ( k x. M ) + B ) <-> A = ( ( k x. M ) + ( A mod M ) ) ) )
23 22 rexbidv 
 |-  ( ( A mod M ) = B -> ( E. k e. ZZ A = ( ( k x. M ) + B ) <-> E. k e. ZZ A = ( ( k x. M ) + ( A mod M ) ) ) )
24 19 23 syl5ibrcom 
 |-  ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) -> ( ( A mod M ) = B -> E. k e. ZZ A = ( ( k x. M ) + B ) ) )
25 oveq1 
 |-  ( A = ( ( k x. M ) + B ) -> ( A mod M ) = ( ( ( k x. M ) + B ) mod M ) )
26 simpr 
 |-  ( ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) /\ k e. ZZ ) -> k e. ZZ )
27 simpl3 
 |-  ( ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) /\ k e. ZZ ) -> M e. RR+ )
28 simpl2 
 |-  ( ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) /\ k e. ZZ ) -> B e. ( 0 [,) M ) )
29 muladdmodid 
 |-  ( ( k e. ZZ /\ M e. RR+ /\ B e. ( 0 [,) M ) ) -> ( ( ( k x. M ) + B ) mod M ) = B )
30 26 27 28 29 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) /\ k e. ZZ ) -> ( ( ( k x. M ) + B ) mod M ) = B )
31 25 30 sylan9eqr 
 |-  ( ( ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) /\ k e. ZZ ) /\ A = ( ( k x. M ) + B ) ) -> ( A mod M ) = B )
32 31 rexlimdva2 
 |-  ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) -> ( E. k e. ZZ A = ( ( k x. M ) + B ) -> ( A mod M ) = B ) )
33 24 32 impbid 
 |-  ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) -> ( ( A mod M ) = B <-> E. k e. ZZ A = ( ( k x. M ) + B ) ) )