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_⁡Ylcmlcm_⁡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_⁡Ylcmlcm_⁡x=lcm_⁡Ylcm1
10 5 9 eqeq12d ⊢x=∅→lcm_⁡Y∪x=lcm_⁡Ylcmlcm_⁡x↔lcm_⁡Y=lcm_⁡Ylcm1
11 1 10 imbi12d ⊢x=∅→x⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪x=lcm_⁡Ylcmlcm_⁡x↔∅⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y=lcm_⁡Ylcm1
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_⁡Ylcmlcm_⁡x=lcm_⁡Ylcmlcm_⁡y
17 14 16 eqeq12d ⊢x=y→lcm_⁡Y∪x=lcm_⁡Ylcmlcm_⁡x↔lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y
18 12 17 imbi12d ⊢x=y→x⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪x=lcm_⁡Ylcmlcm_⁡x↔y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡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_⁡Ylcmlcm_⁡x=lcm_⁡Ylcmlcm_⁡y∪z
24 21 23 eqeq12d ⊢x=y∪z→lcm_⁡Y∪x=lcm_⁡Ylcmlcm_⁡x↔lcm_⁡Y∪y∪z=lcm_⁡Ylcmlcm_⁡y∪z
25 19 24 imbi12d ⊢x=y∪z→x⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪x=lcm_⁡Ylcmlcm_⁡x↔y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y∪z=lcm_⁡Ylcmlcm_⁡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_⁡Ylcmlcm_⁡x=lcm_⁡Ylcmlcm_⁡Z
31 28 30 eqeq12d ⊢x=Z→lcm_⁡Y∪x=lcm_⁡Ylcmlcm_⁡x↔lcm_⁡Y∪Z=lcm_⁡Ylcmlcm_⁡Z
32 26 31 imbi12d ⊢x=Z→x⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪x=lcm_⁡Ylcmlcm_⁡x↔Z⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪Z=lcm_⁡Ylcmlcm_⁡Z
33 lcmfcl ⊢Y⊆ℤ∧Y∈Fin→lcm_⁡Y∈ℕ0
34 33 nn0zd ⊢Y⊆ℤ∧Y∈Fin→lcm_⁡Y∈ℤ
35 lcm1 ⊢lcm_⁡Y∈ℤ→lcm_⁡Ylcm1=lcm_⁡Y
36 34 35 syl ⊢Y⊆ℤ∧Y∈Fin→lcm_⁡Ylcm1=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_⁡Ylcm1=lcm_⁡Y
44 43 adantl ⊢∅⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Ylcm1=lcm_⁡Y
45 44 eqcomd ⊢∅⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y=lcm_⁡Ylcm1
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∪ylcmz
71 57 62 69 70 syl3anc ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y∪z=lcm_⁡Y∪ylcmz
72 49 71 eqtrd ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y∪z=lcm_⁡Y∪ylcmz
73 72 adantr ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin∧y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y→lcm_⁡Y∪y∪z=lcm_⁡Y∪ylcmz
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_⁡Ylcmlcm_⁡y→y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y
77 75 76 mpan9 ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin∧y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y
78 77 oveq1d ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin∧y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y→lcm_⁡Y∪ylcmz=lcm_⁡Ylcmlcm_⁡ylcmz
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_⁡Ylcmlcm_⁡ylcmz=lcm_⁡Ylcmlcm_⁡ylcmz
87 80 85 69 86 syl3anc ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Ylcmlcm_⁡ylcmz=lcm_⁡Ylcmlcm_⁡ylcmz
88 87 adantr ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin∧y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y→lcm_⁡Ylcmlcm_⁡ylcmz=lcm_⁡Ylcmlcm_⁡ylcmz
89 78 88 eqtrd ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin∧y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y→lcm_⁡Y∪ylcmz=lcm_⁡Ylcmlcm_⁡ylcmz
90 73 89 eqtrd ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin∧y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y→lcm_⁡Y∪y∪z=lcm_⁡Ylcmlcm_⁡ylcmz
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_⁡ylcmz
100 98 99 syl ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡y∪z=lcm_⁡ylcmz
101 100 oveq2d ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Ylcmlcm_⁡y∪z=lcm_⁡Ylcmlcm_⁡ylcmz
102 101 eqeq2d ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y∪z=lcm_⁡Ylcmlcm_⁡y∪z↔lcm_⁡Y∪y∪z=lcm_⁡Ylcmlcm_⁡ylcmz
103 102 adantr ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin∧y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y→lcm_⁡Y∪y∪z=lcm_⁡Ylcmlcm_⁡y∪z↔lcm_⁡Y∪y∪z=lcm_⁡Ylcmlcm_⁡ylcmz
104 90 103 mpbird ⊢y∈Fin∧y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin∧y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y→lcm_⁡Y∪y∪z=lcm_⁡Ylcmlcm_⁡y∪z
105 104 exp31 ⊢y∈Fin→y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin→y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y→lcm_⁡Y∪y∪z=lcm_⁡Ylcmlcm_⁡y∪z
106 105 com23 ⊢y∈Fin→y⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y=lcm_⁡Ylcmlcm_⁡y→y∪z⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪y∪z=lcm_⁡Ylcmlcm_⁡y∪z
107 11 18 25 32 45 106 findcard2 ⊢Z∈Fin→Z⊆ℤ∧Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪Z=lcm_⁡Ylcmlcm_⁡Z
108 107 expd ⊢Z∈Fin→Z⊆ℤ→Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪Z=lcm_⁡Ylcmlcm_⁡Z
109 108 impcom ⊢Z⊆ℤ∧Z∈Fin→Y⊆ℤ∧Y∈Fin→lcm_⁡Y∪Z=lcm_⁡Ylcmlcm_⁡Z
110 109 impcom ⊢Y⊆ℤ∧Y∈Fin∧Z⊆ℤ∧Z∈Fin→lcm_⁡Y∪Z=lcm_⁡Ylcmlcm_⁡Z