Metamath Proof Explorer

Theorem dfgcd3

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

Ref Expression
Assertion dfgcd3 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = ι d ∈ ℕ 0 | ∀ z ∈ ℤ z ∥ d ↔ z ∥ M ∧ z ∥ N

Proof

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