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

Metamath Proof Explorer

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 𝑁 ) ≤ 𝐾 ) )