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

Metamath Proof Explorer

Theorem lcmdvdsb

Description: Biconditional form of lcmdvds . (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion lcmdvdsb ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ↔ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 lcmdvds ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) → ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) )
2 dvdslcm ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ ( 𝑀 lcm 𝑁 ) ∧ 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ) )
3 2 simpld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ ( 𝑀 lcm 𝑁 ) )
4 3 3adant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ ( 𝑀 lcm 𝑁 ) )
5 simp2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ )
6 lcmcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) ∈ ℕ0 )
7 6 nn0zd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) ∈ ℤ )
8 7 3adant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) ∈ ℤ )
9 simp1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℤ )
10 dvdstr ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 lcm 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 ∥ ( 𝑀 lcm 𝑁 ) ∧ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) → 𝑀 ∥ 𝐾 ) )
11 5 8 9 10 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∥ ( 𝑀 lcm 𝑁 ) ∧ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) → 𝑀 ∥ 𝐾 ) )
12 4 11 mpand ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) ∥ 𝐾 → 𝑀 ∥ 𝐾 ) )
13 2 simprd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( 𝑀 lcm 𝑁 ) )
14 13 3adant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( 𝑀 lcm 𝑁 ) )
15 dvdstr ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 lcm 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ∧ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) → 𝑁 ∥ 𝐾 ) )
16 15 3com13 ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 lcm 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ∧ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) → 𝑁 ∥ 𝐾 ) )
17 8 16 syld3an2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ∧ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) → 𝑁 ∥ 𝐾 ) )
18 14 17 mpand ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) ∥ 𝐾 → 𝑁 ∥ 𝐾 ) )
19 12 18 jcad ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) ∥ 𝐾 → ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ) )
20 1 19 impbid ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ↔ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) )