Metamath Proof Explorer

Theorem lcmfunsn

Description: The _lcm function for a union of a set of integer and a singleton. (Contributed by AV, 26-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 lcmfunsnlem 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( A. k e. ZZ ( A. m e. Y m || k -> ( _lcm ` Y ) || k ) /\ A. n e. ZZ ( _lcm ` ( Y u. { n } ) ) = ( ( _lcm ` Y ) lcm n ) ) )
2 sneq 
 |-  ( n = N -> { n } = { N } )
3 2 uneq2d 
 |-  ( n = N -> ( Y u. { n } ) = ( Y u. { N } ) )
4 3 fveq2d 
 |-  ( n = N -> ( _lcm ` ( Y u. { n } ) ) = ( _lcm ` ( Y u. { N } ) ) )
5 oveq2 
 |-  ( n = N -> ( ( _lcm ` Y ) lcm n ) = ( ( _lcm ` Y ) lcm N ) )
6 4 5 eqeq12d 
 |-  ( n = N -> ( ( _lcm ` ( Y u. { n } ) ) = ( ( _lcm ` Y ) lcm n ) <-> ( _lcm ` ( Y u. { N } ) ) = ( ( _lcm ` Y ) lcm N ) ) )
7 6 rspccv 
 |-  ( A. n e. ZZ ( _lcm ` ( Y u. { n } ) ) = ( ( _lcm ` Y ) lcm n ) -> ( N e. ZZ -> ( _lcm ` ( Y u. { N } ) ) = ( ( _lcm ` Y ) lcm N ) ) )
8 1 7 simpl2im 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( N e. ZZ -> ( _lcm ` ( Y u. { N } ) ) = ( ( _lcm ` Y ) lcm N ) ) )
9 8 3impia 
 |-  ( ( Y C_ ZZ /\ Y e. Fin /\ N e. ZZ ) -> ( _lcm ` ( Y u. { N } ) ) = ( ( _lcm ` Y ) lcm N ) )