Theorem quoremnn0ALT

Description: Alternate proof of quoremnn0 not using quoremz . TODO - Keep either quoremnn0ALT (if we don't keep quoremz ) or quoremnn0 ? (Contributed by NM, 14-Aug-2008) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	quorem.1	$$⊢Q=⌊\frac{A}{B}⌋$$
	quorem.2	$$⊢R=A-BQ$$
Assertion	quoremnn0ALT	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left(\left(Q\in {\mathbb{N}}_0\wedge R\in {\mathbb{N}}_0\right)\wedge \left(R<B\wedge A=BQ+R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		quorem.1	$$⊢Q=⌊\frac{A}{B}⌋$$
2		quorem.2	$$⊢R=A-BQ$$
3		fldivnn0	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to ⌊\frac{A}{B}⌋\in {\mathbb{N}}_0$$
4	1 3	eqeltrid	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to Q\in {\mathbb{N}}_0$$
5		nnnn0	$$⊢B\in \mathbb{N}\to B\in {\mathbb{N}}_0$$
6	5	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to B\in {\mathbb{N}}_0$$
7	6 4	nn0mulcld	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to BQ\in {\mathbb{N}}_0$$
8		simpl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to A\in {\mathbb{N}}_0$$
9	4	nn0cnd	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to Q\in ℂ$$
10		nncn	$$⊢B\in \mathbb{N}\to B\in ℂ$$
11	10	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to B\in ℂ$$
12		nnne0	$$⊢B\in \mathbb{N}\to B\ne 0$$
13	12	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to B\ne 0$$
14	9 11 13	divcan3d	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \frac{BQ}{B}=Q$$
15		nn0nndivcl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \frac{A}{B}\in ℝ$$
16		flle	$$⊢\frac{A}{B}\in ℝ\to ⌊\frac{A}{B}⌋\le \frac{A}{B}$$
17	15 16	syl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to ⌊\frac{A}{B}⌋\le \frac{A}{B}$$
18	1 17	eqbrtrid	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to Q\le \frac{A}{B}$$
19	14 18	eqbrtrd	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \frac{BQ}{B}\le \frac{A}{B}$$
20	7	nn0red	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to BQ\in ℝ$$
21		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
22	21	adantr	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to A\in ℝ$$
23		nnre	$$⊢B\in \mathbb{N}\to B\in ℝ$$
24	23	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to B\in ℝ$$
25		nngt0	$$⊢B\in \mathbb{N}\to 0<B$$
26	25	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to 0<B$$
27		lediv1	$$⊢\left(BQ\in ℝ\wedge A\in ℝ\wedge \left(B\in ℝ\wedge 0<B\right)\right)\to \left(BQ\le A\leftrightarrow \frac{BQ}{B}\le \frac{A}{B}\right)$$
28	20 22 24 26 27	syl112anc	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left(BQ\le A\leftrightarrow \frac{BQ}{B}\le \frac{A}{B}\right)$$
29	19 28	mpbird	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to BQ\le A$$
30		nn0sub2	$$⊢\left(BQ\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge BQ\le A\right)\to A-BQ\in {\mathbb{N}}_0$$
31	7 8 29 30	syl3anc	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to A-BQ\in {\mathbb{N}}_0$$
32	2 31	eqeltrid	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to R\in {\mathbb{N}}_0$$
33	1	oveq2i	$$⊢\left(\frac{A}{B}\right)-Q=\left(\frac{A}{B}\right)-⌊\frac{A}{B}⌋$$
34		fraclt1	$$⊢\frac{A}{B}\in ℝ\to \left(\frac{A}{B}\right)-⌊\frac{A}{B}⌋<1$$
35	15 34	syl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left(\frac{A}{B}\right)-⌊\frac{A}{B}⌋<1$$
36	33 35	eqbrtrid	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left(\frac{A}{B}\right)-Q<1$$
37	2	oveq1i	$$⊢\frac{R}{B}=\frac{A-BQ}{B}$$
38		nn0cn	$$⊢A\in {\mathbb{N}}_0\to A\in ℂ$$
39	38	adantr	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to A\in ℂ$$
40	7	nn0cnd	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to BQ\in ℂ$$
41	10 12	jca	$$⊢B\in \mathbb{N}\to \left(B\in ℂ\wedge B\ne 0\right)$$
42	41	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left(B\in ℂ\wedge B\ne 0\right)$$
43		divsubdir	$$⊢\left(A\in ℂ\wedge BQ\in ℂ\wedge \left(B\in ℂ\wedge B\ne 0\right)\right)\to \frac{A-BQ}{B}=\left(\frac{A}{B}\right)-\left(\frac{BQ}{B}\right)$$
44	39 40 42 43	syl3anc	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \frac{A-BQ}{B}=\left(\frac{A}{B}\right)-\left(\frac{BQ}{B}\right)$$
45	14	oveq2d	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left(\frac{A}{B}\right)-\left(\frac{BQ}{B}\right)=\left(\frac{A}{B}\right)-Q$$
46	44 45	eqtrd	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \frac{A-BQ}{B}=\left(\frac{A}{B}\right)-Q$$
47	37 46	syl5eq	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \frac{R}{B}=\left(\frac{A}{B}\right)-Q$$
48	10 12	dividd	$$⊢B\in \mathbb{N}\to \frac{B}{B}=1$$
49	48	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \frac{B}{B}=1$$
50	36 47 49	3brtr4d	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \frac{R}{B}<\frac{B}{B}$$
51	32	nn0red	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to R\in ℝ$$
52		ltdiv1	$$⊢\left(R\in ℝ\wedge B\in ℝ\wedge \left(B\in ℝ\wedge 0<B\right)\right)\to \left(R<B\leftrightarrow \frac{R}{B}<\frac{B}{B}\right)$$
53	51 24 24 26 52	syl112anc	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left(R<B\leftrightarrow \frac{R}{B}<\frac{B}{B}\right)$$
54	50 53	mpbird	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to R<B$$
55	2	oveq2i	$$⊢BQ+R=BQ+A-BQ$$
56	40 39	pncan3d	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to BQ+A-BQ=A$$
57	55 56	syl5req	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to A=BQ+R$$
58	54 57	jca	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left(R<B\wedge A=BQ+R\right)$$
59	4 32 58	jca31	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left(\left(Q\in {\mathbb{N}}_0\wedge R\in {\mathbb{N}}_0\right)\wedge \left(R<B\wedge A=BQ+R\right)\right)$$