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 sselid ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 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 ( 𝑅 , ℝ , < ) ) ) )