lcmfunsnlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lcmfunsnlem2		Structured version Visualization version GIF version

Theorem lcmfunsnlem2 16334

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

**Assertion**
Ref	Expression
lcmfunsnlem2	⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → ∀𝑛 ∈ ℤ (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))

Distinct variable groups: 𝑦,𝑚,𝑧 𝑘,𝑛,𝑦,𝑧,𝑚

**Proof of Theorem lcmfunsnlem2**
Step	Hyp	Ref	Expression
1		nfv 1917	. . 3 ⊢ Ⅎ𝑛(𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)
2		nfv 1917	. . . 4 ⊢ Ⅎ𝑛∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)
3		nfra1 3144	. . . 4 ⊢ Ⅎ𝑛∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)
4	2, 3	nfan 1902	. . 3 ⊢ Ⅎ𝑛(∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))
5	1, 4	nfan 1902	. 2 ⊢ Ⅎ𝑛((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)))
6		0z 12319	. . . . 5 ⊢ 0 ∈ ℤ
7		eqoreldif 4622	. . . . 5 ⊢ (0 ∈ ℤ → (𝑛 ∈ ℤ ↔ (𝑛 = 0 ∨ 𝑛 ∈ (ℤ ∖ {0}))))
8	6, 7	ax-mp 5	. . . 4 ⊢ (𝑛 ∈ ℤ ↔ (𝑛 = 0 ∨ 𝑛 ∈ (ℤ ∖ {0})))
9		simp2 1136	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑦 ⊆ ℤ)
10		snssi 4743	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℤ → {𝑧} ⊆ ℤ)
11	10	3ad2ant1 1132	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → {𝑧} ⊆ ℤ)
12	9, 11	unssd 4121	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑦 ∪ {𝑧}) ⊆ ℤ)
13		snssi 4743	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℤ → {0} ⊆ ℤ)
14	6, 13	mp1i 13	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → {0} ⊆ ℤ)
15	12, 14	unssd 4121	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → ((𝑦 ∪ {𝑧}) ∪ {0}) ⊆ ℤ)
16		c0ex 10958	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
17	16	snid 4599	. . . . . . . . . . . . 13 ⊢ 0 ∈ {0}
18	17	olci 863	. . . . . . . . . . . 12 ⊢ (0 ∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {0})
19		elun 4084	. . . . . . . . . . . 12 ⊢ (0 ∈ ((𝑦 ∪ {𝑧}) ∪ {0}) ↔ (0 ∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {0}))
20	18, 19	mpbir 230	. . . . . . . . . . 11 ⊢ 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {0})
21		lcmf0val 16316	. . . . . . . . . . 11 ⊢ ((((𝑦 ∪ {𝑧}) ∪ {0}) ⊆ ℤ ∧ 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {0})) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {0})) = 0)
22	15, 20, 21	sylancl 586	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {0})) = 0)
23	22	adantr 481	. . . . . . . . 9 ⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 = 0) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {0})) = 0)
24		sneq 4573	. . . . . . . . . . . 12 ⊢ (𝑛 = 0 → {𝑛} = {0})
25	24	adantl 482	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 = 0) → {𝑛} = {0})
26	25	uneq2d 4098	. . . . . . . . . 10 ⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 = 0) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) = ((𝑦 ∪ {𝑧}) ∪ {0}))
27	26	fveq2d 6772	. . . . . . . . 9 ⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 = 0) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {0})))
28		oveq2 7277	. . . . . . . . . 10 ⊢ (𝑛 = 0 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 0))
29		snfi 8823	. . . . . . . . . . . . . . 15 ⊢ {𝑧} ∈ Fin
30		unfi 8944	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
31	29, 30	mpan2 688	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ Fin → (𝑦 ∪ {𝑧}) ∈ Fin)
32	31	3ad2ant3 1134	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
33		lcmfcl 16322	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑦 ∪ {𝑧}) ∈ Fin) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ₀)
34	12, 32, 33	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ₀)
35	34	nn0zd 12413	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ)
36		lcm0val 16288	. . . . . . . . . . 11 ⊢ ((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ → ((lcm‘(𝑦 ∪ {𝑧})) lcm 0) = 0)
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 0) = 0)
38	28, 37	sylan9eqr 2800	. . . . . . . . 9 ⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 = 0) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = 0)
39	23, 27, 38	3eqtr4d 2788	. . . . . . . 8 ⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 = 0) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))
40	39	ex 413	. . . . . . 7 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 = 0 → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
41	40	adantr 481	. . . . . 6 ⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (𝑛 = 0 → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
42	41	com12 32	. . . . 5 ⊢ (𝑛 = 0 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
43	9	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → 𝑦 ⊆ ℤ)
44	11	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → {𝑧} ⊆ ℤ)
45	43, 44	unssd 4121	. . . . . . . . . . . . 13 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (𝑦 ∪ {𝑧}) ⊆ ℤ)
46		elun1 4111	. . . . . . . . . . . . . 14 ⊢ (0 ∈ 𝑦 → 0 ∈ (𝑦 ∪ {𝑧}))
47	46	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → 0 ∈ (𝑦 ∪ {𝑧}))
48		lcmf0val 16316	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ 0 ∈ (𝑦 ∪ {𝑧})) → (lcm‘(𝑦 ∪ {𝑧})) = 0)
49	45, 47, 48	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (lcm‘(𝑦 ∪ {𝑧})) = 0)
50	49	oveq2d 7285	. . . . . . . . . . 11 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (𝑛 lcm (lcm‘(𝑦 ∪ {𝑧}))) = (𝑛 lcm 0))
51		eldifi 4062	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ℤ ∖ {0}) → 𝑛 ∈ ℤ)
52		lcm0val 16288	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℤ → (𝑛 lcm 0) = 0)
53	51, 52	syl 17	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ℤ ∖ {0}) → (𝑛 lcm 0) = 0)
54	53	ad2antlr 724	. . . . . . . . . . 11 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (𝑛 lcm 0) = 0)
55	50, 54	eqtrd 2778	. . . . . . . . . 10 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (𝑛 lcm (lcm‘(𝑦 ∪ {𝑧}))) = 0)
56		simp3 1137	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑦 ∈ Fin)
57	56, 29, 30	sylancl 586	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
58	12, 57, 33	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ₀)
59	58	nn0zd 12413	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ)
60	51	adantl 482	. . . . . . . . . . 11 ⊢ ((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) → 𝑛 ∈ ℤ)
61		lcmcom 16287	. . . . . . . . . . 11 ⊢ (((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (𝑛 lcm (lcm‘(𝑦 ∪ {𝑧}))))
62	59, 60, 61	syl2anr 597	. . . . . . . . . 10 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (𝑛 lcm (lcm‘(𝑦 ∪ {𝑧}))))
63	12	adantl 482	. . . . . . . . . . . 12 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (𝑦 ∪ {𝑧}) ⊆ ℤ)
64	51	snssd 4744	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ℤ ∖ {0}) → {𝑛} ⊆ ℤ)
65	64	ad2antlr 724	. . . . . . . . . . . 12 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → {𝑛} ⊆ ℤ)
66	63, 65	unssd 4121	. . . . . . . . . . 11 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ)
67	46	orcd 870	. . . . . . . . . . . . 13 ⊢ (0 ∈ 𝑦 → (0 ∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {𝑛}))
68		elun 4084	. . . . . . . . . . . . 13 ⊢ (0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ (0 ∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {𝑛}))
69	67, 68	sylibr 233	. . . . . . . . . . . 12 ⊢ (0 ∈ 𝑦 → 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))
70	69	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))
71		lcmf0val 16316	. . . . . . . . . . 11 ⊢ ((((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = 0)
72	66, 70, 71	syl2anc 584	. . . . . . . . . 10 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = 0)
73	55, 62, 72	3eqtr4rd 2789	. . . . . . . . 9 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))
74	73	a1d 25	. . . . . . . 8 ⊢ (((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → ((∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
75	74	expimpd 454	. . . . . . 7 ⊢ ((0 ∈ 𝑦 ∧ 𝑛 ∈ (ℤ ∖ {0})) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
76	75	ex 413	. . . . . 6 ⊢ (0 ∈ 𝑦 → (𝑛 ∈ (ℤ ∖ {0}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
77		elsng 4577	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ℤ → (0 ∈ {𝑧} ↔ 0 = 𝑧))
78		eqcom 2745	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 = 𝑧 ↔ 𝑧 = 0)
79	77, 78	bitrdi 287	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ∈ ℤ → (0 ∈ {𝑧} ↔ 𝑧 = 0))
80	6, 79	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ {𝑧} ↔ 𝑧 = 0)
81	80	biimpri 227	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 0 → 0 ∈ {𝑧})
82	81	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → 0 ∈ {𝑧})
83	82	olcd 871	. . . . . . . . . . . . . 14 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (0 ∈ 𝑦 ∨ 0 ∈ {𝑧}))
84		elun 4084	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (𝑦 ∪ {𝑧}) ↔ (0 ∈ 𝑦 ∨ 0 ∈ {𝑧}))
85	83, 84	sylibr 233	. . . . . . . . . . . . 13 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → 0 ∈ (𝑦 ∪ {𝑧}))
86	12, 85, 48	syl2an2 683	. . . . . . . . . . . 12 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (lcm‘(𝑦 ∪ {𝑧})) = 0)
87	86	oveq2d 7285	. . . . . . . . . . 11 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (𝑛 lcm (lcm‘(𝑦 ∪ {𝑧}))) = (𝑛 lcm 0))
88	51	ad2antlr 724	. . . . . . . . . . . 12 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → 𝑛 ∈ ℤ)
89	88, 52	syl 17	. . . . . . . . . . 11 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (𝑛 lcm 0) = 0)
90	87, 89	eqtrd 2778	. . . . . . . . . 10 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (𝑛 lcm (lcm‘(𝑦 ∪ {𝑧}))) = 0)
91	59, 88, 61	syl2an2 683	. . . . . . . . . 10 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (𝑛 lcm (lcm‘(𝑦 ∪ {𝑧}))))
92	12	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (𝑦 ∪ {𝑧}) ⊆ ℤ)
93	64	ad2antlr 724	. . . . . . . . . . . 12 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → {𝑛} ⊆ ℤ)
94	92, 93	unssd 4121	. . . . . . . . . . 11 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ)
95		sneq 4573	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 0 → {𝑧} = {0})
96	17, 95	eleqtrrid 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 0 → 0 ∈ {𝑧})
97	96	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → 0 ∈ {𝑧})
98	97	olcd 871	. . . . . . . . . . . . . 14 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (0 ∈ 𝑦 ∨ 0 ∈ {𝑧}))
99	98, 84	sylibr 233	. . . . . . . . . . . . 13 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → 0 ∈ (𝑦 ∪ {𝑧}))
100	99	orcd 870	. . . . . . . . . . . 12 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (0 ∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {𝑛}))
101	100, 68	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))
102	94, 101, 71	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = 0)
103	90, 91, 102	3eqtr4rd 2789	. . . . . . . . 9 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))
104	103	a1d 25	. . . . . . . 8 ⊢ (((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) ∧ (𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) → ((∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
105	104	expimpd 454	. . . . . . 7 ⊢ ((𝑧 = 0 ∧ 𝑛 ∈ (ℤ ∖ {0})) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
106	105	ex 413	. . . . . 6 ⊢ (𝑧 = 0 → (𝑛 ∈ (ℤ ∖ {0}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
107		ioran 981	. . . . . . . 8 ⊢ (¬ (0 ∈ 𝑦 ∨ 𝑧 = 0) ↔ (¬ 0 ∈ 𝑦 ∧ ¬ 𝑧 = 0))
108		df-nel 3050	. . . . . . . . 9 ⊢ (0 ∉ 𝑦 ↔ ¬ 0 ∈ 𝑦)
109		df-ne 2944	. . . . . . . . 9 ⊢ (𝑧 ≠ 0 ↔ ¬ 𝑧 = 0)
110	108, 109	anbi12i 627	. . . . . . . 8 ⊢ ((0 ∉ 𝑦 ∧ 𝑧 ≠ 0) ↔ (¬ 0 ∈ 𝑦 ∧ ¬ 𝑧 = 0))
111	107, 110	bitr4i 277	. . . . . . 7 ⊢ (¬ (0 ∈ 𝑦 ∨ 𝑧 = 0) ↔ (0 ∉ 𝑦 ∧ 𝑧 ≠ 0))
112		eldif 3898	. . . . . . . 8 ⊢ (𝑛 ∈ (ℤ ∖ {0}) ↔ (𝑛 ∈ ℤ ∧ ¬ 𝑛 ∈ {0}))
113		velsn 4579	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ {0} ↔ 𝑛 = 0)
114	113	bicomi 223	. . . . . . . . . . 11 ⊢ (𝑛 = 0 ↔ 𝑛 ∈ {0})
115	114	necon3abii 2990	. . . . . . . . . 10 ⊢ (𝑛 ≠ 0 ↔ ¬ 𝑛 ∈ {0})
116		lcmfunsnlem2lem2 16333	. . . . . . . . . . . 12 ⊢ (((0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))
117	116	exp520 1356	. . . . . . . . . . 11 ⊢ (0 ∉ 𝑦 → (𝑧 ≠ 0 → (𝑛 ≠ 0 → (𝑛 ∈ ℤ → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))))
118	117	imp 407	. . . . . . . . . 10 ⊢ ((0 ∉ 𝑦 ∧ 𝑧 ≠ 0) → (𝑛 ≠ 0 → (𝑛 ∈ ℤ → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))))
119	115, 118	syl5bir 242	. . . . . . . . 9 ⊢ ((0 ∉ 𝑦 ∧ 𝑧 ≠ 0) → (¬ 𝑛 ∈ {0} → (𝑛 ∈ ℤ → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))))
120	119	impcomd 412	. . . . . . . 8 ⊢ ((0 ∉ 𝑦 ∧ 𝑧 ≠ 0) → ((𝑛 ∈ ℤ ∧ ¬ 𝑛 ∈ {0}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
121	112, 120	syl5bi 241	. . . . . . 7 ⊢ ((0 ∉ 𝑦 ∧ 𝑧 ≠ 0) → (𝑛 ∈ (ℤ ∖ {0}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
122	111, 121	sylbi 216	. . . . . 6 ⊢ (¬ (0 ∈ 𝑦 ∨ 𝑧 = 0) → (𝑛 ∈ (ℤ ∖ {0}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
123	76, 106, 122	ecase3 1029	. . . . 5 ⊢ (𝑛 ∈ (ℤ ∖ {0}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
124	42, 123	jaoi 854	. . . 4 ⊢ ((𝑛 = 0 ∨ 𝑛 ∈ (ℤ ∖ {0})) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
125	8, 124	sylbi 216	. . 3 ⊢ (𝑛 ∈ ℤ → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
126	125	com12 32	. 2 ⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (𝑛 ∈ ℤ → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
127	5, 126	ralrimi 3141	1 ⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → ∀𝑛 ∈ ℤ (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∉ wnel 3049 ∀wral 3064 ∖ cdif 3885 ∪ cun 3886 ⊆ wss 3888 {csn 4563 class class class wbr 5075 ‘cfv 6428 (class class class)co 7269 Fincfn 8722 0cc0 10860 ℕ₀cn0 12222 ℤcz 12308 ∥ cdvds 15952 lcm clcm 16282 lcmclcmf 16283

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5210 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7580 ax-inf2 9388 ax-cnex 10916 ax-resscn 10917 ax-1cn 10918 ax-icn 10919 ax-addcl 10920 ax-addrcl 10921 ax-mulcl 10922 ax-mulrcl 10923 ax-mulcom 10924 ax-addass 10925 ax-mulass 10926 ax-distr 10927 ax-i2m1 10928 ax-1ne0 10929 ax-1rid 10930 ax-rnegex 10931 ax-rrecex 10932 ax-cnre 10933 ax-pre-lttri 10934 ax-pre-lttrn 10935 ax-pre-ltadd 10936 ax-pre-mulgt0 10937 ax-pre-sup 10938

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3433 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4259 df-if 4462 df-pw 4537 df-sn 4564 df-pr 4566 df-op 4570 df-uni 4842 df-int 4882 df-iun 4928 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5486 df-eprel 5492 df-po 5500 df-so 5501 df-fr 5541 df-se 5542 df-we 5543 df-xp 5592 df-rel 5593 df-cnv 5594 df-co 5595 df-dm 5596 df-rn 5597 df-res 5598 df-ima 5599 df-pred 6197 df-ord 6264 df-on 6265 df-lim 6266 df-suc 6267 df-iota 6386 df-fun 6430 df-fn 6431 df-f 6432 df-f1 6433 df-fo 6434 df-f1o 6435 df-fv 6436 df-isom 6437 df-riota 7226 df-ov 7272 df-oprab 7273 df-mpo 7274 df-om 7705 df-1st 7822 df-2nd 7823 df-frecs 8086 df-wrecs 8117 df-recs 8191 df-rdg 8230 df-1o 8286 df-er 8487 df-en 8723 df-dom 8724 df-sdom 8725 df-fin 8726 df-sup 9190 df-inf 9191 df-oi 9258 df-card 9686 df-pnf 11000 df-mnf 11001 df-xr 11002 df-ltxr 11003 df-le 11004 df-sub 11196 df-neg 11197 df-div 11622 df-nn 11963 df-2 12025 df-3 12026 df-n0 12223 df-z 12309 df-uz 12572 df-rp 12720 df-fz 13229 df-fzo 13372 df-fl 13501 df-mod 13579 df-seq 13711 df-exp 13772 df-hash 14034 df-cj 14799 df-re 14800 df-im 14801 df-sqrt 14935 df-abs 14936 df-clim 15186 df-prod 15605 df-dvds 15953 df-gcd 16191 df-lcm 16284 df-lcmf 16285

This theorem is referenced by: lcmfunsnlem 16335

W3C validator