Metamath Proof Explorer

Theorem gcdcllem3

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

Ref Expression
Hypotheses gcdcllem2.1 ⊢ 𝑆 = { 𝑧 ∈ ℤ ∣ ∀ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑧 ∥ 𝑛 }
gcdcllem2.2 ⊢ 𝑅 = { 𝑧 ∈ ℤ ∣ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) }
Assertion gcdcllem3 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( 𝑅 , ℝ , < ) ∈ ℕ ∧ ( sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ∧ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ sup ( 𝑅 , ℝ , < ) ) ) )

Proof

Step Hyp Ref Expression
1 gcdcllem2.1 ⊢ 𝑆 = { 𝑧 ∈ ℤ ∣ ∀ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑧 ∥ 𝑛 }
2 gcdcllem2.2 ⊢ 𝑅 = { 𝑧 ∈ ℤ ∣ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) }
3 2 ssrab3 ⊢ 𝑅 ⊆ ℤ
4 prssi ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → { 𝑀 , 𝑁 } ⊆ ℤ )
5 neorian ⊢ ( ( 𝑀 ≠ 0 ∨ 𝑁 ≠ 0 ) ↔ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) )
6 prid1g ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ { 𝑀 , 𝑁 } )
7 neeq1 ⊢ ( 𝑛 = 𝑀 → ( 𝑛 ≠ 0 ↔ 𝑀 ≠ 0 ) )
8 7 rspcev ⊢ ( ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 )
9 6 8 sylan ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 )
10 9 adantlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 )
11 prid2g ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ { 𝑀 , 𝑁 } )
12 neeq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ≠ 0 ↔ 𝑁 ≠ 0 ) )
13 12 rspcev ⊢ ( ( 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 )
14 11 13 sylan ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 )
15 14 adantll ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 )
16 10 15 jaodan ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∨ 𝑁 ≠ 0 ) ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 )
17 5 16 sylan2br ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 )
18 1 gcdcllem1 ⊢ ( ( { 𝑀 , 𝑁 } ⊆ ℤ ∧ ∃ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑛 ≠ 0 ) → ( 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) )
19 4 17 18 syl2an2r ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) )
20 1 2 gcdcllem2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑅 = 𝑆 )
21 neeq1 ⊢ ( 𝑅 = 𝑆 → ( 𝑅 ≠ ∅ ↔ 𝑆 ≠ ∅ ) )
22 raleq ⊢ ( 𝑅 = 𝑆 → ( ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) )
23 22 rexbidv ⊢ ( 𝑅 = 𝑆 → ( ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) )
24 21 23 anbi12d ⊢ ( 𝑅 = 𝑆 → ( ( 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) ↔ ( 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) ) )
25 20 24 syl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) ↔ ( 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) ) )
26 25 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) ↔ ( 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) ) )
27 19 26 mpbird ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) )
28 suprzcl2 ⊢ ( ( 𝑅 ⊆ ℤ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) → sup ( 𝑅 , ℝ , < ) ∈ 𝑅 )
29 3 28 mp3an1 ⊢ ( ( 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) → sup ( 𝑅 , ℝ , < ) ∈ 𝑅 )
30 27 29 syl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → sup ( 𝑅 , ℝ , < ) ∈ 𝑅 )
31 3 30 sseldi ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → sup ( 𝑅 , ℝ , < ) ∈ ℤ )
32 27 simprd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 )
33 1dvds ⊢ ( 𝑀 ∈ ℤ → 1 ∥ 𝑀 )
34 1dvds ⊢ ( 𝑁 ∈ ℤ → 1 ∥ 𝑁 )
35 33 34 anim12i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 1 ∥ 𝑀 ∧ 1 ∥ 𝑁 ) )
36 1z ⊢ 1 ∈ ℤ
37 breq1 ⊢ ( 𝑧 = 1 → ( 𝑧 ∥ 𝑀 ↔ 1 ∥ 𝑀 ) )
38 breq1 ⊢ ( 𝑧 = 1 → ( 𝑧 ∥ 𝑁 ↔ 1 ∥ 𝑁 ) )
39 37 38 anbi12d ⊢ ( 𝑧 = 1 → ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ↔ ( 1 ∥ 𝑀 ∧ 1 ∥ 𝑁 ) ) )
40 39 2 elrab2 ⊢ ( 1 ∈ 𝑅 ↔ ( 1 ∈ ℤ ∧ ( 1 ∥ 𝑀 ∧ 1 ∥ 𝑁 ) ) )
41 36 40 mpbiran ⊢ ( 1 ∈ 𝑅 ↔ ( 1 ∥ 𝑀 ∧ 1 ∥ 𝑁 ) )
42 35 41 sylibr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 1 ∈ 𝑅 )
43 42 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → 1 ∈ 𝑅 )
44 suprzub ⊢ ( ( 𝑅 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ∧ 1 ∈ 𝑅 ) → 1 ≤ sup ( 𝑅 , ℝ , < ) )
45 3 32 43 44 mp3an2i ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → 1 ≤ sup ( 𝑅 , ℝ , < ) )
46 elnnz1 ⊢ ( sup ( 𝑅 , ℝ , < ) ∈ ℕ ↔ ( sup ( 𝑅 , ℝ , < ) ∈ ℤ ∧ 1 ≤ sup ( 𝑅 , ℝ , < ) ) )
47 31 45 46 sylanbrc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → sup ( 𝑅 , ℝ , < ) ∈ ℕ )
48 breq1 ⊢ ( 𝑥 = sup ( 𝑅 , ℝ , < ) → ( 𝑥 ∥ 𝑀 ↔ sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ) )
49 breq1 ⊢ ( 𝑥 = sup ( 𝑅 , ℝ , < ) → ( 𝑥 ∥ 𝑁 ↔ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) )
50 48 49 anbi12d ⊢ ( 𝑥 = sup ( 𝑅 , ℝ , < ) → ( ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) ↔ ( sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ∧ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) ) )
51 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∥ 𝑀 ↔ 𝑥 ∥ 𝑀 ) )
52 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∥ 𝑁 ↔ 𝑥 ∥ 𝑁 ) )
53 51 52 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ↔ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) ) )
54 53 cbvrabv ⊢ { 𝑧 ∈ ℤ ∣ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) } = { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) }
55 2 54 eqtri ⊢ 𝑅 = { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) }
56 50 55 elrab2 ⊢ ( sup ( 𝑅 , ℝ , < ) ∈ 𝑅 ↔ ( sup ( 𝑅 , ℝ , < ) ∈ ℤ ∧ ( sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ∧ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) ) )
57 30 56 sylib ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( 𝑅 , ℝ , < ) ∈ ℤ ∧ ( sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ∧ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) ) )
58 57 simprd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ∧ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) )
59 breq1 ⊢ ( 𝑧 = 𝐾 → ( 𝑧 ∥ 𝑀 ↔ 𝐾 ∥ 𝑀 ) )
60 breq1 ⊢ ( 𝑧 = 𝐾 → ( 𝑧 ∥ 𝑁 ↔ 𝐾 ∥ 𝑁 ) )
61 59 60 anbi12d ⊢ ( 𝑧 = 𝐾 → ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ↔ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) )
62 61 2 elrab2 ⊢ ( 𝐾 ∈ 𝑅 ↔ ( 𝐾 ∈ ℤ ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) )
63 62 biimpri ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) → 𝐾 ∈ 𝑅 )
64 63 3impb ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∈ 𝑅 )
65 suprzub ⊢ ( ( 𝑅 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ∧ 𝐾 ∈ 𝑅 ) → 𝐾 ≤ sup ( 𝑅 , ℝ , < ) )
66 65 3expia ⊢ ( ( 𝑅 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ) → ( 𝐾 ∈ 𝑅 → 𝐾 ≤ sup ( 𝑅 , ℝ , < ) ) )
67 3 66 mpan ⊢ ( ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 → ( 𝐾 ∈ 𝑅 → 𝐾 ≤ sup ( 𝑅 , ℝ , < ) ) )
68 32 64 67 syl2im ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ sup ( 𝑅 , ℝ , < ) ) )
69 47 58 68 3jca ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( 𝑅 , ℝ , < ) ∈ ℕ ∧ ( sup ( 𝑅 , ℝ , < ) ∥ 𝑀 ∧ sup ( 𝑅 , ℝ , < ) ∥ 𝑁 ) ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ sup ( 𝑅 , ℝ , < ) ) ) )