# Metamath Proof Explorer

Description: Lemma for lgsquad2 . (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses lgsquad2.1 ${⊢}{\phi }\to {M}\in ℕ$
lgsquad2.2 ${⊢}{\phi }\to ¬2\parallel {M}$
lgsquad2.3 ${⊢}{\phi }\to {N}\in ℕ$
lgsquad2.4 ${⊢}{\phi }\to ¬2\parallel {N}$
lgsquad2.5 ${⊢}{\phi }\to {M}\mathrm{gcd}{N}=1$
lgsquad2lem1.a ${⊢}{\phi }\to {A}\in ℕ$
lgsquad2lem1.b ${⊢}{\phi }\to {B}\in ℕ$
lgsquad2lem1.m ${⊢}{\phi }\to {A}{B}={M}$
lgsquad2lem1.1 ${⊢}{\phi }\to \left({A}{/}_{L}{N}\right)\left({N}{/}_{L}{A}\right)={\left(-1\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
lgsquad2lem1.2 ${⊢}{\phi }\to \left({B}{/}_{L}{N}\right)\left({N}{/}_{L}{B}\right)={\left(-1\right)}^{\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
Assertion lgsquad2lem1 ${⊢}{\phi }\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)}$

### Proof

Step Hyp Ref Expression
1 lgsquad2.1 ${⊢}{\phi }\to {M}\in ℕ$
2 lgsquad2.2 ${⊢}{\phi }\to ¬2\parallel {M}$
3 lgsquad2.3 ${⊢}{\phi }\to {N}\in ℕ$
4 lgsquad2.4 ${⊢}{\phi }\to ¬2\parallel {N}$
5 lgsquad2.5 ${⊢}{\phi }\to {M}\mathrm{gcd}{N}=1$
6 lgsquad2lem1.a ${⊢}{\phi }\to {A}\in ℕ$
7 lgsquad2lem1.b ${⊢}{\phi }\to {B}\in ℕ$
8 lgsquad2lem1.m ${⊢}{\phi }\to {A}{B}={M}$
9 lgsquad2lem1.1 ${⊢}{\phi }\to \left({A}{/}_{L}{N}\right)\left({N}{/}_{L}{A}\right)={\left(-1\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
10 lgsquad2lem1.2 ${⊢}{\phi }\to \left({B}{/}_{L}{N}\right)\left({N}{/}_{L}{B}\right)={\left(-1\right)}^{\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
11 6 nnzd ${⊢}{\phi }\to {A}\in ℤ$
12 11 zcnd ${⊢}{\phi }\to {A}\in ℂ$
13 ax-1cn ${⊢}1\in ℂ$
14 npcan ${⊢}\left({A}\in ℂ\wedge 1\in ℂ\right)\to {A}-1+1={A}$
15 12 13 14 sylancl ${⊢}{\phi }\to {A}-1+1={A}$
16 7 nnzd ${⊢}{\phi }\to {B}\in ℤ$
17 16 zcnd ${⊢}{\phi }\to {B}\in ℂ$
18 npcan ${⊢}\left({B}\in ℂ\wedge 1\in ℂ\right)\to {B}-1+1={B}$
19 17 13 18 sylancl ${⊢}{\phi }\to {B}-1+1={B}$
20 15 19 oveq12d ${⊢}{\phi }\to \left({A}-1+1\right)\left({B}-1+1\right)={A}{B}$
21 peano2zm ${⊢}{A}\in ℤ\to {A}-1\in ℤ$
22 11 21 syl ${⊢}{\phi }\to {A}-1\in ℤ$
23 22 zcnd ${⊢}{\phi }\to {A}-1\in ℂ$
24 13 a1i ${⊢}{\phi }\to 1\in ℂ$
25 peano2zm ${⊢}{B}\in ℤ\to {B}-1\in ℤ$
26 16 25 syl ${⊢}{\phi }\to {B}-1\in ℤ$
27 26 zcnd ${⊢}{\phi }\to {B}-1\in ℂ$
28 23 24 27 24 muladdd ${⊢}{\phi }\to \left({A}-1+1\right)\left({B}-1+1\right)=\left({A}-1\right)\left({B}-1\right)+1\cdot 1+\left({A}-1\right)\cdot 1+\left({B}-1\right)\cdot 1$
29 1t1e1 ${⊢}1\cdot 1=1$
30 29 a1i ${⊢}{\phi }\to 1\cdot 1=1$
31 30 oveq2d ${⊢}{\phi }\to \left({A}-1\right)\left({B}-1\right)+1\cdot 1=\left({A}-1\right)\left({B}-1\right)+1$
32 23 mulid1d ${⊢}{\phi }\to \left({A}-1\right)\cdot 1={A}-1$
33 27 mulid1d ${⊢}{\phi }\to \left({B}-1\right)\cdot 1={B}-1$
34 32 33 oveq12d ${⊢}{\phi }\to \left({A}-1\right)\cdot 1+\left({B}-1\right)\cdot 1=\left({A}-1\right)+{B}-1$
35 31 34 oveq12d ${⊢}{\phi }\to \left({A}-1\right)\left({B}-1\right)+1\cdot 1+\left({A}-1\right)\cdot 1+\left({B}-1\right)\cdot 1=\left({A}-1\right)\left({B}-1\right)+1+\left({A}-1\right)+\left({B}-1\right)$
36 28 35 eqtrd ${⊢}{\phi }\to \left({A}-1+1\right)\left({B}-1+1\right)=\left({A}-1\right)\left({B}-1\right)+1+\left({A}-1\right)+\left({B}-1\right)$
37 20 36 eqtr3d ${⊢}{\phi }\to {A}{B}=\left({A}-1\right)\left({B}-1\right)+1+\left({A}-1\right)+\left({B}-1\right)$
38 8 37 eqtr3d ${⊢}{\phi }\to {M}=\left({A}-1\right)\left({B}-1\right)+1+\left({A}-1\right)+\left({B}-1\right)$
39 38 oveq1d ${⊢}{\phi }\to {M}-1=\left(\left({A}-1\right)\left({B}-1\right)+1\right)+\left(\left({A}-1\right)+{B}-1\right)-1$
40 23 27 mulcld ${⊢}{\phi }\to \left({A}-1\right)\left({B}-1\right)\in ℂ$
41 addcl ${⊢}\left(\left({A}-1\right)\left({B}-1\right)\in ℂ\wedge 1\in ℂ\right)\to \left({A}-1\right)\left({B}-1\right)+1\in ℂ$
42 40 13 41 sylancl ${⊢}{\phi }\to \left({A}-1\right)\left({B}-1\right)+1\in ℂ$
43 23 27 addcld ${⊢}{\phi }\to \left({A}-1\right)+{B}-1\in ℂ$
44 42 43 24 addsubd ${⊢}{\phi }\to \left(\left({A}-1\right)\left({B}-1\right)+1\right)+\left(\left({A}-1\right)+{B}-1\right)-1=\left(\left({A}-1\right)\left({B}-1\right)+1-1\right)+\left({A}-1\right)+\left({B}-1\right)$
45 pncan ${⊢}\left(\left({A}-1\right)\left({B}-1\right)\in ℂ\wedge 1\in ℂ\right)\to \left({A}-1\right)\left({B}-1\right)+1-1=\left({A}-1\right)\left({B}-1\right)$
46 40 13 45 sylancl ${⊢}{\phi }\to \left({A}-1\right)\left({B}-1\right)+1-1=\left({A}-1\right)\left({B}-1\right)$
47 46 oveq1d ${⊢}{\phi }\to \left(\left({A}-1\right)\left({B}-1\right)+1-1\right)+\left({A}-1\right)+\left({B}-1\right)=\left({A}-1\right)\left({B}-1\right)+\left({A}-1\right)+\left({B}-1\right)$
48 39 44 47 3eqtrd ${⊢}{\phi }\to {M}-1=\left({A}-1\right)\left({B}-1\right)+\left({A}-1\right)+\left({B}-1\right)$
49 48 oveq1d ${⊢}{\phi }\to \frac{{M}-1}{2}=\frac{\left({A}-1\right)\left({B}-1\right)+\left({A}-1\right)+\left({B}-1\right)}{2}$
50 2cnd ${⊢}{\phi }\to 2\in ℂ$
51 2ne0 ${⊢}2\ne 0$
52 51 a1i ${⊢}{\phi }\to 2\ne 0$
53 40 43 50 52 divdird ${⊢}{\phi }\to \frac{\left({A}-1\right)\left({B}-1\right)+\left({A}-1\right)+\left({B}-1\right)}{2}=\left(\frac{\left({A}-1\right)\left({B}-1\right)}{2}\right)+\left(\frac{\left({A}-1\right)+{B}-1}{2}\right)$
54 23 27 50 52 divassd ${⊢}{\phi }\to \frac{\left({A}-1\right)\left({B}-1\right)}{2}=\left({A}-1\right)\left(\frac{{B}-1}{2}\right)$
55 23 50 52 divcan2d ${⊢}{\phi }\to 2\left(\frac{{A}-1}{2}\right)={A}-1$
56 55 oveq1d ${⊢}{\phi }\to 2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)=\left({A}-1\right)\left(\frac{{B}-1}{2}\right)$
57 dvdsmul1 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}\parallel {A}{B}$
58 11 16 57 syl2anc ${⊢}{\phi }\to {A}\parallel {A}{B}$
59 58 8 breqtrd ${⊢}{\phi }\to {A}\parallel {M}$
60 2z ${⊢}2\in ℤ$
61 1 nnzd ${⊢}{\phi }\to {M}\in ℤ$
62 dvdstr ${⊢}\left(2\in ℤ\wedge {A}\in ℤ\wedge {M}\in ℤ\right)\to \left(\left(2\parallel {A}\wedge {A}\parallel {M}\right)\to 2\parallel {M}\right)$
63 60 11 61 62 mp3an2i ${⊢}{\phi }\to \left(\left(2\parallel {A}\wedge {A}\parallel {M}\right)\to 2\parallel {M}\right)$
64 59 63 mpan2d ${⊢}{\phi }\to \left(2\parallel {A}\to 2\parallel {M}\right)$
65 2 64 mtod ${⊢}{\phi }\to ¬2\parallel {A}$
66 1zzd ${⊢}{\phi }\to 1\in ℤ$
67 2prm ${⊢}2\in ℙ$
68 nprmdvds1 ${⊢}2\in ℙ\to ¬2\parallel 1$
69 67 68 mp1i ${⊢}{\phi }\to ¬2\parallel 1$
70 omoe ${⊢}\left(\left({A}\in ℤ\wedge ¬2\parallel {A}\right)\wedge \left(1\in ℤ\wedge ¬2\parallel 1\right)\right)\to 2\parallel \left({A}-1\right)$
71 11 65 66 69 70 syl22anc ${⊢}{\phi }\to 2\parallel \left({A}-1\right)$
72 dvdsval2 ${⊢}\left(2\in ℤ\wedge 2\ne 0\wedge {A}-1\in ℤ\right)\to \left(2\parallel \left({A}-1\right)↔\frac{{A}-1}{2}\in ℤ\right)$
73 60 52 22 72 mp3an2i ${⊢}{\phi }\to \left(2\parallel \left({A}-1\right)↔\frac{{A}-1}{2}\in ℤ\right)$
74 71 73 mpbid ${⊢}{\phi }\to \frac{{A}-1}{2}\in ℤ$
75 74 zcnd ${⊢}{\phi }\to \frac{{A}-1}{2}\in ℂ$
76 dvdsmul2 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {B}\parallel {A}{B}$
77 11 16 76 syl2anc ${⊢}{\phi }\to {B}\parallel {A}{B}$
78 77 8 breqtrd ${⊢}{\phi }\to {B}\parallel {M}$
79 dvdstr ${⊢}\left(2\in ℤ\wedge {B}\in ℤ\wedge {M}\in ℤ\right)\to \left(\left(2\parallel {B}\wedge {B}\parallel {M}\right)\to 2\parallel {M}\right)$
80 60 16 61 79 mp3an2i ${⊢}{\phi }\to \left(\left(2\parallel {B}\wedge {B}\parallel {M}\right)\to 2\parallel {M}\right)$
81 78 80 mpan2d ${⊢}{\phi }\to \left(2\parallel {B}\to 2\parallel {M}\right)$
82 2 81 mtod ${⊢}{\phi }\to ¬2\parallel {B}$
83 omoe ${⊢}\left(\left({B}\in ℤ\wedge ¬2\parallel {B}\right)\wedge \left(1\in ℤ\wedge ¬2\parallel 1\right)\right)\to 2\parallel \left({B}-1\right)$
84 16 82 66 69 83 syl22anc ${⊢}{\phi }\to 2\parallel \left({B}-1\right)$
85 dvdsval2 ${⊢}\left(2\in ℤ\wedge 2\ne 0\wedge {B}-1\in ℤ\right)\to \left(2\parallel \left({B}-1\right)↔\frac{{B}-1}{2}\in ℤ\right)$
86 60 52 26 85 mp3an2i ${⊢}{\phi }\to \left(2\parallel \left({B}-1\right)↔\frac{{B}-1}{2}\in ℤ\right)$
87 84 86 mpbid ${⊢}{\phi }\to \frac{{B}-1}{2}\in ℤ$
88 87 zcnd ${⊢}{\phi }\to \frac{{B}-1}{2}\in ℂ$
89 50 75 88 mulassd ${⊢}{\phi }\to 2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)=2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)$
90 54 56 89 3eqtr2d ${⊢}{\phi }\to \frac{\left({A}-1\right)\left({B}-1\right)}{2}=2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)$
91 23 27 50 52 divdird ${⊢}{\phi }\to \frac{\left({A}-1\right)+{B}-1}{2}=\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)$
92 90 91 oveq12d ${⊢}{\phi }\to \left(\frac{\left({A}-1\right)\left({B}-1\right)}{2}\right)+\left(\frac{\left({A}-1\right)+{B}-1}{2}\right)=2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)+\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)$
93 49 53 92 3eqtrd ${⊢}{\phi }\to \frac{{M}-1}{2}=2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)+\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)$
94 93 oveq1d ${⊢}{\phi }\to \left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)=\left(2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)+\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)$
95 60 a1i ${⊢}{\phi }\to 2\in ℤ$
96 74 87 zmulcld ${⊢}{\phi }\to \left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\in ℤ$
97 95 96 zmulcld ${⊢}{\phi }\to 2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\in ℤ$
98 97 zcnd ${⊢}{\phi }\to 2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\in ℂ$
99 74 87 zaddcld ${⊢}{\phi }\to \left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\in ℤ$
100 99 zcnd ${⊢}{\phi }\to \left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\in ℂ$
101 3 nnzd ${⊢}{\phi }\to {N}\in ℤ$
102 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)$
103 101 4 66 69 102 syl22anc ${⊢}{\phi }\to 2\parallel \left({N}-1\right)$
104 peano2zm ${⊢}{N}\in ℤ\to {N}-1\in ℤ$
105 101 104 syl ${⊢}{\phi }\to {N}-1\in ℤ$
106 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)$
107 60 52 105 106 mp3an2i ${⊢}{\phi }\to \left(2\parallel \left({N}-1\right)↔\frac{{N}-1}{2}\in ℤ\right)$
108 103 107 mpbid ${⊢}{\phi }\to \frac{{N}-1}{2}\in ℤ$
109 108 zcnd ${⊢}{\phi }\to \frac{{N}-1}{2}\in ℂ$
110 98 100 109 adddird ${⊢}{\phi }\to \left(2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)+\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)=2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)$
111 96 zcnd ${⊢}{\phi }\to \left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\in ℂ$
112 50 111 109 mulassd ${⊢}{\phi }\to 2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)=2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)$
113 112 oveq1d ${⊢}{\phi }\to 2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)=2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)$
114 94 110 113 3eqtrd ${⊢}{\phi }\to \left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)=2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)$
115 114 oveq2d ${⊢}{\phi }\to {\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}$
116 neg1cn ${⊢}-1\in ℂ$
117 116 a1i ${⊢}{\phi }\to -1\in ℂ$
118 neg1ne0 ${⊢}-1\ne 0$
119 118 a1i ${⊢}{\phi }\to -1\ne 0$
120 96 108 zmulcld ${⊢}{\phi }\to \left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)\in ℤ$
121 95 120 zmulcld ${⊢}{\phi }\to 2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)\in ℤ$
122 99 108 zmulcld ${⊢}{\phi }\to \left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)\in ℤ$
123 expaddz ${⊢}\left(\left(-1\in ℂ\wedge -1\ne 0\right)\wedge \left(2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)\in ℤ\wedge \left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)\in ℤ\right)\right)\to {\left(-1\right)}^{2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}{\left(-1\right)}^{\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}$
124 117 119 121 122 123 syl22anc ${⊢}{\phi }\to {\left(-1\right)}^{2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}{\left(-1\right)}^{\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}$
125 expmulz ${⊢}\left(\left(-1\in ℂ\wedge -1\ne 0\right)\wedge \left(2\in ℤ\wedge \left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)\in ℤ\right)\right)\to {\left(-1\right)}^{2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={\left({-1}^{2}\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
126 117 119 95 120 125 syl22anc ${⊢}{\phi }\to {\left(-1\right)}^{2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={\left({-1}^{2}\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
127 neg1sqe1 ${⊢}{\left(-1\right)}^{2}=1$
128 127 oveq1i ${⊢}{\left({-1}^{2}\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={1}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
129 1exp ${⊢}\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)\in ℤ\to {1}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}=1$
130 120 129 syl ${⊢}{\phi }\to {1}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}=1$
131 128 130 syl5eq ${⊢}{\phi }\to {\left({-1}^{2}\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}=1$
132 126 131 eqtrd ${⊢}{\phi }\to {\left(-1\right)}^{2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}=1$
133 132 oveq1d ${⊢}{\phi }\to {\left(-1\right)}^{2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}{\left(-1\right)}^{\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}=1{\left(-1\right)}^{\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}$
134 124 133 eqtrd ${⊢}{\phi }\to {\left(-1\right)}^{2\left(\frac{{A}-1}{2}\right)\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}=1{\left(-1\right)}^{\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}$
135 117 119 122 expclzd ${⊢}{\phi }\to {\left(-1\right)}^{\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}\in ℂ$
136 135 mulid2d ${⊢}{\phi }\to 1{\left(-1\right)}^{\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}$
137 75 88 109 adddird ${⊢}{\phi }\to \left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)=\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)$
138 137 oveq2d ${⊢}{\phi }\to {\left(-1\right)}^{\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
139 136 138 eqtrd ${⊢}{\phi }\to 1{\left(-1\right)}^{\left(\left(\frac{{A}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
140 115 134 139 3eqtrd ${⊢}{\phi }\to {\left(-1\right)}^{\left(\frac{{M}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
141 9 10 oveq12d ${⊢}{\phi }\to \left({A}{/}_{L}{N}\right)\left({N}{/}_{L}{A}\right)\left({B}{/}_{L}{N}\right)\left({N}{/}_{L}{B}\right)={\left(-1\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}{\left(-1\right)}^{\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
142 74 108 zmulcld ${⊢}{\phi }\to \left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)\in ℤ$
143 87 108 zmulcld ${⊢}{\phi }\to \left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)\in ℤ$
144 expaddz ${⊢}\left(\left(-1\in ℂ\wedge -1\ne 0\right)\wedge \left(\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)\in ℤ\wedge \left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)\in ℤ\right)\right)\to {\left(-1\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}{\left(-1\right)}^{\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
145 117 119 142 143 144 syl22anc ${⊢}{\phi }\to {\left(-1\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}={\left(-1\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}{\left(-1\right)}^{\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
146 141 145 eqtr4d ${⊢}{\phi }\to \left({A}{/}_{L}{N}\right)\left({N}{/}_{L}{A}\right)\left({B}{/}_{L}{N}\right)\left({N}{/}_{L}{B}\right)={\left(-1\right)}^{\left(\frac{{A}-1}{2}\right)\left(\frac{{N}-1}{2}\right)+\left(\frac{{B}-1}{2}\right)\left(\frac{{N}-1}{2}\right)}$
147 lgscl ${⊢}\left({A}\in ℤ\wedge {N}\in ℤ\right)\to {A}{/}_{L}{N}\in ℤ$
148 11 101 147 syl2anc ${⊢}{\phi }\to {A}{/}_{L}{N}\in ℤ$
149 148 zcnd ${⊢}{\phi }\to {A}{/}_{L}{N}\in ℂ$
150 lgscl ${⊢}\left({B}\in ℤ\wedge {N}\in ℤ\right)\to {B}{/}_{L}{N}\in ℤ$
151 16 101 150 syl2anc ${⊢}{\phi }\to {B}{/}_{L}{N}\in ℤ$
152 151 zcnd ${⊢}{\phi }\to {B}{/}_{L}{N}\in ℂ$
153 lgscl ${⊢}\left({N}\in ℤ\wedge {A}\in ℤ\right)\to {N}{/}_{L}{A}\in ℤ$
154 101 11 153 syl2anc ${⊢}{\phi }\to {N}{/}_{L}{A}\in ℤ$
155 154 zcnd ${⊢}{\phi }\to {N}{/}_{L}{A}\in ℂ$
156 lgscl ${⊢}\left({N}\in ℤ\wedge {B}\in ℤ\right)\to {N}{/}_{L}{B}\in ℤ$
157 101 16 156 syl2anc ${⊢}{\phi }\to {N}{/}_{L}{B}\in ℤ$
158 157 zcnd ${⊢}{\phi }\to {N}{/}_{L}{B}\in ℂ$
159 149 152 155 158 mul4d ${⊢}{\phi }\to \left({A}{/}_{L}{N}\right)\left({B}{/}_{L}{N}\right)\left({N}{/}_{L}{A}\right)\left({N}{/}_{L}{B}\right)=\left({A}{/}_{L}{N}\right)\left({N}{/}_{L}{A}\right)\left({B}{/}_{L}{N}\right)\left({N}{/}_{L}{B}\right)$
160 6 nnne0d ${⊢}{\phi }\to {A}\ne 0$
161 7 nnne0d ${⊢}{\phi }\to {B}\ne 0$
162 lgsdir ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({A}\ne 0\wedge {B}\ne 0\right)\right)\to {A}{B}{/}_{L}{N}=\left({A}{/}_{L}{N}\right)\left({B}{/}_{L}{N}\right)$
163 11 16 101 160 161 162 syl32anc ${⊢}{\phi }\to {A}{B}{/}_{L}{N}=\left({A}{/}_{L}{N}\right)\left({B}{/}_{L}{N}\right)$
164 8 oveq1d ${⊢}{\phi }\to {A}{B}{/}_{L}{N}={M}{/}_{L}{N}$
165 163 164 eqtr3d ${⊢}{\phi }\to \left({A}{/}_{L}{N}\right)\left({B}{/}_{L}{N}\right)={M}{/}_{L}{N}$
166 lgsdi ${⊢}\left(\left({N}\in ℤ\wedge {A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({A}\ne 0\wedge {B}\ne 0\right)\right)\to {N}{/}_{L}{A}{B}=\left({N}{/}_{L}{A}\right)\left({N}{/}_{L}{B}\right)$
167 101 11 16 160 161 166 syl32anc ${⊢}{\phi }\to {N}{/}_{L}{A}{B}=\left({N}{/}_{L}{A}\right)\left({N}{/}_{L}{B}\right)$
168 8 oveq2d ${⊢}{\phi }\to {N}{/}_{L}{A}{B}={N}{/}_{L}{M}$
169 167 168 eqtr3d ${⊢}{\phi }\to \left({N}{/}_{L}{A}\right)\left({N}{/}_{L}{B}\right)={N}{/}_{L}{M}$
170 165 169 oveq12d ${⊢}{\phi }\to \left({A}{/}_{L}{N}\right)\left({B}{/}_{L}{N}\right)\left({N}{/}_{L}{A}\right)\left({N}{/}_{L}{B}\right)=\left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)$
171 159 170 eqtr3d ${⊢}{\phi }\to \left({A}{/}_{L}{N}\right)\left({N}{/}_{L}{A}\right)\left({B}{/}_{L}{N}\right)\left({N}{/}_{L}{B}\right)=\left({M}{/}_{L}{N}\right)\left({N}{/}_{L}{M}\right)$
172 140 146 171 3eqtr2rd ${⊢}{\phi }\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)}$