Metamath Proof Explorer


Theorem modmuladdnn0

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

Ref Expression
Assertion modmuladdnn0 A 0 M + A mod M = B k 0 A = k M + B

Proof

Step Hyp Ref Expression
1 simpr A 0 M + A mod M = B i i
2 1 adantr A 0 M + A mod M = B i A = i M + B i
3 nn0cn A 0 A
4 3 adantr A 0 M + A
5 4 ad2antrr A 0 M + A mod M = B i A
6 nn0re A 0 A
7 modcl A M + A mod M
8 6 7 sylan A 0 M + A mod M
9 8 recnd A 0 M + A mod M
10 9 adantr A 0 M + A mod M = B A mod M
11 eleq1 A mod M = B A mod M B
12 11 adantl A 0 M + A mod M = B A mod M B
13 10 12 mpbid A 0 M + A mod M = B B
14 13 adantr A 0 M + A mod M = B i B
15 zcn i i
16 15 adantl A 0 M + A mod M = B i i
17 rpcn M + M
18 17 adantl A 0 M + M
19 18 ad2antrr A 0 M + A mod M = B i M
20 16 19 mulcld A 0 M + A mod M = B i i M
21 5 14 20 subadd2d A 0 M + A mod M = B i A B = i M i M + B = A
22 eqcom A = i M + B i M + B = A
23 21 22 syl6rbbr A 0 M + A mod M = B i A = i M + B A B = i M
24 3 ad2antrr A 0 M + A mod M = B A
25 24 13 subcld A 0 M + A mod M = B A B
26 25 adantr A 0 M + A mod M = B i A B
27 rpcnne0 M + M M 0
28 27 adantl A 0 M + M M 0
29 28 ad2antrr A 0 M + A mod M = B i M M 0
30 divmul3 A B i M M 0 A B M = i A B = i M
31 26 16 29 30 syl3anc A 0 M + A mod M = B i A B M = i A B = i M
32 oveq2 B = A mod M A B = A A mod M
33 32 oveq1d B = A mod M A B M = A A mod M M
34 33 eqcoms A mod M = B A B M = A A mod M M
35 34 adantl A 0 M + A mod M = B A B M = A A mod M M
36 35 adantr A 0 M + A mod M = B i A B M = A A mod M M
37 moddiffl A M + A A mod M M = A M
38 6 37 sylan A 0 M + A A mod M M = A M
39 38 ad2antrr A 0 M + A mod M = B i A A mod M M = A M
40 36 39 eqtrd A 0 M + A mod M = B i A B M = A M
41 40 eqeq1d A 0 M + A mod M = B i A B M = i A M = i
42 23 31 41 3bitr2d A 0 M + A mod M = B i A = i M + B A M = i
43 nn0ge0 A 0 0 A
44 6 43 jca A 0 A 0 A
45 rpregt0 M + M 0 < M
46 divge0 A 0 A M 0 < M 0 A M
47 44 45 46 syl2an A 0 M + 0 A M
48 6 adantr A 0 M + A
49 rpre M + M
50 49 adantl A 0 M + M
51 rpne0 M + M 0
52 51 adantl A 0 M + M 0
53 48 50 52 redivcld A 0 M + A M
54 0z 0
55 flge A M 0 0 A M 0 A M
56 53 54 55 sylancl A 0 M + 0 A M 0 A M
57 47 56 mpbid A 0 M + 0 A M
58 breq2 A M = i 0 A M 0 i
59 57 58 syl5ibcom A 0 M + A M = i 0 i
60 59 ad2antrr A 0 M + A mod M = B i A M = i 0 i
61 42 60 sylbid A 0 M + A mod M = B i A = i M + B 0 i
62 61 imp A 0 M + A mod M = B i A = i M + B 0 i
63 elnn0z i 0 i 0 i
64 2 62 63 sylanbrc A 0 M + A mod M = B i A = i M + B i 0
65 oveq1 k = i k M = i M
66 65 oveq1d k = i k M + B = i M + B
67 66 eqeq2d k = i A = k M + B A = i M + B
68 67 adantl A 0 M + A mod M = B i A = i M + B k = i A = k M + B A = i M + B
69 simpr A 0 M + A mod M = B i A = i M + B A = i M + B
70 64 68 69 rspcedvd A 0 M + A mod M = B i A = i M + B k 0 A = k M + B
71 nn0z A 0 A
72 modmuladdim A M + A mod M = B i A = i M + B
73 71 72 sylan A 0 M + A mod M = B i A = i M + B
74 73 imp A 0 M + A mod M = B i A = i M + B
75 70 74 r19.29a A 0 M + A mod M = B k 0 A = k M + B
76 75 ex A 0 M + A mod M = B k 0 A = k M + B