lcmfunsnlem1

Description: Lemma for lcmfdvds and lcmfunsnlem (Induction step part 1). (Contributed by AV, 25-Aug-2020)

		Ref	Expression
	Assertion	lcmfunsnlem1	$⊢ ((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 m \in (y \cup \{z\}) m ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ k (z \in ℤ \land y \subseteq ℤ \land y \in Fin)$
2		nfra1	$⊢ Ⅎ k \forall k \in ℤ (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)$
3		nfv	$⊢ Ⅎ k \forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n$
4	2 3	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)$
5	1 4	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))$
6		breq2	$⊢ k = l \to (m ∥ k \leftrightarrow m ∥ l)$
7	6	ralbidv	$⊢ k = l \to (\forall m \in y m ∥ k \leftrightarrow \forall m \in y m ∥ l)$
8		breq2	$⊢ k = l \to (\underline{lcm} (y) ∥ k \leftrightarrow \underline{lcm} (y) ∥ l)$
9	7 8	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))$
10	9	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)$
11		breq2	$⊢ l = k \to (m ∥ l \leftrightarrow m ∥ k)$
12	11	ralbidv	$⊢ l = k \to (\forall m \in y m ∥ l \leftrightarrow \forall m \in y m ∥ k)$
13		breq2	$⊢ l = k \to (\underline{lcm} (y) ∥ l \leftrightarrow \underline{lcm} (y) ∥ k)$
14	12 13	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))$
15	14	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))$
16	15	adantl	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land 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))$
17		sneq	$⊢ n = z \to \{n\} = \{z\}$
18	17	uneq2d	$⊢ n = z \to y \cup \{n\} = y \cup \{z\}$
19	18	fveq2d	$⊢ n = z \to \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y \cup \{z\})$
20		oveq2	$⊢ n = z \to \underline{lcm} (y) lcm n = \underline{lcm} (y) lcm z$
21	19 20	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)$
22	21	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)$
23	22	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)$
24	23	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \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)$
25		simpr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \to k \in ℤ$
26		lcmfcl	$⊢ (y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℕ_{0}$
27	26	nn0zd	$⊢ (y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℤ$
28	27	3adant1	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to \underline{lcm} (y) \in ℤ$
29	28	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \to \underline{lcm} (y) \in ℤ$
30		simpl1	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \to z \in ℤ$
31	25 29 30	3jca	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \to (k \in ℤ \land \underline{lcm} (y) \in ℤ \land z \in ℤ)$
32	31	adantr	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \land (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)) \to (k \in ℤ \land \underline{lcm} (y) \in ℤ \land z \in ℤ)$
33	32	adantr	$⊢ ((((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \land (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)) \land \forall m \in (y \cup \{z\}) m ∥ k) \to (k \in ℤ \land \underline{lcm} (y) \in ℤ \land z \in ℤ)$
34		ssun1	$⊢ y \subseteq y \cup \{z\}$
35		ssralv	$⊢ y \subseteq y \cup \{z\} \to (\forall m \in (y \cup \{z\}) m ∥ k \to \forall m \in y m ∥ k)$
36	34 35	mp1i	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \to (\forall m \in (y \cup \{z\}) m ∥ k \to \forall m \in y m ∥ k)$
37	36	imim1d	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \to ((\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \to (\forall m \in (y \cup \{z\}) m ∥ k \to \underline{lcm} (y) ∥ k))$
38	37	imp31	$⊢ ((((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \land (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)) \land \forall m \in (y \cup \{z\}) m ∥ k) \to \underline{lcm} (y) ∥ k$
39		snidg	$⊢ z \in ℤ \to z \in \{z\}$
40	39	olcd	$⊢ z \in ℤ \to (z \in y \lor z \in \{z\})$
41		elun	$⊢ z \in (y \cup \{z\}) \leftrightarrow (z \in y \lor z \in \{z\})$
42	40 41	sylibr	$⊢ z \in ℤ \to z \in (y \cup \{z\})$
43		breq1	$⊢ m = z \to (m ∥ k \leftrightarrow z ∥ k)$
44	43	rspcv	$⊢ z \in (y \cup \{z\}) \to (\forall m \in (y \cup \{z\}) m ∥ k \to z ∥ k)$
45	42 44	syl	$⊢ z \in ℤ \to (\forall m \in (y \cup \{z\}) m ∥ k \to z ∥ k)$
46	45	3ad2ant1	$⊢ (z \in ℤ \land y \subseteq ℤ \land y \in Fin) \to (\forall m \in (y \cup \{z\}) m ∥ k \to z ∥ k)$
47	46	adantr	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \to (\forall m \in (y \cup \{z\}) m ∥ k \to z ∥ k)$
48	47	adantr	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \land (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)) \to (\forall m \in (y \cup \{z\}) m ∥ k \to z ∥ k)$
49	48	imp	$⊢ ((((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \land (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)) \land \forall m \in (y \cup \{z\}) m ∥ k) \to z ∥ k$
50	38 49	jca	$⊢ ((((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \land (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)) \land \forall m \in (y \cup \{z\}) m ∥ k) \to (\underline{lcm} (y) ∥ k \land z ∥ k)$
51		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)$
52	33 50 51	sylc	$⊢ ((((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \land (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)) \land \forall m \in (y \cup \{z\}) m ∥ k) \to (\underline{lcm} (y) lcm z) ∥ k$
53		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)$
54	52 53	syl5ibrcom	$⊢ ((((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \land (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)) \land \forall m \in (y \cup \{z\}) m ∥ k) \to (\underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \to \underline{lcm} (y \cup \{z\}) ∥ k)$
55	54	ex	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \land (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)) \to (\forall m \in (y \cup \{z\}) m ∥ k \to (\underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \to \underline{lcm} (y \cup \{z\}) ∥ k))$
56	55	com23	$⊢ (((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \land (\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k)) \to (\underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \to (\forall m \in (y \cup \{z\}) m ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k))$
57	56	ex	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \to ((\forall m \in y m ∥ k \to \underline{lcm} (y) ∥ k) \to (\underline{lcm} (y \cup \{z\}) = \underline{lcm} (y) lcm z \to (\forall m \in (y \cup \{z\}) m ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)))$
58	24 57	syl5d	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \to ((\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 (\forall m \in (y \cup \{z\}) m ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)))$
59	16 58	syld	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \to (\forall l \in ℤ (\forall m \in y m ∥ l \to \underline{lcm} (y) ∥ l) \to (\forall n \in ℤ \underline{lcm} (y \cup \{n\}) = \underline{lcm} (y) lcm n \to (\forall m \in (y \cup \{z\}) m ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)))$
60	10 59	syl5bi	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \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 (\forall m \in (y \cup \{z\}) m ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)))$
61	60	impd	$⊢ ((z \in ℤ \land y \subseteq ℤ \land y \in Fin) \land k \in ℤ) \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 (\forall m \in (y \cup \{z\}) m ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k))$
62	61	impancom	$⊢ ((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 m \in (y \cup \{z\}) m ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k))$
63	5 62	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 k \in ℤ (\forall m \in (y \cup \{z\}) m ∥ k \to \underline{lcm} (y \cup \{z\}) ∥ k)$

Metamath Proof Explorer

Theorem lcmfunsnlem1

Proof