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 B 0 M M + A mod M = B k A = k M + B

Proof

Step Hyp Ref Expression
1 oveq1 k = A M k M = A M M
2 1 oveq1d k = A M k M + A mod M = A M M + A mod M
3 2 eqeq2d k = A M A = k M + A mod M A = A M M + A mod M
4 zre A A
5 4 adantr A M + A
6 rpre M + M
7 6 adantl A M + M
8 rpne0 M + M 0
9 8 adantl A M + M 0
10 5 7 9 redivcld A M + A M
11 10 flcld A M + A M
12 11 3adant2 A B 0 M M + A M
13 flpmodeq A M + A M M + A mod M = A
14 4 13 sylan A M + A M M + A mod M = A
15 14 eqcomd A M + A = A M M + A mod M
16 15 3adant2 A B 0 M M + A = A M M + A mod M
17 3 12 16 rspcedvdw A B 0 M M + k A = k M + A mod M
18 oveq2 B = A mod M k M + B = k M + A mod M
19 18 eqeq2d B = A mod M A = k M + B A = k M + A mod M
20 19 eqcoms A mod M = B A = k M + B A = k M + A mod M
21 20 rexbidv A mod M = B k A = k M + B k A = k M + A mod M
22 17 21 syl5ibrcom A B 0 M M + A mod M = B k A = k M + B
23 oveq1 A = k M + B A mod M = k M + B mod M
24 simpr A B 0 M M + k k
25 simpl3 A B 0 M M + k M +
26 simpl2 A B 0 M M + k B 0 M
27 muladdmodid k M + B 0 M k M + B mod M = B
28 24 25 26 27 syl3anc A B 0 M M + k k M + B mod M = B
29 23 28 sylan9eqr A B 0 M M + k A = k M + B A mod M = B
30 29 rexlimdva2 A B 0 M M + k A = k M + B A mod M = B
31 22 30 impbid A B 0 M M + A mod M = B k A = k M + B