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