lcmfunsnlem2lem1

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

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ k (0 \notin y \land z \neq 0 \land n \neq 0)$
2		nfv	$⊢ Ⅎ k n \in ℤ$
3		nfv	$⊢ Ⅎ k (z \in ℤ \land y \subseteq ℤ \land y \in Fin)$
4		nfra1	$⊢ Ⅎ k \forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)$
5		nfv	$⊢ Ⅎ k \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n$
6	4 5	nfan	$⊢ Ⅎ k (\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)$
7	3 6	nfan	$⊢ Ⅎ k ((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))$
8	2 7	nfan	$⊢ Ⅎ k (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)))$
9	1 8	nfan	$⊢ Ⅎ k ((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))))$
10		simprr	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to k \in ℕ$
11		simp2	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \subseteq ℤ$
12		snssi	$⊢ z \in ℤ \to \{z\} \subseteq ℤ$
13	12	3ad2ant1	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \{z\} \subseteq ℤ$
14	11 13	unssd	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \cup \{z\} \subseteq ℤ$
15		simp3	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \in Fin$
16		snfi	$⊢ \{z\} \in Fin$
17		unfi	$⊢ (y \in Fin \land \{z\} \in Fin) \to y \cup \{z\} \in Fin$
18	15 16 17	sylancl	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to y \cup \{z\} \in Fin$
19	14 18	jca	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (y \cup \{z\} \subseteq ℤ \land y \cup \{z\} \in Fin)$
20		lcmfcl	$⊢ (y \cup \{z\} \subseteq ℤ \land y \cup \{z\} \in Fin) \to \underline{lcm} (y \cup \{z\}) \in ℕ_{0}$
21	19 20	syl	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y \cup \{z\}) \in ℕ_{0}$
22	21	nn0zd	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y \cup \{z\}) \in ℤ$
23	22	adantl	$⊢ ((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to \underline{lcm} (y \cup \{z\}) \in ℤ$
24	23	adantr	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to \underline{lcm} (y \cup \{z\}) \in ℤ$
25		simprl	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to n \in ℤ$
26	10 24 25	3jca	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to (k \in ℕ \land \underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ)$
27	14	adantl	$⊢ ((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to y \cup \{z\} \subseteq ℤ$
28	18	adantl	$⊢ ((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to y \cup \{z\} \in Fin$
29		df-nel	$⊢ 0 \notin y \leftrightarrow \neg 0 \in y$
30	29	biimpi	$⊢ 0 \notin y \to \neg 0 \in y$
31		elsni	$⊢ 0 \in \{z\} \to 0 = z$
32	31	eqcomd	$⊢ 0 \in \{z\} \to z = 0$
33	32	necon3ai	$⊢ z \neq 0 \to \neg 0 \in \{z\}$
34	30 33	anim12i	$⊢ (0 \notin y \land z \neq 0) \to (\neg 0 \in y \land \neg 0 \in \{z\})$
35	34	3adant3	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to (\neg 0 \in y \land \neg 0 \in \{z\})$
36		df-nel	$⊢ 0 \notin (y \cup \{z\}) \leftrightarrow \neg 0 \in (y \cup \{z\})$
37		ioran	$⊢ \neg (0 \in y \lor 0 \in \{z\}) \leftrightarrow (\neg 0 \in y \land \neg 0 \in \{z\})$
38		elun	$⊢ 0 \in (y \cup \{z\}) \leftrightarrow (0 \in y \lor 0 \in \{z\})$
39	37 38	xchnxbir	$⊢ \neg 0 \in (y \cup \{z\}) \leftrightarrow (\neg 0 \in y \land \neg 0 \in \{z\})$
40	36 39	bitri	$⊢ 0 \notin (y \cup \{z\}) \leftrightarrow (\neg 0 \in y \land \neg 0 \in \{z\})$
41	35 40	sylibr	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to 0 \notin (y \cup \{z\})$
42	41	adantr	$⊢ ((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to 0 \notin (y \cup \{z\})$
43	27 28 42	3jca	$⊢ ((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \to (y \cup \{z\} \subseteq ℤ \land y \cup \{z\} \in Fin \land 0 \notin (y \cup \{z\}))$
44	43	adantr	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to (y \cup \{z\} \subseteq ℤ \land y \cup \{z\} \in Fin \land 0 \notin (y \cup \{z\}))$
45		lcmfn0cl	$⊢ (y \cup \{z\} \subseteq ℤ \land y \cup \{z\} \in Fin \land 0 \notin (y \cup \{z\})) \to \underline{lcm} (y \cup \{z\}) \in ℕ$
46	44 45	syl	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to \underline{lcm} (y \cup \{z\}) \in ℕ$
47	46	nnne0d	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to \underline{lcm} (y \cup \{z\}) \neq 0$
48	47	neneqd	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to \neg \underline{lcm} (y \cup \{z\}) = 0$
49		neneq	$⊢ n \neq 0 \to \neg n = 0$
50	49	3ad2ant3	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to \neg n = 0$
51	50	ad2antrr	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to \neg n = 0$
52	48 51	jca	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to (\neg \underline{lcm} (y \cup \{z\}) = 0 \land \neg n = 0)$
53		ioran	$⊢ \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0) \leftrightarrow (\neg \underline{lcm} (y \cup \{z\}) = 0 \land \neg n = 0)$
54	52 53	sylibr	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0)$
55	26 54	jca	$⊢ (((0 \notin y \land z \neq 0 \land n \neq 0) \land (z \in ℤ \land y \subseteq ℤ \land y \in Fin)) \land (n \in ℤ \land k \in ℕ)) \to ((k \in ℕ \land \underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ) \land \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0))$
56	55	exp43	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (n \in ℤ \to (k \in ℕ \to ((k \in ℕ \land \underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ) \land \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0)))))$
57	56	adantrd	$⊢ (0 \notin y \land z \neq 0 \land n \neq 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 (n \in ℤ \to (k \in ℕ \to ((k \in ℕ \land \underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ) \land \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0)))))$
58	57	com23	$⊢ (0 \notin y \land z \neq 0 \land 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 (k \in ℕ \to ((k \in ℕ \land \underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ) \land \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0)))))$
59	58	imp32	$⊢ ((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 (k \in ℕ \to ((k \in ℕ \land \underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ) \land \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0)))$
60	59	imp	$⊢ (((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)))) \land k \in ℕ) \to ((k \in ℕ \land \underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ) \land \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0))$
61	60	adantr	$⊢ ((((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)))) \land k \in ℕ) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to ((k \in ℕ \land \underline{lcm} (y \cup \{z\}) \in ℤ \land n \in ℤ) \land \neg (\underline{lcm} (y \cup \{z\}) = 0 \lor n = 0))$
62		sneq	$⊢ n = z \to \{n\} = \{z\}$
63	62	uneq2d	$⊢ n = z \to y \cup \{n\} = y \cup \{z\}$
64	63	fveq2d	$⊢ n = z \to \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y \cup \{z\})$
65		oveq2	$⊢ n = z \to \underline{lcm} (y) lcm n = \underline{lcm} (y) lcm z$
66	64 65	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)$
67	66	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)$
68	67	3ad2ant1	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \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)$
69		nnz	$⊢ k \in ℕ \to k \in ℤ$
70	69	adantl	$⊢ (n \in ℤ \land k \in ℕ) \to k \in ℤ$
71	70	adantl	$⊢ (((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 (n \in ℤ \land k \in ℕ)) \to k \in ℤ$
72		lcmfcl	$⊢ (y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℕ_{0}$
73	72	nn0zd	$⊢ (y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℤ$
74	73	3adant1	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℤ$
75	74	ad2antrr	$⊢ (((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 (n \in ℤ \land k \in ℕ)) \to \underline{lcm} (y) \in ℤ$
76		simpll1	$⊢ (((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 (n \in ℤ \land k \in ℕ)) \to z \in ℤ$
77	71 75 76	3jca	$⊢ (((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 (n \in ℤ \land k \in ℕ)) \to (k \in ℤ \land \underline{lcm} (y) \in ℤ \land z \in ℤ)$
78	77	ad2antrr	$⊢ (((((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 (n \in ℤ \land k \in ℕ)) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to (k \in ℤ \land \underline{lcm} (y) \in ℤ \land z \in ℤ)$
79		elun1	$⊢ m \in y \to m \in (y \cup \{z\})$
80	79	orcd	$⊢ m \in y \to (m \in (y \cup \{z\}) \lor m \in \{n\})$
81		elun	$⊢ m \in ((y \cup \{z\}) \cup \{n\}) \leftrightarrow (m \in (y \cup \{z\}) \lor m \in \{n\})$
82	80 81	sylibr	$⊢ m \in y \to m \in ((y \cup \{z\}) \cup \{n\})$
83		breq1	$⊢ i = m \to (i ∥ k \leftrightarrow m ∥ k)$
84	83	rspcv	$⊢ m \in ((y \cup \{z\}) \cup \{n\}) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to m ∥ k)$
85	82 84	syl	$⊢ m \in y \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to m ∥ k)$
86	85	com12	$⊢ \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to (m \in y \to m ∥ k)$
87	86	adantl	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to (m \in y \to m ∥ k)$
88	87	ralrimiv	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to \forall m \in y m ∥ k$
89	88	adantr	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \land ((n \in ℤ \land k \in ℕ) \land (0 \notin y \land z \neq 0 \land n \neq 0))) \to \forall m \in y m ∥ k$
90		breq2	$⊢ k = l \to (m ∥ k \leftrightarrow m ∥ l)$
91	90	ralbidv	$⊢ k = l \to (\forall m \in y m ∥ k \leftrightarrow \forall m \in y m ∥ l)$
92		breq2	$⊢ k = l \to (\underline{lcm} (y) ∥ k \leftrightarrow \underline{lcm} (y) ∥ l)$
93	91 92	imbi12d	$⊢ k = l \to ((\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \leftrightarrow (\forall m \in y m ∥ l \to \underline{lcm} (y) ∥ l))$
94	93	cbvralvw	$⊢ \forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \leftrightarrow \forall l \in ℤ (\forall m \in y m ∥ l \to \underline{lcm} (y) ∥ l)$
95	70	adantr	$⊢ ((n \in ℤ \land k \in ℕ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to k \in ℤ$
96	95	adantl	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \land ((n \in ℤ \land k \in ℕ) \land (0 \notin y \land z \neq 0 \land n \neq 0))) \to k \in ℤ$
97		breq2	$⊢ l = k \to (m ∥ l \leftrightarrow m ∥ k)$
98	97	ralbidv	$⊢ l = k \to (\forall m \in y m ∥ l \leftrightarrow \forall m \in y m ∥ k)$
99		breq2	$⊢ l = k \to (\underline{lcm} (y) ∥ l \leftrightarrow \underline{lcm} (y) ∥ k)$
100	98 99	imbi12d	$⊢ l = k \to ((\forall m \in y m ∥ l \to \underline{lcm} (y) ∥ l) \leftrightarrow (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k))$
101	100	rspcv	$⊢ k \in ℤ \to (\forall l \in ℤ (\forall m \in y m ∥ l \to \underline{lcm} (y) ∥ l) \to (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k))$
102	96 101	syl	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \land ((n \in ℤ \land k \in ℕ) \land (0 \notin y \land z \neq 0 \land n \neq 0))) \to (\forall l \in ℤ (\forall m \in y m ∥ l \to \underline{lcm} (y) ∥ l) \to (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k))$
103	94 102	syl5bi	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \land ((n \in ℤ \land k \in ℕ) \land (0 \notin y \land z \neq 0 \land n \neq 0))) \to (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \to (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k))$
104	89 103	mpid	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \land ((n \in ℤ \land k \in ℕ) \land (0 \notin y \land z \neq 0 \land n \neq 0))) \to (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \to \underline{lcm} (y) ∥ k)$
105	104	exp31	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to (((n \in ℤ \land k \in ℕ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \to \underline{lcm} (y) ∥ k)))$
106	105	com24	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \to (((n \in ℤ \land k \in ℕ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y) ∥ k)))$
107	106	imp	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land \forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)) \to (((n \in ℤ \land k \in ℕ) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y) ∥ k))$
108	107	impl	$⊢ ((((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 (n \in ℤ \land k \in ℕ)) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y) ∥ k)$
109	108	imp	$⊢ (((((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 (n \in ℤ \land k \in ℕ)) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to \underline{lcm} (y) ∥ k$
110		vsnid	$⊢ z \in \{z\}$
111	110	olci	$⊢ (z \in y \lor z \in \{z\})$
112		elun	$⊢ z \in (y \cup \{z\}) \leftrightarrow (z \in y \lor z \in \{z\})$
113	111 112	mpbir	$⊢ z \in (y \cup \{z\})$
114	113	orci	$⊢ (z \in (y \cup \{z\}) \lor z \in \{n\})$
115		elun	$⊢ z \in ((y \cup \{z\}) \cup \{n\}) \leftrightarrow (z \in (y \cup \{z\}) \lor z \in \{n\})$
116	114 115	mpbir	$⊢ z \in ((y \cup \{z\}) \cup \{n\})$
117		breq1	$⊢ i = z \to (i ∥ k \leftrightarrow z ∥ k)$
118	117	rspcv	$⊢ z \in ((y \cup \{z\}) \cup \{n\}) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to z ∥ k)$
119	116 118	mp1i	$⊢ ((((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 (n \in ℤ \land k \in ℕ)) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to z ∥ k)$
120	119	imp	$⊢ (((((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 (n \in ℤ \land k \in ℕ)) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to z ∥ k$
121	109 120	jca	$⊢ (((((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 (n \in ℤ \land k \in ℕ)) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to (\underline{lcm} (y) ∥ k \land z ∥ k)$
122		lcmdvds	$⊢ (k \in ℤ \land \underline{lcm} (y) \in ℤ \land z \in ℤ) \to ((\underline{lcm} (y) ∥ k \land z ∥ k) \to (\underline{lcm} (y) lcm z) ∥ k)$
123	78 121 122	sylc	$⊢ (((((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 (n \in ℤ \land k \in ℕ)) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to (\underline{lcm} (y) lcm z) ∥ k$
124		breq1	$⊢ \underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \to (\underline{lcm} (y \cup \{z\}) ∥ k \leftrightarrow (\underline{lcm} (y) lcm z) ∥ k)$
125	123 124	syl5ibr	$⊢ \underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \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 (n \in ℤ \land k \in ℕ)) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to \underline{lcm} (y \cup \{z\}) ∥ k)$
126	125	expd	$⊢ \underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \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 (n \in ℤ \land k \in ℕ)) \land (0 \notin y \land z \neq 0 \land n \neq 0)) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k))$
127	126	exp5j	$⊢ \underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \to ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \to ((n \in ℤ \land k \in ℕ) \to ((0 \notin y \land z \neq 0 \land n \neq 0) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)))))$
128	127	com12	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (\underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \to (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \to ((n \in ℤ \land k \in ℕ) \to ((0 \notin y \land z \neq 0 \land n \neq 0) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)))))$
129	68 128	syld	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \to ((n \in ℤ \land k \in ℕ) \to ((0 \notin y \land z \neq 0 \land n \neq 0) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)))))$
130	129	com23	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (\forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to ((n \in ℤ \land k \in ℕ) \to ((0 \notin y \land z \neq 0 \land n \neq 0) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)))))$
131	130	imp32	$⊢ ((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 ℤ \land k \in ℕ) \to ((0 \notin y \land z \neq 0 \land n \neq 0) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)))$
132	131	expd	$⊢ ((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 (k \in ℕ \to ((0 \notin y \land z \neq 0 \land n \neq 0) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k))))$
133	132	com34	$⊢ ((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 (k \in ℕ \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k))))$
134	133	com12	$⊢ 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 ((0 \notin y \land z \neq 0 \land n \neq 0) \to (k \in ℕ \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k))))$
135	134	imp	$⊢ (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 (k \in ℕ \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)))$
136	135	com12	$⊢ (0 \notin y \land z \neq 0 \land n \neq 0) \to ((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 (k \in ℕ \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)))$
137	136	imp	$⊢ ((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 (k \in ℕ \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k))$
138	137	imp	$⊢ (((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)))) \land k \in ℕ) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)$
139	138	imp	$⊢ ((((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)))) \land k \in ℕ) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to \underline{lcm} (y \cup \{z\}) ∥ k$
140		vsnid	$⊢ n \in \{n\}$
141	140	olci	$⊢ (n \in (y \cup \{z\}) \lor n \in \{n\})$
142		elun	$⊢ n \in ((y \cup \{z\}) \cup \{n\}) \leftrightarrow (n \in (y \cup \{z\}) \lor n \in \{n\})$
143	141 142	mpbir	$⊢ n \in ((y \cup \{z\}) \cup \{n\})$
144		breq1	$⊢ i = n \to (i ∥ k \leftrightarrow n ∥ k)$
145	144	rspcv	$⊢ n \in ((y \cup \{z\}) \cup \{n\}) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to n ∥ k)$
146	143 145	mp1i	$⊢ (((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)))) \land k \in ℕ) \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to n ∥ k)$
147	146	imp	$⊢ ((((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)))) \land k \in ℕ) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to n ∥ k$
148	139 147	jca	$⊢ ((((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)))) \land k \in ℕ) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to (\underline{lcm} (y \cup \{z\}) ∥ k \land n ∥ k)$
149		lcmledvds	$⊢ ((k \in ℕ \land \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\}) ∥ k \land n ∥ k) \to \underline{lcm} (y \cup \{z\}) lcm n \leq k)$
150	61 148 149	sylc	$⊢ ((((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)))) \land k \in ℕ) \land \forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k) \to \underline{lcm} (y \cup \{z\}) lcm n \leq k$
151	150	exp31	$⊢ ((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 (k \in ℕ \to (\forall i \in ((y \cup \{z\}) \cup \{n\}) i ∥ k \to \underline{lcm} (y \cup \{z\}) lcm n \leq k))$
152	9 151	ralrimi	$⊢ ((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)$

Metamath Proof Explorer

Theorem lcmfunsnlem2lem1

Proof