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

Metamath Proof Explorer

Theorem lcmcllem

Description: Lemma for lcmn0cl and dvdslcm . (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmcllem ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } )

Proof

Step Hyp Ref Expression
1 lcmn0val ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) )
2 ssrab2 ⊢ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ⊆ ℕ
3 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
4 2 3 sseqtri ⊢ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ⊆ ( ℤ≥ ‘ 1 )
5 zmulcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
6 5 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
7 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
8 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
9 7 8 anim12i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
10 ioran ⊢ ( ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ↔ ( ¬ 𝑀 = 0 ∧ ¬ 𝑁 = 0 ) )
11 df-ne ⊢ ( 𝑀 ≠ 0 ↔ ¬ 𝑀 = 0 )
12 df-ne ⊢ ( 𝑁 ≠ 0 ↔ ¬ 𝑁 = 0 )
13 11 12 anbi12i ⊢ ( ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ↔ ( ¬ 𝑀 = 0 ∧ ¬ 𝑁 = 0 ) )
14 10 13 sylbb2 ⊢ ( ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) → ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) )
15 mulne0 ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) ∧ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) ≠ 0 )
16 15 an4s ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 · 𝑁 ) ≠ 0 )
17 9 14 16 syl2an ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 · 𝑁 ) ≠ 0 )
18 nnabscl ⊢ ( ( ( 𝑀 · 𝑁 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ≠ 0 ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ℕ )
19 6 17 18 syl2anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ℕ )
20 dvdsmul1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ ( 𝑀 · 𝑁 ) )
21 dvdsabsb ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( 𝑀 ∥ ( 𝑀 · 𝑁 ) ↔ 𝑀 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
22 5 21 syldan ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ ( 𝑀 · 𝑁 ) ↔ 𝑀 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
23 20 22 mpbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) )
24 dvdsmul2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( 𝑀 · 𝑁 ) )
25 dvdsabsb ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( 𝑁 ∥ ( 𝑀 · 𝑁 ) ↔ 𝑁 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
26 5 25 sylan2 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑁 ∥ ( 𝑀 · 𝑁 ) ↔ 𝑁 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
27 26 anabss7 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∥ ( 𝑀 · 𝑁 ) ↔ 𝑁 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
28 24 27 mpbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) )
29 23 28 jca ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ∧ 𝑁 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
30 29 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ∧ 𝑁 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
31 breq2 ⊢ ( 𝑛 = ( abs ‘ ( 𝑀 · 𝑁 ) ) → ( 𝑀 ∥ 𝑛 ↔ 𝑀 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
32 breq2 ⊢ ( 𝑛 = ( abs ‘ ( 𝑀 · 𝑁 ) ) → ( 𝑁 ∥ 𝑛 ↔ 𝑁 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) )
33 31 32 anbi12d ⊢ ( 𝑛 = ( abs ‘ ( 𝑀 · 𝑁 ) ) → ( ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) ↔ ( 𝑀 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ∧ 𝑁 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) )
34 33 rspcev ⊢ ( ( ( abs ‘ ( 𝑀 · 𝑁 ) ) ∈ ℕ ∧ ( 𝑀 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ∧ 𝑁 ∥ ( abs ‘ ( 𝑀 · 𝑁 ) ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) )
35 19 30 34 syl2anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ∃ 𝑛 ∈ ℕ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) )
36 rabn0 ⊢ ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ≠ ∅ ↔ ∃ 𝑛 ∈ ℕ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) )
37 35 36 sylibr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ≠ ∅ )
38 infssuzcl ⊢ ( ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ≠ ∅ ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } )
39 4 37 38 sylancr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } )
40 1 39 eqeltrd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } )