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