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 x. Q ) )
Assertion quoremnn0 
|- ( ( A e. NN0 /\ B e. NN ) -> ( ( Q e. NN0 /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )

Proof

Step Hyp Ref Expression
1 quorem.1 
 |-  Q = ( |_ ` ( A / B ) )
2 quorem.2 
 |-  R = ( A - ( B x. Q ) )
3 fldivnn0 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( |_ ` ( A / B ) ) e. NN0 )
4 1 3 eqeltrid 
 |-  ( ( A e. NN0 /\ B e. NN ) -> Q e. NN0 )
5 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
6 1 2 quoremz 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( Q e. ZZ /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )
7 5 6 sylan 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( Q e. ZZ /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )
8 simpl 
 |-  ( ( Q e. NN0 /\ Q e. ZZ ) -> Q e. NN0 )
9 8 anim1i 
 |-  ( ( ( Q e. NN0 /\ Q e. ZZ ) /\ R e. NN0 ) -> ( Q e. NN0 /\ R e. NN0 ) )
10 9 anasss 
 |-  ( ( Q e. NN0 /\ ( Q e. ZZ /\ R e. NN0 ) ) -> ( Q e. NN0 /\ R e. NN0 ) )
11 10 anim1i 
 |-  ( ( ( Q e. NN0 /\ ( Q e. ZZ /\ R e. NN0 ) ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) -> ( ( Q e. NN0 /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )
12 11 anasss 
 |-  ( ( Q e. NN0 /\ ( ( Q e. ZZ /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) ) -> ( ( Q e. NN0 /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )
13 4 7 12 syl2anc 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( Q e. NN0 /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )