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∈ℤ→Mlcm- N=MlcmN

Proof

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