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