# Metamath Proof Explorer

## Theorem dfgcd2

Description: Alternate definition of the gcd operator, see definition in ApostolNT p. 15. (Contributed by AV, 8-Aug-2021)

Ref Expression
Assertion dfgcd2
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( D = ( M gcd N ) <-> ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) )

### Proof

Step Hyp Ref Expression
1 gcdcl
|-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )
2 1 nn0ge0d
|-  ( ( M e. ZZ /\ N e. ZZ ) -> 0 <_ ( M gcd N ) )
3 gcddvds
|-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
4 3anass
|-  ( ( e e. ZZ /\ M e. ZZ /\ N e. ZZ ) <-> ( e e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) )
5 4 biancomi
|-  ( ( e e. ZZ /\ M e. ZZ /\ N e. ZZ ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ e e. ZZ ) )
6 dvdsgcd
|-  ( ( e e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( e || M /\ e || N ) -> e || ( M gcd N ) ) )
7 5 6 sylbir
|-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ e e. ZZ ) -> ( ( e || M /\ e || N ) -> e || ( M gcd N ) ) )
8 7 ralrimiva
|-  ( ( M e. ZZ /\ N e. ZZ ) -> A. e e. ZZ ( ( e || M /\ e || N ) -> e || ( M gcd N ) ) )
9 2 3 8 3jca
|-  ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 <_ ( M gcd N ) /\ ( ( M gcd N ) || M /\ ( M gcd N ) || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || ( M gcd N ) ) ) )
|-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ D = ( M gcd N ) ) -> ( 0 <_ ( M gcd N ) /\ ( ( M gcd N ) || M /\ ( M gcd N ) || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || ( M gcd N ) ) ) )
11 breq2
|-  ( D = ( M gcd N ) -> ( 0 <_ D <-> 0 <_ ( M gcd N ) ) )
12 breq1
|-  ( D = ( M gcd N ) -> ( D || M <-> ( M gcd N ) || M ) )
13 breq1
|-  ( D = ( M gcd N ) -> ( D || N <-> ( M gcd N ) || N ) )
14 12 13 anbi12d
|-  ( D = ( M gcd N ) -> ( ( D || M /\ D || N ) <-> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) ) )
15 breq2
|-  ( D = ( M gcd N ) -> ( e || D <-> e || ( M gcd N ) ) )
16 15 imbi2d
|-  ( D = ( M gcd N ) -> ( ( ( e || M /\ e || N ) -> e || D ) <-> ( ( e || M /\ e || N ) -> e || ( M gcd N ) ) ) )
17 16 ralbidv
|-  ( D = ( M gcd N ) -> ( A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) <-> A. e e. ZZ ( ( e || M /\ e || N ) -> e || ( M gcd N ) ) ) )
18 11 14 17 3anbi123d
|-  ( D = ( M gcd N ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) <-> ( 0 <_ ( M gcd N ) /\ ( ( M gcd N ) || M /\ ( M gcd N ) || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || ( M gcd N ) ) ) ) )
|-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ D = ( M gcd N ) ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) <-> ( 0 <_ ( M gcd N ) /\ ( ( M gcd N ) || M /\ ( M gcd N ) || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || ( M gcd N ) ) ) ) )
20 10 19 mpbird
|-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ D = ( M gcd N ) ) -> ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) )
21 gcdval
|-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) )
|-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) -> ( M gcd N ) = if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) )
23 iftrue
|-  ( ( M = 0 /\ N = 0 ) -> if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) = 0 )
|-  ( ( ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) -> if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) = 0 )
25 breq2
|-  ( M = 0 -> ( D || M <-> D || 0 ) )
26 breq2
|-  ( N = 0 -> ( D || N <-> D || 0 ) )
27 25 26 bi2anan9
|-  ( ( M = 0 /\ N = 0 ) -> ( ( D || M /\ D || N ) <-> ( D || 0 /\ D || 0 ) ) )
28 breq2
|-  ( M = 0 -> ( e || M <-> e || 0 ) )
29 breq2
|-  ( N = 0 -> ( e || N <-> e || 0 ) )
30 28 29 bi2anan9
|-  ( ( M = 0 /\ N = 0 ) -> ( ( e || M /\ e || N ) <-> ( e || 0 /\ e || 0 ) ) )
31 30 imbi1d
|-  ( ( M = 0 /\ N = 0 ) -> ( ( ( e || M /\ e || N ) -> e || D ) <-> ( ( e || 0 /\ e || 0 ) -> e || D ) ) )
32 31 ralbidv
|-  ( ( M = 0 /\ N = 0 ) -> ( A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) <-> A. e e. ZZ ( ( e || 0 /\ e || 0 ) -> e || D ) ) )
33 27 32 3anbi23d
|-  ( ( M = 0 /\ N = 0 ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) <-> ( 0 <_ D /\ ( D || 0 /\ D || 0 ) /\ A. e e. ZZ ( ( e || 0 /\ e || 0 ) -> e || D ) ) ) )
34 dvdszrcl
|-  ( D || 0 -> ( D e. ZZ /\ 0 e. ZZ ) )
35 dvds0
|-  ( e e. ZZ -> e || 0 )
36 35 35 jca
|-  ( e e. ZZ -> ( e || 0 /\ e || 0 ) )
|-  ( ( ( D e. ZZ /\ 0 <_ D ) /\ e e. ZZ ) -> ( e || 0 /\ e || 0 ) )
38 pm5.5
|-  ( ( e || 0 /\ e || 0 ) -> ( ( ( e || 0 /\ e || 0 ) -> e || D ) <-> e || D ) )
39 37 38 syl
|-  ( ( ( D e. ZZ /\ 0 <_ D ) /\ e e. ZZ ) -> ( ( ( e || 0 /\ e || 0 ) -> e || D ) <-> e || D ) )
40 39 ralbidva
|-  ( ( D e. ZZ /\ 0 <_ D ) -> ( A. e e. ZZ ( ( e || 0 /\ e || 0 ) -> e || D ) <-> A. e e. ZZ e || D ) )
41 0z
|-  0 e. ZZ
42 breq1
|-  ( e = 0 -> ( e || D <-> 0 || D ) )
43 42 rspcv
|-  ( 0 e. ZZ -> ( A. e e. ZZ e || D -> 0 || D ) )
44 41 43 ax-mp
|-  ( A. e e. ZZ e || D -> 0 || D )
45 0dvds
|-  ( D e. ZZ -> ( 0 || D <-> D = 0 ) )
46 45 biimpd
|-  ( D e. ZZ -> ( 0 || D -> D = 0 ) )
47 eqcom
|-  ( 0 = D <-> D = 0 )
48 46 47 syl6ibr
|-  ( D e. ZZ -> ( 0 || D -> 0 = D ) )
49 44 48 syl5
|-  ( D e. ZZ -> ( A. e e. ZZ e || D -> 0 = D ) )
|-  ( ( D e. ZZ /\ 0 <_ D ) -> ( A. e e. ZZ e || D -> 0 = D ) )
51 40 50 sylbid
|-  ( ( D e. ZZ /\ 0 <_ D ) -> ( A. e e. ZZ ( ( e || 0 /\ e || 0 ) -> e || D ) -> 0 = D ) )
52 51 ex
|-  ( D e. ZZ -> ( 0 <_ D -> ( A. e e. ZZ ( ( e || 0 /\ e || 0 ) -> e || D ) -> 0 = D ) ) )
|-  ( ( D e. ZZ /\ 0 e. ZZ ) -> ( 0 <_ D -> ( A. e e. ZZ ( ( e || 0 /\ e || 0 ) -> e || D ) -> 0 = D ) ) )
54 34 53 syl
|-  ( D || 0 -> ( 0 <_ D -> ( A. e e. ZZ ( ( e || 0 /\ e || 0 ) -> e || D ) -> 0 = D ) ) )
|-  ( ( D || 0 /\ D || 0 ) -> ( 0 <_ D -> ( A. e e. ZZ ( ( e || 0 /\ e || 0 ) -> e || D ) -> 0 = D ) ) )
56 55 3imp21
|-  ( ( 0 <_ D /\ ( D || 0 /\ D || 0 ) /\ A. e e. ZZ ( ( e || 0 /\ e || 0 ) -> e || D ) ) -> 0 = D )
57 33 56 syl6bi
|-  ( ( M = 0 /\ N = 0 ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) -> 0 = D ) )
|-  ( ( M = 0 /\ N = 0 ) -> ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) -> 0 = D ) )
59 58 imp
|-  ( ( ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) -> 0 = D )
60 24 59 eqtrd
|-  ( ( ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) -> if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) = D )
61 iffalse
|-  ( -. ( M = 0 /\ N = 0 ) -> if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) = sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) )
|-  ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) -> if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) = sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) )
63 ltso
|-  < Or RR
64 63 a1i
|-  ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) -> < Or RR )
65 dvdszrcl
|-  ( D || M -> ( D e. ZZ /\ M e. ZZ ) )
66 65 simpld
|-  ( D || M -> D e. ZZ )
67 66 zred
|-  ( D || M -> D e. RR )
|-  ( ( D || M /\ D || N ) -> D e. RR )
|-  ( ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) -> D e. RR )
|-  ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) -> D e. RR )
71 breq1
|-  ( n = y -> ( n || M <-> y || M ) )
72 breq1
|-  ( n = y -> ( n || N <-> y || N ) )
73 71 72 anbi12d
|-  ( n = y -> ( ( n || M /\ n || N ) <-> ( y || M /\ y || N ) ) )
74 73 elrab
|-  ( y e. { n e. ZZ | ( n || M /\ n || N ) } <-> ( y e. ZZ /\ ( y || M /\ y || N ) ) )
75 breq1
|-  ( e = y -> ( e || M <-> y || M ) )
76 breq1
|-  ( e = y -> ( e || N <-> y || N ) )
77 75 76 anbi12d
|-  ( e = y -> ( ( e || M /\ e || N ) <-> ( y || M /\ y || N ) ) )
78 breq1
|-  ( e = y -> ( e || D <-> y || D ) )
79 77 78 imbi12d
|-  ( e = y -> ( ( ( e || M /\ e || N ) -> e || D ) <-> ( ( y || M /\ y || N ) -> y || D ) ) )
80 79 rspcv
|-  ( y e. ZZ -> ( A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) -> ( ( y || M /\ y || N ) -> y || D ) ) )
81 80 com23
|-  ( y e. ZZ -> ( ( y || M /\ y || N ) -> ( A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) -> y || D ) ) )
82 81 imp
|-  ( ( y e. ZZ /\ ( y || M /\ y || N ) ) -> ( A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) -> y || D ) )
|-  ( ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) -> y || D ) )
84 elnn0z
|-  ( D e. NN0 <-> ( D e. ZZ /\ 0 <_ D ) )
85 84 simplbi2
|-  ( D e. ZZ -> ( 0 <_ D -> D e. NN0 ) )
|-  ( ( D e. ZZ /\ M e. ZZ ) -> ( 0 <_ D -> D e. NN0 ) )
87 65 86 syl
|-  ( D || M -> ( 0 <_ D -> D e. NN0 ) )
|-  ( ( D || M /\ D || N ) -> ( 0 <_ D -> D e. NN0 ) )
89 88 impcom
|-  ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> D e. NN0 )
90 simp-4l
|-  ( ( ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) /\ D e. NN0 ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) ) ) -> y e. ZZ )
91 elnn0
|-  ( D e. NN0 <-> ( D e. NN \/ D = 0 ) )
92 2a1
|-  ( D e. NN -> ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> D e. NN ) ) )
93 breq1
|-  ( D = 0 -> ( D || M <-> 0 || M ) )
94 breq1
|-  ( D = 0 -> ( D || N <-> 0 || N ) )
95 93 94 anbi12d
|-  ( D = 0 -> ( ( D || M /\ D || N ) <-> ( 0 || M /\ 0 || N ) ) )
96 95 anbi2d
|-  ( D = 0 -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) <-> ( 0 <_ D /\ ( 0 || M /\ 0 || N ) ) ) )
|-  ( ( D = 0 /\ ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) <-> ( 0 <_ D /\ ( 0 || M /\ 0 || N ) ) ) )
98 ianor
|-  ( -. ( M = 0 /\ N = 0 ) <-> ( -. M = 0 \/ -. N = 0 ) )
99 dvdszrcl
|-  ( 0 || M -> ( 0 e. ZZ /\ M e. ZZ ) )
100 0dvds
|-  ( M e. ZZ -> ( 0 || M <-> M = 0 ) )
101 pm2.24
|-  ( M = 0 -> ( -. M = 0 -> D e. NN ) )
102 100 101 syl6bi
|-  ( M e. ZZ -> ( 0 || M -> ( -. M = 0 -> D e. NN ) ) )
|-  ( ( 0 e. ZZ /\ M e. ZZ ) -> ( 0 || M -> ( -. M = 0 -> D e. NN ) ) )
104 99 103 mpcom
|-  ( 0 || M -> ( -. M = 0 -> D e. NN ) )
|-  ( ( 0 || M /\ 0 || N ) -> ( -. M = 0 -> D e. NN ) )
106 105 com12
|-  ( -. M = 0 -> ( ( 0 || M /\ 0 || N ) -> D e. NN ) )
107 dvdszrcl
|-  ( 0 || N -> ( 0 e. ZZ /\ N e. ZZ ) )
108 0dvds
|-  ( N e. ZZ -> ( 0 || N <-> N = 0 ) )
109 pm2.24
|-  ( N = 0 -> ( -. N = 0 -> D e. NN ) )
110 108 109 syl6bi
|-  ( N e. ZZ -> ( 0 || N -> ( -. N = 0 -> D e. NN ) ) )
|-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 || N -> ( -. N = 0 -> D e. NN ) ) )
112 107 111 mpcom
|-  ( 0 || N -> ( -. N = 0 -> D e. NN ) )
|-  ( ( 0 || M /\ 0 || N ) -> ( -. N = 0 -> D e. NN ) )
114 113 com12
|-  ( -. N = 0 -> ( ( 0 || M /\ 0 || N ) -> D e. NN ) )
115 106 114 jaoi
|-  ( ( -. M = 0 \/ -. N = 0 ) -> ( ( 0 || M /\ 0 || N ) -> D e. NN ) )
116 98 115 sylbi
|-  ( -. ( M = 0 /\ N = 0 ) -> ( ( 0 || M /\ 0 || N ) -> D e. NN ) )
|-  ( -. ( M = 0 /\ N = 0 ) -> ( ( 0 <_ D /\ ( 0 || M /\ 0 || N ) ) -> D e. NN ) )
|-  ( ( D = 0 /\ ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) ) -> ( ( 0 <_ D /\ ( 0 || M /\ 0 || N ) ) -> D e. NN ) )
119 97 118 sylbid
|-  ( ( D = 0 /\ ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> D e. NN ) )
120 119 ex
|-  ( D = 0 -> ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> D e. NN ) ) )
121 92 120 jaoi
|-  ( ( D e. NN \/ D = 0 ) -> ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> D e. NN ) ) )
122 91 121 sylbi
|-  ( D e. NN0 -> ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> D e. NN ) ) )
123 122 impcom
|-  ( ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) /\ D e. NN0 ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> D e. NN ) )
124 123 imp
|-  ( ( ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) /\ D e. NN0 ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) ) ) -> D e. NN )
125 dvdsle
|-  ( ( y e. ZZ /\ D e. NN ) -> ( y || D -> y <_ D ) )
126 90 124 125 syl2anc
|-  ( ( ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) /\ D e. NN0 ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) ) ) -> ( y || D -> y <_ D ) )
127 126 exp31
|-  ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( D e. NN0 -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> ( y || D -> y <_ D ) ) ) )
128 127 com14
|-  ( y || D -> ( D e. NN0 -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> y <_ D ) ) ) )
129 128 imp
|-  ( ( y || D /\ D e. NN0 ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> y <_ D ) ) )
130 129 impcom
|-  ( ( ( 0 <_ D /\ ( D || M /\ D || N ) ) /\ ( y || D /\ D e. NN0 ) ) -> ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> y <_ D ) )
131 130 imp
|-  ( ( ( ( 0 <_ D /\ ( D || M /\ D || N ) ) /\ ( y || D /\ D e. NN0 ) ) /\ ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) ) -> y <_ D )
132 zre
|-  ( y e. ZZ -> y e. RR )
|-  ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> y e. RR )
|-  ( ( ( 0 <_ D /\ ( D || M /\ D || N ) ) /\ ( y || D /\ D e. NN0 ) ) -> D e. RR )
135 lenlt
|-  ( ( y e. RR /\ D e. RR ) -> ( y <_ D <-> -. D < y ) )
136 133 134 135 syl2anr
|-  ( ( ( ( 0 <_ D /\ ( D || M /\ D || N ) ) /\ ( y || D /\ D e. NN0 ) ) /\ ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) ) -> ( y <_ D <-> -. D < y ) )
137 131 136 mpbid
|-  ( ( ( ( 0 <_ D /\ ( D || M /\ D || N ) ) /\ ( y || D /\ D e. NN0 ) ) /\ ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) ) -> -. D < y )
138 137 exp31
|-  ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> ( ( y || D /\ D e. NN0 ) -> ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> -. D < y ) ) )
139 89 138 mpan2d
|-  ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> ( y || D -> ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> -. D < y ) ) )
140 139 com13
|-  ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( y || D -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> -. D < y ) ) )
|-  ( ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( y || D -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> -. D < y ) ) )
142 83 141 syld
|-  ( ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> -. D < y ) ) )
143 142 com13
|-  ( ( 0 <_ D /\ ( D || M /\ D || N ) ) -> ( A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) -> ( ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> -. D < y ) ) )
144 143 3impia
|-  ( ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) -> ( ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> -. D < y ) )
145 144 com12
|-  ( ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) -> -. D < y ) )
146 145 expimpd
|-  ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) -> -. D < y ) )
147 146 expimpd
|-  ( ( y e. ZZ /\ ( y || M /\ y || N ) ) -> ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) -> -. D < y ) )
148 74 147 sylbi
|-  ( y e. { n e. ZZ | ( n || M /\ n || N ) } -> ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) -> -. D < y ) )
149 148 impcom
|-  ( ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) /\ y e. { n e. ZZ | ( n || M /\ n || N ) } ) -> -. D < y )
|-  ( ( D || M /\ D || N ) -> D e. ZZ )
151 150 ancri
|-  ( ( D || M /\ D || N ) -> ( D e. ZZ /\ ( D || M /\ D || N ) ) )
|-  ( ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) -> ( D e. ZZ /\ ( D || M /\ D || N ) ) )
|-  ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) -> ( D e. ZZ /\ ( D || M /\ D || N ) ) )
|-  ( ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) /\ ( y e. RR /\ y < D ) ) -> ( D e. ZZ /\ ( D || M /\ D || N ) ) )
155 breq1
|-  ( n = D -> ( n || M <-> D || M ) )
156 breq1
|-  ( n = D -> ( n || N <-> D || N ) )
157 155 156 anbi12d
|-  ( n = D -> ( ( n || M /\ n || N ) <-> ( D || M /\ D || N ) ) )
158 157 elrab
|-  ( D e. { n e. ZZ | ( n || M /\ n || N ) } <-> ( D e. ZZ /\ ( D || M /\ D || N ) ) )
159 154 158 sylibr
|-  ( ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) /\ ( y e. RR /\ y < D ) ) -> D e. { n e. ZZ | ( n || M /\ n || N ) } )
160 breq2
|-  ( z = D -> ( y < z <-> y < D ) )
|-  ( ( ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) /\ ( y e. RR /\ y < D ) ) /\ z = D ) -> ( y < z <-> y < D ) )
162 simprr
|-  ( ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) /\ ( y e. RR /\ y < D ) ) -> y < D )
163 159 161 162 rspcedvd
|-  ( ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) /\ ( y e. RR /\ y < D ) ) -> E. z e. { n e. ZZ | ( n || M /\ n || N ) } y < z )
164 64 70 149 163 eqsupd
|-  ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) -> sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) = D )
165 62 164 eqtrd
|-  ( ( -. ( M = 0 /\ N = 0 ) /\ ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) ) -> if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) = D )
166 60 165 pm2.61ian
|-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) -> if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) = D )
167 22 166 eqtr2d
|-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) -> D = ( M gcd N ) )
168 20 167 impbida
|-  ( ( M e. ZZ /\ N e. ZZ ) -> ( D = ( M gcd N ) <-> ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) )