Metamath Proof Explorer

Theorem lcmneg

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

Ref Expression
Assertion lcmneg ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm -N = M lcm N

Proof

Step Hyp Ref Expression
1 lcm0val ⊢ N ∈ ℤ → N lcm 0 = 0
2 znegcl ⊢ N ∈ ℤ → − N ∈ ℤ
3 lcm0val ⊢ − N ∈ ℤ → -N lcm 0 = 0
4 2 3 syl ⊢ N ∈ ℤ → -N lcm 0 = 0
5 1 4 eqtr4d ⊢ N ∈ ℤ → N lcm 0 = -N lcm 0
6 5 ad2antlr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 → N lcm 0 = -N lcm 0
7 oveq2 ⊢ M = 0 → N lcm M = N lcm 0
8 oveq2 ⊢ M = 0 → -N lcm M = -N lcm 0
9 7 8 eqeq12d ⊢ M = 0 → N lcm M = -N lcm M ↔ N lcm 0 = -N lcm 0
10 9 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 → N lcm M = -N lcm M ↔ N lcm 0 = -N lcm 0
11 6 10 mpbird ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 → N lcm M = -N lcm M
12 lcmcom ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = N lcm M
13 lcmcom ⊢ M ∈ ℤ ∧ − N ∈ ℤ → M lcm -N = -N lcm M
14 2 13 sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm -N = -N lcm M
15 12 14 eqeq12d ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = M lcm -N ↔ N lcm M = -N lcm M
16 15 adantr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 → M lcm N = M lcm -N ↔ N lcm M = -N lcm M
17 11 16 mpbird ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 → M lcm N = M lcm -N
18 neg0 ⊢ − 0 = 0
19 18 oveq2i ⊢ M lcm -0 = M lcm 0
20 19 eqcomi ⊢ M lcm 0 = M lcm -0
21 oveq2 ⊢ N = 0 → M lcm N = M lcm 0
22 negeq ⊢ N = 0 → − N = − 0
23 22 oveq2d ⊢ N = 0 → M lcm -N = M lcm -0
24 20 21 23 3eqtr4a ⊢ N = 0 → M lcm N = M lcm -N
25 24 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N = 0 → M lcm N = M lcm -N
26 17 25 jaodan ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 ∨ N = 0 → M lcm N = M lcm -N
27 dvdslcm ⊢ M ∈ ℤ ∧ − N ∈ ℤ → M ∥ M lcm -N ∧ -N ∥ M lcm -N
28 2 27 sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ M lcm -N ∧ -N ∥ M lcm -N
29 simpr ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ
30 lcmcl ⊢ M ∈ ℤ ∧ − N ∈ ℤ → M lcm -N ∈ ℕ 0
31 2 30 sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm -N ∈ ℕ 0
32 31 nn0zd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm -N ∈ ℤ
33 negdvdsb ⊢ N ∈ ℤ ∧ M lcm -N ∈ ℤ → N ∥ M lcm -N ↔ -N ∥ M lcm -N
34 29 32 33 syl2anc ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∥ M lcm -N ↔ -N ∥ M lcm -N
35 34 anbi2d ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ M lcm -N ∧ N ∥ M lcm -N ↔ M ∥ M lcm -N ∧ -N ∥ M lcm -N
36 28 35 mpbird ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ M lcm -N ∧ N ∥ M lcm -N
37 36 adantr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∥ M lcm -N ∧ N ∥ M lcm -N
38 zcn ⊢ N ∈ ℤ → N ∈ ℂ
39 38 negeq0d ⊢ N ∈ ℤ → N = 0 ↔ − N = 0
40 39 orbi2d ⊢ N ∈ ℤ → M = 0 ∨ N = 0 ↔ M = 0 ∨ − N = 0
41 40 notbid ⊢ N ∈ ℤ → ¬ M = 0 ∨ N = 0 ↔ ¬ M = 0 ∨ − N = 0
42 41 biimpa ⊢ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → ¬ M = 0 ∨ − N = 0
43 42 adantll ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → ¬ M = 0 ∨ − N = 0
44 lcmn0cl ⊢ M ∈ ℤ ∧ − N ∈ ℤ ∧ ¬ M = 0 ∨ − N = 0 → M lcm -N ∈ ℕ
45 2 44 sylanl2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ − N = 0 → M lcm -N ∈ ℕ
46 43 45 syldan ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm -N ∈ ℕ
47 simpl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∈ ℤ ∧ N ∈ ℤ
48 3anass ⊢ M lcm -N ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ ↔ M lcm -N ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ
49 46 47 48 sylanbrc ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm -N ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ
50 simpr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → ¬ M = 0 ∨ N = 0
51 lcmledvds ⊢ M lcm -N ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∥ M lcm -N ∧ N ∥ M lcm -N → M lcm N ≤ M lcm -N
52 49 50 51 syl2anc ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∥ M lcm -N ∧ N ∥ M lcm -N → M lcm N ≤ M lcm -N
53 37 52 mpd ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N ≤ M lcm -N
54 dvdslcm ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ M lcm N ∧ N ∥ M lcm N
55 54 adantr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∥ M lcm N ∧ N ∥ M lcm N
56 simplr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → N ∈ ℤ
57 lcmn0cl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N ∈ ℕ
58 57 nnzd ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N ∈ ℤ
59 negdvdsb ⊢ N ∈ ℤ ∧ M lcm N ∈ ℤ → N ∥ M lcm N ↔ -N ∥ M lcm N
60 56 58 59 syl2anc ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → N ∥ M lcm N ↔ -N ∥ M lcm N
61 60 anbi2d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∥ M lcm N ∧ N ∥ M lcm N ↔ M ∥ M lcm N ∧ -N ∥ M lcm N
62 lcmledvds ⊢ M lcm N ∈ ℕ ∧ M ∈ ℤ ∧ − N ∈ ℤ ∧ ¬ M = 0 ∨ − N = 0 → M ∥ M lcm N ∧ -N ∥ M lcm N → M lcm -N ≤ M lcm N
63 62 ex ⊢ M lcm N ∈ ℕ ∧ M ∈ ℤ ∧ − N ∈ ℤ → ¬ M = 0 ∨ − N = 0 → M ∥ M lcm N ∧ -N ∥ M lcm N → M lcm -N ≤ M lcm N
64 2 63 syl3an3 ⊢ M lcm N ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ → ¬ M = 0 ∨ − N = 0 → M ∥ M lcm N ∧ -N ∥ M lcm N → M lcm -N ≤ M lcm N
65 64 3expib ⊢ M lcm N ∈ ℕ → M ∈ ℤ ∧ N ∈ ℤ → ¬ M = 0 ∨ − N = 0 → M ∥ M lcm N ∧ -N ∥ M lcm N → M lcm -N ≤ M lcm N
66 57 47 43 65 syl3c ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∥ M lcm N ∧ -N ∥ M lcm N → M lcm -N ≤ M lcm N
67 61 66 sylbid ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∥ M lcm N ∧ N ∥ M lcm N → M lcm -N ≤ M lcm N
68 55 67 mpd ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm -N ≤ M lcm N
69 lcmcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N ∈ ℕ 0
70 69 nn0red ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N ∈ ℝ
71 30 nn0red ⊢ M ∈ ℤ ∧ − N ∈ ℤ → M lcm -N ∈ ℝ
72 2 71 sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm -N ∈ ℝ
73 70 72 letri3d ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = M lcm -N ↔ M lcm N ≤ M lcm -N ∧ M lcm -N ≤ M lcm N
74 73 adantr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N = M lcm -N ↔ M lcm N ≤ M lcm -N ∧ M lcm -N ≤ M lcm N
75 53 68 74 mpbir2and ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N = M lcm -N
76 26 75 pm2.61dan ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = M lcm -N
77 76 eqcomd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm -N = M lcm N