Metamath Proof Explorer

Theorem lcmfdvdsb

Description: Biconditional form of lcmfdvds . (Contributed by AV, 26-Aug-2020)

Ref Expression
Assertion lcmfdvdsb 
|- ( ( K e. ZZ /\ Z C_ ZZ /\ Z e. Fin ) -> ( A. m e. Z m || K <-> ( _lcm ` Z ) || K ) )

Proof

Step Hyp Ref Expression
1 lcmfdvds 
 |-  ( ( K e. ZZ /\ Z C_ ZZ /\ Z e. Fin ) -> ( A. m e. Z m || K -> ( _lcm ` Z ) || K ) )
2 dvdslcmf 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> A. x e. Z x || ( _lcm ` Z ) )
3 breq1 
 |-  ( x = m -> ( x || ( _lcm ` Z ) <-> m || ( _lcm ` Z ) ) )
4 3 rspcv 
 |-  ( m e. Z -> ( A. x e. Z x || ( _lcm ` Z ) -> m || ( _lcm ` Z ) ) )
5 ssel 
 |-  ( Z C_ ZZ -> ( m e. Z -> m e. ZZ ) )
6 5 adantr 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( m e. Z -> m e. ZZ ) )
7 6 com12 
 |-  ( m e. Z -> ( ( Z C_ ZZ /\ Z e. Fin ) -> m e. ZZ ) )
8 7 adantr 
 |-  ( ( m e. Z /\ K e. ZZ ) -> ( ( Z C_ ZZ /\ Z e. Fin ) -> m e. ZZ ) )
9 8 imp 
 |-  ( ( ( m e. Z /\ K e. ZZ ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> m e. ZZ )
10 lcmfcl 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( _lcm ` Z ) e. NN0 )
11 10 nn0zd 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( _lcm ` Z ) e. ZZ )
12 11 adantl 
 |-  ( ( ( m e. Z /\ K e. ZZ ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> ( _lcm ` Z ) e. ZZ )
13 simplr 
 |-  ( ( ( m e. Z /\ K e. ZZ ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> K e. ZZ )
14 dvdstr 
 |-  ( ( m e. ZZ /\ ( _lcm ` Z ) e. ZZ /\ K e. ZZ ) -> ( ( m || ( _lcm ` Z ) /\ ( _lcm ` Z ) || K ) -> m || K ) )
15 9 12 13 14 syl3anc 
 |-  ( ( ( m e. Z /\ K e. ZZ ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> ( ( m || ( _lcm ` Z ) /\ ( _lcm ` Z ) || K ) -> m || K ) )
16 15 expd 
 |-  ( ( ( m e. Z /\ K e. ZZ ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> ( m || ( _lcm ` Z ) -> ( ( _lcm ` Z ) || K -> m || K ) ) )
17 16 exp31 
 |-  ( m e. Z -> ( K e. ZZ -> ( ( Z C_ ZZ /\ Z e. Fin ) -> ( m || ( _lcm ` Z ) -> ( ( _lcm ` Z ) || K -> m || K ) ) ) ) )
18 17 com23 
 |-  ( m e. Z -> ( ( Z C_ ZZ /\ Z e. Fin ) -> ( K e. ZZ -> ( m || ( _lcm ` Z ) -> ( ( _lcm ` Z ) || K -> m || K ) ) ) ) )
19 18 com24 
 |-  ( m e. Z -> ( m || ( _lcm ` Z ) -> ( K e. ZZ -> ( ( Z C_ ZZ /\ Z e. Fin ) -> ( ( _lcm ` Z ) || K -> m || K ) ) ) ) )
20 19 com45 
 |-  ( m e. Z -> ( m || ( _lcm ` Z ) -> ( K e. ZZ -> ( ( _lcm ` Z ) || K -> ( ( Z C_ ZZ /\ Z e. Fin ) -> m || K ) ) ) ) )
21 4 20 syld 
 |-  ( m e. Z -> ( A. x e. Z x || ( _lcm ` Z ) -> ( K e. ZZ -> ( ( _lcm ` Z ) || K -> ( ( Z C_ ZZ /\ Z e. Fin ) -> m || K ) ) ) ) )
22 21 com15 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( A. x e. Z x || ( _lcm ` Z ) -> ( K e. ZZ -> ( ( _lcm ` Z ) || K -> ( m e. Z -> m || K ) ) ) ) )
23 2 22 mpd 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( K e. ZZ -> ( ( _lcm ` Z ) || K -> ( m e. Z -> m || K ) ) ) )
24 23 com12 
 |-  ( K e. ZZ -> ( ( Z C_ ZZ /\ Z e. Fin ) -> ( ( _lcm ` Z ) || K -> ( m e. Z -> m || K ) ) ) )
25 24 3impib 
 |-  ( ( K e. ZZ /\ Z C_ ZZ /\ Z e. Fin ) -> ( ( _lcm ` Z ) || K -> ( m e. Z -> m || K ) ) )
26 25 ralrimdv 
 |-  ( ( K e. ZZ /\ Z C_ ZZ /\ Z e. Fin ) -> ( ( _lcm ` Z ) || K -> A. m e. Z m || K ) )
27 1 26 impbid 
 |-  ( ( K e. ZZ /\ Z C_ ZZ /\ Z e. Fin ) -> ( A. m e. Z m || K <-> ( _lcm ` Z ) || K ) )