Metamath Proof Explorer

Theorem lcmfunsnlem

Description: Lemma for lcmfdvds and lcmfunsn . These two theorems must be proven simultaneously by induction on the cardinality of a finite set Y , because they depend on each other. This can be seen by the two parts lcmfunsnlem1 and lcmfunsnlem2 of the induction step, each of them using both induction hypotheses. (Contributed by AV, 26-Aug-2020)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( x = (/) -> ( x C_ ZZ <-> (/) C_ ZZ ) )
2 raleq 
 |-  ( x = (/) -> ( A. m e. x m || k <-> A. m e. (/) m || k ) )
3 fveq2 
 |-  ( x = (/) -> ( _lcm ` x ) = ( _lcm ` (/) ) )
4 3 breq1d 
 |-  ( x = (/) -> ( ( _lcm ` x ) || k <-> ( _lcm ` (/) ) || k ) )
5 2 4 imbi12d 
 |-  ( x = (/) -> ( ( A. m e. x m || k -> ( _lcm ` x ) || k ) <-> ( A. m e. (/) m || k -> ( _lcm ` (/) ) || k ) ) )
6 5 ralbidv 
 |-  ( x = (/) -> ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) <-> A. k e. ZZ ( A. m e. (/) m || k -> ( _lcm ` (/) ) || k ) ) )
7 uneq1 
 |-  ( x = (/) -> ( x u. { n } ) = ( (/) u. { n } ) )
8 7 fveq2d 
 |-  ( x = (/) -> ( _lcm ` ( x u. { n } ) ) = ( _lcm ` ( (/) u. { n } ) ) )
9 3 oveq1d 
 |-  ( x = (/) -> ( ( _lcm ` x ) lcm n ) = ( ( _lcm ` (/) ) lcm n ) )
10 8 9 eqeq12d 
 |-  ( x = (/) -> ( ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) <-> ( _lcm ` ( (/) u. { n } ) ) = ( ( _lcm ` (/) ) lcm n ) ) )
11 10 ralbidv 
 |-  ( x = (/) -> ( A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) <-> A. n e. ZZ ( _lcm ` ( (/) u. { n } ) ) = ( ( _lcm ` (/) ) lcm n ) ) )
12 6 11 anbi12d 
 |-  ( x = (/) -> ( ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) /\ A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) ) <-> ( A. k e. ZZ ( A. m e. (/) m || k -> ( _lcm ` (/) ) || k ) /\ A. n e. ZZ ( _lcm ` ( (/) u. { n } ) ) = ( ( _lcm ` (/) ) lcm n ) ) ) )
13 1 12 imbi12d 
 |-  ( x = (/) -> ( ( x C_ ZZ -> ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) /\ A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) ) ) <-> ( (/) C_ ZZ -> ( A. k e. ZZ ( A. m e. (/) m || k -> ( _lcm ` (/) ) || k ) /\ A. n e. ZZ ( _lcm ` ( (/) u. { n } ) ) = ( ( _lcm ` (/) ) lcm n ) ) ) ) )
14 sseq1 
 |-  ( x = y -> ( x C_ ZZ <-> y C_ ZZ ) )
15 raleq 
 |-  ( x = y -> ( A. m e. x m || k <-> A. m e. y m || k ) )
16 fveq2 
 |-  ( x = y -> ( _lcm ` x ) = ( _lcm ` y ) )
17 16 breq1d 
 |-  ( x = y -> ( ( _lcm ` x ) || k <-> ( _lcm ` y ) || k ) )
18 15 17 imbi12d 
 |-  ( x = y -> ( ( A. m e. x m || k -> ( _lcm ` x ) || k ) <-> ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) )
19 18 ralbidv 
 |-  ( x = y -> ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) <-> A. k e. ZZ ( A. m e. y m || k -> ( _lcm ` y ) || k ) ) )
20 uneq1 
 |-  ( x = y -> ( x u. { n } ) = ( y u. { n } ) )
21 20 fveq2d 
 |-  ( x = y -> ( _lcm ` ( x u. { n } ) ) = ( _lcm ` ( y u. { n } ) ) )
22 16 oveq1d 
 |-  ( x = y -> ( ( _lcm ` x ) lcm n ) = ( ( _lcm ` y ) lcm n ) )
23 21 22 eqeq12d 
 |-  ( x = y -> ( ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) <-> ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) )
24 23 ralbidv 
 |-  ( x = y -> ( A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) <-> A. n e. ZZ ( _lcm ` ( y u. { n } ) ) = ( ( _lcm ` y ) lcm n ) ) )
25 19 24 anbi12d 
 |-  ( x = y -> ( ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) /\ A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) ) <-> ( 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 ) ) ) )
26 14 25 imbi12d 
 |-  ( x = y -> ( ( x C_ ZZ -> ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) /\ A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) ) ) <-> ( y C_ ZZ -> ( 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 ) ) ) ) )
27 sseq1 
 |-  ( x = ( y u. { z } ) -> ( x C_ ZZ <-> ( y u. { z } ) C_ ZZ ) )
28 raleq 
 |-  ( x = ( y u. { z } ) -> ( A. m e. x m || k <-> A. m e. ( y u. { z } ) m || k ) )
29 fveq2 
 |-  ( x = ( y u. { z } ) -> ( _lcm ` x ) = ( _lcm ` ( y u. { z } ) ) )
30 29 breq1d 
 |-  ( x = ( y u. { z } ) -> ( ( _lcm ` x ) || k <-> ( _lcm ` ( y u. { z } ) ) || k ) )
31 28 30 imbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( A. m e. x m || k -> ( _lcm ` x ) || k ) <-> ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) )
32 31 ralbidv 
 |-  ( x = ( y u. { z } ) -> ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) <-> A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) ) )
