Metamath Proof Explorer

Theorem lcmfun

Description: The _lcm function for a union of sets of integers. (Contributed by AV, 27-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 cleq1lem 
 |-  ( x = (/) -> ( ( x C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) <-> ( (/) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) )
2 uneq2 
 |-  ( x = (/) -> ( Y u. x ) = ( Y u. (/) ) )
3 un0 
 |-  ( Y u. (/) ) = Y
4 2 3 eqtrdi 
 |-  ( x = (/) -> ( Y u. x ) = Y )
5 4 fveq2d 
 |-  ( x = (/) -> ( _lcm ` ( Y u. x ) ) = ( _lcm ` Y ) )
6 fveq2 
 |-  ( x = (/) -> ( _lcm ` x ) = ( _lcm ` (/) ) )
7 lcmf0 
 |-  ( _lcm ` (/) ) = 1
8 6 7 eqtrdi 
 |-  ( x = (/) -> ( _lcm ` x ) = 1 )
9 8 oveq2d 
 |-  ( x = (/) -> ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) = ( ( _lcm ` Y ) lcm 1 ) )
10 5 9 eqeq12d 
 |-  ( x = (/) -> ( ( _lcm ` ( Y u. x ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) <-> ( _lcm ` Y ) = ( ( _lcm ` Y ) lcm 1 ) ) )
11 1 10 imbi12d 
 |-  ( x = (/) -> ( ( ( x C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. x ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) ) <-> ( ( (/) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` Y ) = ( ( _lcm ` Y ) lcm 1 ) ) ) )
12 cleq1lem 
 |-  ( x = y -> ( ( x C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) <-> ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) )
13 uneq2 
 |-  ( x = y -> ( Y u. x ) = ( Y u. y ) )
14 13 fveq2d 
 |-  ( x = y -> ( _lcm ` ( Y u. x ) ) = ( _lcm ` ( Y u. y ) ) )
15 fveq2 
 |-  ( x = y -> ( _lcm ` x ) = ( _lcm ` y ) )
16 15 oveq2d 
 |-  ( x = y -> ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) )
17 14 16 eqeq12d 
 |-  ( x = y -> ( ( _lcm ` ( Y u. x ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) <-> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) )
18 12 17 imbi12d 
 |-  ( x = y -> ( ( ( x C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. x ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) ) <-> ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) ) )
19 cleq1lem 
 |-  ( x = ( y u. { z } ) -> ( ( x C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) <-> ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) )
20 uneq2 
 |-  ( x = ( y u. { z } ) -> ( Y u. x ) = ( Y u. ( y u. { z } ) ) )
21 20 fveq2d 
 |-  ( x = ( y u. { z } ) -> ( _lcm ` ( Y u. x ) ) = ( _lcm ` ( Y u. ( y u. { z } ) ) ) )
22 fveq2 
 |-  ( x = ( y u. { z } ) -> ( _lcm ` x ) = ( _lcm ` ( y u. { z } ) ) )
23 22 oveq2d 
 |-  ( x = ( y u. { z } ) -> ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` ( y u. { z } ) ) ) )
24 21 23 eqeq12d 
 |-  ( x = ( y u. { z } ) -> ( ( _lcm ` ( Y u. x ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) <-> ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` ( y u. { z } ) ) ) ) )
25 19 24 imbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( ( x C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. x ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) ) <-> ( ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` ( y u. { z } ) ) ) ) ) )
26 cleq1lem 
 |-  ( x = Z -> ( ( x C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) <-> ( Z C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) )
27 uneq2 
 |-  ( x = Z -> ( Y u. x ) = ( Y u. Z ) )
28 27 fveq2d 
 |-  ( x = Z -> ( _lcm ` ( Y u. x ) ) = ( _lcm ` ( Y u. Z ) ) )
29 fveq2 
 |-  ( x = Z -> ( _lcm ` x ) = ( _lcm ` Z ) )
30 29 oveq2d 
 |-  ( x = Z -> ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` Z ) ) )
31 28 30 eqeq12d 
 |-  ( x = Z -> ( ( _lcm ` ( Y u. x ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) <-> ( _lcm ` ( Y u. Z ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` Z ) ) ) )
32 26 31 imbi12d 
 |-  ( x = Z -> ( ( ( x C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. x ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` x ) ) ) <-> ( ( Z C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. Z ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` Z ) ) ) ) )
33 lcmfcl 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( _lcm ` Y ) e. NN0 )
34 33 nn0zd 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( _lcm ` Y ) e. ZZ )
35 lcm1 
 |-  ( ( _lcm ` Y ) e. ZZ -> ( ( _lcm ` Y ) lcm 1 ) = ( abs ` ( _lcm ` Y ) ) )
36 34 35 syl 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( ( _lcm ` Y ) lcm 1 ) = ( abs ` ( _lcm ` Y ) ) )
37 nn0re 
 |-  ( ( _lcm ` Y ) e. NN0 -> ( _lcm ` Y ) e. RR )
