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 ) ) ) )
10 9 adantr 
 |-  ( ( ( 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 ) ) ) ) )
19 18 adantl 
 |-  ( ( ( 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 , < ) ) )
22 21 adantr 
 |-  ( ( ( 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 )
24 23 adantr 
 |-  ( ( ( 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 ) )
37 36 adantl 
 |-  ( ( ( 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 ) )
50 49 adantr 
 |-  ( ( 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 ) ) )
53 52 adantr 
 |-  ( ( 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 ) ) )
55 54 adantr 
 |-  ( ( 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 ) )
58 57 adantld 
 |-  ( ( 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 , < ) )
62 61 adantr 
 |-  ( ( -. ( 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 )
68 67 adantr 
 |-  ( ( D || M /\ D || N ) -> D e. RR )
69 68 3ad2ant2 
 |-  ( ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) -> D e. RR )
70 69 ad2antll 
 |-  ( ( -. ( 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 ) )
83 82 ad2antrr 
 |-  ( ( ( ( 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 ) )
86 85 adantr 
 |-  ( ( D e. ZZ /\ M e. ZZ ) -> ( 0 <_ D -> D e. NN0 ) )
87 65 86 syl 
 |-  ( D || M -> ( 0 <_ D -> D e. NN0 ) )
88 87 adantr 
 |-  ( ( 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 ) ) ) )
97 96 adantr 
 |-  ( ( 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 ) ) )
103 102 adantl 
 |-  ( ( 0 e. ZZ /\ M e. ZZ ) -> ( 0 || M -> ( -. M = 0 -> D e. NN ) ) )
104 99 103 mpcom 
 |-  ( 0 || M -> ( -. M = 0 -> D e. NN ) )
105 104 adantr 
 |-  ( ( 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 ) ) )
111 110 adantl 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 || N -> ( -. N = 0 -> D e. NN ) ) )
112 107 111 mpcom 
 |-  ( 0 || N -> ( -. N = 0 -> D e. NN ) )
113 112 adantl 
 |-  ( ( 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 ) )
117 116 adantld 
 |-  ( -. ( M = 0 /\ N = 0 ) -> ( ( 0 <_ D /\ ( 0 || M /\ 0 || N ) ) -> D e. NN ) )
118 117 ad2antll 
 |-  ( ( 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 )
133 132 ad2antrr 
 |-  ( ( ( y e. ZZ /\ ( y || M /\ y || N ) ) /\ -. ( M = 0 /\ N = 0 ) ) -> y e. RR )
134 68 ad2antlr 
 |-  ( ( ( 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 ) ) )
141 140 adantr 
 |-  ( ( ( ( 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 )
150 66 adantr 
 |-  ( ( D || M /\ D || N ) -> D e. ZZ )
151 150 ancri 
 |-  ( ( D || M /\ D || N ) -> ( D e. ZZ /\ ( D || M /\ D || N ) ) )
152 151 3ad2ant2 
 |-  ( ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) -> ( D e. ZZ /\ ( D || M /\ D || N ) ) )
153 152 ad2antll 
 |-  ( ( -. ( 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 ) ) )
154 153 adantr 
 |-  ( ( ( -. ( 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 ) )
161 160 adantl 
 |-  ( ( ( ( -. ( 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 ) ) ) )