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 โŠข ๐‘„ = ( โŒŠ โ€˜ ( ๐ด / ๐ต ) )
quorem.2 โŠข ๐‘… = ( ๐ด โˆ’ ( ๐ต ยท ๐‘„ ) )
Assertion quoremnn0 ( ( ๐ด โˆˆ โ„•0 โˆง ๐ต โˆˆ โ„• ) โ†’ ( ( ๐‘„ โˆˆ โ„•0 โˆง ๐‘… โˆˆ โ„•0 ) โˆง ( ๐‘… < ๐ต โˆง ๐ด = ( ( ๐ต ยท ๐‘„ ) + ๐‘… ) ) ) )

Proof

Step Hyp Ref Expression
1 quorem.1 โŠข ๐‘„ = ( โŒŠ โ€˜ ( ๐ด / ๐ต ) )
2 quorem.2 โŠข ๐‘… = ( ๐ด โˆ’ ( ๐ต ยท ๐‘„ ) )
3 fldivnn0 โŠข ( ( ๐ด โˆˆ โ„•0 โˆง ๐ต โˆˆ โ„• ) โ†’ ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) โˆˆ โ„•0 )
4 1 3 eqeltrid โŠข ( ( ๐ด โˆˆ โ„•0 โˆง ๐ต โˆˆ โ„• ) โ†’ ๐‘„ โˆˆ โ„•0 )
5 nn0z โŠข ( ๐ด โˆˆ โ„•0 โ†’ ๐ด โˆˆ โ„ค )
6 1 2 quoremz โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„• ) โ†’ ( ( ๐‘„ โˆˆ โ„ค โˆง ๐‘… โˆˆ โ„•0 ) โˆง ( ๐‘… < ๐ต โˆง ๐ด = ( ( ๐ต ยท ๐‘„ ) + ๐‘… ) ) ) )
7 5 6 sylan โŠข ( ( ๐ด โˆˆ โ„•0 โˆง ๐ต โˆˆ โ„• ) โ†’ ( ( ๐‘„ โˆˆ โ„ค โˆง ๐‘… โˆˆ โ„•0 ) โˆง ( ๐‘… < ๐ต โˆง ๐ด = ( ( ๐ต ยท ๐‘„ ) + ๐‘… ) ) ) )
8 simpl โŠข ( ( ๐‘„ โˆˆ โ„•0 โˆง ๐‘„ โˆˆ โ„ค ) โ†’ ๐‘„ โˆˆ โ„•0 )
9 8 anim1i โŠข ( ( ( ๐‘„ โˆˆ โ„•0 โˆง ๐‘„ โˆˆ โ„ค ) โˆง ๐‘… โˆˆ โ„•0 ) โ†’ ( ๐‘„ โˆˆ โ„•0 โˆง ๐‘… โˆˆ โ„•0 ) )
10 9 anasss โŠข ( ( ๐‘„ โˆˆ โ„•0 โˆง ( ๐‘„ โˆˆ โ„ค โˆง ๐‘… โˆˆ โ„•0 ) ) โ†’ ( ๐‘„ โˆˆ โ„•0 โˆง ๐‘… โˆˆ โ„•0 ) )
11 10 anim1i โŠข ( ( ( ๐‘„ โˆˆ โ„•0 โˆง ( ๐‘„ โˆˆ โ„ค โˆง ๐‘… โˆˆ โ„•0 ) ) โˆง ( ๐‘… < ๐ต โˆง ๐ด = ( ( ๐ต ยท ๐‘„ ) + ๐‘… ) ) ) โ†’ ( ( ๐‘„ โˆˆ โ„•0 โˆง ๐‘… โˆˆ โ„•0 ) โˆง ( ๐‘… < ๐ต โˆง ๐ด = ( ( ๐ต ยท ๐‘„ ) + ๐‘… ) ) ) )
12 11 anasss โŠข ( ( ๐‘„ โˆˆ โ„•0 โˆง ( ( ๐‘„ โˆˆ โ„ค โˆง ๐‘… โˆˆ โ„•0 ) โˆง ( ๐‘… < ๐ต โˆง ๐ด = ( ( ๐ต ยท ๐‘„ ) + ๐‘… ) ) ) ) โ†’ ( ( ๐‘„ โˆˆ โ„•0 โˆง ๐‘… โˆˆ โ„•0 ) โˆง ( ๐‘… < ๐ต โˆง ๐ด = ( ( ๐ต ยท ๐‘„ ) + ๐‘… ) ) ) )
13 4 7 12 syl2anc โŠข ( ( ๐ด โˆˆ โ„•0 โˆง ๐ต โˆˆ โ„• ) โ†’ ( ( ๐‘„ โˆˆ โ„•0 โˆง ๐‘… โˆˆ โ„•0 ) โˆง ( ๐‘… < ๐ต โˆง ๐ด = ( ( ๐ต ยท ๐‘„ ) + ๐‘… ) ) ) )