gcdcllem3

	Ref	Expression
Hypotheses	gcdcllem2.1	$⊢ S = \{z \in ℤ \| \forall n \in \{M, N\} z ∥ n\}$
	gcdcllem2.2	$⊢ R = \{z \in ℤ \| (z ∥ M \land z ∥ N)\}$
Assertion	gcdcllem3	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (sup (R ℝ <) \in ℕ \land (sup (R ℝ <) ∥ M \land sup (R ℝ <) ∥ N) \land ((K \in ℤ \land K ∥ M \land K ∥ N) \to K \leq sup (R ℝ <)))$

Proof

Step	Hyp	Ref	Expression
1		gcdcllem2.1	$⊢ S = \{z \in ℤ \| \forall n \in \{M, N\} z ∥ n\}$
2		gcdcllem2.2	$⊢ R = \{z \in ℤ \| (z ∥ M \land z ∥ N)\}$
3	2	ssrab3	$⊢ R \subseteq ℤ$
4		prssi	$⊢ (M \in ℤ \land N \in ℤ) \to \{M, N\} \subseteq ℤ$
5		neorian	$⊢ (M \neq 0 \lor N \neq 0) \leftrightarrow \neg (M = 0 \land N = 0)$
6		prid1g	$⊢ M \in ℤ \to M \in \{M, N\}$
7		neeq1	$⊢ n = M \to (n \neq 0 \leftrightarrow M \neq 0)$
8	7	rspcev	$⊢ (M \in \{M, N\} \land M \neq 0) \to \exists n \in \{M, N\} n \neq 0$
9	6 8	sylan	$⊢ (M \in ℤ \land M \neq 0) \to \exists n \in \{M, N\} n \neq 0$
10	9	adantlr	$⊢ ((M \in ℤ \land N \in ℤ) \land M \neq 0) \to \exists n \in \{M, N\} n \neq 0$
11		prid2g	$⊢ N \in ℤ \to N \in \{M, N\}$
12		neeq1	$⊢ n = N \to (n \neq 0 \leftrightarrow N \neq 0)$
13	12	rspcev	$⊢ (N \in \{M, N\} \land N \neq 0) \to \exists n \in \{M, N\} n \neq 0$
14	11 13	sylan	$⊢ (N \in ℤ \land N \neq 0) \to \exists n \in \{M, N\} n \neq 0$
15	14	adantll	$⊢ ((M \in ℤ \land N \in ℤ) \land N \neq 0) \to \exists n \in \{M, N\} n \neq 0$
16	10 15	jaodan	$⊢ ((M \in ℤ \land N \in ℤ) \land (M \neq 0 \lor N \neq 0)) \to \exists n \in \{M, N\} n \neq 0$
17	5 16	sylan2br	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to \exists n \in \{M, N\} n \neq 0$
18	1	gcdcllem1	$⊢ (\{M, N\} \subseteq ℤ \land \exists n \in \{M, N\} n \neq 0) \to (S \neq \emptyset \land \exists x \in ℤ \forall y \in S y \leq x)$
19	4 17 18	syl2an2r	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (S \neq \emptyset \land \exists x \in ℤ \forall y \in S y \leq x)$
20	1 2	gcdcllem2	$⊢ (M \in ℤ \land N \in ℤ) \to R = S$
21		neeq1	$⊢ R = S \to (R \neq \emptyset \leftrightarrow S \neq \emptyset)$
22		raleq	$⊢ R = S \to (\forall y \in R y \leq x \leftrightarrow \forall y \in S y \leq x)$
23	22	rexbidv	$⊢ R = S \to (\exists x \in ℤ \forall y \in R y \leq x \leftrightarrow \exists x \in ℤ \forall y \in S y \leq x)$
24	21 23	anbi12d	$⊢ R = S \to ((R \neq \emptyset \land \exists x \in ℤ \forall y \in R y \leq x) \leftrightarrow (S \neq \emptyset \land \exists x \in ℤ \forall y \in S y \leq x))$
25	20 24	syl	$⊢ (M \in ℤ \land N \in ℤ) \to ((R \neq \emptyset \land \exists x \in ℤ \forall y \in R y \leq x) \leftrightarrow (S \neq \emptyset \land \exists x \in ℤ \forall y \in S y \leq x))$
26	25	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to ((R \neq \emptyset \land \exists x \in ℤ \forall y \in R y \leq x) \leftrightarrow (S \neq \emptyset \land \exists x \in ℤ \forall y \in S y \leq x))$
27	19 26	mpbird	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (R \neq \emptyset \land \exists x \in ℤ \forall y \in R y \leq x)$
28		suprzcl2	$⊢ (R \subseteq ℤ \land R \neq \emptyset \land \exists x \in ℤ \forall y \in R y \leq x) \to sup (R ℝ <) \in R$
29	3 28	mp3an1	$⊢ (R \neq \emptyset \land \exists x \in ℤ \forall y \in R y \leq x) \to sup (R ℝ <) \in R$
30	27 29	syl	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to sup (R ℝ <) \in R$
31	3 30	sselid	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to sup (R ℝ <) \in ℤ$
32	27	simprd	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to \exists x \in ℤ \forall y \in R y \leq x$
33		1dvds	$⊢ M \in ℤ \to 1 ∥ M$
34		1dvds	$⊢ N \in ℤ \to 1 ∥ N$
35	33 34	anim12i	$⊢ (M \in ℤ \land N \in ℤ) \to (1 ∥ M \land 1 ∥ N)$
36		1z	$⊢ 1 \in ℤ$
37		breq1	$⊢ z = 1 \to (z ∥ M \leftrightarrow 1 ∥ M)$
38		breq1	$⊢ z = 1 \to (z ∥ N \leftrightarrow 1 ∥ N)$
39	37 38	anbi12d	$⊢ z = 1 \to ((z ∥ M \land z ∥ N) \leftrightarrow (1 ∥ M \land 1 ∥ N))$
40	39 2	elrab2	$⊢ 1 \in R \leftrightarrow (1 \in ℤ \land (1 ∥ M \land 1 ∥ N))$
41	36 40	mpbiran	$⊢ 1 \in R \leftrightarrow (1 ∥ M \land 1 ∥ N)$
42	35 41	sylibr	$⊢ (M \in ℤ \land N \in ℤ) \to 1 \in R$
43	42	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to 1 \in R$
44		suprzub	$⊢ (R \subseteq ℤ \land \exists x \in ℤ \forall y \in R y \leq x \land 1 \in R) \to 1 \leq sup (R ℝ <)$
45	3 32 43 44	mp3an2i	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to 1 \leq sup (R ℝ <)$
46		elnnz1	$⊢ sup (R ℝ <) \in ℕ \leftrightarrow (sup (R ℝ <) \in ℤ \land 1 \leq sup (R ℝ <))$
47	31 45 46	sylanbrc	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to sup (R ℝ <) \in ℕ$
48		breq1	$⊢ x = sup (R ℝ <) \to (x ∥ M \leftrightarrow sup (R ℝ <) ∥ M)$
49		breq1	$⊢ x = sup (R ℝ <) \to (x ∥ N \leftrightarrow sup (R ℝ <) ∥ N)$
50	48 49	anbi12d	$⊢ x = sup (R ℝ <) \to ((x ∥ M \land x ∥ N) \leftrightarrow (sup (R ℝ <) ∥ M \land sup (R ℝ <) ∥ N))$
51		breq1	$⊢ z = x \to (z ∥ M \leftrightarrow x ∥ M)$
52		breq1	$⊢ z = x \to (z ∥ N \leftrightarrow x ∥ N)$
53	51 52	anbi12d	$⊢ z = x \to ((z ∥ M \land z ∥ N) \leftrightarrow (x ∥ M \land x ∥ N))$
54	53	cbvrabv	$⊢ \{z \in ℤ \| (z ∥ M \land z ∥ N)\} = \{x \in ℤ \| (x ∥ M \land x ∥ N)\}$
55	2 54	eqtri	$⊢ R = \{x \in ℤ \| (x ∥ M \land x ∥ N)\}$
56	50 55	elrab2	$⊢ sup (R ℝ <) \in R \leftrightarrow (sup (R ℝ <) \in ℤ \land (sup (R ℝ <) ∥ M \land sup (R ℝ <) ∥ N))$
57	30 56	sylib	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (sup (R ℝ <) \in ℤ \land (sup (R ℝ <) ∥ M \land sup (R ℝ <) ∥ N))$
58	57	simprd	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (sup (R ℝ <) ∥ M \land sup (R ℝ <) ∥ N)$
59		breq1	$⊢ z = K \to (z ∥ M \leftrightarrow K ∥ M)$
60		breq1	$⊢ z = K \to (z ∥ N \leftrightarrow K ∥ N)$
61	59 60	anbi12d	$⊢ z = K \to ((z ∥ M \land z ∥ N) \leftrightarrow (K ∥ M \land K ∥ N))$
62	61 2	elrab2	$⊢ K \in R \leftrightarrow (K \in ℤ \land (K ∥ M \land K ∥ N))$
63	62	biimpri	$⊢ (K \in ℤ \land (K ∥ M \land K ∥ N)) \to K \in R$
64	63	3impb	$⊢ (K \in ℤ \land K ∥ M \land K ∥ N) \to K \in R$
65		suprzub	$⊢ (R \subseteq ℤ \land \exists x \in ℤ \forall y \in R y \leq x \land K \in R) \to K \leq sup (R ℝ <)$
66	65	3expia	$⊢ (R \subseteq ℤ \land \exists x \in ℤ \forall y \in R y \leq x) \to (K \in R \to K \leq sup (R ℝ <))$
67	3 66	mpan	$⊢ \exists x \in ℤ \forall y \in R y \leq x \to (K \in R \to K \leq sup (R ℝ <))$
68	32 64 67	syl2im	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to ((K \in ℤ \land K ∥ M \land K ∥ N) \to K \leq sup (R ℝ <))$
69	47 58 68	3jca	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (sup (R ℝ <) \in ℕ \land (sup (R ℝ <) ∥ M \land sup (R ℝ <) ∥ N) \land ((K \in ℤ \land K ∥ M \land K ∥ N) \to K \leq sup (R ℝ <)))$

Metamath Proof Explorer

Theorem gcdcllem3

Proof