lcmneg - Metamath Proof Explorer

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

Theorem lcmneg 16640

Description: Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.)

**Assertion**
Ref	Expression
lcmneg	⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) = (𝑀 lcm 𝑁))

**Proof of Theorem lcmneg**
Step	Hyp	Ref	Expression
1		lcm0val 16631	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (𝑁 lcm 0) = 0)
2		znegcl 12652	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
3		lcm0val 16631	. . . . . . . . 9 ⊢ (-𝑁 ∈ ℤ → (-𝑁 lcm 0) = 0)
4	2, 3	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (-𝑁 lcm 0) = 0)
5	1, 4	eqtr4d 2780	. . . . . . 7 ⊢ (𝑁 ∈ ℤ → (𝑁 lcm 0) = (-𝑁 lcm 0))
6	5	ad2antlr 727	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑁 lcm 0) = (-𝑁 lcm 0))
7		oveq2 7439	. . . . . . . 8 ⊢ (𝑀 = 0 → (𝑁 lcm 𝑀) = (𝑁 lcm 0))
8		oveq2 7439	. . . . . . . 8 ⊢ (𝑀 = 0 → (-𝑁 lcm 𝑀) = (-𝑁 lcm 0))
9	7, 8	eqeq12d 2753	. . . . . . 7 ⊢ (𝑀 = 0 → ((𝑁 lcm 𝑀) = (-𝑁 lcm 𝑀) ↔ (𝑁 lcm 0) = (-𝑁 lcm 0)))
10	9	adantl 481	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → ((𝑁 lcm 𝑀) = (-𝑁 lcm 𝑀) ↔ (𝑁 lcm 0) = (-𝑁 lcm 0)))
11	6, 10	mpbird 257	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑁 lcm 𝑀) = (-𝑁 lcm 𝑀))
12		lcmcom 16630	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) = (𝑁 lcm 𝑀))
13		lcmcom 16630	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) = (-𝑁 lcm 𝑀))
14	2, 13	sylan2 593	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) = (-𝑁 lcm 𝑀))
15	12, 14	eqeq12d 2753	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 lcm 𝑁) = (𝑀 lcm -𝑁) ↔ (𝑁 lcm 𝑀) = (-𝑁 lcm 𝑀)))
16	15	adantr 480	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → ((𝑀 lcm 𝑁) = (𝑀 lcm -𝑁) ↔ (𝑁 lcm 𝑀) = (-𝑁 lcm 𝑀)))
17	11, 16	mpbird 257	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁))
18		neg0 11555	. . . . . . . 8 ⊢ -0 = 0
19	18	oveq2i 7442	. . . . . . 7 ⊢ (𝑀 lcm -0) = (𝑀 lcm 0)
20	19	eqcomi 2746	. . . . . 6 ⊢ (𝑀 lcm 0) = (𝑀 lcm -0)
21		oveq2 7439	. . . . . 6 ⊢ (𝑁 = 0 → (𝑀 lcm 𝑁) = (𝑀 lcm 0))
22		negeq 11500	. . . . . . 7 ⊢ (𝑁 = 0 → -𝑁 = -0)
23	22	oveq2d 7447	. . . . . 6 ⊢ (𝑁 = 0 → (𝑀 lcm -𝑁) = (𝑀 lcm -0))
24	20, 21, 23	3eqtr4a 2803	. . . . 5 ⊢ (𝑁 = 0 → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁))
25	24	adantl 481	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁))
26	17, 25	jaodan 960	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁))
27		dvdslcm 16635	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ -𝑁 ∥ (𝑀 lcm -𝑁)))
28	2, 27	sylan2 593	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ -𝑁 ∥ (𝑀 lcm -𝑁)))
29		simpr 484	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
30		lcmcl 16638	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℕ₀)
31	2, 30	sylan2 593	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℕ₀)
32	31	nn0zd 12639	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℤ)
33		negdvdsb 16310	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 lcm -𝑁) ∈ ℤ) → (𝑁 ∥ (𝑀 lcm -𝑁) ↔ -𝑁 ∥ (𝑀 lcm -𝑁)))
34	29, 32, 33	syl2anc 584	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∥ (𝑀 lcm -𝑁) ↔ -𝑁 ∥ (𝑀 lcm -𝑁)))
35	34	anbi2d 630	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)) ↔ (𝑀 ∥ (𝑀 lcm -𝑁) ∧ -𝑁 ∥ (𝑀 lcm -𝑁))))
36	28, 35	mpbird 257	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)))
37	36	adantr 480	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)))
38		zcn 12618	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
39	38	negeq0d 11612	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → (𝑁 = 0 ↔ -𝑁 = 0))
40	39	orbi2d 916	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → ((𝑀 = 0 ∨ 𝑁 = 0) ↔ (𝑀 = 0 ∨ -𝑁 = 0)))
41	40	notbid 318	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℤ → (¬ (𝑀 = 0 ∨ 𝑁 = 0) ↔ ¬ (𝑀 = 0 ∨ -𝑁 = 0)))
42	41	biimpa 476	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ¬ (𝑀 = 0 ∨ -𝑁 = 0))
43	42	adantll 714	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ¬ (𝑀 = 0 ∨ -𝑁 = 0))
44		lcmn0cl 16634	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ -𝑁 = 0)) → (𝑀 lcm -𝑁) ∈ ℕ)
45	2, 44	sylanl2 681	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ -𝑁 = 0)) → (𝑀 lcm -𝑁) ∈ ℕ)
46	43, 45	syldan 591	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm -𝑁) ∈ ℕ)
47		simpl 482	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
48		3anass 1095	. . . . . . 7 ⊢ (((𝑀 lcm -𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑀 lcm -𝑁) ∈ ℕ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
49	46, 47, 48	sylanbrc 583	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 lcm -𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
50		simpr 484	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ¬ (𝑀 = 0 ∨ 𝑁 = 0))
51		lcmledvds 16636	. . . . . 6 ⊢ ((((𝑀 lcm -𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)) → (𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁)))
52	49, 50, 51	syl2anc 584	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)) → (𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁)))
53	37, 52	mpd 15	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁))
54		dvdslcm 16635	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁)))
55	54	adantr 480	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁)))
56		simplr 769	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → 𝑁 ∈ ℤ)
57		lcmn0cl 16634	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) ∈ ℕ)
58	57	nnzd 12640	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) ∈ ℤ)
59		negdvdsb 16310	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 lcm 𝑁) ∈ ℤ) → (𝑁 ∥ (𝑀 lcm 𝑁) ↔ -𝑁 ∥ (𝑀 lcm 𝑁)))
60	56, 58, 59	syl2anc 584	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑁 ∥ (𝑀 lcm 𝑁) ↔ -𝑁 ∥ (𝑀 lcm 𝑁)))
61	60	anbi2d 630	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁)) ↔ (𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁))))
62		lcmledvds 16636	. . . . . . . . . 10 ⊢ ((((𝑀 lcm 𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ -𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁)))
63	62	ex 412	. . . . . . . . 9 ⊢ (((𝑀 lcm 𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∨ -𝑁 = 0) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))))
64	2, 63	syl3an3 1166	. . . . . . . 8 ⊢ (((𝑀 lcm 𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∨ -𝑁 = 0) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))))
65	64	3expib 1123	. . . . . . 7 ⊢ ((𝑀 lcm 𝑁) ∈ ℕ → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∨ -𝑁 = 0) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁)))))
66	57, 47, 43, 65	syl3c 66	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁)))
67	61, 66	sylbid 240	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁)))
68	55, 67	mpd 15	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))
69		lcmcl 16638	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈ ℕ₀)
70	69	nn0red 12588	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈ ℝ)
71	30	nn0red 12588	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℝ)
72	2, 71	sylan2 593	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℝ)
73	70, 72	letri3d 11403	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 lcm 𝑁) = (𝑀 lcm -𝑁) ↔ ((𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁) ∧ (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))))
74	73	adantr 480	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 lcm 𝑁) = (𝑀 lcm -𝑁) ↔ ((𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁) ∧ (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))))
75	53, 68, 74	mpbir2and 713	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁))
76	26, 75	pm2.61dan 813	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁))
77	76	eqcomd 2743	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) = (𝑀 lcm 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 class class class wbr 5143 (class class class)co 7431 ℝcr 11154 0cc0 11155 ≤ cle 11296 -cneg 11493 ℕcn 12266 ℕ₀cn0 12526 ℤcz 12613 ∥ cdvds 16290 lcm clcm 16625

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-sup 9482 df-inf 9483 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-n0 12527 df-z 12614 df-uz 12879 df-rp 13035 df-seq 14043 df-exp 14103 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-dvds 16291 df-lcm 16627

This theorem is referenced by: neglcm 16641 lcmabs 16642

W3C validator