lcmfun

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

		Ref	Expression
	Assertion	lcmfun	$⊢ ((Y \subseteq ℤ \land Y \in Fin) \land (Z \subseteq ℤ \land Z \in Fin)) \to \underline{lcm} (Y \cup Z) = \underline{lcm} (Y) lcm \underline{lcm} (Z)$

Proof

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

Metamath Proof Explorer

Theorem lcmfun

Proof