Metamath Proof Explorer

Theorem modmuladdim

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

Ref Expression
Assertion modmuladdim 
|- ( ( A e. ZZ /\ 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 modelico 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) e. ( 0 [,) M ) )
3 1 2 sylan 
 |-  ( ( A e. ZZ /\ M e. RR+ ) -> ( A mod M ) e. ( 0 [,) M ) )
4 3 adantr 
 |-  ( ( ( A e. ZZ /\ M e. RR+ ) /\ ( A mod M ) = B ) -> ( A mod M ) e. ( 0 [,) M ) )
5 eleq1 
 |-  ( ( A mod M ) = B -> ( ( A mod M ) e. ( 0 [,) M ) <-> B e. ( 0 [,) M ) ) )
6 5 adantl 
 |-  ( ( ( A e. ZZ /\ M e. RR+ ) /\ ( A mod M ) = B ) -> ( ( A mod M ) e. ( 0 [,) M ) <-> B e. ( 0 [,) M ) ) )
7 4 6 mpbid 
 |-  ( ( ( A e. ZZ /\ M e. RR+ ) /\ ( A mod M ) = B ) -> B e. ( 0 [,) M ) )
8 simpll 
 |-  ( ( ( A e. ZZ /\ M e. RR+ ) /\ B e. ( 0 [,) M ) ) -> A e. ZZ )
9 simpr 
 |-  ( ( ( A e. ZZ /\ M e. RR+ ) /\ B e. ( 0 [,) M ) ) -> B e. ( 0 [,) M ) )
10 simpr 
 |-  ( ( A e. ZZ /\ M e. RR+ ) -> M e. RR+ )
11 10 adantr 
 |-  ( ( ( A e. ZZ /\ M e. RR+ ) /\ B e. ( 0 [,) M ) ) -> M e. RR+ )
12 modmuladd 
 |-  ( ( A e. ZZ /\ B e. ( 0 [,) M ) /\ M e. RR+ ) -> ( ( A mod M ) = B <-> E. k e. ZZ A = ( ( k x. M ) + B ) ) )
13 8 9 11 12 syl3anc 
 |-  ( ( ( A e. ZZ /\ M e. RR+ ) /\ B e. ( 0 [,) M ) ) -> ( ( A mod M ) = B <-> E. k e. ZZ A = ( ( k x. M ) + B ) ) )
14 13 biimpd 
 |-  ( ( ( A e. ZZ /\ M e. RR+ ) /\ B e. ( 0 [,) M ) ) -> ( ( A mod M ) = B -> E. k e. ZZ A = ( ( k x. M ) + B ) ) )
15 14 impancom 
 |-  ( ( ( A e. ZZ /\ M e. RR+ ) /\ ( A mod M ) = B ) -> ( B e. ( 0 [,) M ) -> E. k e. ZZ A = ( ( k x. M ) + B ) ) )
16 7 15 mpd 
 |-  ( ( ( A e. ZZ /\ M e. RR+ ) /\ ( A mod M ) = B ) -> E. k e. ZZ A = ( ( k x. M ) + B ) )
17 16 ex 
 |-  ( ( A e. ZZ /\ M e. RR+ ) -> ( ( A mod M ) = B -> E. k e. ZZ A = ( ( k x. M ) + B ) ) )