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	biimpri	$⊢ \{z\} \subseteq ℤ \to z \in ℤ$
66	65	adantl	$⊢ (y \subseteq ℤ \land \{z\} \subseteq ℤ) \to z \in ℤ$
67	52 66	sylbir	$⊢ y \cup \{z\} \subseteq ℤ \to z \in ℤ$
68	67	adantr	$⊢ (y \cup \{z\} \subseteq ℤ \land (Y \subseteq ℤ \land Y \in Fin)) \to z \in ℤ$
69	68	adantl	$⊢ (y \in Fin \land (y \cup \{z\} \subseteq ℤ \land (Y \subseteq ℤ \land Y \in Fin))) \to z \in ℤ$
70		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$
71	57 62 69 70	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$
72	49 71	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$
73	72	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$
74	54	anim1i	$⊢ (y \cup \{z\} \subseteq ℤ \land (Y \subseteq ℤ \land Y \in Fin)) \to (y \subseteq ℤ \land (Y \subseteq ℤ \land Y \in Fin))$
75	74	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))$
76		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))$
77	75 76	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)$
78	77	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$
79	34	adantl	$⊢ (y \cup \{z\} \subseteq ℤ \land (Y \subseteq ℤ \land Y \in Fin)) \to \underline{lcm} (Y) \in ℤ$
80	79	adantl	$⊢ (y \in Fin \land (y \cup \{z\} \subseteq ℤ \land (Y \subseteq ℤ \land Y \in Fin))) \to \underline{lcm} (Y) \in ℤ$
81	55	anim2i	$⊢ (y \in Fin \land (y \cup \{z\} \subseteq ℤ \land (Y \subseteq ℤ \land Y \in Fin))) \to (y \in Fin \land y \subseteq ℤ)$
82	81	ancomd	$⊢ (y \in Fin \land (y \cup \{z\} \subseteq ℤ \land (Y \subseteq ℤ \land Y \in Fin))) \to (y \subseteq ℤ \land y \in Fin)$
83		lcmfcl	$⊢ (y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℕ_{0}$
84	82 83	syl	$⊢ (y \in Fin \land (y \cup \{z\} \subseteq ℤ \land (Y \subseteq ℤ \land Y \in Fin))) \to \underline{lcm} (y) \in ℕ_{0}$
85	84	nn0zd	$⊢ (y \in Fin \land (y \cup \{z\} \subseteq ℤ \land (Y \subseteq ℤ \land Y \in Fin))) \to \underline{lcm} (y) \in ℤ$
86		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)$
87	80 85 69 86	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)$
88	87	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)$
89	78 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) lcm z = \underline{lcm} (Y) lcm (\underline{lcm} (y) lcm z)$
90	73 89	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)$
91	53	adantr	$⊢ ((y \subseteq ℤ \land \{z\} \subseteq ℤ) \land y \in Fin) \to y \subseteq ℤ$
92		simpr	$⊢ ((y \subseteq ℤ \land \{z\} \subseteq ℤ) \land y \in Fin) \to y \in Fin$
93	66	adantr	$⊢ ((y \subseteq ℤ \land \{z\} \subseteq ℤ) \land y \in Fin) \to z \in ℤ$
94	91 92 93	3jca	$⊢ ((y \subseteq ℤ \land \{z\} \subseteq ℤ) \land y \in Fin) \to (y \subseteq ℤ \land y \in Fin \land z \in ℤ)$
95	94	ex	$⊢ (y \subseteq ℤ \land \{z\} \subseteq ℤ) \to (y \in Fin \to (y \subseteq ℤ \land y \in Fin \land z \in ℤ))$
96	52 95	sylbir	$⊢ y \cup \{z\} \subseteq ℤ \to (y \in Fin \to (y \subseteq ℤ \land y \in Fin \land z \in ℤ))$
97	96	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 ℤ))$
98	97	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 ℤ)$
99		lcmfunsn	$⊢ (y \subseteq ℤ \land y \in Fin \land z \in ℤ) \to \underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z$
100	98 99	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$
101	100	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)$
102	101	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))$
103	102	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))$
104	90 103	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\})$
105	104	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\})))$
106	105	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\})))$
107	11 18 25 32 45 106	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))$
108	107	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)))$
109	108	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))$
110	109	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