divalgb

Description: Express the division algorithm as stated in divalg in terms of || . (Contributed by Paul Chapman, 31-Mar-2011)

		Ref	Expression
	Assertion	divalgb	$⊢ (N \in ℤ \land D \in ℤ \land D \neq 0) \to (\exists! r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r) \leftrightarrow \exists! r \in ℕ_{0} (r < \|D\| \land D ∥ (N - r)))$

Proof

Step	Hyp	Ref	Expression
1		zsubcl	$⊢ (N \in ℤ \land r \in ℤ) \to N - r \in ℤ$
2		divides	$⊢ (D \in ℤ \land N - r \in ℤ) \to (D ∥ (N - r) \leftrightarrow \exists q \in ℤ q D = N - r)$
3	1 2	sylan2	$⊢ (D \in ℤ \land (N \in ℤ \land r \in ℤ)) \to (D ∥ (N - r) \leftrightarrow \exists q \in ℤ q D = N - r)$
4	3	3impb	$⊢ (D \in ℤ \land N \in ℤ \land r \in ℤ) \to (D ∥ (N - r) \leftrightarrow \exists q \in ℤ q D = N - r)$
5	4	3com12	$⊢ (N \in ℤ \land D \in ℤ \land r \in ℤ) \to (D ∥ (N - r) \leftrightarrow \exists q \in ℤ q D = N - r)$
6		zcn	$⊢ N \in ℤ \to N \in ℂ$
7		zcn	$⊢ r \in ℤ \to r \in ℂ$
8		zmulcl	$⊢ (q \in ℤ \land D \in ℤ) \to q D \in ℤ$
9	8	zcnd	$⊢ (q \in ℤ \land D \in ℤ) \to q D \in ℂ$
10		subadd	$⊢ (N \in ℂ \land r \in ℂ \land q D \in ℂ) \to (N - r = q D \leftrightarrow r + q D = N)$
11	6 7 9 10	syl3an	$⊢ (N \in ℤ \land r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to (N - r = q D \leftrightarrow r + q D = N)$
12		addcom	$⊢ (r \in ℂ \land q D \in ℂ) \to r + q D = q D + r$
13	7 9 12	syl2an	$⊢ (r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to r + q D = q D + r$
14	13	3adant1	$⊢ (N \in ℤ \land r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to r + q D = q D + r$
15	14	eqeq1d	$⊢ (N \in ℤ \land r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to (r + q D = N \leftrightarrow q D + r = N)$
16	11 15	bitrd	$⊢ (N \in ℤ \land r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to (N - r = q D \leftrightarrow q D + r = N)$
17		eqcom	$⊢ N - r = q D \leftrightarrow q D = N - r$
18		eqcom	$⊢ q D + r = N \leftrightarrow N = q D + r$
19	16 17 18	3bitr3g	$⊢ (N \in ℤ \land r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to (q D = N - r \leftrightarrow N = q D + r)$
20	19	3expia	$⊢ (N \in ℤ \land r \in ℤ) \to ((q \in ℤ \land D \in ℤ) \to (q D = N - r \leftrightarrow N = q D + r))$
21	20	expcomd	$⊢ (N \in ℤ \land r \in ℤ) \to (D \in ℤ \to (q \in ℤ \to (q D = N - r \leftrightarrow N = q D + r)))$
22	21	3impia	$⊢ (N \in ℤ \land r \in ℤ \land D \in ℤ) \to (q \in ℤ \to (q D = N - r \leftrightarrow N = q D + r))$
23	22	imp	$⊢ ((N \in ℤ \land r \in ℤ \land D \in ℤ) \land q \in ℤ) \to (q D = N - r \leftrightarrow N = q D + r)$
24	23	rexbidva	$⊢ (N \in ℤ \land r \in ℤ \land D \in ℤ) \to (\exists q \in ℤ q D = N - r \leftrightarrow \exists q \in ℤ N = q D + r)$
25	24	3com23	$⊢ (N \in ℤ \land D \in ℤ \land r \in ℤ) \to (\exists q \in ℤ q D = N - r \leftrightarrow \exists q \in ℤ N = q D + r)$
26	5 25	bitrd	$⊢ (N \in ℤ \land D \in ℤ \land r \in ℤ) \to (D ∥ (N - r) \leftrightarrow \exists q \in ℤ N = q D + r)$
27	26	anbi2d	$⊢ (N \in ℤ \land D \in ℤ \land r \in ℤ) \to (((0 \leq r \land r < \|D\|) \land D ∥ (N - r)) \leftrightarrow ((0 \leq r \land r < \|D\|) \land \exists q \in ℤ N = q D + r))$
28		df-3an	$⊢ (0 \leq r \land r < \|D\| \land N = q D + r) \leftrightarrow ((0 \leq r \land r < \|D\|) \land N = q D + r)$
29	28	rexbii	$⊢ \exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r) \leftrightarrow \exists q \in ℤ ((0 \leq r \land r < \|D\|) \land N = q D + r)$
30		r19.42v	$⊢ \exists q \in ℤ ((0 \leq r \land r < \|D\|) \land N = q D + r) \leftrightarrow ((0 \leq r \land r < \|D\|) \land \exists q \in ℤ N = q D + r)$
31	29 30	bitri	$⊢ \exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r) \leftrightarrow ((0 \leq r \land r < \|D\|) \land \exists q \in ℤ N = q D + r)$
32	27 31	syl6rbbr	$⊢ (N \in ℤ \land D \in ℤ \land r \in ℤ) \to (\exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r) \leftrightarrow ((0 \leq r \land r < \|D\|) \land D ∥ (N - r)))$
33		anass	$⊢ ((0 \leq r \land r < \|D\|) \land D ∥ (N - r)) \leftrightarrow (0 \leq r \land (r < \|D\| \land D ∥ (N - r)))$
34	32 33	syl6bb	$⊢ (N \in ℤ \land D \in ℤ \land r \in ℤ) \to (\exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r) \leftrightarrow (0 \leq r \land (r < \|D\| \land D ∥ (N - r))))$
35	34	3expa	$⊢ ((N \in ℤ \land D \in ℤ) \land r \in ℤ) \to (\exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r) \leftrightarrow (0 \leq r \land (r < \|D\| \land D ∥ (N - r))))$
36	35	reubidva	$⊢ (N \in ℤ \land D \in ℤ) \to (\exists! r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r) \leftrightarrow \exists! r \in ℤ (0 \leq r \land (r < \|D\| \land D ∥ (N - r))))$
37		elnn0z	$⊢ r \in ℕ_{0} \leftrightarrow (r \in ℤ \land 0 \leq r)$
38	37	anbi1i	$⊢ (r \in ℕ_{0} \land (r < \|D\| \land D ∥ (N - r))) \leftrightarrow ((r \in ℤ \land 0 \leq r) \land (r < \|D\| \land D ∥ (N - r)))$
39		anass	$⊢ ((r \in ℤ \land 0 \leq r) \land (r < \|D\| \land D ∥ (N - r))) \leftrightarrow (r \in ℤ \land (0 \leq r \land (r < \|D\| \land D ∥ (N - r))))$
40	38 39	bitri	$⊢ (r \in ℕ_{0} \land (r < \|D\| \land D ∥ (N - r))) \leftrightarrow (r \in ℤ \land (0 \leq r \land (r < \|D\| \land D ∥ (N - r))))$
41	40	eubii	$⊢ \exists! r (r \in ℕ_{0} \land (r < \|D\| \land D ∥ (N - r))) \leftrightarrow \exists! r (r \in ℤ \land (0 \leq r \land (r < \|D\| \land D ∥ (N - r))))$
42		df-reu	$⊢ \exists! r \in ℕ_{0} (r < \|D\| \land D ∥ (N - r)) \leftrightarrow \exists! r (r \in ℕ_{0} \land (r < \|D\| \land D ∥ (N - r)))$
43		df-reu	$⊢ \exists! r \in ℤ (0 \leq r \land (r < \|D\| \land D ∥ (N - r))) \leftrightarrow \exists! r (r \in ℤ \land (0 \leq r \land (r < \|D\| \land D ∥ (N - r))))$
44	41 42 43	3bitr4ri	$⊢ \exists! r \in ℤ (0 \leq r \land (r < \|D\| \land D ∥ (N - r))) \leftrightarrow \exists! r \in ℕ_{0} (r < \|D\| \land D ∥ (N - r))$
45	36 44	syl6bb	$⊢ (N \in ℤ \land D \in ℤ) \to (\exists! r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r) \leftrightarrow \exists! r \in ℕ_{0} (r < \|D\| \land D ∥ (N - r)))$
46	45	3adant3	$⊢ (N \in ℤ \land D \in ℤ \land D \neq 0) \to (\exists! r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r) \leftrightarrow \exists! r \in ℕ_{0} (r < \|D\| \land D ∥ (N - r)))$

Metamath Proof Explorer

Theorem divalgb

Proof