Theorem gcdcllem1

Description: Lemma for gcdn0cl , gcddvds and dvdslegcd . (Contributed by Paul Chapman, 21-Mar-2011)

	Ref	Expression
Hypothesis	gcdcllem1.1	$$⊢S=\left\{z\in \mathbb{Z}|\forall n\in Az\parallel n\right\}$$
Assertion	gcdcllem1	$$⊢\left(A\subseteq \mathbb{Z}\wedge \exists n\in An\ne 0\right)\to \left(S\ne \varnothing \wedge \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)$$

Proof

Step	Hyp	Ref	Expression
1		gcdcllem1.1	$$⊢S=\left\{z\in \mathbb{Z}|\forall n\in Az\parallel n\right\}$$
2		1z	$$⊢1\in \mathbb{Z}$$
3		ssel	$$⊢A\subseteq \mathbb{Z}\to \left(n\in A\to n\in \mathbb{Z}\right)$$
4		1dvds	$$⊢n\in \mathbb{Z}\to 1\parallel n$$
5	3 4	syl6	$$⊢A\subseteq \mathbb{Z}\to \left(n\in A\to 1\parallel n\right)$$
6	5	ralrimiv	$$⊢A\subseteq \mathbb{Z}\to \forall n\in A1\parallel n$$
7		breq1	$$⊢z=1\to \left(z\parallel n\leftrightarrow 1\parallel n\right)$$
8	7	ralbidv	$$⊢z=1\to \left(\forall n\in Az\parallel n\leftrightarrow \forall n\in A1\parallel n\right)$$
9	8 1	elrab2	$$⊢1\in S\leftrightarrow \left(1\in \mathbb{Z}\wedge \forall n\in A1\parallel n\right)$$
10	9	biimpri	$$⊢\left(1\in \mathbb{Z}\wedge \forall n\in A1\parallel n\right)\to 1\in S$$
11	2 6 10	sylancr	$$⊢A\subseteq \mathbb{Z}\to 1\in S$$
12	11	ne0d	$$⊢A\subseteq \mathbb{Z}\to S\ne \varnothing$$
13	12	adantr	$$⊢\left(A\subseteq \mathbb{Z}\wedge \exists n\in An\ne 0\right)\to S\ne \varnothing$$
14		neeq1	$$⊢n=w\to \left(n\ne 0\leftrightarrow w\ne 0\right)$$
15	14	cbvrexvw	$$⊢\exists n\in An\ne 0\leftrightarrow \exists w\in Aw\ne 0$$
16		breq1	$$⊢z=y\to \left(z\parallel n\leftrightarrow y\parallel n\right)$$
17	16	ralbidv	$$⊢z=y\to \left(\forall n\in Az\parallel n\leftrightarrow \forall n\in Ay\parallel n\right)$$
18	17 1	elrab2	$$⊢y\in S\leftrightarrow \left(y\in \mathbb{Z}\wedge \forall n\in Ay\parallel n\right)$$
19	18	simprbi	$$⊢y\in S\to \forall n\in Ay\parallel n$$
20	18	simplbi	$$⊢y\in S\to y\in \mathbb{Z}$$
21		ssel2	$$⊢\left(A\subseteq \mathbb{Z}\wedge n\in A\right)\to n\in \mathbb{Z}$$
22		dvdsleabs	$$⊢\left(y\in \mathbb{Z}\wedge n\in \mathbb{Z}\wedge n\ne 0\right)\to \left(y\parallel n\to y\le \left|n\right|\right)$$
23	22	3expia	$$⊢\left(y\in \mathbb{Z}\wedge n\in \mathbb{Z}\right)\to \left(n\ne 0\to \left(y\parallel n\to y\le \left|n\right|\right)\right)$$
24	21 23	sylan2	$$⊢\left(y\in \mathbb{Z}\wedge \left(A\subseteq \mathbb{Z}\wedge n\in A\right)\right)\to \left(n\ne 0\to \left(y\parallel n\to y\le \left|n\right|\right)\right)$$
25	24	anassrs	$$⊢\left(\left(y\in \mathbb{Z}\wedge A\subseteq \mathbb{Z}\right)\wedge n\in A\right)\to \left(n\ne 0\to \left(y\parallel n\to y\le \left|n\right|\right)\right)$$
26	25	com23	$$⊢\left(\left(y\in \mathbb{Z}\wedge A\subseteq \mathbb{Z}\right)\wedge n\in A\right)\to \left(y\parallel n\to \left(n\ne 0\to y\le \left|n\right|\right)\right)$$
27	26	ralrimiva	$$⊢\left(y\in \mathbb{Z}\wedge A\subseteq \mathbb{Z}\right)\to \forall n\in A\left(y\parallel n\to \left(n\ne 0\to y\le \left|n\right|\right)\right)$$
28	27	ancoms	$$⊢\left(A\subseteq \mathbb{Z}\wedge y\in \mathbb{Z}\right)\to \forall n\in A\left(y\parallel n\to \left(n\ne 0\to y\le \left|n\right|\right)\right)$$
29	20 28	sylan2	$$⊢\left(A\subseteq \mathbb{Z}\wedge y\in S\right)\to \forall n\in A\left(y\parallel n\to \left(n\ne 0\to y\le \left|n\right|\right)\right)$$
30		r19.26	$$⊢\forall n\in A\left(y\parallel n\wedge \left(y\parallel n\to \left(n\ne 0\to y\le \left|n\right|\right)\right)\right)\leftrightarrow \left(\forall n\in Ay\parallel n\wedge \forall n\in A\left(y\parallel n\to \left(n\ne 0\to y\le \left|n\right|\right)\right)\right)$$
31		pm3.35	$$⊢\left(y\parallel n\wedge \left(y\parallel n\to \left(n\ne 0\to y\le \left|n\right|\right)\right)\right)\to \left(n\ne 0\to y\le \left|n\right|\right)$$
32	31	ralimi	$$⊢\forall n\in A\left(y\parallel n\wedge \left(y\parallel n\to \left(n\ne 0\to y\le \left|n\right|\right)\right)\right)\to \forall n\in A\left(n\ne 0\to y\le \left|n\right|\right)$$
33	30 32	sylbir	$$⊢\left(\forall n\in Ay\parallel n\wedge \forall n\in A\left(y\parallel n\to \left(n\ne 0\to y\le \left|n\right|\right)\right)\right)\to \forall n\in A\left(n\ne 0\to y\le \left|n\right|\right)$$
34	19 29 33	syl2an2	$$⊢\left(A\subseteq \mathbb{Z}\wedge y\in S\right)\to \forall n\in A\left(n\ne 0\to y\le \left|n\right|\right)$$
35	34	ralrimiva	$$⊢A\subseteq \mathbb{Z}\to \forall y\in S\forall n\in A\left(n\ne 0\to y\le \left|n\right|\right)$$
36		fveq2	$$⊢n=w\to \left|n\right|=\left|w\right|$$
37	36	breq2d	$$⊢n=w\to \left(y\le \left|n\right|\leftrightarrow y\le \left|w\right|\right)$$
38	14 37	imbi12d	$$⊢n=w\to \left(\left(n\ne 0\to y\le \left|n\right|\right)\leftrightarrow \left(w\ne 0\to y\le \left|w\right|\right)\right)$$
39	38	cbvralvw	$$⊢\forall n\in A\left(n\ne 0\to y\le \left|n\right|\right)\leftrightarrow \forall w\in A\left(w\ne 0\to y\le \left|w\right|\right)$$
40	39	ralbii	$$⊢\forall y\in S\forall n\in A\left(n\ne 0\to y\le \left|n\right|\right)\leftrightarrow \forall y\in S\forall w\in A\left(w\ne 0\to y\le \left|w\right|\right)$$
41		ralcom	$$⊢\forall y\in S\forall w\in A\left(w\ne 0\to y\le \left|w\right|\right)\leftrightarrow \forall w\in A\forall y\in S\left(w\ne 0\to y\le \left|w\right|\right)$$
42		r19.21v	$$⊢\forall y\in S\left(w\ne 0\to y\le \left|w\right|\right)\leftrightarrow \left(w\ne 0\to \forall y\in Sy\le \left|w\right|\right)$$
43	42	ralbii	$$⊢\forall w\in A\forall y\in S\left(w\ne 0\to y\le \left|w\right|\right)\leftrightarrow \forall w\in A\left(w\ne 0\to \forall y\in Sy\le \left|w\right|\right)$$
44	40 41 43	3bitri	$$⊢\forall y\in S\forall n\in A\left(n\ne 0\to y\le \left|n\right|\right)\leftrightarrow \forall w\in A\left(w\ne 0\to \forall y\in Sy\le \left|w\right|\right)$$
45	35 44	sylib	$$⊢A\subseteq \mathbb{Z}\to \forall w\in A\left(w\ne 0\to \forall y\in Sy\le \left|w\right|\right)$$
46		ssel2	$$⊢\left(A\subseteq \mathbb{Z}\wedge w\in A\right)\to w\in \mathbb{Z}$$
47		nn0abscl	$$⊢w\in \mathbb{Z}\to \left|w\right|\in {\mathbb{N}}_0$$
48	46 47	syl	$$⊢\left(A\subseteq \mathbb{Z}\wedge w\in A\right)\to \left|w\right|\in {\mathbb{N}}_0$$
49	48	nn0zd	$$⊢\left(A\subseteq \mathbb{Z}\wedge w\in A\right)\to \left|w\right|\in \mathbb{Z}$$
50		breq2	$$⊢x=\left|w\right|\to \left(y\le x\leftrightarrow y\le \left|w\right|\right)$$
51	50	ralbidv	$$⊢x=\left|w\right|\to \left(\forall y\in Sy\le x\leftrightarrow \forall y\in Sy\le \left|w\right|\right)$$
52	51	adantl	$$⊢\left(\left(A\subseteq \mathbb{Z}\wedge w\in A\right)\wedge x=\left|w\right|\right)\to \left(\forall y\in Sy\le x\leftrightarrow \forall y\in Sy\le \left|w\right|\right)$$
53	49 52	rspcedv	$$⊢\left(A\subseteq \mathbb{Z}\wedge w\in A\right)\to \left(\forall y\in Sy\le \left|w\right|\to \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)$$
54	53	imim2d	$$⊢\left(A\subseteq \mathbb{Z}\wedge w\in A\right)\to \left(\left(w\ne 0\to \forall y\in Sy\le \left|w\right|\right)\to \left(w\ne 0\to \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)\right)$$
55	54	ralimdva	$$⊢A\subseteq \mathbb{Z}\to \left(\forall w\in A\left(w\ne 0\to \forall y\in Sy\le \left|w\right|\right)\to \forall w\in A\left(w\ne 0\to \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)\right)$$
56	45 55	mpd	$$⊢A\subseteq \mathbb{Z}\to \forall w\in A\left(w\ne 0\to \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)$$
57		r19.23v	$$⊢\forall w\in A\left(w\ne 0\to \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)\leftrightarrow \left(\exists w\in Aw\ne 0\to \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)$$
58	56 57	sylib	$$⊢A\subseteq \mathbb{Z}\to \left(\exists w\in Aw\ne 0\to \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)$$
59	58	imp	$$⊢\left(A\subseteq \mathbb{Z}\wedge \exists w\in Aw\ne 0\right)\to \exists x\in \mathbb{Z}\forall y\in Sy\le x$$
60	15 59	sylan2b	$$⊢\left(A\subseteq \mathbb{Z}\wedge \exists n\in An\ne 0\right)\to \exists x\in \mathbb{Z}\forall y\in Sy\le x$$
61	13 60	jca	$$⊢\left(A\subseteq \mathbb{Z}\wedge \exists n\in An\ne 0\right)\to \left(S\ne \varnothing \wedge \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)$$