Metamath Proof Explorer

Theorem lcmfass

Description: Associative law for the _lcm function. (Contributed by AV, 27-Aug-2020)

Ref Expression
Assertion lcmfass 
|- ( ( ( Y C_ ZZ /\ Y e. Fin ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> ( _lcm ` ( { ( _lcm ` Y ) } u. Z ) ) = ( _lcm ` ( Y u. { ( _lcm ` Z ) } ) ) )

Proof

Step Hyp Ref Expression
1 lcmfcl 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( _lcm ` Y ) e. NN0 )
2 1 nn0zd 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( _lcm ` Y ) e. ZZ )
3 lcmfsn 
 |-  ( ( _lcm ` Y ) e. ZZ -> ( _lcm ` { ( _lcm ` Y ) } ) = ( abs ` ( _lcm ` Y ) ) )
4 2 3 syl 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( _lcm ` { ( _lcm ` Y ) } ) = ( abs ` ( _lcm ` Y ) ) )
5 nn0re 
 |-  ( ( _lcm ` Y ) e. NN0 -> ( _lcm ` Y ) e. RR )
6 nn0ge0 
 |-  ( ( _lcm ` Y ) e. NN0 -> 0 <_ ( _lcm ` Y ) )
7 5 6 jca 
 |-  ( ( _lcm ` Y ) e. NN0 -> ( ( _lcm ` Y ) e. RR /\ 0 <_ ( _lcm ` Y ) ) )
8 absid 
 |-  ( ( ( _lcm ` Y ) e. RR /\ 0 <_ ( _lcm ` Y ) ) -> ( abs ` ( _lcm ` Y ) ) = ( _lcm ` Y ) )
9 1 7 8 3syl 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( abs ` ( _lcm ` Y ) ) = ( _lcm ` Y ) )
10 4 9 eqtrd 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( _lcm ` { ( _lcm ` Y ) } ) = ( _lcm ` Y ) )
11 lcmfcl 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( _lcm ` Z ) e. NN0 )
12 11 nn0zd 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( _lcm ` Z ) e. ZZ )
13 lcmfsn 
 |-  ( ( _lcm ` Z ) e. ZZ -> ( _lcm ` { ( _lcm ` Z ) } ) = ( abs ` ( _lcm ` Z ) ) )
14 12 13 syl 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( _lcm ` { ( _lcm ` Z ) } ) = ( abs ` ( _lcm ` Z ) ) )
15 nn0re 
 |-  ( ( _lcm ` Z ) e. NN0 -> ( _lcm ` Z ) e. RR )
16 nn0ge0 
 |-  ( ( _lcm ` Z ) e. NN0 -> 0 <_ ( _lcm ` Z ) )
17 15 16 jca 
 |-  ( ( _lcm ` Z ) e. NN0 -> ( ( _lcm ` Z ) e. RR /\ 0 <_ ( _lcm ` Z ) ) )
18 absid 
 |-  ( ( ( _lcm ` Z ) e. RR /\ 0 <_ ( _lcm ` Z ) ) -> ( abs ` ( _lcm ` Z ) ) = ( _lcm ` Z ) )
19 11 17 18 3syl 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( abs ` ( _lcm ` Z ) ) = ( _lcm ` Z ) )
20 14 19 eqtr2d 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( _lcm ` Z ) = ( _lcm ` { ( _lcm ` Z ) } ) )
21 10 20 oveqan12d 
 |-  ( ( ( Y C_ ZZ /\ Y e. Fin ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> ( ( _lcm ` { ( _lcm ` Y ) } ) lcm ( _lcm ` Z ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` { ( _lcm ` Z ) } ) ) )
22 2 snssd 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> { ( _lcm ` Y ) } C_ ZZ )
23 snfi 
 |-  { ( _lcm ` Y ) } e. Fin
24 22 23 jctir 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( { ( _lcm ` Y ) } C_ ZZ /\ { ( _lcm ` Y ) } e. Fin ) )
25 lcmfun 
 |-  ( ( ( { ( _lcm ` Y ) } C_ ZZ /\ { ( _lcm ` Y ) } e. Fin ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> ( _lcm ` ( { ( _lcm ` Y ) } u. Z ) ) = ( ( _lcm ` { ( _lcm ` Y ) } ) lcm ( _lcm ` Z ) ) )
26 24 25 sylan 
 |-  ( ( ( Y C_ ZZ /\ Y e. Fin ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> ( _lcm ` ( { ( _lcm ` Y ) } u. Z ) ) = ( ( _lcm ` { ( _lcm ` Y ) } ) lcm ( _lcm ` Z ) ) )
27 12 snssd 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> { ( _lcm ` Z ) } C_ ZZ )
28 snfi 
 |-  { ( _lcm ` Z ) } e. Fin
29 27 28 jctir 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( { ( _lcm ` Z ) } C_ ZZ /\ { ( _lcm ` Z ) } e. Fin ) )
30 lcmfun 
 |-  ( ( ( Y C_ ZZ /\ Y e. Fin ) /\ ( { ( _lcm ` Z ) } C_ ZZ /\ { ( _lcm ` Z ) } e. Fin ) ) -> ( _lcm ` ( Y u. { ( _lcm ` Z ) } ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` { ( _lcm ` Z ) } ) ) )
31 29 30 sylan2 
 |-  ( ( ( Y C_ ZZ /\ Y e. Fin ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> ( _lcm ` ( Y u. { ( _lcm ` Z ) } ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` { ( _lcm ` Z ) } ) ) )
32 21 26 31 3eqtr4d 
 |-  ( ( ( Y C_ ZZ /\ Y e. Fin ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> ( _lcm ` ( { ( _lcm ` Y ) } u. Z ) ) = ( _lcm ` ( Y u. { ( _lcm ` Z ) } ) ) )