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 𝑁 ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } )