Theorem lcmledvds

Description: A positive integer which both operands of the lcm operator divide bounds it. (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

	Ref	Expression
Assertion	lcmledvds	⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) → ( 𝑀 lcm 𝑁 ) ≤ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		lcmn0val	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) )
2	1	3adantl1	⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) )
3	2	adantr	⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) ∧ ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ) → ( 𝑀 lcm 𝑁 ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) )
4		breq2	⊢ ( 𝑛 = 𝐾 → ( 𝑀 ∥ 𝑛 ↔ 𝑀 ∥ 𝐾 ) )
5		breq2	⊢ ( 𝑛 = 𝐾 → ( 𝑁 ∥ 𝑛 ↔ 𝑁 ∥ 𝐾 ) )
6	4 5	anbi12d	⊢ ( 𝑛 = 𝐾 → ( ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) ↔ ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ) )
7	6	elrab	⊢ ( 𝐾 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ↔ ( 𝐾 ∈ ℕ ∧ ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ) )
8		ssrab2	⊢ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ⊆ ℕ
9		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
10	8 9	sseqtri	⊢ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ⊆ ( ℤ≥ ‘ 1 )
11		infssuzle	⊢ ( ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝐾 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ≤ 𝐾 )
12	10 11	mpan	⊢ ( 𝐾 ∈ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } → inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ≤ 𝐾 )
13	7 12	sylbir	⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ≤ 𝐾 )
14	13	ex	⊢ ( 𝐾 ∈ ℕ → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ≤ 𝐾 ) )
15	14	3ad2ant1	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ≤ 𝐾 ) )
16	15	adantr	⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ≤ 𝐾 ) )
17	16	imp	⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) ∧ ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ≤ 𝐾 )
18	3 17	eqbrtrd	⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) ∧ ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ) → ( 𝑀 lcm 𝑁 ) ≤ 𝐾 )
19	18	ex	⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) → ( 𝑀 lcm 𝑁 ) ≤ 𝐾 ) )