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 16573

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 16564	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (𝑁 lcm 0) = 0)
2		znegcl 12627	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
3		lcm0val 16564	. . . . . . . . 9 ⊢ (-𝑁 ∈ ℤ → (-𝑁 lcm 0) = 0)
4	2, 3	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (-𝑁 lcm 0) = 0)
5	1, 4	eqtr4d 2771	. . . . . . 7 ⊢ (𝑁 ∈ ℤ → (𝑁 lcm 0) = (-𝑁 lcm 0))
6	5	ad2antlr 726	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑁 lcm 0) = (-𝑁 lcm 0))
7		oveq2 7428	. . . . . . . 8 ⊢ (𝑀 = 0 → (𝑁 lcm 𝑀) = (𝑁 lcm 0))
8		oveq2 7428	. . . . . . . 8 ⊢ (𝑀 = 0 → (-𝑁 lcm 𝑀) = (-𝑁 lcm 0))
9	7, 8	eqeq12d 2744	. . . . . . 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 16563	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) = (𝑁 lcm 𝑀))
13		lcmcom 16563	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) = (-𝑁 lcm 𝑀))
14	2, 13	sylan2 592	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) = (-𝑁 lcm 𝑀))
15	12, 14	eqeq12d 2744	. . . . . 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 11536	. . . . . . . 8 ⊢ -0 = 0
19	18	oveq2i 7431	. . . . . . 7 ⊢ (𝑀 lcm -0) = (𝑀 lcm 0)
20	19	eqcomi 2737	. . . . . 6 ⊢ (𝑀 lcm 0) = (𝑀 lcm -0)
21		oveq2 7428	. . . . . 6 ⊢ (𝑁 = 0 → (𝑀 lcm 𝑁) = (𝑀 lcm 0))
22		negeq 11482	. . . . . . 7 ⊢ (𝑁 = 0 → -𝑁 = -0)
23	22	oveq2d 7436	. . . . . 6 ⊢ (𝑁 = 0 → (𝑀 lcm -𝑁) = (𝑀 lcm -0))
24	20, 21, 23	3eqtr4a 2794	. . . . 5 ⊢ (𝑁 = 0 → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁))
25	24	adantl 481	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁))
26	17, 25	jaodan 956	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁))
27		dvdslcm 16568	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ -𝑁 ∥ (𝑀 lcm -𝑁)))
28	2, 27	sylan2 592	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ -𝑁 ∥ (𝑀 lcm -𝑁)))
29		simpr 484	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
30		lcmcl 16571	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℕ₀)
31	2, 30	sylan2 592	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℕ₀)
32	31	nn0zd 12614	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℤ)
33		negdvdsb 16249	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 lcm -𝑁) ∈ ℤ) → (𝑁 ∥ (𝑀 lcm -𝑁) ↔ -𝑁 ∥ (𝑀 lcm -𝑁)))
34	29, 32, 33	syl2anc 583	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∥ (𝑀 lcm -𝑁) ↔ -𝑁 ∥ (𝑀 lcm -𝑁)))
35	34	anbi2d 629	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)) ↔ (𝑀 ∥ (𝑀 lcm -𝑁) ∧ -𝑁 ∥ (𝑀 lcm -𝑁))))
36	28, 35	mpbird 257	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)))
37	36	adantr 480	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)))
38		zcn 12593	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
39	38	negeq0d 11593	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → (𝑁 = 0 ↔ -𝑁 = 0))
40	39	orbi2d 914	. . . . . . . . . . 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 713	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ¬ (𝑀 = 0 ∨ -𝑁 = 0))
44		lcmn0cl 16567	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ -𝑁 = 0)) → (𝑀 lcm -𝑁) ∈ ℕ)
45	2, 44	sylanl2 680	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ -𝑁 = 0)) → (𝑀 lcm -𝑁) ∈ ℕ)
46	43, 45	syldan 590	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm -𝑁) ∈ ℕ)
47		simpl 482	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
48		3anass 1093	. . . . . . 7 ⊢ (((𝑀 lcm -𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑀 lcm -𝑁) ∈ ℕ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
49	46, 47, 48	sylanbrc 582	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 lcm -𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
50		simpr 484	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ¬ (𝑀 = 0 ∨ 𝑁 = 0))
51		lcmledvds 16569	. . . . . 6 ⊢ ((((𝑀 lcm -𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)) → (𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁)))
52	49, 50, 51	syl2anc 583	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm -𝑁) ∧ 𝑁 ∥ (𝑀 lcm -𝑁)) → (𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁)))
53	37, 52	mpd 15	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) ≤ (𝑀 lcm -𝑁))
54		dvdslcm 16568	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁)))
55	54	adantr 480	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁)))
56		simplr 768	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → 𝑁 ∈ ℤ)
57		lcmn0cl 16567	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) ∈ ℕ)
58	57	nnzd 12615	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) ∈ ℤ)
59		negdvdsb 16249	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 lcm 𝑁) ∈ ℤ) → (𝑁 ∥ (𝑀 lcm 𝑁) ↔ -𝑁 ∥ (𝑀 lcm 𝑁)))
60	56, 58, 59	syl2anc 583	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑁 ∥ (𝑀 lcm 𝑁) ↔ -𝑁 ∥ (𝑀 lcm 𝑁)))
61	60	anbi2d 629	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁)) ↔ (𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁))))
62		lcmledvds 16569	. . . . . . . . . 10 ⊢ ((((𝑀 lcm 𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ -𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁)))
63	62	ex 412	. . . . . . . . 9 ⊢ (((𝑀 lcm 𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∨ -𝑁 = 0) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))))
64	2, 63	syl3an3 1163	. . . . . . . 8 ⊢ (((𝑀 lcm 𝑁) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∨ -𝑁 = 0) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ -𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))))
65	64	3expib 1120	. . . . . . 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 239	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁)))
68	55, 67	mpd 15	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm -𝑁) ≤ (𝑀 lcm 𝑁))
69		lcmcl 16571	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈ ℕ₀)
70	69	nn0red 12563	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈ ℝ)
71	30	nn0red 12563	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℝ)
72	2, 71	sylan2 592	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) ∈ ℝ)
73	70, 72	letri3d 11386	. . . . 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 712	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁))
76	26, 75	pm2.61dan 812	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) = (𝑀 lcm -𝑁))
77	76	eqcomd 2734	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm -𝑁) = (𝑀 lcm 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 846 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 class class class wbr 5148 (class class class)co 7420 ℝcr 11137 0cc0 11138 ≤ cle 11279 -cneg 11475 ℕcn 12242 ℕ₀cn0 12502 ℤcz 12588 ∥ cdvds 16230 lcm clcm 16558

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-sep 5299 ax-nul 5306 ax-pow 5365 ax-pr 5429 ax-un 7740 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-pre-sup 11216

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3373 df-reu 3374 df-rab 3430 df-v 3473 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6500 df-fun 6550 df-fn 6551 df-f 6552 df-f1 6553 df-fo 6554 df-f1o 6555 df-fv 6556 df-riota 7376 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7871 df-2nd 7994 df-frecs 8286 df-wrecs 8317 df-recs 8391 df-rdg 8430 df-er 8724 df-en 8964 df-dom 8965 df-sdom 8966 df-sup 9465 df-inf 9466 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11476 df-neg 11477 df-div 11902 df-nn 12243 df-2 12305 df-3 12306 df-n0 12503 df-z 12589 df-uz 12853 df-rp 13007 df-seq 13999 df-exp 14059 df-cj 15078 df-re 15079 df-im 15080 df-sqrt 15214 df-abs 15215 df-dvds 16231 df-lcm 16560

This theorem is referenced by: neglcm 16574 lcmabs 16575

W3C validator

	
		OSZAR »