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 ∈ ℤ | ∀ n ∈ A z ∥ n
Assertion gcdcllem1 ⊢ A ⊆ ℤ ∧ ∃ n ∈ A n ≠ 0 → S ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ S y ≤ x

Proof

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