lcmfunsnlem2lem2

		Ref	Expression
	Assertion	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$

Proof

Step	Hyp	Ref	Expression
1		elun	$⊢ i \in ((y \cup \{z\}) \cup \{n\}) \leftrightarrow (i \in (y \cup \{z\}) \lor i \in \{n\})$
2		elun	$⊢ i \in (y \cup \{z\}) \leftrightarrow (i \in y \lor i \in \{z\})$
3		simp1	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to z \in ℤ$
4	3	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to z \in ℤ$
5	4	adantl	$⊢ ((i \in y \lor i \in \{z\}) \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to z \in ℤ$
6		sneq	$⊢ n = z \to \{n\} = \{z\}$
7	6	uneq2d	$⊢ n = z \to y \cup \{n\} = y \cup \{z\}$
8	7	fveq2d	$⊢ n = z \to \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y \cup \{z\})$
9		oveq2	$⊢ n = z \to \underline{lcm} (y) lcm n = \underline{lcm} (y) lcm z$
10	8 9	eqeq12d	$⊢ n = z \to (\underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \leftrightarrow \underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z)$
11	10	rspcv	$⊢ z \in ℤ \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to \underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z)$
12	5 11	syl	$⊢ ((i \in y \lor i \in \{z\}) \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to \underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z)$
13		ssel	$⊢ y \subseteq ℤ \to (i \in y \to i \in ℤ)$
14	13	3ad2ant2	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (i \in y \to i \in ℤ)$
15	14	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (i \in y \to i \in ℤ)$
16	15	impcom	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to i \in ℤ$
17		lcmfcl	$⊢ (y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℕ_{0}$
18	17	nn0zd	$⊢ (y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℤ$
19	18	3adant1	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℤ$
20	19	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to \underline{lcm} (y) \in ℤ$
21	20	adantl	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to \underline{lcm} (y) \in ℤ$
22		lcmcl	$⊢ (z \in ℤ \land n \in ℤ) \to z lcm n \in ℕ_{0}$
23	3 22	sylan	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to z lcm n \in ℕ_{0}$
24	23	nn0zd	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to z lcm n \in ℤ$
25	24	adantl	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to z lcm n \in ℤ$
26		lcmcl	$⊢ (\underline{lcm} (y) \in ℤ \land z lcm n \in ℤ) \to \underline{lcm} (y) lcm (z lcm n) \in ℕ_{0}$
27	21 25 26	syl2anc	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to \underline{lcm} (y) lcm (z lcm n) \in ℕ_{0}$
28	27	nn0zd	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to \underline{lcm} (y) lcm (z lcm n) \in ℤ$
29		breq1	$⊢ k = i \to (k ∥ \underline{lcm} (y) \leftrightarrow i ∥ \underline{lcm} (y))$
30	29	rspcv	$⊢ i \in y \to (\forall k \in y k ∥ \underline{lcm} (y) \to i ∥ \underline{lcm} (y))$
31		dvdslcmf	$⊢ (y \subseteq ℤ \land y \in Fin) \to \forall k \in y k ∥ \underline{lcm} (y)$
32	31	3adant1	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \forall k \in y k ∥ \underline{lcm} (y)$
33	32	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to \forall k \in y k ∥ \underline{lcm} (y)$
34	30 33	impel	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to i ∥ \underline{lcm} (y)$
35	20 24	jca	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\underline{lcm} (y) \in ℤ \land z lcm n \in ℤ)$
36	35	adantl	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to (\underline{lcm} (y) \in ℤ \land z lcm n \in ℤ)$
37		dvdslcm	$⊢ (\underline{lcm} (y) \in ℤ \land z lcm n \in ℤ) \to (\underline{lcm} (y) ∥ (\underline{lcm} (y) lcm (z lcm n)) \land (z lcm n) ∥ (\underline{lcm} (y) lcm (z lcm n)))$
38	37	simpld	$⊢ (\underline{lcm} (y) \in ℤ \land z lcm n \in ℤ) \to \underline{lcm} (y) ∥ (\underline{lcm} (y) lcm (z lcm n))$
39	36 38	syl	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to \underline{lcm} (y) ∥ (\underline{lcm} (y) lcm (z lcm n))$
40	16 21 28 34 39	dvdstrd	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to i ∥ (\underline{lcm} (y) lcm (z lcm n))$
41	4	adantl	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to z \in ℤ$
42		simprr	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to n \in ℤ$
43		lcmass	$⊢ (\underline{lcm} (y) \in ℤ \land z \in ℤ \land n \in ℤ) \to (\underline{lcm} (y) lcm z) lcm n = \underline{lcm} (y) lcm (z lcm n)$
44	21 41 42 43	syl3anc	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to (\underline{lcm} (y) lcm z) lcm n = \underline{lcm} (y) lcm (z lcm n)$
45	40 44	breqtrrd	$⊢ (i \in y \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to i ∥ ((\underline{lcm} (y) lcm z) lcm n)$
46	45	ex	$⊢ i \in y \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to i ∥ ((\underline{lcm} (y) lcm z) lcm n))$
47		elsni	$⊢ i \in \{z\} \to i = z$
48	17	3adant1	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℕ_{0}$
49	48	nn0zd	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℤ$
50		lcmcl	$⊢ (\underline{lcm} (y) \in ℤ \land z \in ℤ) \to \underline{lcm} (y) lcm z \in ℕ_{0}$
51	49 3 50	syl2anc	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) lcm z \in ℕ_{0}$
52	51	nn0zd	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) lcm z \in ℤ$
53	52	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to \underline{lcm} (y) lcm z \in ℤ$
54		lcmcl	$⊢ (\underline{lcm} (y) lcm z \in ℤ \land n \in ℤ) \to (\underline{lcm} (y) lcm z) lcm n \in ℕ_{0}$
55	52 54	sylan	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\underline{lcm} (y) lcm z) lcm n \in ℕ_{0}$
56	55	nn0zd	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\underline{lcm} (y) lcm z) lcm n \in ℤ$
57	19 3	jca	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (\underline{lcm} (y) \in ℤ \land z \in ℤ)$
58	57	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\underline{lcm} (y) \in ℤ \land z \in ℤ)$
59		dvdslcm	$⊢ (\underline{lcm} (y) \in ℤ \land z \in ℤ) \to (\underline{lcm} (y) ∥ (\underline{lcm} (y) lcm z) \land z ∥ (\underline{lcm} (y) lcm z))$
60	59	simprd	$⊢ (\underline{lcm} (y) \in ℤ \land z \in ℤ) \to z ∥ (\underline{lcm} (y) lcm z)$
61	58 60	syl	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to z ∥ (\underline{lcm} (y) lcm z)$
62		dvdslcm	$⊢ (\underline{lcm} (y) lcm z \in ℤ \land n \in ℤ) \to ((\underline{lcm} (y) lcm z) ∥ ((\underline{lcm} (y) lcm z) lcm n) \land n ∥ ((\underline{lcm} (y) lcm z) lcm n))$
63	62	simpld	$⊢ (\underline{lcm} (y) lcm z \in ℤ \land n \in ℤ) \to (\underline{lcm} (y) lcm z) ∥ ((\underline{lcm} (y) lcm z) lcm n)$
64	52 63	sylan	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\underline{lcm} (y) lcm z) ∥ ((\underline{lcm} (y) lcm z) lcm n)$
65	4 53 56 61 64	dvdstrd	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to z ∥ ((\underline{lcm} (y) lcm z) lcm n)$
66		breq1	$⊢ i = z \to (i ∥ ((\underline{lcm} (y) lcm z) lcm n) \leftrightarrow z ∥ ((\underline{lcm} (y) lcm z) lcm n))$
67	65 66	imbitrrid	$⊢ i = z \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to i ∥ ((\underline{lcm} (y) lcm z) lcm n))$
68	47 67	syl	$⊢ i \in \{z\} \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to i ∥ ((\underline{lcm} (y) lcm z) lcm n))$
69	46 68	jaoi	$⊢ (i \in y \lor i \in \{z\}) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to i ∥ ((\underline{lcm} (y) lcm z) lcm n))$
70	69	imp	$⊢ ((i \in y \lor i \in \{z\}) \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to i ∥ ((\underline{lcm} (y) lcm z) lcm n)$
71		oveq1	$⊢ \underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \to \underline{lcm} (y \cup \{z\}) lcm n = (\underline{lcm} (y) lcm z) lcm n$
72	71	breq2d	$⊢ \underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \to (i ∥ (\underline{lcm} (y \cup \{z\}) lcm n) \leftrightarrow i ∥ ((\underline{lcm} (y) lcm z) lcm n))$
73	70 72	syl5ibrcom	$⊢ ((i \in y \lor i \in \{z\}) \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to (\underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n))$
74	12 73	syld	$⊢ ((i \in y \lor i \in \{z\}) \land ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ)) \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n))$
75	74	ex	$⊢ (i \in y \lor i \in \{z\}) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n)))$
76	2 75	sylbi	$⊢ i \in (y \cup \{z\}) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n)))$
77		elsni	$⊢ i \in \{n\} \to i = n$
78		simp2	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \subseteq ℤ$
79		snssi	$⊢ z \in ℤ \to \{z\} \subseteq ℤ$
80	79	3ad2ant1	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \{z\} \subseteq ℤ$
81	78 80	unssd	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \cup \{z\} \subseteq ℤ$
82		simp3	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \in Fin$
83		snfi	$⊢ \{z\} \in Fin$
84		unfi	$⊢ (y \in Fin \land \{z\} \in Fin) \to y \cup \{z\} \in Fin$
85	82 83 84	sylancl	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \cup \{z\} \in Fin$
86		lcmfcl	$⊢ (y \cup \{z\} \subseteq ℤ \land y \cup \{z\} \in Fin) \to \underline{lcm} (y \cup \{z\}) \in ℕ_{0}$
87	81 85 86	syl2anc	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y \cup \{z\}) \in ℕ_{0}$
88	87	nn0zd	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y \cup \{z\}) \in ℤ$
89	88	anim1i	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ)$
90	89	adantr	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n) \to (\underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ)$
91		dvdslcm	$⊢ (\underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ) \to (\underline{lcm} (y \cup \{z\}) ∥ (\underline{lcm} (y \cup \{z\}) lcm n) \land n ∥ (\underline{lcm} (y \cup \{z\}) lcm n))$
92	90 91	syl	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n) \to (\underline{lcm} (y \cup \{z\}) ∥ (\underline{lcm} (y \cup \{z\}) lcm n) \land n ∥ (\underline{lcm} (y \cup \{z\}) lcm n))$
93	92	simprd	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n) \to n ∥ (\underline{lcm} (y \cup \{z\}) lcm n)$
94		breq1	$⊢ i = n \to (i ∥ (\underline{lcm} (y \cup \{z\}) lcm n) \leftrightarrow n ∥ (\underline{lcm} (y \cup \{z\}) lcm n))$
95	93 94	imbitrrid	$⊢ i = n \to ((((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n) \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n))$
96	95	expd	$⊢ i = n \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n)))$
97	77 96	syl	$⊢ i \in \{n\} \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n)))$
98	76 97	jaoi	$⊢ (i \in (y \cup \{z\}) \lor i \in \{n\}) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n)))$
99	1 98	sylbi	$⊢ i \in ((y \cup \{z\}) \cup \{n\}) \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n)))$
100	99	com13	$⊢ \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (i \in ((y \cup \{z\}) \cup \{n\}) \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n)))$
101	100	expd	$⊢ \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (n \in ℤ \to (i \in ((y \cup \{z\}) \cup \{n\}) \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n))))$
102	101	adantl	$⊢ (\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 ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (n \in ℤ \to (i \in ((y \cup \{z\}) \cup \{n\}) \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n))))$
103	102	impcom	$⊢ ((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 (i \in ((y \cup \{z\}) \cup \{n\}) \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n)))$
104	103	impcom	$⊢ (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 (i \in ((y \cup \{z\}) \cup \{n\}) \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n))$
105	104	adantl	$⊢ ((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 (i \in ((y \cup \{z\}) \cup \{n\}) \to i ∥ (\underline{lcm} (y \cup \{z\}) lcm n))$
106	105	ralrimiv	$⊢ ((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 \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ (\underline{lcm} (y \cup \{z\}) lcm n)$
107		lcmfunsnlem2lem1	$⊢ ((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 \forall k \in ℕ (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) lcm n \leq k)$
108	89	adantr	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to (\underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ)$
109	81	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to y \cup \{z\} \subseteq ℤ$
110	85	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to y \cup \{z\} \in Fin$
111		df-nel	$⊢ 0 \notin y \leftrightarrow \neg 0 \in y$
112	111	biimpi	$⊢ 0 \notin y \to \neg 0 \in y$
113	112	3ad2ant1	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to \neg 0 \in y$
114		elsni	$⊢ 0 \in \{z\} \to 0 = z$
115	114	eqcomd	$⊢ 0 \in \{z\} \to z = 0$
116	115	necon3ai	$⊢ z \neq 0 \to \neg 0 \in \{z\}$
117	116	3ad2ant2	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to \neg 0 \in \{z\}$
118		ioran	$⊢ \neg (0 \in y \lor 0 \in \{z\}) \leftrightarrow (\neg 0 \in y \land \neg 0 \in \{z\})$
119	113 117 118	sylanbrc	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to \neg (0 \in y \lor 0 \in \{z\})$
120		elun	$⊢ 0 \in (y \cup \{z\}) \leftrightarrow (0 \in y \lor 0 \in \{z\})$
121	119 120	sylnibr	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to \neg 0 \in (y \cup \{z\})$
122		df-nel	$⊢ 0 \notin (y \cup \{z\}) \leftrightarrow \neg 0 \in (y \cup \{z\})$
123	121 122	sylibr	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to 0 \notin (y \cup \{z\})$
124		lcmfn0cl	$⊢ (y \cup \{z\} \subseteq ℤ \land y \cup \{z\} \in Fin \land 0 \notin (y \cup \{z\})) \to \underline{lcm} (y \cup \{z\}) \in ℕ$
125	109 110 123 124	syl2an3an	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to \underline{lcm} (y \cup \{z\}) \in ℕ$
126	125	nnne0d	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to \underline{lcm} (y \cup \{z\}) \neq 0$
127	126	neneqd	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to \neg \underline{lcm} (y \cup \{z\}) = 0$
128		neneq	$⊢ n \neq 0 \to \neg n = 0$
129	128	3ad2ant3	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to \neg n = 0$
130	129	adantl	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to \neg n = 0$
131		ioran	$⊢ \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0) \leftrightarrow (\neg \underline{lcm} (y \cup \{z\}) = 0 \land \neg n = 0)$
132	127 130 131	sylanbrc	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0)$
133		lcmn0cl	$⊢ ((\underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ) \land \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0)) \to \underline{lcm} (y \cup \{z\}) lcm n \in ℕ$
134	108 132 133	syl2anc	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to \underline{lcm} (y \cup \{z\}) lcm n \in ℕ$
135		snssi	$⊢ n \in ℤ \to \{n\} \subseteq ℤ$
136	135	adantl	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to \{n\} \subseteq ℤ$
137	109 136	unssd	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (y \cup \{z\}) \cup \{n\} \subseteq ℤ$
138	137	adantr	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to (y \cup \{z\}) \cup \{n\} \subseteq ℤ$
139	83 84	mpan2	$⊢ y \in Fin \to y \cup \{z\} \in Fin$
140		snfi	$⊢ \{n\} \in Fin$
141		unfi	$⊢ (y \cup \{z\} \in Fin \land \{n\} \in Fin) \to (y \cup \{z\}) \cup \{n\} \in Fin$
142	139 140 141	sylancl	$⊢ y \in Fin \to (y \cup \{z\}) \cup \{n\} \in Fin$
143	142	3ad2ant3	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (y \cup \{z\}) \cup \{n\} \in Fin$
144	143	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to (y \cup \{z\}) \cup \{n\} \in Fin$
145	144	adantr	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to (y \cup \{z\}) \cup \{n\} \in Fin$
146		elun	$⊢ 0 \in ((y \cup \{z\}) \cup \{n\}) \leftrightarrow (0 \in (y \cup \{z\}) \lor 0 \in \{n\})$
147		nnel	$⊢ \neg 0 \notin y \leftrightarrow 0 \in y$
148	147	biimpri	$⊢ 0 \in y \to \neg 0 \notin y$
149	148	3mix1d	$⊢ 0 \in y \to (\neg 0 \notin y \lor \neg z \neq 0 \lor \neg n \neq 0)$
150		nne	$⊢ \neg z \neq 0 \leftrightarrow z = 0$
151	115 150	sylibr	$⊢ 0 \in \{z\} \to \neg z \neq 0$
152	151	3mix2d	$⊢ 0 \in \{z\} \to (\neg 0 \notin y \lor \neg z \neq 0 \lor \neg n \neq 0)$
153	149 152	jaoi	$⊢ (0 \in y \lor 0 \in \{z\}) \to (\neg 0 \notin y \lor \neg z \neq 0 \lor \neg n \neq 0)$
154	120 153	sylbi	$⊢ 0 \in (y \cup \{z\}) \to (\neg 0 \notin y \lor \neg z \neq 0 \lor \neg n \neq 0)$
155		elsni	$⊢ 0 \in \{n\} \to 0 = n$
156	155	eqcomd	$⊢ 0 \in \{n\} \to n = 0$
157		nne	$⊢ \neg n \neq 0 \leftrightarrow n = 0$
158	156 157	sylibr	$⊢ 0 \in \{n\} \to \neg n \neq 0$
159	158	3mix3d	$⊢ 0 \in \{n\} \to (\neg 0 \notin y \lor \neg z \neq 0 \lor \neg n \neq 0)$
160	154 159	jaoi	$⊢ (0 \in (y \cup \{z\}) \lor 0 \in \{n\}) \to (\neg 0 \notin y \lor \neg z \neq 0 \lor \neg n \neq 0)$
161	146 160	sylbi	$⊢ 0 \in ((y \cup \{z\}) \cup \{n\}) \to (\neg 0 \notin y \lor \neg z \neq 0 \lor \neg n \neq 0)$
162		3ianor	$⊢ \neg (0 \notin y \land z \neq 0 \land n \neq 0) \leftrightarrow (\neg 0 \notin y \lor \neg z \neq 0 \lor \neg n \neq 0)$
163	161 162	sylibr	$⊢ 0 \in ((y \cup \{z\}) \cup \{n\}) \to \neg (0 \notin y \land z \neq 0 \land n \neq 0)$
164	163	con2i	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to \neg 0 \in ((y \cup \{z\}) \cup \{n\})$
165		df-nel	$⊢ 0 \notin ((y \cup \{z\}) \cup \{n\}) \leftrightarrow \neg 0 \in ((y \cup \{z\}) \cup \{n\})$
166	164 165	sylibr	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to 0 \notin ((y \cup \{z\}) \cup \{n\})$
167	166	adantl	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to 0 \notin ((y \cup \{z\}) \cup \{n\})$
168	138 145 167	3jca	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to ((y \cup \{z\}) \cup \{n\} \subseteq ℤ \land (y \cup \{z\}) \cup \{n\} \in Fin \land 0 \notin ((y \cup \{z\}) \cup \{n\}))$
169	134 168	jca	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to (\underline{lcm} (y \cup \{z\}) lcm n \in ℕ \land ((y \cup \{z\}) \cup \{n\} \subseteq ℤ \land (y \cup \{z\}) \cup \{n\} \in Fin \land 0 \notin ((y \cup \{z\}) \cup \{n\})))$
170	169	ex	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land n \in ℤ) \to ((0 \notin y \land z \neq 0 \land n \neq 0) \to (\underline{lcm} (y \cup \{z\}) lcm n \in ℕ \land ((y \cup \{z\}) \cup \{n\} \subseteq ℤ \land (y \cup \{z\}) \cup \{n\} \in Fin \land 0 \notin ((y \cup \{z\}) \cup \{n\}))))$
171	170	ex	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (n \in ℤ \to ((0 \notin y \land z \neq 0 \land n \neq 0) \to (\underline{lcm} (y \cup \{z\}) lcm n \in ℕ \land ((y \cup \{z\}) \cup \{n\} \subseteq ℤ \land (y \cup \{z\}) \cup \{n\} \in Fin \land 0 \notin ((y \cup \{z\}) \cup \{n\})))))$
172	171	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 \in ℤ \to ((0 \notin y \land z \neq 0 \land n \neq 0) \to (\underline{lcm} (y \cup \{z\}) lcm n \in ℕ \land ((y \cup \{z\}) \cup \{n\} \subseteq ℤ \land (y \cup \{z\}) \cup \{n\} \in Fin \land 0 \notin ((y \cup \{z\}) \cup \{n\})))))$
173	172	impcom	$⊢ (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 ((0 \notin y \land z \neq 0 \land n \neq 0) \to (\underline{lcm} (y \cup \{z\}) lcm n \in ℕ \land ((y \cup \{z\}) \cup \{n\} \subseteq ℤ \land (y \cup \{z\}) \cup \{n\} \in Fin \land 0 \notin ((y \cup \{z\}) \cup \{n\}))))$
174	173	impcom	$⊢ ((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\}) lcm n \in ℕ \land ((y \cup \{z\}) \cup \{n\} \subseteq ℤ \land (y \cup \{z\}) \cup \{n\} \in Fin \land 0 \notin ((y \cup \{z\}) \cup \{n\})))$
175		lcmf	$⊢ (\underline{lcm} (y \cup \{z\}) lcm n \in ℕ \land ((y \cup \{z\}) \cup \{n\} \subseteq ℤ \land (y \cup \{z\}) \cup \{n\} \in Fin \land 0 \notin ((y \cup \{z\}) \cup \{n\}))) \to (\underline{lcm} (y \cup \{z\}) lcm n = \underline{lcm} ((y \cup \{z\}) \cup \{n\}) \leftrightarrow (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ (\underline{lcm} (y \cup \{z\}) lcm n) \land \forall k \in ℕ (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) lcm n \leq k)))$
176	174 175	syl	$⊢ ((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\}) lcm n = \underline{lcm} ((y \cup \{z\}) \cup \{n\}) \leftrightarrow (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ (\underline{lcm} (y \cup \{z\}) lcm n) \land \forall k \in ℕ (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) lcm n \leq k)))$
177	106 107 176	mpbir2and	$⊢ ((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\}) lcm n = \underline{lcm} ((y \cup \{z\}) \cup \{n\})$
178	177	eqcomd	$⊢ ((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$

Metamath Proof Explorer

Theorem lcmfunsnlem2lem2

Proof