lgsquad2lem1

	Ref	Expression
Hypotheses	lgsquad2.1	$⊢ φ \to M \in ℕ$
	lgsquad2.2	$⊢ φ \to \neg 2 ∥ M$
	lgsquad2.3	$⊢ φ \to N \in ℕ$
	lgsquad2.4	$⊢ φ \to \neg 2 ∥ N$
	lgsquad2.5	$⊢ φ \to M \gcd N = 1$
	lgsquad2lem1.a	$⊢ φ \to A \in ℕ$
	lgsquad2lem1.b	$⊢ φ \to B \in ℕ$
	lgsquad2lem1.m	$⊢ φ \to A B = M$
	lgsquad2lem1.1	$⊢ φ \to (A /_{L} N) (N /_{L} A) = {(- 1)}^{(\frac{A - 1}{2}) (\frac{N - 1}{2})}$
	lgsquad2lem1.2	$⊢ φ \to (B /_{L} N) (N /_{L} B) = {(- 1)}^{(\frac{B - 1}{2}) (\frac{N - 1}{2})}$
Assertion	lgsquad2lem1	$⊢ φ \to (M /_{L} N) (N /_{L} M) = {(- 1)}^{(\frac{M - 1}{2}) (\frac{N - 1}{2})}$

Proof

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

Metamath Proof Explorer

Theorem lgsquad2lem1

Proof