This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gcdcllem1

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

Ref Expression
Hypothesis gcdcllem1.1 ⊢ 𝑆 = { 𝑧 ∈ ℤ ∣ ∀ 𝑛 ∈ 𝐴 𝑧 ∥ 𝑛 }
Assertion gcdcllem1 ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑛 ∈ 𝐴 𝑛 ≠ 0 ) → ( 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) )

Proof

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