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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm - 𝑁 ) = ( 𝑀 lcm 𝑁 ) )

Proof

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