Theorem dfgcd3

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

	Ref	Expression
Assertion	dfgcd3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = ( ℩ 𝑑 ∈ ℕ0 ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gcdcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ0 )
2		simplr	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) ∧ ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) → 𝑑 ∈ ℕ0 )
3	2	nn0zd	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) ∧ ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) → 𝑑 ∈ ℤ )
4		iddvds	⊢ ( 𝑑 ∈ ℤ → 𝑑 ∥ 𝑑 )
5	3 4	syl	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) ∧ ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) → 𝑑 ∥ 𝑑 )
6		simpr	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) ∧ ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) → ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) )
7		breq1	⊢ ( 𝑧 = 𝑑 → ( 𝑧 ∥ 𝑑 ↔ 𝑑 ∥ 𝑑 ) )
8		breq1	⊢ ( 𝑧 = 𝑑 → ( 𝑧 ∥ 𝑀 ↔ 𝑑 ∥ 𝑀 ) )
9		breq1	⊢ ( 𝑧 = 𝑑 → ( 𝑧 ∥ 𝑁 ↔ 𝑑 ∥ 𝑁 ) )
10	8 9	anbi12d	⊢ ( 𝑧 = 𝑑 → ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ↔ ( 𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁 ) ) )
11	7 10	bibi12d	⊢ ( 𝑧 = 𝑑 → ( ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ↔ ( 𝑑 ∥ 𝑑 ↔ ( 𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁 ) ) ) )
12	11	rspcv	⊢ ( 𝑑 ∈ ℤ → ( ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) → ( 𝑑 ∥ 𝑑 ↔ ( 𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁 ) ) ) )
13	3 6 12	sylc	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) ∧ ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) → ( 𝑑 ∥ 𝑑 ↔ ( 𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁 ) ) )
14	5 13	mpbid	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) ∧ ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) → ( 𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁 ) )
15		biimpr	⊢ ( ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) → ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) → 𝑧 ∥ 𝑑 ) )
16	15	ralimi	⊢ ( ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) → ∀ 𝑧 ∈ ℤ ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) → 𝑧 ∥ 𝑑 ) )
17	6 16	syl	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) ∧ ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) → ∀ 𝑧 ∈ ℤ ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) → 𝑧 ∥ 𝑑 ) )
18		dfgcd2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑑 = ( 𝑀 gcd 𝑁 ) ↔ ( 0 ≤ 𝑑 ∧ ( 𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁 ) ∧ ∀ 𝑧 ∈ ℤ ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) → 𝑧 ∥ 𝑑 ) ) ) )
19	18	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑑 = ( 𝑀 gcd 𝑁 ) ↔ ( 0 ≤ 𝑑 ∧ ( 𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁 ) ∧ ∀ 𝑧 ∈ ℤ ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) → 𝑧 ∥ 𝑑 ) ) ) )
20		simpr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) → 𝑑 ∈ ℕ0 )
21	20	nn0ge0d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) → 0 ≤ 𝑑 )
22	21	3biant1d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) → ( ( ( 𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁 ) ∧ ∀ 𝑧 ∈ ℤ ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) → 𝑧 ∥ 𝑑 ) ) ↔ ( 0 ≤ 𝑑 ∧ ( 𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁 ) ∧ ∀ 𝑧 ∈ ℤ ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) → 𝑧 ∥ 𝑑 ) ) ) )
23	19 22	bitr4d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑑 = ( 𝑀 gcd 𝑁 ) ↔ ( ( 𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁 ) ∧ ∀ 𝑧 ∈ ℤ ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) → 𝑧 ∥ 𝑑 ) ) ) )
24	23	adantr	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) ∧ ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) → ( 𝑑 = ( 𝑀 gcd 𝑁 ) ↔ ( ( 𝑑 ∥ 𝑀 ∧ 𝑑 ∥ 𝑁 ) ∧ ∀ 𝑧 ∈ ℤ ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) → 𝑧 ∥ 𝑑 ) ) ) )
25	14 17 24	mpbir2and	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) ∧ ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) → 𝑑 = ( 𝑀 gcd 𝑁 ) )
26	25	ex	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) → ( ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) → 𝑑 = ( 𝑀 gcd 𝑁 ) ) )
27		dvdsgcdb	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ↔ 𝑧 ∥ ( 𝑀 gcd 𝑁 ) ) )
28	27	bicomd	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑧 ∥ ( 𝑀 gcd 𝑁 ) ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) )
29	28	3coml	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ∥ ( 𝑀 gcd 𝑁 ) ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) )
30	29	ad4ant124	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 = ( 𝑀 gcd 𝑁 ) ) ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ∥ ( 𝑀 gcd 𝑁 ) ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) )
31		breq2	⊢ ( 𝑑 = ( 𝑀 gcd 𝑁 ) → ( 𝑧 ∥ 𝑑 ↔ 𝑧 ∥ ( 𝑀 gcd 𝑁 ) ) )
32	31	bibi1d	⊢ ( 𝑑 = ( 𝑀 gcd 𝑁 ) → ( ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ↔ ( 𝑧 ∥ ( 𝑀 gcd 𝑁 ) ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) )
33	32	ad2antlr	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 = ( 𝑀 gcd 𝑁 ) ) ∧ 𝑧 ∈ ℤ ) → ( ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ↔ ( 𝑧 ∥ ( 𝑀 gcd 𝑁 ) ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) )
34	30 33	mpbird	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 = ( 𝑀 gcd 𝑁 ) ) ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) )
35	34	ralrimiva	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 = ( 𝑀 gcd 𝑁 ) ) → ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) )
36	35	ex	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑑 = ( 𝑀 gcd 𝑁 ) → ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) )
37	36	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) → ( 𝑑 = ( 𝑀 gcd 𝑁 ) → ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) )
38	26 37	impbid	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑑 ∈ ℕ0 ) → ( ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ↔ 𝑑 = ( 𝑀 gcd 𝑁 ) ) )
39	1 38	riota5	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ℩ 𝑑 ∈ ℕ0 ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) = ( 𝑀 gcd 𝑁 ) )
40	39	eqcomd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = ( ℩ 𝑑 ∈ ℕ0 ∀ 𝑧 ∈ ℤ ( 𝑧 ∥ 𝑑 ↔ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ) ) )