Metamath Proof Explorer


Theorem modremain

Description: The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021)

Ref Expression
Assertion modremain N D R 0 R < D N mod D = R z z D + R = N

Proof

Step Hyp Ref Expression
1 eqcom N mod D = R R = N mod D
2 divalgmodcl N D R 0 R = N mod D R < D D N R
3 2 3adant3r N D R 0 R < D R = N mod D R < D D N R
4 ibar R < D D N R R < D D N R
5 4 adantl R 0 R < D D N R R < D D N R
6 5 3ad2ant3 N D R 0 R < D D N R R < D D N R
7 nnz D D
8 7 3ad2ant2 N D R 0 R < D D
9 simp1 N D R 0 R < D N
10 nn0z R 0 R
11 10 adantr R 0 R < D R
12 11 3ad2ant3 N D R 0 R < D R
13 9 12 zsubcld N D R 0 R < D N R
14 divides D N R D N R z z D = N R
15 8 13 14 syl2anc N D R 0 R < D D N R z z D = N R
16 eqcom z D = N R N R = z D
17 zcn N N
18 17 3ad2ant1 N D R 0 R < D N
19 18 adantr N D R 0 R < D z N
20 nn0cn R 0 R
21 20 adantr R 0 R < D R
22 21 3ad2ant3 N D R 0 R < D R
23 22 adantr N D R 0 R < D z R
24 simpr N D R 0 R < D z z
25 8 adantr N D R 0 R < D z D
26 24 25 zmulcld N D R 0 R < D z z D
27 26 zcnd N D R 0 R < D z z D
28 19 23 27 subadd2d N D R 0 R < D z N R = z D z D + R = N
29 16 28 syl5bb N D R 0 R < D z z D = N R z D + R = N
30 29 rexbidva N D R 0 R < D z z D = N R z z D + R = N
31 15 30 bitrd N D R 0 R < D D N R z z D + R = N
32 3 6 31 3bitr2d N D R 0 R < D R = N mod D z z D + R = N
33 1 32 syl5bb N D R 0 R < D N mod D = R z z D + R = N