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		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)$
2	1	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)$
3		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)$
4	2 3	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)$
5		zsubcl	$⊢ (N \in ℤ \land r \in ℤ) \to N - r \in ℤ$
6		divides	$⊢ (D \in ℤ \land N - r \in ℤ) \to (D ∥ (N - r) \leftrightarrow \exists q \in ℤ q D = N - r)$
7	5 6	sylan2	$⊢ (D \in ℤ \land (N \in ℤ \land r \in ℤ)) \to (D ∥ (N - r) \leftrightarrow \exists q \in ℤ q D = N - r)$
8	7	3impb	$⊢ (D \in ℤ \land N \in ℤ \land r \in ℤ) \to (D ∥ (N - r) \leftrightarrow \exists q \in ℤ q D = N - r)$
9	8	3com12	$⊢ (N \in ℤ \land D \in ℤ \land r \in ℤ) \to (D ∥ (N - r) \leftrightarrow \exists q \in ℤ q D = N - r)$
10		zcn	$⊢ N \in ℤ \to N \in ℂ$
11		zcn	$⊢ r \in ℤ \to r \in ℂ$
12		zmulcl	$⊢ (q \in ℤ \land D \in ℤ) \to q D \in ℤ$
13	12	zcnd	$⊢ (q \in ℤ \land D \in ℤ) \to q D \in ℂ$
14		subadd	$⊢ (N \in ℂ \land r \in ℂ \land q D \in ℂ) \to (N - r = q D \leftrightarrow r + q D = N)$
15	10 11 13 14	syl3an	$⊢ (N \in ℤ \land r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to (N - r = q D \leftrightarrow r + q D = N)$
16		addcom	$⊢ (r \in ℂ \land q D \in ℂ) \to r + q D = q D + r$
17	11 13 16	syl2an	$⊢ (r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to r + q D = q D + r$
18	17	3adant1	$⊢ (N \in ℤ \land r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to r + q D = q D + r$
19	18	eqeq1d	$⊢ (N \in ℤ \land r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to (r + q D = N \leftrightarrow q D + r = N)$
20	15 19	bitrd	$⊢ (N \in ℤ \land r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to (N - r = q D \leftrightarrow q D + r = N)$
21		eqcom	$⊢ N - r = q D \leftrightarrow q D = N - r$
22		eqcom	$⊢ q D + r = N \leftrightarrow N = q D + r$
23	20 21 22	3bitr3g	$⊢ (N \in ℤ \land r \in ℤ \land (q \in ℤ \land D \in ℤ)) \to (q D = N - r \leftrightarrow N = q D + r)$
24	23	3expia	$⊢ (N \in ℤ \land r \in ℤ) \to ((q \in ℤ \land D \in ℤ) \to (q D = N - r \leftrightarrow N = q D + r))$
25	24	expcomd	$⊢ (N \in ℤ \land r \in ℤ) \to (D \in ℤ \to (q \in ℤ \to (q D = N - r \leftrightarrow N = q D + r)))$
26	25	3impia	$⊢ (N \in ℤ \land r \in ℤ \land D \in ℤ) \to (q \in ℤ \to (q D = N - r \leftrightarrow N = q D + r))$
27	26	imp	$⊢ ((N \in ℤ \land r \in ℤ \land D \in ℤ) \land q \in ℤ) \to (q D = N - r \leftrightarrow N = q D + r)$
28	27	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)$
29	28	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)$
30	9 29	bitrd	$⊢ (N \in ℤ \land D \in ℤ \land r \in ℤ) \to (D ∥ (N - r) \leftrightarrow \exists q \in ℤ N = q D + r)$
31	30	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))$
32	4 31	bitr4id	$⊢ (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	bitrdi	$⊢ (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	bitrdi	$⊢ (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