Metamath Proof Explorer

Theorem gcdcllem3

Description: Lemma for gcdn0cl , gcddvds and dvdslegcd . (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Hypotheses gcdcllem2.1 
|- S = { z e. ZZ | A. n e. { M , N } z || n }
gcdcllem2.2 
|- R = { z e. ZZ | ( z || M /\ z || N ) }
Assertion gcdcllem3 
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( sup ( R , RR , < ) e. NN /\ ( sup ( R , RR , < ) || M /\ sup ( R , RR , < ) || N ) /\ ( ( K e. ZZ /\ K || M /\ K || N ) -> K <_ sup ( R , RR , < ) ) ) )

Proof

Step Hyp Ref Expression
1 gcdcllem2.1 
 |-  S = { z e. ZZ | A. n e. { M , N } z || n }
2 gcdcllem2.2 
 |-  R = { z e. ZZ | ( z || M /\ z || N ) }
3 2 ssrab3 
 |-  R C_ ZZ
4 prssi 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> { M , N } C_ ZZ )
5 neorian 
 |-  ( ( M =/= 0 \/ N =/= 0 ) <-> -. ( M = 0 /\ N = 0 ) )
6 prid1g 
 |-  ( M e. ZZ -> M e. { M , N } )
7 neeq1 
 |-  ( n = M -> ( n =/= 0 <-> M =/= 0 ) )
8 7 rspcev 
 |-  ( ( M e. { M , N } /\ M =/= 0 ) -> E. n e. { M , N } n =/= 0 )
9 6 8 sylan 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> E. n e. { M , N } n =/= 0 )
10 9 adantlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) -> E. n e. { M , N } n =/= 0 )
11 prid2g 
 |-  ( N e. ZZ -> N e. { M , N } )
12 neeq1 
 |-  ( n = N -> ( n =/= 0 <-> N =/= 0 ) )
13 12 rspcev 
 |-  ( ( N e. { M , N } /\ N =/= 0 ) -> E. n e. { M , N } n =/= 0 )
14 11 13 sylan 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> E. n e. { M , N } n =/= 0 )
15 14 adantll 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ N =/= 0 ) -> E. n e. { M , N } n =/= 0 )
16 10 15 jaodan 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 \/ N =/= 0 ) ) -> E. n e. { M , N } n =/= 0 )
17 5 16 sylan2br 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> E. n e. { M , N } n =/= 0 )
18 1 gcdcllem1 
 |-  ( ( { M , N } C_ ZZ /\ E. n e. { M , N } n =/= 0 ) -> ( S =/= (/) /\ E. x e. ZZ A. y e. S y <_ x ) )
19 4 17 18 syl2an2r 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( S =/= (/) /\ E. x e. ZZ A. y e. S y <_ x ) )
20 1 2 gcdcllem2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> R = S )
21 neeq1 
 |-  ( R = S -> ( R =/= (/) <-> S =/= (/) ) )
22 raleq 
 |-  ( R = S -> ( A. y e. R y <_ x <-> A. y e. S y <_ x ) )
23 22 rexbidv 
 |-  ( R = S -> ( E. x e. ZZ A. y e. R y <_ x <-> E. x e. ZZ A. y e. S y <_ x ) )
24 21 23 anbi12d 
 |-  ( R = S -> ( ( R =/= (/) /\ E. x e. ZZ A. y e. R y <_ x ) <-> ( S =/= (/) /\ E. x e. ZZ A. y e. S y <_ x ) ) )
25 20 24 syl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( R =/= (/) /\ E. x e. ZZ A. y e. R y <_ x ) <-> ( S =/= (/) /\ E. x e. ZZ A. y e. S y <_ x ) ) )
26 25 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( R =/= (/) /\ E. x e. ZZ A. y e. R y <_ x ) <-> ( S =/= (/) /\ E. x e. ZZ A. y e. S y <_ x ) ) )
27 19 26 mpbird 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( R =/= (/) /\ E. x e. ZZ A. y e. R y <_ x ) )
28 suprzcl2 
 |-  ( ( R C_ ZZ /\ R =/= (/) /\ E. x e. ZZ A. y e. R y <_ x ) -> sup ( R , RR , < ) e. R )
29 3 28 mp3an1 
 |-  ( ( R =/= (/) /\ E. x e. ZZ A. y e. R y <_ x ) -> sup ( R , RR , < ) e. R )
30 27 29 syl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> sup ( R , RR , < ) e. R )
31 3 30 sselid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> sup ( R , RR , < ) e. ZZ )
32 27 simprd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> E. x e. ZZ A. y e. R y <_ x )
33 1dvds 
 |-  ( M e. ZZ -> 1 || M )
34 1dvds 
 |-  ( N e. ZZ -> 1 || N )
