divalglem9

Description: Lemma for divalg . (Contributed by Paul Chapman, 21-Mar-2011) (Revised 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)\}$
	divalglem9.5	$⊢ R = sup (S ℝ <)$
Assertion	divalglem9	$⊢ \exists! x \in S x < \|D\|$

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		divalglem9.5	$⊢ R = sup (S ℝ <)$
6	1 2 3 4	divalglem2	$⊢ sup (S ℝ <) \in S$
7	5 6	eqeltri	$⊢ R \in S$
8	1 2 3 4 5	divalglem5	$⊢ (0 \leq R \land R < \|D\|)$
9	8	simpri	$⊢ R < \|D\|$
10		breq1	$⊢ x = R \to (x < \|D\| \leftrightarrow R < \|D\|)$
11	10	rspcev	$⊢ (R \in S \land R < \|D\|) \to \exists x \in S x < \|D\|$
12	7 9 11	mp2an	$⊢ \exists x \in S x < \|D\|$
13		oveq2	$⊢ r = x \to N - r = N - x$
14	13	breq2d	$⊢ r = x \to (D ∥ (N - r) \leftrightarrow D ∥ (N - x))$
15	14 4	elrab2	$⊢ x \in S \leftrightarrow (x \in ℕ_{0} \land D ∥ (N - x))$
16	15	simplbi	$⊢ x \in S \to x \in ℕ_{0}$
17	16	nn0zd	$⊢ x \in S \to x \in ℤ$
18		oveq2	$⊢ r = y \to N - r = N - y$
19	18	breq2d	$⊢ r = y \to (D ∥ (N - r) \leftrightarrow D ∥ (N - y))$
20	19 4	elrab2	$⊢ y \in S \leftrightarrow (y \in ℕ_{0} \land D ∥ (N - y))$
21	20	simplbi	$⊢ y \in S \to y \in ℕ_{0}$
22	21	nn0zd	$⊢ y \in S \to y \in ℤ$
23		zsubcl	$⊢ (N \in ℤ \land x \in ℤ) \to N - x \in ℤ$
24	1 23	mpan	$⊢ x \in ℤ \to N - x \in ℤ$
25		zsubcl	$⊢ (N \in ℤ \land y \in ℤ) \to N - y \in ℤ$
26	1 25	mpan	$⊢ y \in ℤ \to N - y \in ℤ$
27	24 26	anim12i	$⊢ (x \in ℤ \land y \in ℤ) \to (N - x \in ℤ \land N - y \in ℤ)$
28	17 22 27	syl2an	$⊢ (x \in S \land y \in S) \to (N - x \in ℤ \land N - y \in ℤ)$
29	15	simprbi	$⊢ x \in S \to D ∥ (N - x)$
30	20	simprbi	$⊢ y \in S \to D ∥ (N - y)$
31	29 30	anim12i	$⊢ (x \in S \land y \in S) \to (D ∥ (N - x) \land D ∥ (N - y))$
32		dvds2sub	$⊢ (D \in ℤ \land N - x \in ℤ \land N - y \in ℤ) \to ((D ∥ (N - x) \land D ∥ (N - y)) \to D ∥ (N - x - (N - y)))$
33	2 32	mp3an1	$⊢ (N - x \in ℤ \land N - y \in ℤ) \to ((D ∥ (N - x) \land D ∥ (N - y)) \to D ∥ (N - x - (N - y)))$
34	28 31 33	sylc	$⊢ (x \in S \land y \in S) \to D ∥ (N - x - (N - y))$
35		zcn	$⊢ x \in ℤ \to x \in ℂ$
36		zcn	$⊢ y \in ℤ \to y \in ℂ$
37	1	zrei	$⊢ N \in ℝ$
38	37	recni	$⊢ N \in ℂ$
39	38	subidi	$⊢ N - N = 0$
40	39	oveq1i	$⊢ N - N - (x - y) = 0 - (x - y)$
41		0cn	$⊢ 0 \in ℂ$
42		subsub2	$⊢ (0 \in ℂ \land x \in ℂ \land y \in ℂ) \to 0 - (x - y) = 0 + y - x$
43	41 42	mp3an1	$⊢ (x \in ℂ \land y \in ℂ) \to 0 - (x - y) = 0 + y - x$
44	40 43	syl5eq	$⊢ (x \in ℂ \land y \in ℂ) \to N - N - (x - y) = 0 + y - x$
45		sub4	$⊢ ((N \in ℂ \land N \in ℂ) \land (x \in ℂ \land y \in ℂ)) \to N - N - (x - y) = N - x - (N - y)$
46	38 38 45	mpanl12	$⊢ (x \in ℂ \land y \in ℂ) \to N - N - (x - y) = N - x - (N - y)$
47		subcl	$⊢ (y \in ℂ \land x \in ℂ) \to y - x \in ℂ$
48	47	ancoms	$⊢ (x \in ℂ \land y \in ℂ) \to y - x \in ℂ$
49	48	addid2d	$⊢ (x \in ℂ \land y \in ℂ) \to 0 + y - x = y - x$
50	44 46 49	3eqtr3d	$⊢ (x \in ℂ \land y \in ℂ) \to N - x - (N - y) = y - x$
51	35 36 50	syl2an	$⊢ (x \in ℤ \land y \in ℤ) \to N - x - (N - y) = y - x$
52	17 22 51	syl2an	$⊢ (x \in S \land y \in S) \to N - x - (N - y) = y - x$
53	52	breq2d	$⊢ (x \in S \land y \in S) \to (D ∥ (N - x - (N - y)) \leftrightarrow D ∥ (y - x))$
54	34 53	mpbid	$⊢ (x \in S \land y \in S) \to D ∥ (y - x)$
55		zsubcl	$⊢ (y \in ℤ \land x \in ℤ) \to y - x \in ℤ$
56	55	ancoms	$⊢ (x \in ℤ \land y \in ℤ) \to y - x \in ℤ$
57		absdvdsb	$⊢ (D \in ℤ \land y - x \in ℤ) \to (D ∥ (y - x) \leftrightarrow \|D\| ∥ (y - x))$
58	2 56 57	sylancr	$⊢ (x \in ℤ \land y \in ℤ) \to (D ∥ (y - x) \leftrightarrow \|D\| ∥ (y - x))$
59	17 22 58	syl2an	$⊢ (x \in S \land y \in S) \to (D ∥ (y - x) \leftrightarrow \|D\| ∥ (y - x))$
60	54 59	mpbid	$⊢ (x \in S \land y \in S) \to \|D\| ∥ (y - x)$
61		nnabscl	$⊢ (D \in ℤ \land D \neq 0) \to \|D\| \in ℕ$
62	2 3 61	mp2an	$⊢ \|D\| \in ℕ$
63	62	nnzi	$⊢ \|D\| \in ℤ$
64		divides	$⊢ (\|D\| \in ℤ \land y - x \in ℤ) \to (\|D\| ∥ (y - x) \leftrightarrow \exists k \in ℤ k \|D\| = y - x)$
65	63 56 64	sylancr	$⊢ (x \in ℤ \land y \in ℤ) \to (\|D\| ∥ (y - x) \leftrightarrow \exists k \in ℤ k \|D\| = y - x)$
66	17 22 65	syl2an	$⊢ (x \in S \land y \in S) \to (\|D\| ∥ (y - x) \leftrightarrow \exists k \in ℤ k \|D\| = y - x)$
67	60 66	mpbid	$⊢ (x \in S \land y \in S) \to \exists k \in ℤ k \|D\| = y - x$
68	67	adantr	$⊢ ((x \in S \land y \in S) \land (x < \|D\| \land y < \|D\|)) \to \exists k \in ℤ k \|D\| = y - x$
69	1 2 3 4	divalglem8	$⊢ ((x \in S \land y \in S) \land (x < \|D\| \land y < \|D\|)) \to (k \in ℤ \to (k \|D\| = y - x \to x = y))$
70	69	rexlimdv	$⊢ ((x \in S \land y \in S) \land (x < \|D\| \land y < \|D\|)) \to (\exists k \in ℤ k \|D\| = y - x \to x = y)$
71	68 70	mpd	$⊢ ((x \in S \land y \in S) \land (x < \|D\| \land y < \|D\|)) \to x = y$
72	71	ex	$⊢ (x \in S \land y \in S) \to ((x < \|D\| \land y < \|D\|) \to x = y)$
73	72	rgen2	$⊢ \forall x \in S \forall y \in S ((x < \|D\| \land y < \|D\|) \to x = y)$
74		breq1	$⊢ x = y \to (x < \|D\| \leftrightarrow y < \|D\|)$
75	74	reu4	$⊢ \exists! x \in S x < \|D\| \leftrightarrow (\exists x \in S x < \|D\| \land \forall x \in S \forall y \in S ((x < \|D\| \land y < \|D\|) \to x = y))$
76	12 73 75	mpbir2an	$⊢ \exists! x \in S x < \|D\|$

Metamath Proof Explorer

Theorem divalglem9

Proof