38 nn0ge0 
 |-  ( ( _lcm ` Y ) e. NN0 -> 0 <_ ( _lcm ` Y ) )
39 37 38 jca 
 |-  ( ( _lcm ` Y ) e. NN0 -> ( ( _lcm ` Y ) e. RR /\ 0 <_ ( _lcm ` Y ) ) )
40 33 39 syl 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( ( _lcm ` Y ) e. RR /\ 0 <_ ( _lcm ` Y ) ) )
41 absid 
 |-  ( ( ( _lcm ` Y ) e. RR /\ 0 <_ ( _lcm ` Y ) ) -> ( abs ` ( _lcm ` Y ) ) = ( _lcm ` Y ) )
42 40 41 syl 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( abs ` ( _lcm ` Y ) ) = ( _lcm ` Y ) )
43 36 42 eqtrd 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( ( _lcm ` Y ) lcm 1 ) = ( _lcm ` Y ) )
44 43 adantl 
 |-  ( ( (/) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( ( _lcm ` Y ) lcm 1 ) = ( _lcm ` Y ) )
45 44 eqcomd 
 |-  ( ( (/) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` Y ) = ( ( _lcm ` Y ) lcm 1 ) )
46 unass 
 |-  ( ( Y u. y ) u. { z } ) = ( Y u. ( y u. { z } ) )
47 46 eqcomi 
 |-  ( Y u. ( y u. { z } ) ) = ( ( Y u. y ) u. { z } )
48 47 a1i 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( Y u. ( y u. { z } ) ) = ( ( Y u. y ) u. { z } ) )
49 48 fveq2d 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( _lcm ` ( ( Y u. y ) u. { z } ) ) )
50 simpl 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> Y C_ ZZ )
51 50 adantl 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> Y C_ ZZ )
52 unss 
 |-  ( ( y C_ ZZ /\ { z } C_ ZZ ) <-> ( y u. { z } ) C_ ZZ )
53 simpl 
 |-  ( ( y C_ ZZ /\ { z } C_ ZZ ) -> y C_ ZZ )
54 52 53 sylbir 
 |-  ( ( y u. { z } ) C_ ZZ -> y C_ ZZ )
55 54 adantr 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> y C_ ZZ )
56 51 55 unssd 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( Y u. y ) C_ ZZ )
57 56 adantl 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( Y u. y ) C_ ZZ )
58 unfi 
 |-  ( ( Y e. Fin /\ y e. Fin ) -> ( Y u. y ) e. Fin )
59 58 ex 
 |-  ( Y e. Fin -> ( y e. Fin -> ( Y u. y ) e. Fin ) )
60 59 adantl 
 |-  ( ( Y C_ ZZ /\ Y e. Fin ) -> ( y e. Fin -> ( Y u. y ) e. Fin ) )
61 60 adantl 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( y e. Fin -> ( Y u. y ) e. Fin ) )
62 61 impcom 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( Y u. y ) e. Fin )
63 vex 
 |-  z e. _V
64 63 snss 
 |-  ( z e. ZZ <-> { z } C_ ZZ )
65 64 biimpri 
 |-  ( { z } C_ ZZ -> z e. ZZ )
66 65 adantl 
 |-  ( ( y C_ ZZ /\ { z } C_ ZZ ) -> z e. ZZ )
67 52 66 sylbir 
 |-  ( ( y u. { z } ) C_ ZZ -> z e. ZZ )
68 67 adantr 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> z e. ZZ )
69 68 adantl 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> z e. ZZ )
70 lcmfunsn 
 |-  ( ( ( Y u. y ) C_ ZZ /\ ( Y u. y ) e. Fin /\ z e. ZZ ) -> ( _lcm ` ( ( Y u. y ) u. { z } ) ) = ( ( _lcm ` ( Y u. y ) ) lcm z ) )
71 57 62 69 70 syl3anc 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( _lcm ` ( ( Y u. y ) u. { z } ) ) = ( ( _lcm ` ( Y u. y ) ) lcm z ) )
72 49 71 eqtrd 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` ( Y u. y ) ) lcm z ) )
73 72 adantr 
 |-  ( ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) /\ ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) ) -> ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` ( Y u. y ) ) lcm z ) )
74 54 anim1i 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) )
75 74 adantl 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) )
76 id 
 |-  ( ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) -> ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) )
77 75 76 mpan9 
 |-  ( ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) /\ ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) )
78 77 oveq1d 
 |-  ( ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) /\ ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) ) -> ( ( _lcm ` ( Y u. y ) ) lcm z ) = ( ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) lcm z ) )
79 34 adantl 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` Y ) e. ZZ )
80 79 adantl 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( _lcm ` Y ) e. ZZ )
81 55 anim2i 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( y e. Fin /\ y C_ ZZ ) )
82 81 ancomd 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( y C_ ZZ /\ y e. Fin ) )
83 lcmfcl 
 |-  ( ( y C_ ZZ /\ y e. Fin ) -> ( _lcm ` y ) e. NN0 )
