quoremz

Description: Quotient and remainder of an integer divided by a positive integer. TODO - is this really needed for anything? Should we use mod to simplify it? Remark (AV): This is a special case of divalg . (Contributed by NM, 14-Aug-2008)

	Ref	Expression
Hypotheses	quorem.1	$⊢ Q = ⌊\frac{A}{B}⌋$
	quorem.2	$⊢ R = A - B Q$
Assertion	quoremz	$⊢ (A \in ℤ \land B \in ℕ) \to ((Q \in ℤ \land R \in ℕ_{0}) \land (R < B \land A = B Q + R))$

Proof

Step	Hyp	Ref	Expression
1		quorem.1	$⊢ Q = ⌊\frac{A}{B}⌋$
2		quorem.2	$⊢ R = A - B Q$
3		zre	$⊢ A \in ℤ \to A \in ℝ$
4	3	adantr	$⊢ (A \in ℤ \land B \in ℕ) \to A \in ℝ$
5		nnre	$⊢ B \in ℕ \to B \in ℝ$
6	5	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to B \in ℝ$
7		nnne0	$⊢ B \in ℕ \to B \neq 0$
8	7	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to B \neq 0$
9	4 6 8	redivcld	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{A}{B} \in ℝ$
10	9	flcld	$⊢ (A \in ℤ \land B \in ℕ) \to ⌊\frac{A}{B}⌋ \in ℤ$
11	1 10	eqeltrid	$⊢ (A \in ℤ \land B \in ℕ) \to Q \in ℤ$
12	11	zcnd	$⊢ (A \in ℤ \land B \in ℕ) \to Q \in ℂ$
13		nncn	$⊢ B \in ℕ \to B \in ℂ$
14	13	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to B \in ℂ$
15	12 14 8	divcan3d	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{B Q}{B} = Q$
16		flle	$⊢ \frac{A}{B} \in ℝ \to ⌊\frac{A}{B}⌋ \leq \frac{A}{B}$
17	9 16	syl	$⊢ (A \in ℤ \land B \in ℕ) \to ⌊\frac{A}{B}⌋ \leq \frac{A}{B}$
18	1 17	eqbrtrid	$⊢ (A \in ℤ \land B \in ℕ) \to Q \leq \frac{A}{B}$
19	15 18	eqbrtrd	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{B Q}{B} \leq \frac{A}{B}$
20		nnz	$⊢ B \in ℕ \to B \in ℤ$
21	20	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to B \in ℤ$
22	21 11	zmulcld	$⊢ (A \in ℤ \land B \in ℕ) \to B Q \in ℤ$
23	22	zred	$⊢ (A \in ℤ \land B \in ℕ) \to B Q \in ℝ$
24		nngt0	$⊢ B \in ℕ \to 0 < B$
25	24	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to 0 < B$
26		lediv1	$⊢ (B Q \in ℝ \land A \in ℝ \land (B \in ℝ \land 0 < B)) \to (B Q \leq A \leftrightarrow \frac{B Q}{B} \leq \frac{A}{B})$
27	23 4 6 25 26	syl112anc	$⊢ (A \in ℤ \land B \in ℕ) \to (B Q \leq A \leftrightarrow \frac{B Q}{B} \leq \frac{A}{B})$
28	19 27	mpbird	$⊢ (A \in ℤ \land B \in ℕ) \to B Q \leq A$
29		simpl	$⊢ (A \in ℤ \land B \in ℕ) \to A \in ℤ$
30		znn0sub	$⊢ (B Q \in ℤ \land A \in ℤ) \to (B Q \leq A \leftrightarrow A - B Q \in ℕ_{0})$
31	22 29 30	syl2anc	$⊢ (A \in ℤ \land B \in ℕ) \to (B Q \leq A \leftrightarrow A - B Q \in ℕ_{0})$
32	28 31	mpbid	$⊢ (A \in ℤ \land B \in ℕ) \to A - B Q \in ℕ_{0}$
33	2 32	eqeltrid	$⊢ (A \in ℤ \land B \in ℕ) \to R \in ℕ_{0}$
34	1	oveq2i	$⊢ (\frac{A}{B}) - Q = (\frac{A}{B}) - ⌊\frac{A}{B}⌋$
35		fraclt1	$⊢ \frac{A}{B} \in ℝ \to (\frac{A}{B}) - ⌊\frac{A}{B}⌋ < 1$
36	9 35	syl	$⊢ (A \in ℤ \land B \in ℕ) \to (\frac{A}{B}) - ⌊\frac{A}{B}⌋ < 1$
37	34 36	eqbrtrid	$⊢ (A \in ℤ \land B \in ℕ) \to (\frac{A}{B}) - Q < 1$
38	2	oveq1i	$⊢ \frac{R}{B} = \frac{A - B Q}{B}$
39		zcn	$⊢ A \in ℤ \to A \in ℂ$
40	39	adantr	$⊢ (A \in ℤ \land B \in ℕ) \to A \in ℂ$
41	22	zcnd	$⊢ (A \in ℤ \land B \in ℕ) \to B Q \in ℂ$
42	13 7	jca	$⊢ B \in ℕ \to (B \in ℂ \land B \neq 0)$
43	42	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to (B \in ℂ \land B \neq 0)$
44		divsubdir	$⊢ (A \in ℂ \land B Q \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{A - B Q}{B} = (\frac{A}{B}) - (\frac{B Q}{B})$
45	40 41 43 44	syl3anc	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{A - B Q}{B} = (\frac{A}{B}) - (\frac{B Q}{B})$
46	15	oveq2d	$⊢ (A \in ℤ \land B \in ℕ) \to (\frac{A}{B}) - (\frac{B Q}{B}) = (\frac{A}{B}) - Q$
47	45 46	eqtrd	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{A - B Q}{B} = (\frac{A}{B}) - Q$
48	38 47	eqtrid	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{R}{B} = (\frac{A}{B}) - Q$
49	13 7	dividd	$⊢ B \in ℕ \to \frac{B}{B} = 1$
50	49	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{B}{B} = 1$
51	37 48 50	3brtr4d	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{R}{B} < \frac{B}{B}$
52	33	nn0red	$⊢ (A \in ℤ \land B \in ℕ) \to R \in ℝ$
53		ltdiv1	$⊢ (R \in ℝ \land B \in ℝ \land (B \in ℝ \land 0 < B)) \to (R < B \leftrightarrow \frac{R}{B} < \frac{B}{B})$
54	52 6 6 25 53	syl112anc	$⊢ (A \in ℤ \land B \in ℕ) \to (R < B \leftrightarrow \frac{R}{B} < \frac{B}{B})$
55	51 54	mpbird	$⊢ (A \in ℤ \land B \in ℕ) \to R < B$
56	2	oveq2i	$⊢ B Q + R = B Q + A - B Q$
57	41 40	pncan3d	$⊢ (A \in ℤ \land B \in ℕ) \to B Q + A - B Q = A$
58	56 57	eqtr2id	$⊢ (A \in ℤ \land B \in ℕ) \to A = B Q + R$
59	55 58	jca	$⊢ (A \in ℤ \land B \in ℕ) \to (R < B \land A = B Q + R)$
60	11 33 59	jca31	$⊢ (A \in ℤ \land B \in ℕ) \to ((Q \in ℤ \land R \in ℕ_{0}) \land (R < B \land A = B Q + R))$

Metamath Proof Explorer

Theorem quoremz

Proof