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 Y Fin Z Z Fin lcm _ Y Z = lcm _ Y lcm lcm _ Z

Proof

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