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 = ⌊\frac{A}{B}⌋$
	quorem.2	$⊢ R = A - B Q$
Assertion	quoremnn0	$⊢ (A \in ℕ_{0} \land B \in ℕ) \to ((Q \in ℕ_{0} \land R \in ℕ_{0}) \land (R < B \land A = B Q + R))$

Step	Hyp	Ref	Expression
1		quorem.1	$⊢ Q = ⌊\frac{A}{B}⌋$
2		quorem.2	$⊢ R = A - B Q$
3		fldivnn0	$⊢ (A \in ℕ_{0} \land B \in ℕ) \to ⌊\frac{A}{B}⌋ \in ℕ_{0}$
4	1 3	eqeltrid	$⊢ (A \in ℕ_{0} \land B \in ℕ) \to Q \in ℕ_{0}$
5		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
6	1 2	quoremz	$⊢ (A \in ℤ \land B \in ℕ) \to ((Q \in ℤ \land R \in ℕ_{0}) \land (R < B \land A = B Q + R))$
7	5 6	sylan	$⊢ (A \in ℕ_{0} \land B \in ℕ) \to ((Q \in ℤ \land R \in ℕ_{0}) \land (R < B \land A = B Q + R))$
8		simpl	$⊢ (Q \in ℕ_{0} \land Q \in ℤ) \to Q \in ℕ_{0}$
9	8	anim1i	$⊢ ((Q \in ℕ_{0} \land Q \in ℤ) \land R \in ℕ_{0}) \to (Q \in ℕ_{0} \land R \in ℕ_{0})$
10	9	anasss	$⊢ (Q \in ℕ_{0} \land (Q \in ℤ \land R \in ℕ_{0})) \to (Q \in ℕ_{0} \land R \in ℕ_{0})$
11	10	anim1i	$⊢ ((Q \in ℕ_{0} \land (Q \in ℤ \land R \in ℕ_{0})) \land (R < B \land A = B Q + R)) \to ((Q \in ℕ_{0} \land R \in ℕ_{0}) \land (R < B \land A = B Q + R))$
12	11	anasss	$⊢ (Q \in ℕ_{0} \land ((Q \in ℤ \land R \in ℕ_{0}) \land (R < B \land A = B Q + R))) \to ((Q \in ℕ_{0} \land R \in ℕ_{0}) \land (R < B \land A = B Q + R))$
13	4 7 12	syl2anc	$⊢ (A \in ℕ_{0} \land B \in ℕ) \to ((Q \in ℕ_{0} \land R \in ℕ_{0}) \land (R < B \land A = B Q + R))$

Metamath Proof Explorer