Metamath Proof Explorer

Theorem gcdcllem1

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

Ref Expression
Hypothesis gcdcllem1.1 
|- S = { z e. ZZ | A. n e. A z || n }
Assertion gcdcllem1 
|- ( ( A C_ ZZ /\ E. n e. A n =/= 0 ) -> ( S =/= (/) /\ E. x e. ZZ A. y e. S y <_ x ) )

Proof

Step Hyp Ref Expression
1 gcdcllem1.1 
 |-  S = { z e. ZZ | A. n e. A z || n }
2 1z 
 |-  1 e. ZZ
3 ssel 
 |-  ( A C_ ZZ -> ( n e. A -> n e. ZZ ) )
4 1dvds 
 |-  ( n e. ZZ -> 1 || n )
5 3 4 syl6 
 |-  ( A C_ ZZ -> ( n e. A -> 1 || n ) )
6 5 ralrimiv 
 |-  ( A C_ ZZ -> A. n e. A 1 || n )
7 breq1 
 |-  ( z = 1 -> ( z || n <-> 1 || n ) )
8 7 ralbidv 
 |-  ( z = 1 -> ( A. n e. A z || n <-> A. n e. A 1 || n ) )
9 8 1 elrab2 
 |-  ( 1 e. S <-> ( 1 e. ZZ /\ A. n e. A 1 || n ) )
10 9 biimpri 
 |-  ( ( 1 e. ZZ /\ A. n e. A 1 || n ) -> 1 e. S )
11 2 6 10 sylancr 
 |-  ( A C_ ZZ -> 1 e. S )
12 11 ne0d 
 |-  ( A C_ ZZ -> S =/= (/) )
13 12 adantr 
 |-  ( ( A C_ ZZ /\ E. n e. A n =/= 0 ) -> S =/= (/) )
14 neeq1 
 |-  ( n = w -> ( n =/= 0 <-> w =/= 0 ) )
15 14 cbvrexvw 
 |-  ( E. n e. A n =/= 0 <-> E. w e. A w =/= 0 )
16 breq1 
 |-  ( z = y -> ( z || n <-> y || n ) )
17 16 ralbidv 
 |-  ( z = y -> ( A. n e. A z || n <-> A. n e. A y || n ) )
18 17 1 elrab2 
 |-  ( y e. S <-> ( y e. ZZ /\ A. n e. A y || n ) )
19 18 simprbi 
 |-  ( y e. S -> A. n e. A y || n )
20 18 simplbi 
 |-  ( y e. S -> y e. ZZ )
21 ssel2 
 |-  ( ( A C_ ZZ /\ n e. A ) -> n e. ZZ )
22 dvdsleabs 
 |-  ( ( y e. ZZ /\ n e. ZZ /\ n =/= 0 ) -> ( y || n -> y <_ ( abs ` n ) ) )
23 22 3expia 
 |-  ( ( y e. ZZ /\ n e. ZZ ) -> ( n =/= 0 -> ( y || n -> y <_ ( abs ` n ) ) ) )
24 21 23 sylan2 
 |-  ( ( y e. ZZ /\ ( A C_ ZZ /\ n e. A ) ) -> ( n =/= 0 -> ( y || n -> y <_ ( abs ` n ) ) ) )
25 24 anassrs 
 |-  ( ( ( y e. ZZ /\ A C_ ZZ ) /\ n e. A ) -> ( n =/= 0 -> ( y || n -> y <_ ( abs ` n ) ) ) )
26 25 com23 
 |-  ( ( ( y e. ZZ /\ A C_ ZZ ) /\ n e. A ) -> ( y || n -> ( n =/= 0 -> y <_ ( abs ` n ) ) ) )
27 26 ralrimiva 
 |-  ( ( y e. ZZ /\ A C_ ZZ ) -> A. n e. A ( y || n -> ( n =/= 0 -> y <_ ( abs ` n ) ) ) )
28 27 ancoms 
 |-  ( ( A C_ ZZ /\ y e. ZZ ) -> A. n e. A ( y || n -> ( n =/= 0 -> y <_ ( abs ` n ) ) ) )
29 20 28 sylan2 
 |-  ( ( A C_ ZZ /\ y e. S ) -> A. n e. A ( y || n -> ( n =/= 0 -> y <_ ( abs ` n ) ) ) )
30 r19.26 
 |-  ( A. n e. A ( y || n /\ ( y || n -> ( n =/= 0 -> y <_ ( abs ` n ) ) ) ) <-> ( A. n e. A y || n /\ A. n e. A ( y || n -> ( n =/= 0 -> y <_ ( abs ` n ) ) ) ) )
