dfgcd3

Description: Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021)

		Ref	Expression
	Assertion	dfgcd3	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N = (ι d \in ℕ_{0} \| \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)))$

Proof

Step	Hyp	Ref	Expression
1		gcdcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℕ_{0}$
2		simplr	$⊢ (((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \land \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))) \to d \in ℕ_{0}$
3	2	nn0zd	$⊢ (((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \land \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))) \to d \in ℤ$
4		iddvds	$⊢ d \in ℤ \to d ∥ d$
5	3 4	syl	$⊢ (((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \land \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))) \to d ∥ d$
6		simpr	$⊢ (((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \land \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))) \to \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))$
7		breq1	$⊢ z = d \to (z ∥ d \leftrightarrow d ∥ d)$
8		breq1	$⊢ z = d \to (z ∥ M \leftrightarrow d ∥ M)$
9		breq1	$⊢ z = d \to (z ∥ N \leftrightarrow d ∥ N)$
10	8 9	anbi12d	$⊢ z = d \to ((z ∥ M \land z ∥ N) \leftrightarrow (d ∥ M \land d ∥ N))$
11	7 10	bibi12d	$⊢ z = d \to ((z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)) \leftrightarrow (d ∥ d \leftrightarrow (d ∥ M \land d ∥ N)))$
12	11	rspcv	$⊢ d \in ℤ \to (\forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)) \to (d ∥ d \leftrightarrow (d ∥ M \land d ∥ N)))$
13	3 6 12	sylc	$⊢ (((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \land \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))) \to (d ∥ d \leftrightarrow (d ∥ M \land d ∥ N))$
14	5 13	mpbid	$⊢ (((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \land \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))) \to (d ∥ M \land d ∥ N)$
15		biimpr	$⊢ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)) \to ((z ∥ M \land z ∥ N) \to z ∥ d)$
16	15	ralimi	$⊢ \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)) \to \forall z \in ℤ ((z ∥ M \land z ∥ N) \to z ∥ d)$
17	6 16	syl	$⊢ (((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \land \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))) \to \forall z \in ℤ ((z ∥ M \land z ∥ N) \to z ∥ d)$
18		dfgcd2	$⊢ (M \in ℤ \land N \in ℤ) \to (d = M \gcd N \leftrightarrow (0 \leq d \land (d ∥ M \land d ∥ N) \land \forall z \in ℤ ((z ∥ M \land z ∥ N) \to z ∥ d)))$
19	18	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \to (d = M \gcd N \leftrightarrow (0 \leq d \land (d ∥ M \land d ∥ N) \land \forall z \in ℤ ((z ∥ M \land z ∥ N) \to z ∥ d)))$
20		simpr	$⊢ ((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \to d \in ℕ_{0}$
21	20	nn0ge0d	$⊢ ((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \to 0 \leq d$
22	21	3biant1d	$⊢ ((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \to (((d ∥ M \land d ∥ N) \land \forall z \in ℤ ((z ∥ M \land z ∥ N) \to z ∥ d)) \leftrightarrow (0 \leq d \land (d ∥ M \land d ∥ N) \land \forall z \in ℤ ((z ∥ M \land z ∥ N) \to z ∥ d)))$
23	19 22	bitr4d	$⊢ ((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \to (d = M \gcd N \leftrightarrow ((d ∥ M \land d ∥ N) \land \forall z \in ℤ ((z ∥ M \land z ∥ N) \to z ∥ d)))$
24	23	adantr	$⊢ (((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \land \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))) \to (d = M \gcd N \leftrightarrow ((d ∥ M \land d ∥ N) \land \forall z \in ℤ ((z ∥ M \land z ∥ N) \to z ∥ d)))$
25	14 17 24	mpbir2and	$⊢ (((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \land \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))) \to d = M \gcd N$
26	25	ex	$⊢ ((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \to (\forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)) \to d = M \gcd N)$
27		dvdsgcdb	$⊢ (z \in ℤ \land M \in ℤ \land N \in ℤ) \to ((z ∥ M \land z ∥ N) \leftrightarrow z ∥ (M \gcd N))$
28	27	bicomd	$⊢ (z \in ℤ \land M \in ℤ \land N \in ℤ) \to (z ∥ (M \gcd N) \leftrightarrow (z ∥ M \land z ∥ N))$
29	28	3coml	$⊢ (M \in ℤ \land N \in ℤ \land z \in ℤ) \to (z ∥ (M \gcd N) \leftrightarrow (z ∥ M \land z ∥ N))$
30	29	ad4ant124	$⊢ (((M \in ℤ \land N \in ℤ) \land d = M \gcd N) \land z \in ℤ) \to (z ∥ (M \gcd N) \leftrightarrow (z ∥ M \land z ∥ N))$
31		breq2	$⊢ d = M \gcd N \to (z ∥ d \leftrightarrow z ∥ (M \gcd N))$
32	31	bibi1d	$⊢ d = M \gcd N \to ((z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)) \leftrightarrow (z ∥ (M \gcd N) \leftrightarrow (z ∥ M \land z ∥ N)))$
33	32	ad2antlr	$⊢ (((M \in ℤ \land N \in ℤ) \land d = M \gcd N) \land z \in ℤ) \to ((z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)) \leftrightarrow (z ∥ (M \gcd N) \leftrightarrow (z ∥ M \land z ∥ N)))$
34	30 33	mpbird	$⊢ (((M \in ℤ \land N \in ℤ) \land d = M \gcd N) \land z \in ℤ) \to (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))$
35	34	ralrimiva	$⊢ ((M \in ℤ \land N \in ℤ) \land d = M \gcd N) \to \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))$
36	35	ex	$⊢ (M \in ℤ \land N \in ℤ) \to (d = M \gcd N \to \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)))$
37	36	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \to (d = M \gcd N \to \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)))$
38	26 37	impbid	$⊢ ((M \in ℤ \land N \in ℤ) \land d \in ℕ_{0}) \to (\forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)) \leftrightarrow d = M \gcd N)$
39	1 38	riota5	$⊢ (M \in ℤ \land N \in ℤ) \to (ι d \in ℕ_{0} \| \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N))) = M \gcd N$
40	39	eqcomd	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N = (ι d \in ℕ_{0} \| \forall z \in ℤ (z ∥ d \leftrightarrow (z ∥ M \land z ∥ N)))$

Metamath Proof Explorer

Theorem dfgcd3

Proof