84 82 83 syl 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( _lcm ` y ) e. NN0 )
85 84 nn0zd 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( _lcm ` y ) e. ZZ )
86 lcmass 
 |-  ( ( ( _lcm ` Y ) e. ZZ /\ ( _lcm ` y ) e. ZZ /\ z e. ZZ ) -> ( ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) lcm z ) = ( ( _lcm ` Y ) lcm ( ( _lcm ` y ) lcm z ) ) )
87 80 85 69 86 syl3anc 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) lcm z ) = ( ( _lcm ` Y ) lcm ( ( _lcm ` y ) lcm z ) ) )
88 87 adantr 
 |-  ( ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) /\ ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) ) -> ( ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) lcm z ) = ( ( _lcm ` Y ) lcm ( ( _lcm ` y ) lcm z ) ) )
89 78 88 eqtrd 
 |-  ( ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) /\ ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) ) -> ( ( _lcm ` ( Y u. y ) ) lcm z ) = ( ( _lcm ` Y ) lcm ( ( _lcm ` y ) lcm z ) ) )
90 73 89 eqtrd 
 |-  ( ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) /\ ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) ) -> ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` Y ) lcm ( ( _lcm ` y ) lcm z ) ) )
91 53 adantr 
 |-  ( ( ( y C_ ZZ /\ { z } C_ ZZ ) /\ y e. Fin ) -> y C_ ZZ )
92 simpr 
 |-  ( ( ( y C_ ZZ /\ { z } C_ ZZ ) /\ y e. Fin ) -> y e. Fin )
93 66 adantr 
 |-  ( ( ( y C_ ZZ /\ { z } C_ ZZ ) /\ y e. Fin ) -> z e. ZZ )
94 91 92 93 3jca 
 |-  ( ( ( y C_ ZZ /\ { z } C_ ZZ ) /\ y e. Fin ) -> ( y C_ ZZ /\ y e. Fin /\ z e. ZZ ) )
95 94 ex 
 |-  ( ( y C_ ZZ /\ { z } C_ ZZ ) -> ( y e. Fin -> ( y C_ ZZ /\ y e. Fin /\ z e. ZZ ) ) )
96 52 95 sylbir 
 |-  ( ( y u. { z } ) C_ ZZ -> ( y e. Fin -> ( y C_ ZZ /\ y e. Fin /\ z e. ZZ ) ) )
97 96 adantr 
 |-  ( ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( y e. Fin -> ( y C_ ZZ /\ y e. Fin /\ z e. ZZ ) ) )
98 97 impcom 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( y C_ ZZ /\ y e. Fin /\ z e. ZZ ) )
99 lcmfunsn 
 |-  ( ( y C_ ZZ /\ y e. Fin /\ z e. ZZ ) -> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) )
100 98 99 syl 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( _lcm ` ( y u. { z } ) ) = ( ( _lcm ` y ) lcm z ) )
101 100 oveq2d 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( ( _lcm ` Y ) lcm ( _lcm ` ( y u. { z } ) ) ) = ( ( _lcm ` Y ) lcm ( ( _lcm ` y ) lcm z ) ) )
102 101 eqeq2d 
 |-  ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) -> ( ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` ( y u. { z } ) ) ) <-> ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` Y ) lcm ( ( _lcm ` y ) lcm z ) ) ) )
103 102 adantr 
 |-  ( ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) /\ ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) ) -> ( ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` ( y u. { z } ) ) ) <-> ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` Y ) lcm ( ( _lcm ` y ) lcm z ) ) ) )
104 90 103 mpbird 
 |-  ( ( ( y e. Fin /\ ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) ) /\ ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) ) -> ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` ( y u. { z } ) ) ) )
105 104 exp31 
 |-  ( y e. Fin -> ( ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) -> ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` ( y u. { z } ) ) ) ) ) )
106 105 com23 
 |-  ( y e. Fin -> ( ( ( y C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. y ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` y ) ) ) -> ( ( ( y u. { z } ) C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. ( y u. { z } ) ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` ( y u. { z } ) ) ) ) ) )
107 11 18 25 32 45 106 findcard2 
 |-  ( Z e. Fin -> ( ( Z C_ ZZ /\ ( Y C_ ZZ /\ Y e. Fin ) ) -> ( _lcm ` ( Y u. Z ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` Z ) ) ) )
108 107 expd 
 |-  ( Z e. Fin -> ( Z C_ ZZ -> ( ( Y C_ ZZ /\ Y e. Fin ) -> ( _lcm ` ( Y u. Z ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` Z ) ) ) ) )
109 108 impcom 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( ( Y C_ ZZ /\ Y e. Fin ) -> ( _lcm ` ( Y u. Z ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` Z ) ) ) )
110 109 impcom 
 |-  ( ( ( Y C_ ZZ /\ Y e. Fin ) /\ ( Z C_ ZZ /\ Z e. Fin ) ) -> ( _lcm ` ( Y u. Z ) ) = ( ( _lcm ` Y ) lcm ( _lcm ` Z ) ) )