33 uneq1 
 |-  ( x = ( y u. { z } ) -> ( x u. { n } ) = ( ( y u. { z } ) u. { n } ) )
34 33 fveq2d 
 |-  ( x = ( y u. { z } ) -> ( _lcm ` ( x u. { n } ) ) = ( _lcm ` ( ( y u. { z } ) u. { n } ) ) )
35 29 oveq1d 
 |-  ( x = ( y u. { z } ) -> ( ( _lcm ` x ) lcm n ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) )
36 34 35 eqeq12d 
 |-  ( x = ( y u. { z } ) -> ( ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) <-> ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
37 36 ralbidv 
 |-  ( x = ( y u. { z } ) -> ( A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) <-> A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
38 32 37 anbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) /\ A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) ) <-> ( A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) /\ A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) )
39 27 38 imbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( x C_ ZZ -> ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) /\ A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) ) ) <-> ( ( y u. { z } ) C_ ZZ -> ( A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) /\ A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) ) )
40 sseq1 
 |-  ( x = Y -> ( x C_ ZZ <-> Y C_ ZZ ) )
41 raleq 
 |-  ( x = Y -> ( A. m e. x m || k <-> A. m e. Y m || k ) )
42 fveq2 
 |-  ( x = Y -> ( _lcm ` x ) = ( _lcm ` Y ) )
43 42 breq1d 
 |-  ( x = Y -> ( ( _lcm ` x ) || k <-> ( _lcm ` Y ) || k ) )
44 41 43 imbi12d 
 |-  ( x = Y -> ( ( A. m e. x m || k -> ( _lcm ` x ) || k ) <-> ( A. m e. Y m || k -> ( _lcm ` Y ) || k ) ) )
45 44 ralbidv 
 |-  ( x = Y -> ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) <-> A. k e. ZZ ( A. m e. Y m || k -> ( _lcm ` Y ) || k ) ) )
46 uneq1 
 |-  ( x = Y -> ( x u. { n } ) = ( Y u. { n } ) )
47 46 fveq2d 
 |-  ( x = Y -> ( _lcm ` ( x u. { n } ) ) = ( _lcm ` ( Y u. { n } ) ) )
48 42 oveq1d 
 |-  ( x = Y -> ( ( _lcm ` x ) lcm n ) = ( ( _lcm ` Y ) lcm n ) )
49 47 48 eqeq12d 
 |-  ( x = Y -> ( ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) <-> ( _lcm ` ( Y u. { n } ) ) = ( ( _lcm ` Y ) lcm n ) ) )
50 49 ralbidv 
 |-  ( x = Y -> ( A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) <-> A. n e. ZZ ( _lcm ` ( Y u. { n } ) ) = ( ( _lcm ` Y ) lcm n ) ) )
51 45 50 anbi12d 
 |-  ( x = Y -> ( ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) /\ A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) ) <-> ( 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 ) ) ) )
