divalglem10

Description: Lemma for divalg . (Contributed by Paul Chapman, 21-Mar-2011) (Proof shortened by AV, 2-Oct-2020)

	Ref	Expression
Hypotheses	divalglem8.1	$⊢ N \in ℤ$
	divalglem8.2	$⊢ D \in ℤ$
	divalglem8.3	$⊢ D \neq 0$
	divalglem8.4	$⊢ S = \{r \in ℕ_{0} \| D ∥ (N - r)\}$
Assertion	divalglem10	$⊢ \exists! r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r)$

Proof

Step	Hyp	Ref	Expression
1		divalglem8.1	$⊢ N \in ℤ$
2		divalglem8.2	$⊢ D \in ℤ$
3		divalglem8.3	$⊢ D \neq 0$
4		divalglem8.4	$⊢ S = \{r \in ℕ_{0} \| D ∥ (N - r)\}$
5		eqid	$⊢ sup (S ℝ <) = sup (S ℝ <)$
6	1 2 3 4 5	divalglem9	$⊢ \exists! x \in S x < \|D\|$
7		elnn0z	$⊢ x \in ℕ_{0} \leftrightarrow (x \in ℤ \land 0 \leq x)$
8	7	anbi2i	$⊢ (x < \|D\| \land x \in ℕ_{0}) \leftrightarrow (x < \|D\| \land (x \in ℤ \land 0 \leq x))$
9		an12	$⊢ (x < \|D\| \land (x \in ℤ \land 0 \leq x)) \leftrightarrow (x \in ℤ \land (x < \|D\| \land 0 \leq x))$
10		ancom	$⊢ (x < \|D\| \land 0 \leq x) \leftrightarrow (0 \leq x \land x < \|D\|)$
11	10	anbi2i	$⊢ (x \in ℤ \land (x < \|D\| \land 0 \leq x)) \leftrightarrow (x \in ℤ \land (0 \leq x \land x < \|D\|))$
12	9 11	bitri	$⊢ (x < \|D\| \land (x \in ℤ \land 0 \leq x)) \leftrightarrow (x \in ℤ \land (0 \leq x \land x < \|D\|))$
13	8 12	bitri	$⊢ (x < \|D\| \land x \in ℕ_{0}) \leftrightarrow (x \in ℤ \land (0 \leq x \land x < \|D\|))$
14	13	anbi1i	$⊢ ((x < \|D\| \land x \in ℕ_{0}) \land \exists q \in ℤ N = q D + x) \leftrightarrow ((x \in ℤ \land (0 \leq x \land x < \|D\|)) \land \exists q \in ℤ N = q D + x)$
15		anass	$⊢ ((x \in ℤ \land (0 \leq x \land x < \|D\|)) \land \exists q \in ℤ N = q D + x) \leftrightarrow (x \in ℤ \land ((0 \leq x \land x < \|D\|) \land \exists q \in ℤ N = q D + x))$
16	14 15	bitri	$⊢ ((x < \|D\| \land x \in ℕ_{0}) \land \exists q \in ℤ N = q D + x) \leftrightarrow (x \in ℤ \land ((0 \leq x \land x < \|D\|) \land \exists q \in ℤ N = q D + x))$
17		oveq2	$⊢ r = x \to q D + r = q D + x$
18	17	eqeq2d	$⊢ r = x \to (N = q D + r \leftrightarrow N = q D + x)$
19	18	rexbidv	$⊢ r = x \to (\exists q \in ℤ N = q D + r \leftrightarrow \exists q \in ℤ N = q D + x)$
20	1 2 3 4	divalglem4	$⊢ S = \{r \in ℕ_{0} \| \exists q \in ℤ N = q D + r\}$
21	19 20	elrab2	$⊢ x \in S \leftrightarrow (x \in ℕ_{0} \land \exists q \in ℤ N = q D + x)$
22	21	anbi2i	$⊢ (x < \|D\| \land x \in S) \leftrightarrow (x < \|D\| \land (x \in ℕ_{0} \land \exists q \in ℤ N = q D + x))$
23		ancom	$⊢ (x \in S \land x < \|D\|) \leftrightarrow (x < \|D\| \land x \in S)$
24		anass	$⊢ ((x < \|D\| \land x \in ℕ_{0}) \land \exists q \in ℤ N = q D + x) \leftrightarrow (x < \|D\| \land (x \in ℕ_{0} \land \exists q \in ℤ N = q D + x))$
25	22 23 24	3bitr4i	$⊢ (x \in S \land x < \|D\|) \leftrightarrow ((x < \|D\| \land x \in ℕ_{0}) \land \exists q \in ℤ N = q D + x)$
26		df-3an	$⊢ (0 \leq x \land x < \|D\| \land N = q D + x) \leftrightarrow ((0 \leq x \land x < \|D\|) \land N = q D + x)$
27	26	rexbii	$⊢ \exists q \in ℤ (0 \leq x \land x < \|D\| \land N = q D + x) \leftrightarrow \exists q \in ℤ ((0 \leq x \land x < \|D\|) \land N = q D + x)$
28		r19.42v	$⊢ \exists q \in ℤ ((0 \leq x \land x < \|D\|) \land N = q D + x) \leftrightarrow ((0 \leq x \land x < \|D\|) \land \exists q \in ℤ N = q D + x)$
29	27 28	bitri	$⊢ \exists q \in ℤ (0 \leq x \land x < \|D\| \land N = q D + x) \leftrightarrow ((0 \leq x \land x < \|D\|) \land \exists q \in ℤ N = q D + x)$
30	29	anbi2i	$⊢ (x \in ℤ \land \exists q \in ℤ (0 \leq x \land x < \|D\| \land N = q D + x)) \leftrightarrow (x \in ℤ \land ((0 \leq x \land x < \|D\|) \land \exists q \in ℤ N = q D + x))$
31	16 25 30	3bitr4i	$⊢ (x \in S \land x < \|D\|) \leftrightarrow (x \in ℤ \land \exists q \in ℤ (0 \leq x \land x < \|D\| \land N = q D + x))$
32	31	eubii	$⊢ \exists! x (x \in S \land x < \|D\|) \leftrightarrow \exists! x (x \in ℤ \land \exists q \in ℤ (0 \leq x \land x < \|D\| \land N = q D + x))$
33		df-reu	$⊢ \exists! x \in S x < \|D\| \leftrightarrow \exists! x (x \in S \land x < \|D\|)$
34		df-reu	$⊢ \exists! x \in ℤ \exists q \in ℤ (0 \leq x \land x < \|D\| \land N = q D + x) \leftrightarrow \exists! x (x \in ℤ \land \exists q \in ℤ (0 \leq x \land x < \|D\| \land N = q D + x))$
35	32 33 34	3bitr4i	$⊢ \exists! x \in S x < \|D\| \leftrightarrow \exists! x \in ℤ \exists q \in ℤ (0 \leq x \land x < \|D\| \land N = q D + x)$
36	6 35	mpbi	$⊢ \exists! x \in ℤ \exists q \in ℤ (0 \leq x \land x < \|D\| \land N = q D + x)$
37		breq2	$⊢ x = r \to (0 \leq x \leftrightarrow 0 \leq r)$
38		breq1	$⊢ x = r \to (x < \|D\| \leftrightarrow r < \|D\|)$
39		oveq2	$⊢ x = r \to q D + x = q D + r$
40	39	eqeq2d	$⊢ x = r \to (N = q D + x \leftrightarrow N = q D + r)$
41	37 38 40	3anbi123d	$⊢ x = r \to ((0 \leq x \land x < \|D\| \land N = q D + x) \leftrightarrow (0 \leq r \land r < \|D\| \land N = q D + r))$
42	41	rexbidv	$⊢ x = r \to (\exists q \in ℤ (0 \leq x \land x < \|D\| \land N = q D + x) \leftrightarrow \exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r))$
43	42	cbvreuvw	$⊢ \exists! x \in ℤ \exists q \in ℤ (0 \leq x \land x < \|D\| \land N = q D + x) \leftrightarrow \exists! r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r)$
44	36 43	mpbi	$⊢ \exists! r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|D\| \land N = q D + r)$

Metamath Proof Explorer

Theorem divalglem10

Proof