lcmfunsnlem2

Description: Lemma for lcmfunsn and lcmfunsnlem (Induction step part 2). (Contributed by AV, 26-Aug-2020)

		Ref	Expression
	Assertion	lcmfunsnlem2	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \forall n \in ℤ \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ n (z \in ℤ \land y \subseteq ℤ \land y \in Fin)$
2		nfv	$⊢ Ⅎ n \forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)$
3		nfra1	$⊢ Ⅎ n \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n$
4	2 3	nfan	$⊢ Ⅎ n (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)$
5	1 4	nfan	$⊢ Ⅎ n ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n))$
6		0z	$⊢ 0 \in ℤ$
7		eqoreldif	$⊢ 0 \in ℤ \to (n \in ℤ \leftrightarrow (n = 0 \lor n \in (ℤ ∖ \{0\})))$
8	6 7	ax-mp	$⊢ n \in ℤ \leftrightarrow (n = 0 \lor n \in (ℤ ∖ \{0\}))$
9		simp2	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \subseteq ℤ$
10		snssi	$⊢ z \in ℤ \to \{z\} \subseteq ℤ$
11	10	3ad2ant1	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \{z\} \subseteq ℤ$
12	9 11	unssd	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \cup \{z\} \subseteq ℤ$
13		snssi	$⊢ 0 \in ℤ \to \{0\} \subseteq ℤ$
14	6 13	mp1i	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \{0\} \subseteq ℤ$
15	12 14	unssd	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (y \cup \{z\}) \cup \{0\} \subseteq ℤ$
16		c0ex	$⊢ 0 \in V$
17	16	snid	$⊢ 0 \in \{0\}$
18	17	olci	$⊢ (0 \in (y \cup \{z\}) \lor 0 \in \{0\})$
19		elun	$⊢ 0 \in ((y \cup \{z\}) \cup \{0\}) \leftrightarrow (0 \in (y \cup \{z\}) \lor 0 \in \{0\})$
20	18 19	mpbir	$⊢ 0 \in ((y \cup \{z\}) \cup \{0\})$
21		lcmf0val	$⊢ ((y \cup \{z\}) \cup \{0\} \subseteq ℤ \land 0 \in ((y \cup \{z\}) \cup \{0\})) \to \underline{lcm} ((y \cup \{z\}) \cup \{0\}) = 0$
22	15 20 21	sylancl	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} ((y \cup \{z\}) \cup \{0\}) = 0$
23	22	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n = 0) \to \underline{lcm} ((y \cup \{z\}) \cup \{0\}) = 0$
24		sneq	$⊢ n = 0 \to \{n\} = \{0\}$
25	24	adantl	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n = 0) \to \{n\} = \{0\}$
26	25	uneq2d	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n = 0) \to (y \cup \{z\}) \cup \{n\} = (y \cup \{z\}) \cup \{0\}$
27	26	fveq2d	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n = 0) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} ((y \cup \{z\}) \cup \{0\})$
28		oveq2	$⊢ n = 0 \to \underline{lcm} (y \cup \{z\}) lcm n = \underline{lcm} (y \cup \{z\}) lcm 0$
29		snfi	$⊢ \{z\} \in Fin$
30		unfi	$⊢ (y \in Fin \land \{z\} \in Fin) \to y \cup \{z\} \in Fin$
31	29 30	mpan2	$⊢ y \in Fin \to y \cup \{z\} \in Fin$
32	31	3ad2ant3	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \cup \{z\} \in Fin$
33		lcmfcl	$⊢ (y \cup \{z\} \subseteq ℤ \land y \cup \{z\} \in Fin) \to \underline{lcm} (y \cup \{z\}) \in ℕ_{0}$
34	12 32 33	syl2anc	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y \cup \{z\}) \in ℕ_{0}$
35	34	nn0zd	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y \cup \{z\}) \in ℤ$
36		lcm0val	$⊢ \underline{lcm} (y \cup \{z\}) \in ℤ \to \underline{lcm} (y \cup \{z\}) lcm 0 = 0$
37	35 36	syl	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y \cup \{z\}) lcm 0 = 0$
38	28 37	sylan9eqr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n = 0) \to \underline{lcm} (y \cup \{z\}) lcm n = 0$
39	23 27 38	3eqtr4d	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n = 0) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n$
40	39	ex	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (n = 0 \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)$
41	40	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to (n = 0 \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)$
42	41	com12	$⊢ n = 0 \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)$
43	9	adantl	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to y \subseteq ℤ$
44	11	adantl	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \{z\} \subseteq ℤ$
45	43 44	unssd	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to y \cup \{z\} \subseteq ℤ$
46		elun1	$⊢ 0 \in y \to 0 \in (y \cup \{z\})$
47	46	ad2antrr	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to 0 \in (y \cup \{z\})$
48		lcmf0val	$⊢ (y \cup \{z\} \subseteq ℤ \land 0 \in (y \cup \{z\})) \to \underline{lcm} (y \cup \{z\}) = 0$
49	45 47 48	syl2anc	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \underline{lcm} (y \cup \{z\}) = 0$
50	49	oveq2d	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to n lcm \underline{lcm} (y \cup \{z\}) = n lcm 0$
51		eldifi	$⊢ n \in (ℤ ∖ \{0\}) \to n \in ℤ$
52		lcm0val	$⊢ n \in ℤ \to n lcm 0 = 0$
53	51 52	syl	$⊢ n \in (ℤ ∖ \{0\}) \to n lcm 0 = 0$
54	53	ad2antlr	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to n lcm 0 = 0$
55	50 54	eqtrd	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to n lcm \underline{lcm} (y \cup \{z\}) = 0$
56		simp3	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \in Fin$
57	56 29 30	sylancl	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \cup \{z\} \in Fin$
58	12 57 33	syl2anc	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y \cup \{z\}) \in ℕ_{0}$
59	58	nn0zd	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y \cup \{z\}) \in ℤ$
60	51	adantl	$⊢ (0 \in y \land n \in (ℤ ∖ \{0\})) \to n \in ℤ$
61		lcmcom	$⊢ (\underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ) \to \underline{lcm} (y \cup \{z\}) lcm n = n lcm \underline{lcm} (y \cup \{z\})$
62	59 60 61	syl2anr	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \underline{lcm} (y \cup \{z\}) lcm n = n lcm \underline{lcm} (y \cup \{z\})$
63	12	adantl	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to y \cup \{z\} \subseteq ℤ$
64	51	snssd	$⊢ n \in (ℤ ∖ \{0\}) \to \{n\} \subseteq ℤ$
65	64	ad2antlr	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \{n\} \subseteq ℤ$
66	63 65	unssd	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to (y \cup \{z\}) \cup \{n\} \subseteq ℤ$
67	46	orcd	$⊢ 0 \in y \to (0 \in (y \cup \{z\}) \lor 0 \in \{n\})$
68		elun	$⊢ 0 \in ((y \cup \{z\}) \cup \{n\}) \leftrightarrow (0 \in (y \cup \{z\}) \lor 0 \in \{n\})$
69	67 68	sylibr	$⊢ 0 \in y \to 0 \in ((y \cup \{z\}) \cup \{n\})$
70	69	ad2antrr	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to 0 \in ((y \cup \{z\}) \cup \{n\})$
71		lcmf0val	$⊢ ((y \cup \{z\}) \cup \{n\} \subseteq ℤ \land 0 \in ((y \cup \{z\}) \cup \{n\})) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = 0$
72	66 70 71	syl2anc	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = 0$
73	55 62 72	3eqtr4rd	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n$
74	73	a1d	$⊢ ((0 \in y \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to ((\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)$
75	74	expimpd	$⊢ (0 \in y \land n \in (ℤ ∖ \{0\})) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)$
76	75	ex	$⊢ 0 \in y \to (n \in (ℤ ∖ \{0\}) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n))$
77		elsng	$⊢ 0 \in ℤ \to (0 \in \{z\} \leftrightarrow 0 = z)$
78		eqcom	$⊢ 0 = z \leftrightarrow z = 0$
79	77 78	bitrdi	$⊢ 0 \in ℤ \to (0 \in \{z\} \leftrightarrow z = 0)$
80	6 79	ax-mp	$⊢ 0 \in \{z\} \leftrightarrow z = 0$
81	80	biimpri	$⊢ z = 0 \to 0 \in \{z\}$
82	81	ad2antrr	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to 0 \in \{z\}$
83	82	olcd	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to (0 \in y \lor 0 \in \{z\})$
84		elun	$⊢ 0 \in (y \cup \{z\}) \leftrightarrow (0 \in y \lor 0 \in \{z\})$
85	83 84	sylibr	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to 0 \in (y \cup \{z\})$
86	12 85 48	syl2an2	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \underline{lcm} (y \cup \{z\}) = 0$
87	86	oveq2d	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to n lcm \underline{lcm} (y \cup \{z\}) = n lcm 0$
88	51	ad2antlr	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to n \in ℤ$
89	88 52	syl	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to n lcm 0 = 0$
90	87 89	eqtrd	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to n lcm \underline{lcm} (y \cup \{z\}) = 0$
91	59 88 61	syl2an2	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \underline{lcm} (y \cup \{z\}) lcm n = n lcm \underline{lcm} (y \cup \{z\})$
92	12	adantl	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to y \cup \{z\} \subseteq ℤ$
93	64	ad2antlr	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \{n\} \subseteq ℤ$
94	92 93	unssd	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to (y \cup \{z\}) \cup \{n\} \subseteq ℤ$
95		sneq	$⊢ z = 0 \to \{z\} = \{0\}$
96	17 95	eleqtrrid	$⊢ z = 0 \to 0 \in \{z\}$
97	96	ad2antrr	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to 0 \in \{z\}$
98	97	olcd	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to (0 \in y \lor 0 \in \{z\})$
99	98 84	sylibr	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to 0 \in (y \cup \{z\})$
100	99	orcd	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to (0 \in (y \cup \{z\}) \lor 0 \in \{n\})$
101	100 68	sylibr	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to 0 \in ((y \cup \{z\}) \cup \{n\})$
102	94 101 71	syl2anc	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = 0$
103	90 91 102	3eqtr4rd	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n$
104	103	a1d	$⊢ ((z = 0 \land n \in (ℤ ∖ \{0\})) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to ((\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)$
105	104	expimpd	$⊢ (z = 0 \land n \in (ℤ ∖ \{0\})) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)$
106	105	ex	$⊢ z = 0 \to (n \in (ℤ ∖ \{0\}) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n))$
107		ioran	$⊢ \neg (0 \in y \lor z = 0) \leftrightarrow (\neg 0 \in y \land \neg z = 0)$
108		df-nel	$⊢ 0 \notin y \leftrightarrow \neg 0 \in y$
109		df-ne	$⊢ z \neq 0 \leftrightarrow \neg z = 0$
110	108 109	anbi12i	$⊢ (0 \notin y \land z \neq 0) \leftrightarrow (\neg 0 \in y \land \neg z = 0)$
111	107 110	bitr4i	$⊢ \neg (0 \in y \lor z = 0) \leftrightarrow (0 \notin y \land z \neq 0)$
112		eldif	$⊢ n \in (ℤ ∖ \{0\}) \leftrightarrow (n \in ℤ \land \neg n \in \{0\})$
113		velsn	$⊢ n \in \{0\} \leftrightarrow n = 0$
114	113	bicomi	$⊢ n = 0 \leftrightarrow n \in \{0\}$
115	114	necon3abii	$⊢ n \neq 0 \leftrightarrow \neg n \in \{0\}$
116		lcmfunsnlem2lem2	$⊢ ((0 \notin y \land z \neq 0 \land n \neq 0) \land (n \in ℤ \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)))) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n$
117	116	exp520	$⊢ 0 \notin y \to (z \neq 0 \to (n \neq 0 \to (n \in ℤ \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n))))$
118	117	imp	$⊢ (0 \notin y \land z \neq 0) \to (n \neq 0 \to (n \in ℤ \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)))$
119	115 118	syl5bir	$⊢ (0 \notin y \land z \neq 0) \to (\neg n \in \{0\} \to (n \in ℤ \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)))$
120	119	impcomd	$⊢ (0 \notin y \land z \neq 0) \to ((n \in ℤ \land \neg n \in \{0\}) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n))$
121	112 120	syl5bi	$⊢ (0 \notin y \land z \neq 0) \to (n \in (ℤ ∖ \{0\}) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n))$
122	111 121	sylbi	$⊢ \neg (0 \in y \lor z = 0) \to (n \in (ℤ ∖ \{0\}) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n))$
123	76 106 122	ecase3	$⊢ n \in (ℤ ∖ \{0\}) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)$
124	42 123	jaoi	$⊢ (n = 0 \lor n \in (ℤ ∖ \{0\})) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)$
125	8 124	sylbi	$⊢ n \in ℤ \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)$
126	125	com12	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to (n \in ℤ \to \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n)$
127	5 126	ralrimi	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n)) \to \forall n \in ℤ \underline{lcm} ((y \cup \{z\}) \cup \{n\}) = \underline{lcm} (y \cup \{z\}) lcm n$

Metamath Proof Explorer

Theorem lcmfunsnlem2

Proof