dfgcd2

Description: Alternate definition of the gcd operator, see definition in ApostolNT p. 15. (Contributed by AV, 8-Aug-2021)

		Ref	Expression
	Assertion	dfgcd2	$⊢ (M \in ℤ \land N \in ℤ) \to (D = M \gcd N \leftrightarrow (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))$

Proof

Step	Hyp	Ref	Expression
1		gcdcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℕ_{0}$
2	1	nn0ge0d	$⊢ (M \in ℤ \land N \in ℤ) \to 0 \leq M \gcd N$
3		gcddvds	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
4		3anass	$⊢ (e \in ℤ \land M \in ℤ \land N \in ℤ) \leftrightarrow (e \in ℤ \land (M \in ℤ \land N \in ℤ))$
5	4	biancomi	$⊢ (e \in ℤ \land M \in ℤ \land N \in ℤ) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land e \in ℤ)$
6		dvdsgcd	$⊢ (e \in ℤ \land M \in ℤ \land N \in ℤ) \to ((e ∥ M \land e ∥ N) \to e ∥ (M \gcd N))$
7	5 6	sylbir	$⊢ ((M \in ℤ \land N \in ℤ) \land e \in ℤ) \to ((e ∥ M \land e ∥ N) \to e ∥ (M \gcd N))$
8	7	ralrimiva	$⊢ (M \in ℤ \land N \in ℤ) \to \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ (M \gcd N))$
9	2 3 8	3jca	$⊢ (M \in ℤ \land N \in ℤ) \to (0 \leq M \gcd N \land ((M \gcd N) ∥ M \land (M \gcd N) ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ (M \gcd N)))$
10	9	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land D = M \gcd N) \to (0 \leq M \gcd N \land ((M \gcd N) ∥ M \land (M \gcd N) ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ (M \gcd N)))$
11		breq2	$⊢ D = M \gcd N \to (0 \leq D \leftrightarrow 0 \leq M \gcd N)$
12		breq1	$⊢ D = M \gcd N \to (D ∥ M \leftrightarrow (M \gcd N) ∥ M)$
13		breq1	$⊢ D = M \gcd N \to (D ∥ N \leftrightarrow (M \gcd N) ∥ N)$
14	12 13	anbi12d	$⊢ D = M \gcd N \to ((D ∥ M \land D ∥ N) \leftrightarrow ((M \gcd N) ∥ M \land (M \gcd N) ∥ N))$
15		breq2	$⊢ D = M \gcd N \to (e ∥ D \leftrightarrow e ∥ (M \gcd N))$
16	15	imbi2d	$⊢ D = M \gcd N \to (((e ∥ M \land e ∥ N) \to e ∥ D) \leftrightarrow ((e ∥ M \land e ∥ N) \to e ∥ (M \gcd N)))$
17	16	ralbidv	$⊢ D = M \gcd N \to (\forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D) \leftrightarrow \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ (M \gcd N)))$
18	11 14 17	3anbi123d	$⊢ D = M \gcd N \to ((0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)) \leftrightarrow (0 \leq M \gcd N \land ((M \gcd N) ∥ M \land (M \gcd N) ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ (M \gcd N))))$
19	18	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land D = M \gcd N) \to ((0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)) \leftrightarrow (0 \leq M \gcd N \land ((M \gcd N) ∥ M \land (M \gcd N) ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ (M \gcd N))))$
20	10 19	mpbird	$⊢ ((M \in ℤ \land N \in ℤ) \land D = M \gcd N) \to (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D))$
21		gcdval	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N = if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <))$
22	21	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D))) \to M \gcd N = if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <))$
23		iftrue	$⊢ (M = 0 \land N = 0) \to if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)) = 0$
24	23	adantr	$⊢ ((M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \to if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)) = 0$
25		breq2	$⊢ M = 0 \to (D ∥ M \leftrightarrow D ∥ 0)$
26		breq2	$⊢ N = 0 \to (D ∥ N \leftrightarrow D ∥ 0)$
27	25 26	bi2anan9	$⊢ (M = 0 \land N = 0) \to ((D ∥ M \land D ∥ N) \leftrightarrow (D ∥ 0 \land D ∥ 0))$
28		breq2	$⊢ M = 0 \to (e ∥ M \leftrightarrow e ∥ 0)$
29		breq2	$⊢ N = 0 \to (e ∥ N \leftrightarrow e ∥ 0)$
30	28 29	bi2anan9	$⊢ (M = 0 \land N = 0) \to ((e ∥ M \land e ∥ N) \leftrightarrow (e ∥ 0 \land e ∥ 0))$
31	30	imbi1d	$⊢ (M = 0 \land N = 0) \to (((e ∥ M \land e ∥ N) \to e ∥ D) \leftrightarrow ((e ∥ 0 \land e ∥ 0) \to e ∥ D))$
32	31	ralbidv	$⊢ (M = 0 \land N = 0) \to (\forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D) \leftrightarrow \forall e \in ℤ ((e ∥ 0 \land e ∥ 0) \to e ∥ D))$
33	27 32	3anbi23d	$⊢ (M = 0 \land N = 0) \to ((0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)) \leftrightarrow (0 \leq D \land (D ∥ 0 \land D ∥ 0) \land \forall e \in ℤ ((e ∥ 0 \land e ∥ 0) \to e ∥ D)))$
34		dvdszrcl	$⊢ D ∥ 0 \to (D \in ℤ \land 0 \in ℤ)$
35		dvds0	$⊢ e \in ℤ \to e ∥ 0$
36	35 35	jca	$⊢ e \in ℤ \to (e ∥ 0 \land e ∥ 0)$
37	36	adantl	$⊢ ((D \in ℤ \land 0 \leq D) \land e \in ℤ) \to (e ∥ 0 \land e ∥ 0)$
38		pm5.5	$⊢ (e ∥ 0 \land e ∥ 0) \to (((e ∥ 0 \land e ∥ 0) \to e ∥ D) \leftrightarrow e ∥ D)$
39	37 38	syl	$⊢ ((D \in ℤ \land 0 \leq D) \land e \in ℤ) \to (((e ∥ 0 \land e ∥ 0) \to e ∥ D) \leftrightarrow e ∥ D)$
40	39	ralbidva	$⊢ (D \in ℤ \land 0 \leq D) \to (\forall e \in ℤ ((e ∥ 0 \land e ∥ 0) \to e ∥ D) \leftrightarrow \forall e \in ℤ e ∥ D)$
41		0z	$⊢ 0 \in ℤ$
42		breq1	$⊢ e = 0 \to (e ∥ D \leftrightarrow 0 ∥ D)$
43	42	rspcv	$⊢ 0 \in ℤ \to (\forall e \in ℤ e ∥ D \to 0 ∥ D)$
44	41 43	ax-mp	$⊢ \forall e \in ℤ e ∥ D \to 0 ∥ D$
45		0dvds	$⊢ D \in ℤ \to (0 ∥ D \leftrightarrow D = 0)$
46	45	biimpd	$⊢ D \in ℤ \to (0 ∥ D \to D = 0)$
47		eqcom	$⊢ 0 = D \leftrightarrow D = 0$
48	46 47	imbitrrdi	$⊢ D \in ℤ \to (0 ∥ D \to 0 = D)$
49	44 48	syl5	$⊢ D \in ℤ \to (\forall e \in ℤ e ∥ D \to 0 = D)$
50	49	adantr	$⊢ (D \in ℤ \land 0 \leq D) \to (\forall e \in ℤ e ∥ D \to 0 = D)$
51	40 50	sylbid	$⊢ (D \in ℤ \land 0 \leq D) \to (\forall e \in ℤ ((e ∥ 0 \land e ∥ 0) \to e ∥ D) \to 0 = D)$
52	51	ex	$⊢ D \in ℤ \to (0 \leq D \to (\forall e \in ℤ ((e ∥ 0 \land e ∥ 0) \to e ∥ D) \to 0 = D))$
53	52	adantr	$⊢ (D \in ℤ \land 0 \in ℤ) \to (0 \leq D \to (\forall e \in ℤ ((e ∥ 0 \land e ∥ 0) \to e ∥ D) \to 0 = D))$
54	34 53	syl	$⊢ D ∥ 0 \to (0 \leq D \to (\forall e \in ℤ ((e ∥ 0 \land e ∥ 0) \to e ∥ D) \to 0 = D))$
55	54	adantr	$⊢ (D ∥ 0 \land D ∥ 0) \to (0 \leq D \to (\forall e \in ℤ ((e ∥ 0 \land e ∥ 0) \to e ∥ D) \to 0 = D))$
56	55	3imp21	$⊢ (0 \leq D \land (D ∥ 0 \land D ∥ 0) \land \forall e \in ℤ ((e ∥ 0 \land e ∥ 0) \to e ∥ D)) \to 0 = D$
57	33 56	biimtrdi	$⊢ (M = 0 \land N = 0) \to ((0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)) \to 0 = D)$
58	57	adantld	$⊢ (M = 0 \land N = 0) \to (((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D))) \to 0 = D)$
59	58	imp	$⊢ ((M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \to 0 = D$
60	24 59	eqtrd	$⊢ ((M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \to if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)) = D$
61		iffalse	$⊢ \neg (M = 0 \land N = 0) \to if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)) = sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)$
62	61	adantr	$⊢ (\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \to if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)) = sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)$
63		ltso	$⊢ < Or ℝ$
64	63	a1i	$⊢ (\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \to < Or ℝ$
65		dvdszrcl	$⊢ D ∥ M \to (D \in ℤ \land M \in ℤ)$
66	65	simpld	$⊢ D ∥ M \to D \in ℤ$
67	66	zred	$⊢ D ∥ M \to D \in ℝ$
68	67	adantr	$⊢ (D ∥ M \land D ∥ N) \to D \in ℝ$
69	68	3ad2ant2	$⊢ (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)) \to D \in ℝ$
70	69	ad2antll	$⊢ (\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \to D \in ℝ$
71		breq1	$⊢ n = y \to (n ∥ M \leftrightarrow y ∥ M)$
72		breq1	$⊢ n = y \to (n ∥ N \leftrightarrow y ∥ N)$
73	71 72	anbi12d	$⊢ n = y \to ((n ∥ M \land n ∥ N) \leftrightarrow (y ∥ M \land y ∥ N))$
74	73	elrab	$⊢ y \in \{n \in ℤ \| (n ∥ M \land n ∥ N)\} \leftrightarrow (y \in ℤ \land (y ∥ M \land y ∥ N))$
75		breq1	$⊢ e = y \to (e ∥ M \leftrightarrow y ∥ M)$
76		breq1	$⊢ e = y \to (e ∥ N \leftrightarrow y ∥ N)$
77	75 76	anbi12d	$⊢ e = y \to ((e ∥ M \land e ∥ N) \leftrightarrow (y ∥ M \land y ∥ N))$
78		breq1	$⊢ e = y \to (e ∥ D \leftrightarrow y ∥ D)$
79	77 78	imbi12d	$⊢ e = y \to (((e ∥ M \land e ∥ N) \to e ∥ D) \leftrightarrow ((y ∥ M \land y ∥ N) \to y ∥ D))$
80	79	rspcv	$⊢ y \in ℤ \to (\forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D) \to ((y ∥ M \land y ∥ N) \to y ∥ D))$
81	80	com23	$⊢ y \in ℤ \to ((y ∥ M \land y ∥ N) \to (\forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D) \to y ∥ D))$
82	81	imp	$⊢ (y \in ℤ \land (y ∥ M \land y ∥ N)) \to (\forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D) \to y ∥ D)$
83	82	ad2antrr	$⊢ (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \land (M \in ℤ \land N \in ℤ)) \to (\forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D) \to y ∥ D)$
84		elnn0z	$⊢ D \in ℕ_{0} \leftrightarrow (D \in ℤ \land 0 \leq D)$
85	84	simplbi2	$⊢ D \in ℤ \to (0 \leq D \to D \in ℕ_{0})$
86	85	adantr	$⊢ (D \in ℤ \land M \in ℤ) \to (0 \leq D \to D \in ℕ_{0})$
87	65 86	syl	$⊢ D ∥ M \to (0 \leq D \to D \in ℕ_{0})$
88	87	adantr	$⊢ (D ∥ M \land D ∥ N) \to (0 \leq D \to D \in ℕ_{0})$
89	88	impcom	$⊢ (0 \leq D \land (D ∥ M \land D ∥ N)) \to D \in ℕ_{0}$
90		simp-4l	$⊢ ((((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \land D \in ℕ_{0}) \land (0 \leq D \land (D ∥ M \land D ∥ N))) \to y \in ℤ$
91		elnn0	$⊢ D \in ℕ_{0} \leftrightarrow (D \in ℕ \lor D = 0)$
92		2a1	$⊢ D \in ℕ \to (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to D \in ℕ))$
93		breq1	$⊢ D = 0 \to (D ∥ M \leftrightarrow 0 ∥ M)$
94		breq1	$⊢ D = 0 \to (D ∥ N \leftrightarrow 0 ∥ N)$
95	93 94	anbi12d	$⊢ D = 0 \to ((D ∥ M \land D ∥ N) \leftrightarrow (0 ∥ M \land 0 ∥ N))$
96	95	anbi2d	$⊢ D = 0 \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \leftrightarrow (0 \leq D \land (0 ∥ M \land 0 ∥ N)))$
97	96	adantr	$⊢ (D = 0 \land ((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0))) \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \leftrightarrow (0 \leq D \land (0 ∥ M \land 0 ∥ N)))$
98		ianor	$⊢ \neg (M = 0 \land N = 0) \leftrightarrow (\neg M = 0 \lor \neg N = 0)$
99		dvdszrcl	$⊢ 0 ∥ M \to (0 \in ℤ \land M \in ℤ)$
100		0dvds	$⊢ M \in ℤ \to (0 ∥ M \leftrightarrow M = 0)$
101		pm2.24	$⊢ M = 0 \to (\neg M = 0 \to D \in ℕ)$
102	100 101	biimtrdi	$⊢ M \in ℤ \to (0 ∥ M \to (\neg M = 0 \to D \in ℕ))$
103	102	adantl	$⊢ (0 \in ℤ \land M \in ℤ) \to (0 ∥ M \to (\neg M = 0 \to D \in ℕ))$
104	99 103	mpcom	$⊢ 0 ∥ M \to (\neg M = 0 \to D \in ℕ)$
105	104	adantr	$⊢ (0 ∥ M \land 0 ∥ N) \to (\neg M = 0 \to D \in ℕ)$
106	105	com12	$⊢ \neg M = 0 \to ((0 ∥ M \land 0 ∥ N) \to D \in ℕ)$
107		dvdszrcl	$⊢ 0 ∥ N \to (0 \in ℤ \land N \in ℤ)$
108		0dvds	$⊢ N \in ℤ \to (0 ∥ N \leftrightarrow N = 0)$
109		pm2.24	$⊢ N = 0 \to (\neg N = 0 \to D \in ℕ)$
110	108 109	biimtrdi	$⊢ N \in ℤ \to (0 ∥ N \to (\neg N = 0 \to D \in ℕ))$
111	110	adantl	$⊢ (0 \in ℤ \land N \in ℤ) \to (0 ∥ N \to (\neg N = 0 \to D \in ℕ))$
112	107 111	mpcom	$⊢ 0 ∥ N \to (\neg N = 0 \to D \in ℕ)$
113	112	adantl	$⊢ (0 ∥ M \land 0 ∥ N) \to (\neg N = 0 \to D \in ℕ)$
114	113	com12	$⊢ \neg N = 0 \to ((0 ∥ M \land 0 ∥ N) \to D \in ℕ)$
115	106 114	jaoi	$⊢ (\neg M = 0 \lor \neg N = 0) \to ((0 ∥ M \land 0 ∥ N) \to D \in ℕ)$
116	98 115	sylbi	$⊢ \neg (M = 0 \land N = 0) \to ((0 ∥ M \land 0 ∥ N) \to D \in ℕ)$
117	116	adantld	$⊢ \neg (M = 0 \land N = 0) \to ((0 \leq D \land (0 ∥ M \land 0 ∥ N)) \to D \in ℕ)$
118	117	ad2antll	$⊢ (D = 0 \land ((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0))) \to ((0 \leq D \land (0 ∥ M \land 0 ∥ N)) \to D \in ℕ)$
119	97 118	sylbid	$⊢ (D = 0 \land ((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0))) \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to D \in ℕ)$
120	119	ex	$⊢ D = 0 \to (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to D \in ℕ))$
121	92 120	jaoi	$⊢ (D \in ℕ \lor D = 0) \to (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to D \in ℕ))$
122	91 121	sylbi	$⊢ D \in ℕ_{0} \to (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to D \in ℕ))$
123	122	impcom	$⊢ (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \land D \in ℕ_{0}) \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to D \in ℕ)$
124	123	imp	$⊢ ((((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \land D \in ℕ_{0}) \land (0 \leq D \land (D ∥ M \land D ∥ N))) \to D \in ℕ$
125		dvdsle	$⊢ (y \in ℤ \land D \in ℕ) \to (y ∥ D \to y \leq D)$
126	90 124 125	syl2anc	$⊢ ((((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \land D \in ℕ_{0}) \land (0 \leq D \land (D ∥ M \land D ∥ N))) \to (y ∥ D \to y \leq D)$
127	126	exp31	$⊢ ((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to (D \in ℕ_{0} \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to (y ∥ D \to y \leq D)))$
128	127	com14	$⊢ y ∥ D \to (D \in ℕ_{0} \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to y \leq D)))$
129	128	imp	$⊢ (y ∥ D \land D \in ℕ_{0}) \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to y \leq D))$
130	129	impcom	$⊢ ((0 \leq D \land (D ∥ M \land D ∥ N)) \land (y ∥ D \land D \in ℕ_{0})) \to (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to y \leq D)$
131	130	imp	$⊢ (((0 \leq D \land (D ∥ M \land D ∥ N)) \land (y ∥ D \land D \in ℕ_{0})) \land ((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0))) \to y \leq D$
132		zre	$⊢ y \in ℤ \to y \in ℝ$
133	132	ad2antrr	$⊢ ((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to y \in ℝ$
134	68	ad2antlr	$⊢ ((0 \leq D \land (D ∥ M \land D ∥ N)) \land (y ∥ D \land D \in ℕ_{0})) \to D \in ℝ$
135		lenlt	$⊢ (y \in ℝ \land D \in ℝ) \to (y \leq D \leftrightarrow \neg D < y)$
136	133 134 135	syl2anr	$⊢ (((0 \leq D \land (D ∥ M \land D ∥ N)) \land (y ∥ D \land D \in ℕ_{0})) \land ((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0))) \to (y \leq D \leftrightarrow \neg D < y)$
137	131 136	mpbid	$⊢ (((0 \leq D \land (D ∥ M \land D ∥ N)) \land (y ∥ D \land D \in ℕ_{0})) \land ((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0))) \to \neg D < y$
138	137	exp31	$⊢ (0 \leq D \land (D ∥ M \land D ∥ N)) \to ((y ∥ D \land D \in ℕ_{0}) \to (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to \neg D < y))$
139	89 138	mpan2d	$⊢ (0 \leq D \land (D ∥ M \land D ∥ N)) \to (y ∥ D \to (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to \neg D < y))$
140	139	com13	$⊢ ((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to (y ∥ D \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to \neg D < y))$
141	140	adantr	$⊢ (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \land (M \in ℤ \land N \in ℤ)) \to (y ∥ D \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to \neg D < y))$
142	83 141	syld	$⊢ (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \land (M \in ℤ \land N \in ℤ)) \to (\forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D) \to ((0 \leq D \land (D ∥ M \land D ∥ N)) \to \neg D < y))$
143	142	com13	$⊢ (0 \leq D \land (D ∥ M \land D ∥ N)) \to (\forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D) \to ((((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \land (M \in ℤ \land N \in ℤ)) \to \neg D < y))$
144	143	3impia	$⊢ (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)) \to ((((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \land (M \in ℤ \land N \in ℤ)) \to \neg D < y)$
145	144	com12	$⊢ (((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \land (M \in ℤ \land N \in ℤ)) \to ((0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)) \to \neg D < y)$
146	145	expimpd	$⊢ ((y \in ℤ \land (y ∥ M \land y ∥ N)) \land \neg (M = 0 \land N = 0)) \to (((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D))) \to \neg D < y)$
147	146	expimpd	$⊢ (y \in ℤ \land (y ∥ M \land y ∥ N)) \to ((\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \to \neg D < y)$
148	74 147	sylbi	$⊢ y \in \{n \in ℤ \| (n ∥ M \land n ∥ N)\} \to ((\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \to \neg D < y)$
149	148	impcom	$⊢ ((\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \land y \in \{n \in ℤ \| (n ∥ M \land n ∥ N)\}) \to \neg D < y$
150	66	adantr	$⊢ (D ∥ M \land D ∥ N) \to D \in ℤ$
151	150	ancri	$⊢ (D ∥ M \land D ∥ N) \to (D \in ℤ \land (D ∥ M \land D ∥ N))$
152	151	3ad2ant2	$⊢ (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)) \to (D \in ℤ \land (D ∥ M \land D ∥ N))$
153	152	ad2antll	$⊢ (\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \to (D \in ℤ \land (D ∥ M \land D ∥ N))$
154	153	adantr	$⊢ ((\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \land (y \in ℝ \land y < D)) \to (D \in ℤ \land (D ∥ M \land D ∥ N))$
155		breq1	$⊢ n = D \to (n ∥ M \leftrightarrow D ∥ M)$
156		breq1	$⊢ n = D \to (n ∥ N \leftrightarrow D ∥ N)$
157	155 156	anbi12d	$⊢ n = D \to ((n ∥ M \land n ∥ N) \leftrightarrow (D ∥ M \land D ∥ N))$
158	157	elrab	$⊢ D \in \{n \in ℤ \| (n ∥ M \land n ∥ N)\} \leftrightarrow (D \in ℤ \land (D ∥ M \land D ∥ N))$
159	154 158	sylibr	$⊢ ((\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \land (y \in ℝ \land y < D)) \to D \in \{n \in ℤ \| (n ∥ M \land n ∥ N)\}$
160		breq2	$⊢ z = D \to (y < z \leftrightarrow y < D)$
161	160	adantl	$⊢ (((\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \land (y \in ℝ \land y < D)) \land z = D) \to (y < z \leftrightarrow y < D)$
162		simprr	$⊢ ((\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \land (y \in ℝ \land y < D)) \to y < D$
163	159 161 162	rspcedvd	$⊢ ((\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \land (y \in ℝ \land y < D)) \to \exists z \in \{n \in ℤ \| (n ∥ M \land n ∥ N)\} y < z$
164	64 70 149 163	eqsupd	$⊢ (\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \to sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) = D$
165	62 164	eqtrd	$⊢ (\neg (M = 0 \land N = 0) \land ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))) \to if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)) = D$
166	60 165	pm2.61ian	$⊢ ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D))) \to if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)) = D$
167	22 166	eqtr2d	$⊢ ((M \in ℤ \land N \in ℤ) \land (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D))) \to D = M \gcd N$
168	20 167	impbida	$⊢ (M \in ℤ \land N \in ℤ) \to (D = M \gcd N \leftrightarrow (0 \leq D \land (D ∥ M \land D ∥ N) \land \forall e \in ℤ ((e ∥ M \land e ∥ N) \to e ∥ D)))$

Metamath Proof Explorer

Theorem dfgcd2

Proof