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 e. ZZ /\ N e. ZZ ) -> ( M lcm -u N ) = ( M lcm N ) )

Proof

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