Metamath Proof Explorer

Theorem lcmdvdsb

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

Ref Expression
Assertion lcmdvdsb 
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M || K /\ N || K ) <-> ( M lcm N ) || K ) )

Proof

Step Hyp Ref Expression
1 lcmdvds 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
2 dvdslcm 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) )
3 2 simpld 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M || ( M lcm N ) )
4 3 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> M || ( M lcm N ) )
5 simp2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> M e. ZZ )
6 lcmcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. NN0 )
7 6 nn0zd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. ZZ )
8 7 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. ZZ )
9 simp1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> K e. ZZ )
10 dvdstr 
 |-  ( ( M e. ZZ /\ ( M lcm N ) e. ZZ /\ K e. ZZ ) -> ( ( M || ( M lcm N ) /\ ( M lcm N ) || K ) -> M || K ) )
11 5 8 9 10 syl3anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M || ( M lcm N ) /\ ( M lcm N ) || K ) -> M || K ) )
12 4 11 mpand 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) || K -> M || K ) )
13 2 simprd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N || ( M lcm N ) )
14 13 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> N || ( M lcm N ) )
15 dvdstr 
 |-  ( ( N e. ZZ /\ ( M lcm N ) e. ZZ /\ K e. ZZ ) -> ( ( N || ( M lcm N ) /\ ( M lcm N ) || K ) -> N || K ) )
16 15 3com13 
 |-  ( ( K e. ZZ /\ ( M lcm N ) e. ZZ /\ N e. ZZ ) -> ( ( N || ( M lcm N ) /\ ( M lcm N ) || K ) -> N || K ) )
17 8 16 syld3an2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( N || ( M lcm N ) /\ ( M lcm N ) || K ) -> N || K ) )
18 14 17 mpand 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) || K -> N || K ) )
19 12 18 jcad 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) || K -> ( M || K /\ N || K ) ) )
20 1 19 impbid 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M || K /\ N || K ) <-> ( M lcm N ) || K ) )