Metamath Proof Explorer

Theorem dfgcd3

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

Ref Expression
Assertion dfgcd3 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( iota_ d e. NN0 A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) )

Proof

Step Hyp Ref Expression
1 gcdcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )
2 simplr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) /\ A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) -> d e. NN0 )
3 2 nn0zd 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) /\ A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) -> d e. ZZ )
4 iddvds 
 |-  ( d e. ZZ -> d || d )
5 3 4 syl 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) /\ A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) -> d || d )
6 simpr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) /\ A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) -> A. z e. ZZ ( 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 e. ZZ -> ( A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) -> ( d || d <-> ( d || M /\ d || N ) ) ) )
13 3 6 12 sylc 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) /\ A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) -> ( d || d <-> ( d || M /\ d || N ) ) )
14 5 13 mpbid 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) /\ A. z e. ZZ ( 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 
 |-  ( A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) -> A. z e. ZZ ( ( z || M /\ z || N ) -> z || d ) )
17 6 16 syl 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) /\ A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) -> A. z e. ZZ ( ( z || M /\ z || N ) -> z || d ) )
18 dfgcd2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( d = ( M gcd N ) <-> ( 0 <_ d /\ ( d || M /\ d || N ) /\ A. z e. ZZ ( ( z || M /\ z || N ) -> z || d ) ) ) )
19 18 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) -> ( d = ( M gcd N ) <-> ( 0 <_ d /\ ( d || M /\ d || N ) /\ A. z e. ZZ ( ( z || M /\ z || N ) -> z || d ) ) ) )
20 simpr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) -> d e. NN0 )
21 20 nn0ge0d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) -> 0 <_ d )
22 21 3biant1d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) -> ( ( ( d || M /\ d || N ) /\ A. z e. ZZ ( ( z || M /\ z || N ) -> z || d ) ) <-> ( 0 <_ d /\ ( d || M /\ d || N ) /\ A. z e. ZZ ( ( z || M /\ z || N ) -> z || d ) ) ) )
23 19 22 bitr4d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) -> ( d = ( M gcd N ) <-> ( ( d || M /\ d || N ) /\ A. z e. ZZ ( ( z || M /\ z || N ) -> z || d ) ) ) )
24 23 adantr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) /\ A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) -> ( d = ( M gcd N ) <-> ( ( d || M /\ d || N ) /\ A. z e. ZZ ( ( z || M /\ z || N ) -> z || d ) ) ) )
25 14 17 24 mpbir2and 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) /\ A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) -> d = ( M gcd N ) )
26 25 ex 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) -> ( A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) -> d = ( M gcd N ) ) )
27 dvdsgcdb 
 |-  ( ( z e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( z || M /\ z || N ) <-> z || ( M gcd N ) ) )
28 27 bicomd 
 |-  ( ( z e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( z || ( M gcd N ) <-> ( z || M /\ z || N ) ) )
29 28 3coml 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ z e. ZZ ) -> ( z || ( M gcd N ) <-> ( z || M /\ z || N ) ) )
30 29 ad4ant124 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ d = ( M gcd N ) ) /\ z e. ZZ ) -> ( 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 e. ZZ /\ N e. ZZ ) /\ d = ( M gcd N ) ) /\ z e. ZZ ) -> ( ( z || d <-> ( z || M /\ z || N ) ) <-> ( z || ( M gcd N ) <-> ( z || M /\ z || N ) ) ) )
34 30 33 mpbird 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ d = ( M gcd N ) ) /\ z e. ZZ ) -> ( z || d <-> ( z || M /\ z || N ) ) )
35 34 ralrimiva 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ d = ( M gcd N ) ) -> A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) )
36 35 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( d = ( M gcd N ) -> A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) )
37 36 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) -> ( d = ( M gcd N ) -> A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) )
38 26 37 impbid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ d e. NN0 ) -> ( A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) <-> d = ( M gcd N ) ) )
39 1 38 riota5 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( iota_ d e. NN0 A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) = ( M gcd N ) )
40 39 eqcomd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( iota_ d e. NN0 A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) )