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 ) ∧ ( 𝑅 < 𝐵𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) )