Metamath Proof Explorer

Description: Extend lgsquad2 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Assertion lgsquad3 ${⊢}\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\to {M}{/}_{L}{N}={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\left({N}{/}_{L}{M}\right)$

Proof

Step Hyp Ref Expression
1 simplrl ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {N}\in ℕ$
2 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
3 1 2 syl ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {N}\in ℤ$
4 nnz ${⊢}{M}\in ℕ\to {M}\in ℤ$
5 4 ad3antrrr ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {M}\in ℤ$
6 lgscl ${⊢}\left({N}\in ℤ\wedge {M}\in ℤ\right)\to {N}{/}_{L}{M}\in ℤ$
7 3 5 6 syl2anc ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {N}{/}_{L}{M}\in ℤ$
8 7 zred ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {N}{/}_{L}{M}\in ℝ$
9 absresq ${⊢}{N}{/}_{L}{M}\in ℝ\to {\left|{N}{/}_{L}{M}\right|}^{2}={\left({N}{/}_{L}{M}\right)}^{2}$
10 8 9 syl ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {\left|{N}{/}_{L}{M}\right|}^{2}={\left({N}{/}_{L}{M}\right)}^{2}$
11 gcdcom ${⊢}\left({N}\in ℤ\wedge {M}\in ℤ\right)\to {N}\mathrm{gcd}{M}={M}\mathrm{gcd}{N}$
12 3 5 11 syl2anc ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {N}\mathrm{gcd}{M}={M}\mathrm{gcd}{N}$
13 simpr ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {M}\mathrm{gcd}{N}=1$
14 12 13 eqtrd ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {N}\mathrm{gcd}{M}=1$
15 lgsabs1 ${⊢}\left({N}\in ℤ\wedge {M}\in ℤ\right)\to \left(\left|{N}{/}_{L}{M}\right|=1↔{N}\mathrm{gcd}{M}=1\right)$
16 3 5 15 syl2anc ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to \left(\left|{N}{/}_{L}{M}\right|=1↔{N}\mathrm{gcd}{M}=1\right)$
17 14 16 mpbird ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to \left|{N}{/}_{L}{M}\right|=1$
18 17 oveq1d ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {\left|{N}{/}_{L}{M}\right|}^{2}={1}^{2}$
19 sq1 ${⊢}{1}^{2}=1$
20 18 19 eqtrdi ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {\left|{N}{/}_{L}{M}\right|}^{2}=1$
21 7 zcnd ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {N}{/}_{L}{M}\in ℂ$
22 21 sqvald ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {\left({N}{/}_{L}{M}\right)}^{2}=\left({N}{/}_{L}{M}\right)\left({N}{/}_{L}{M}\right)$
23 10 20 22 3eqtr3d ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to 1=\left({N}{/}_{L}{M}\right)\left({N}{/}_{L}{M}\right)$
24 23 oveq2d ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to \left({M}{/}_{L}{N}\right)\cdot 1=\left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)\left({N}{/}_{L}{M}\right)$
25 lgscl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}{/}_{L}{N}\in ℤ$
26 5 3 25 syl2anc ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {M}{/}_{L}{N}\in ℤ$
27 26 zcnd ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {M}{/}_{L}{N}\in ℂ$
28 27 21 21 mulassd ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to \left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)\left({N}{/}_{L}{M}\right)=\left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)\left({N}{/}_{L}{M}\right)$
29 24 28 eqtr4d ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to \left({M}{/}_{L}{N}\right)\cdot 1=\left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)\left({N}{/}_{L}{M}\right)$
30 27 mulid1d ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to \left({M}{/}_{L}{N}\right)\cdot 1={M}{/}_{L}{N}$
31 simplll ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {M}\in ℕ$
32 simpllr ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to ¬2\parallel {M}$
33 simplrr ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to ¬2\parallel {N}$
34 31 32 1 33 13 lgsquad2 ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to \left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
35 34 oveq1d ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to \left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)\left({N}{/}_{L}{M}\right)={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\left({N}{/}_{L}{M}\right)$
36 29 30 35 3eqtr3d ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge {M}\mathrm{gcd}{N}=1\right)\to {M}{/}_{L}{N}={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\left({N}{/}_{L}{M}\right)$
37 neg1cn ${⊢}-1\in ℂ$
38 37 a1i ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to -1\in ℂ$
39 neg1ne0 ${⊢}-1\ne 0$
40 39 a1i ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to -1\ne 0$
41 4 ad3antrrr ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to {M}\in ℤ$
42 simpllr ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to ¬2\parallel {M}$
43 1zzd ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to 1\in ℤ$
44 2prm ${⊢}2\in ℙ$
45 nprmdvds1 ${⊢}2\in ℙ\to ¬2\parallel 1$
46 44 45 mp1i ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to ¬2\parallel 1$
47 omoe ${⊢}\left(\left({M}\in ℤ\wedge ¬2\parallel {M}\right)\wedge \left(1\in ℤ\wedge ¬2\parallel 1\right)\right)\to 2\parallel \left({M}-1\right)$
48 41 42 43 46 47 syl22anc ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to 2\parallel \left({M}-1\right)$
49 2z ${⊢}2\in ℤ$
50 2ne0 ${⊢}2\ne 0$
51 peano2zm ${⊢}{M}\in ℤ\to {M}-1\in ℤ$
52 41 51 syl ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to {M}-1\in ℤ$
53 dvdsval2 ${⊢}\left(2\in ℤ\wedge 2\ne 0\wedge {M}-1\in ℤ\right)\to \left(2\parallel \left({M}-1\right)↔\frac{{M}-1}{2}\in ℤ\right)$
54 49 50 52 53 mp3an12i ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to \left(2\parallel \left({M}-1\right)↔\frac{{M}-1}{2}\in ℤ\right)$
55 48 54 mpbid ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to \frac{{M}-1}{2}\in ℤ$
56 2 adantr ${⊢}\left({N}\in ℕ\wedge ¬2\parallel {N}\right)\to {N}\in ℤ$
57 56 ad2antlr ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to {N}\in ℤ$
58 simplrr ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to ¬2\parallel {N}$
59 omoe ${⊢}\left(\left({N}\in ℤ\wedge ¬2\parallel {N}\right)\wedge \left(1\in ℤ\wedge ¬2\parallel 1\right)\right)\to 2\parallel \left({N}-1\right)$
60 57 58 43 46 59 syl22anc ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to 2\parallel \left({N}-1\right)$
61 peano2zm ${⊢}{N}\in ℤ\to {N}-1\in ℤ$
62 57 61 syl ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to {N}-1\in ℤ$
63 dvdsval2 ${⊢}\left(2\in ℤ\wedge 2\ne 0\wedge {N}-1\in ℤ\right)\to \left(2\parallel \left({N}-1\right)↔\frac{{N}-1}{2}\in ℤ\right)$
64 49 50 62 63 mp3an12i ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to \left(2\parallel \left({N}-1\right)↔\frac{{N}-1}{2}\in ℤ\right)$
65 60 64 mpbid ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to \frac{{N}-1}{2}\in ℤ$
66 55 65 zmulcld ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to \left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)\in ℤ$
67 38 40 66 expclzd ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to {\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\in ℂ$
68 67 mul01d ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to {\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\cdot 0=0$
69 lgsne0 ${⊢}\left({N}\in ℤ\wedge {M}\in ℤ\right)\to \left({N}{/}_{L}{M}\ne 0↔{N}\mathrm{gcd}{M}=1\right)$
70 11 eqeq1d ${⊢}\left({N}\in ℤ\wedge {M}\in ℤ\right)\to \left({N}\mathrm{gcd}{M}=1↔{M}\mathrm{gcd}{N}=1\right)$
71 69 70 bitrd ${⊢}\left({N}\in ℤ\wedge {M}\in ℤ\right)\to \left({N}{/}_{L}{M}\ne 0↔{M}\mathrm{gcd}{N}=1\right)$
72 2 4 71 syl2anr ${⊢}\left({M}\in ℕ\wedge {N}\in ℕ\right)\to \left({N}{/}_{L}{M}\ne 0↔{M}\mathrm{gcd}{N}=1\right)$
73 72 necon1bbid ${⊢}\left({M}\in ℕ\wedge {N}\in ℕ\right)\to \left(¬{M}\mathrm{gcd}{N}=1↔{N}{/}_{L}{M}=0\right)$
74 73 ad2ant2r ${⊢}\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\to \left(¬{M}\mathrm{gcd}{N}=1↔{N}{/}_{L}{M}=0\right)$
75 74 biimpa ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to {N}{/}_{L}{M}=0$
76 75 oveq2d ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to {\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\left({N}{/}_{L}{M}\right)={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\cdot 0$
77 lgsne0 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}{/}_{L}{N}\ne 0↔{M}\mathrm{gcd}{N}=1\right)$
78 77 necon1bbid ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left(¬{M}\mathrm{gcd}{N}=1↔{M}{/}_{L}{N}=0\right)$
79 4 2 78 syl2an ${⊢}\left({M}\in ℕ\wedge {N}\in ℕ\right)\to \left(¬{M}\mathrm{gcd}{N}=1↔{M}{/}_{L}{N}=0\right)$
80 79 ad2ant2r ${⊢}\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\to \left(¬{M}\mathrm{gcd}{N}=1↔{M}{/}_{L}{N}=0\right)$
81 80 biimpa ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to {M}{/}_{L}{N}=0$
82 68 76 81 3eqtr4rd ${⊢}\left(\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\wedge ¬{M}\mathrm{gcd}{N}=1\right)\to {M}{/}_{L}{N}={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\left({N}{/}_{L}{M}\right)$
83 36 82 pm2.61dan ${⊢}\left(\left({M}\in ℕ\wedge ¬2\parallel {M}\right)\wedge \left({N}\in ℕ\wedge ¬2\parallel {N}\right)\right)\to {M}{/}_{L}{N}={\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}\left({N}{/}_{L}{M}\right)$