52 40 51 imbi12d 
 |-  ( x = Y -> ( ( x C_ ZZ -> ( A. k e. ZZ ( A. m e. x m || k -> ( _lcm ` x ) || k ) /\ A. n e. ZZ ( _lcm ` ( x u. { n } ) ) = ( ( _lcm ` x ) lcm n ) ) ) <-> ( Y C_ ZZ -> ( 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 ) ) ) ) )
53 lcmf0 
 |-  ( _lcm ` (/) ) = 1
54 1dvds 
 |-  ( k e. ZZ -> 1 || k )
55 53 54 eqbrtrid 
 |-  ( k e. ZZ -> ( _lcm ` (/) ) || k )
56 55 a1d 
 |-  ( k e. ZZ -> ( A. m e. (/) m || k -> ( _lcm ` (/) ) || k ) )
57 56 adantl 
 |-  ( ( (/) C_ ZZ /\ k e. ZZ ) -> ( A. m e. (/) m || k -> ( _lcm ` (/) ) || k ) )
58 57 ralrimiva 
 |-  ( (/) C_ ZZ -> A. k e. ZZ ( A. m e. (/) m || k -> ( _lcm ` (/) ) || k ) )
59 uncom 
 |-  ( (/) u. { n } ) = ( { n } u. (/) )
60 un0 
 |-  ( { n } u. (/) ) = { n }
61 59 60 eqtri 
 |-  ( (/) u. { n } ) = { n }
62 61 a1i 
 |-  ( n e. ZZ -> ( (/) u. { n } ) = { n } )
63 62 fveq2d 
 |-  ( n e. ZZ -> ( _lcm ` ( (/) u. { n } ) ) = ( _lcm ` { n } ) )
64 lcmfsn 
 |-  ( n e. ZZ -> ( _lcm ` { n } ) = ( abs ` n ) )
65 53 a1i 
 |-  ( n e. ZZ -> ( _lcm ` (/) ) = 1 )
66 65 oveq1d 
 |-  ( n e. ZZ -> ( ( _lcm ` (/) ) lcm n ) = ( 1 lcm n ) )
67 1z 
 |-  1 e. ZZ
68 lcmcom 
 |-  ( ( 1 e. ZZ /\ n e. ZZ ) -> ( 1 lcm n ) = ( n lcm 1 ) )
69 67 68 mpan 
 |-  ( n e. ZZ -> ( 1 lcm n ) = ( n lcm 1 ) )
70 lcm1 
 |-  ( n e. ZZ -> ( n lcm 1 ) = ( abs ` n ) )
71 66 69 70 3eqtrrd 
 |-  ( n e. ZZ -> ( abs ` n ) = ( ( _lcm ` (/) ) lcm n ) )
72 63 64 71 3eqtrd 
 |-  ( n e. ZZ -> ( _lcm ` ( (/) u. { n } ) ) = ( ( _lcm ` (/) ) lcm n ) )
73 72 adantl 
 |-  ( ( (/) C_ ZZ /\ n e. ZZ ) -> ( _lcm ` ( (/) u. { n } ) ) = ( ( _lcm ` (/) ) lcm n ) )
74 73 ralrimiva 
 |-  ( (/) C_ ZZ -> A. n e. ZZ ( _lcm ` ( (/) u. { n } ) ) = ( ( _lcm ` (/) ) lcm n ) )
75 58 74 jca 
 |-  ( (/) C_ ZZ -> ( A. k e. ZZ ( A. m e. (/) m || k -> ( _lcm ` (/) ) || k ) /\ A. n e. ZZ ( _lcm ` ( (/) u. { n } ) ) = ( ( _lcm ` (/) ) lcm n ) ) )
76 unss 
 |-  ( ( y C_ ZZ /\ { z } C_ ZZ ) <-> ( y u. { z } ) C_ ZZ )
77 simpl 
 |-  ( ( y C_ ZZ /\ { z } C_ ZZ ) -> y C_ ZZ )
78 76 77 sylbir 
 |-  ( ( y u. { z } ) C_ ZZ -> y C_ ZZ )
79 78 adantl 
 |-  ( ( y e. Fin /\ ( y u. { z } ) C_ ZZ ) -> y C_ ZZ )
80 vex 
 |-  z e. _V
81 80 snss 
 |-  ( z e. ZZ <-> { z } C_ ZZ )
82 lcmfunsnlem1 
 |-  ( ( ( z e. ZZ /\ 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 ) ) ) -> A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) )
83 lcmfunsnlem2 
 |-  ( ( ( z e. ZZ /\ 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 ) ) ) -> A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) )
84 82 83 jca 
 |-  ( ( ( z e. ZZ /\ 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 ) ) ) -> ( A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) /\ A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) )
85 84 3exp1 
 |-  ( z e. ZZ -> ( 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 ) ) -> ( A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) /\ A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) ) ) )
86 81 85 sylbir 
 |-  ( { z } C_ ZZ -> ( 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 ) ) -> ( A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) /\ A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) ) ) )
87 86 impcom 
 |-  ( ( y C_ ZZ /\ { z } 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 ) ) -> ( A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) /\ A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) ) )
88 76 87 sylbir 
 |-  ( ( y u. { z } ) 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 ) ) -> ( A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) /\ A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) ) )
89 88 impcom 
 |-  ( ( y e. Fin /\ ( y u. { z } ) C_ ZZ ) -> ( ( 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 ) ) -> ( A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) /\ A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) )
90 79 89 embantd 
 |-  ( ( y e. Fin /\ ( y u. { z } ) C_ ZZ ) -> ( ( y C_ ZZ -> ( 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 ) ) ) -> ( A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) /\ A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) )
91 90 ex 
 |-  ( y e. Fin -> ( ( y u. { z } ) C_ ZZ -> ( ( y C_ ZZ -> ( 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 ) ) ) -> ( A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) /\ A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) ) )
92 91 com23 
 |-  ( y e. Fin -> ( ( y C_ ZZ -> ( 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 ) ) ) -> ( ( y u. { z } ) C_ ZZ -> ( A. k e. ZZ ( A. m e. ( y u. { z } ) m || k -> ( _lcm ` ( y u. { z } ) ) || k ) /\ A. n e. ZZ ( _lcm ` ( ( y u. { z } ) u. { n } ) ) = ( ( _lcm ` ( y u. { z } ) ) lcm n ) ) ) ) )
93 13 26 39 52 75 92 findcard2 
 |-  ( Y e. Fin -> ( Y C_ ZZ -> ( 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 ) ) ) )
94 93 impcom 
 |-  ( ( 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 ) ) )