31 pm3.35 
 |-  ( ( y || n /\ ( y || n -> ( n =/= 0 -> y <_ ( abs ` n ) ) ) ) -> ( n =/= 0 -> y <_ ( abs ` n ) ) )
32 31 ralimi 
 |-  ( A. n e. A ( y || n /\ ( y || n -> ( n =/= 0 -> y <_ ( abs ` n ) ) ) ) -> A. n e. A ( n =/= 0 -> y <_ ( abs ` n ) ) )
33 30 32 sylbir 
 |-  ( ( A. n e. A y || n /\ A. n e. A ( y || n -> ( n =/= 0 -> y <_ ( abs ` n ) ) ) ) -> A. n e. A ( n =/= 0 -> y <_ ( abs ` n ) ) )
34 19 29 33 syl2an2 
 |-  ( ( A C_ ZZ /\ y e. S ) -> A. n e. A ( n =/= 0 -> y <_ ( abs ` n ) ) )
35 34 ralrimiva 
 |-  ( A C_ ZZ -> A. y e. S A. n e. A ( n =/= 0 -> y <_ ( abs ` n ) ) )
36 fveq2 
 |-  ( n = w -> ( abs ` n ) = ( abs ` w ) )
37 36 breq2d 
 |-  ( n = w -> ( y <_ ( abs ` n ) <-> y <_ ( abs ` w ) ) )
38 14 37 imbi12d 
 |-  ( n = w -> ( ( n =/= 0 -> y <_ ( abs ` n ) ) <-> ( w =/= 0 -> y <_ ( abs ` w ) ) ) )
39 38 cbvralvw 
 |-  ( A. n e. A ( n =/= 0 -> y <_ ( abs ` n ) ) <-> A. w e. A ( w =/= 0 -> y <_ ( abs ` w ) ) )
40 39 ralbii 
 |-  ( A. y e. S A. n e. A ( n =/= 0 -> y <_ ( abs ` n ) ) <-> A. y e. S A. w e. A ( w =/= 0 -> y <_ ( abs ` w ) ) )
41 ralcom 
 |-  ( A. y e. S A. w e. A ( w =/= 0 -> y <_ ( abs ` w ) ) <-> A. w e. A A. y e. S ( w =/= 0 -> y <_ ( abs ` w ) ) )
42 r19.21v 
 |-  ( A. y e. S ( w =/= 0 -> y <_ ( abs ` w ) ) <-> ( w =/= 0 -> A. y e. S y <_ ( abs ` w ) ) )
43 42 ralbii 
 |-  ( A. w e. A A. y e. S ( w =/= 0 -> y <_ ( abs ` w ) ) <-> A. w e. A ( w =/= 0 -> A. y e. S y <_ ( abs ` w ) ) )
44 40 41 43 3bitri 
 |-  ( A. y e. S A. n e. A ( n =/= 0 -> y <_ ( abs ` n ) ) <-> A. w e. A ( w =/= 0 -> A. y e. S y <_ ( abs ` w ) ) )
45 35 44 sylib 
 |-  ( A C_ ZZ -> A. w e. A ( w =/= 0 -> A. y e. S y <_ ( abs ` w ) ) )
46 ssel2 
 |-  ( ( A C_ ZZ /\ w e. A ) -> w e. ZZ )
47 nn0abscl 
 |-  ( w e. ZZ -> ( abs ` w ) e. NN0 )
48 46 47 syl 
 |-  ( ( A C_ ZZ /\ w e. A ) -> ( abs ` w ) e. NN0 )
49 48 nn0zd 
 |-  ( ( A C_ ZZ /\ w e. A ) -> ( abs ` w ) e. ZZ )
50 breq2 
 |-  ( x = ( abs ` w ) -> ( y <_ x <-> y <_ ( abs ` w ) ) )
51 50 ralbidv 
 |-  ( x = ( abs ` w ) -> ( A. y e. S y <_ x <-> A. y e. S y <_ ( abs ` w ) ) )
52 51 adantl 
 |-  ( ( ( A C_ ZZ /\ w e. A ) /\ x = ( abs ` w ) ) -> ( A. y e. S y <_ x <-> A. y e. S y <_ ( abs ` w ) ) )
53 49 52 rspcedv 
 |-  ( ( A C_ ZZ /\ w e. A ) -> ( A. y e. S y <_ ( abs ` w ) -> E. x e. ZZ A. y e. S y <_ x ) )
54 53 imim2d 
 |-  ( ( A C_ ZZ /\ w e. A ) -> ( ( w =/= 0 -> A. y e. S y <_ ( abs ` w ) ) -> ( w =/= 0 -> E. x e. ZZ A. y e. S y <_ x ) ) )
55 54 ralimdva 
 |-  ( A C_ ZZ -> ( A. w e. A ( w =/= 0 -> A. y e. S y <_ ( abs ` w ) ) -> A. w e. A ( w =/= 0 -> E. x e. ZZ A. y e. S y <_ x ) ) )
56 45 55 mpd 
 |-  ( A C_ ZZ -> A. w e. A ( w =/= 0 -> E. x e. ZZ A. y e. S y <_ x ) )
57 r19.23v 
 |-  ( A. w e. A ( w =/= 0 -> E. x e. ZZ A. y e. S y <_ x ) <-> ( E. w e. A w =/= 0 -> E. x e. ZZ A. y e. S y <_ x ) )
58 56 57 sylib 
 |-  ( A C_ ZZ -> ( E. w e. A w =/= 0 -> E. x e. ZZ A. y e. S y <_ x ) )
59 58 imp 
 |-  ( ( A C_ ZZ /\ E. w e. A w =/= 0 ) -> E. x e. ZZ A. y e. S y <_ x )
60 15 59 sylan2b 
 |-  ( ( A C_ ZZ /\ E. n e. A n =/= 0 ) -> E. x e. ZZ A. y e. S y <_ x )
61 13 60 jca 
 |-  ( ( A C_ ZZ /\ E. n e. A n =/= 0 ) -> ( S =/= (/) /\ E. x e. ZZ A. y e. S y <_ x ) )