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