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