Metamath Proof Explorer


Theorem quoremnn0

Description: Quotient and remainder of a nonnegative integer divided by a positive integer. (Contributed by NM, 14-Aug-2008)

Ref Expression
Hypotheses quorem.1 Q = A B
quorem.2 R = A B Q
Assertion quoremnn0 A 0 B Q 0 R 0 R < B A = B Q + R

Proof

Step Hyp Ref Expression
1 quorem.1 Q = A B
2 quorem.2 R = A B Q
3 fldivnn0 A 0 B A B 0
4 1 3 eqeltrid A 0 B Q 0
5 nn0z A 0 A
6 1 2 quoremz A B Q R 0 R < B A = B Q + R
7 5 6 sylan A 0 B Q R 0 R < B A = B Q + R
8 simpl Q 0 Q Q 0
9 8 anim1i Q 0 Q R 0 Q 0 R 0
10 9 anasss Q 0 Q R 0 Q 0 R 0
11 10 anim1i Q 0 Q R 0 R < B A = B Q + R Q 0 R 0 R < B A = B Q + R
12 11 anasss Q 0 Q R 0 R < B A = B Q + R Q 0 R 0 R < B A = B Q + R
13 4 7 12 syl2anc A 0 B Q 0 R 0 R < B A = B Q + R