35 33 34 anim12i 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( 1 || M /\ 1 || N ) )
36 1z 
 |-  1 e. ZZ
37 breq1 
 |-  ( z = 1 -> ( z || M <-> 1 || M ) )
38 breq1 
 |-  ( z = 1 -> ( z || N <-> 1 || N ) )
39 37 38 anbi12d 
 |-  ( z = 1 -> ( ( z || M /\ z || N ) <-> ( 1 || M /\ 1 || N ) ) )
40 39 2 elrab2 
 |-  ( 1 e. R <-> ( 1 e. ZZ /\ ( 1 || M /\ 1 || N ) ) )
41 36 40 mpbiran 
 |-  ( 1 e. R <-> ( 1 || M /\ 1 || N ) )
42 35 41 sylibr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> 1 e. R )
43 42 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> 1 e. R )
44 suprzub 
 |-  ( ( R C_ ZZ /\ E. x e. ZZ A. y e. R y <_ x /\ 1 e. R ) -> 1 <_ sup ( R , RR , < ) )
45 3 32 43 44 mp3an2i 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> 1 <_ sup ( R , RR , < ) )
46 elnnz1 
 |-  ( sup ( R , RR , < ) e. NN <-> ( sup ( R , RR , < ) e. ZZ /\ 1 <_ sup ( R , RR , < ) ) )
47 31 45 46 sylanbrc 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> sup ( R , RR , < ) e. NN )
48 breq1 
 |-  ( x = sup ( R , RR , < ) -> ( x || M <-> sup ( R , RR , < ) || M ) )
49 breq1 
 |-  ( x = sup ( R , RR , < ) -> ( x || N <-> sup ( R , RR , < ) || N ) )
50 48 49 anbi12d 
 |-  ( x = sup ( R , RR , < ) -> ( ( x || M /\ x || N ) <-> ( sup ( R , RR , < ) || M /\ sup ( R , RR , < ) || N ) ) )
51 breq1 
 |-  ( z = x -> ( z || M <-> x || M ) )
52 breq1 
 |-  ( z = x -> ( z || N <-> x || N ) )
53 51 52 anbi12d 
 |-  ( z = x -> ( ( z || M /\ z || N ) <-> ( x || M /\ x || N ) ) )
54 53 cbvrabv 
 |-  { z e. ZZ | ( z || M /\ z || N ) } = { x e. ZZ | ( x || M /\ x || N ) }
55 2 54 eqtri 
 |-  R = { x e. ZZ | ( x || M /\ x || N ) }
56 50 55 elrab2 
 |-  ( sup ( R , RR , < ) e. R <-> ( sup ( R , RR , < ) e. ZZ /\ ( sup ( R , RR , < ) || M /\ sup ( R , RR , < ) || N ) ) )
57 30 56 sylib 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( sup ( R , RR , < ) e. ZZ /\ ( sup ( R , RR , < ) || M /\ sup ( R , RR , < ) || N ) ) )
58 57 simprd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( sup ( R , RR , < ) || M /\ sup ( R , RR , < ) || N ) )
59 breq1 
 |-  ( z = K -> ( z || M <-> K || M ) )
60 breq1 
 |-  ( z = K -> ( z || N <-> K || N ) )
61 59 60 anbi12d 
 |-  ( z = K -> ( ( z || M /\ z || N ) <-> ( K || M /\ K || N ) ) )
62 61 2 elrab2 
 |-  ( K e. R <-> ( K e. ZZ /\ ( K || M /\ K || N ) ) )
63 62 biimpri 
 |-  ( ( K e. ZZ /\ ( K || M /\ K || N ) ) -> K e. R )
64 63 3impb 
 |-  ( ( K e. ZZ /\ K || M /\ K || N ) -> K e. R )
65 suprzub 
 |-  ( ( R C_ ZZ /\ E. x e. ZZ A. y e. R y <_ x /\ K e. R ) -> K <_ sup ( R , RR , < ) )
66 65 3expia 
 |-  ( ( R C_ ZZ /\ E. x e. ZZ A. y e. R y <_ x ) -> ( K e. R -> K <_ sup ( R , RR , < ) ) )
67 3 66 mpan 
 |-  ( E. x e. ZZ A. y e. R y <_ x -> ( K e. R -> K <_ sup ( R , RR , < ) ) )
68 32 64 67 syl2im 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( K e. ZZ /\ K || M /\ K || N ) -> K <_ sup ( R , RR , < ) ) )
69 47 58 68 3jca 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( sup ( R , RR , < ) e. NN /\ ( sup ( R , RR , < ) || M /\ sup ( R , RR , < ) || N ) /\ ( ( K e. ZZ /\ K || M /\ K || N ) -> K <_ sup ( R , RR , < ) ) ) )