Theorem lgsquad2lem2 24366

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

Hypotheses

Ref	Expression
lgsquad2.1	|- ( ph -> M e. NN )
lgsquad2.2	|- ( ph -> -. 2 || M )
lgsquad2.3	|- ( ph -> N e. NN )
lgsquad2.4	|- ( ph -> -. 2 || N )
lgsquad2.5	|- ( ph -> ( M gcd N ) = 1 )
lgsquad2lem2.f	|- ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
lgsquad2lem2.s	|- ( ps <-> A. x e. ( 1 ... k ) ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )

Assertion

Ref	Expression
lgsquad2lem2	|- ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )

Distinct variable groups:   m, M   x, m, N   ph, m, x

Allowed substitution hints:   ph( k)   ps( x, k, m)   M( x, k)   N( k)

Proof of Theorem lgsquad2lem2

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lgsquad2.1	. . . 4 |- ( ph -> M e. NN )
2		2nn 10790	. . . . 5 |- 2 e. NN
3	2	a1i 11	. . . 4 |- ( ph -> 2 e. NN )
4		lgsquad2.3	. . . 4 |- ( ph -> N e. NN )
5	1	nnzd 11062	. . . . . 6 |- ( ph -> M e. ZZ )
6		2z 10993	. . . . . 6 |- 2 e. ZZ
7		gcdcom 14563	. . . . . 6 |- ( ( M e. ZZ /\ 2 e. ZZ ) -> ( M gcd 2 ) = ( 2 gcd M ) )
8	5, 6, 7	sylancl 675	. . . . 5 |- ( ph -> ( M gcd 2 ) = ( 2 gcd M ) )
9		lgsquad2.2	. . . . . 6 |- ( ph -> -. 2 || M )
10		2prm 14719	. . . . . . 7 |- 2 e. Prime
11		coprm 14736	. . . . . . 7 |- ( ( 2 e. Prime /\ M e. ZZ ) -> ( -. 2 || M <-> ( 2 gcd M ) = 1 ) )
12	10, 5, 11	sylancr 676	. . . . . 6 |- ( ph -> ( -. 2 || M <-> ( 2 gcd M ) = 1 ) )
13	9, 12	mpbid 215	. . . . 5 |- ( ph -> ( 2 gcd M ) = 1 )
14	8, 13	eqtrd 2505	. . . 4 |- ( ph -> ( M gcd 2 ) = 1 )
15		rpmulgcd 14602	. . . 4 |- ( ( ( M e. NN /\ 2 e. NN /\ N e. NN ) /\ ( M gcd 2 ) = 1 ) -> ( M gcd ( 2 x. N ) ) = ( M gcd N ) )
16	1, 3, 4, 14, 15	syl31anc 1295	. . 3 |- ( ph -> ( M gcd ( 2 x. N ) ) = ( M gcd N ) )
17		lgsquad2.5	. . 3 |- ( ph -> ( M gcd N ) = 1 )
18	16, 17	eqtrd 2505	. 2 |- ( ph -> ( M gcd ( 2 x. N ) ) = 1 )
19		oveq1 6315	. . . . . . . 8 |- ( m = 1 -> ( m /L N ) = ( 1 /L N ) )
20		oveq2 6316	. . . . . . . 8 |- ( m = 1 -> ( N /L m ) = ( N /L 1 ) )
21	19, 20	oveq12d 6326	. . . . . . 7 |- ( m = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( ( 1 /L N ) x. ( N /L 1 ) ) )
22		oveq1 6315	. . . . . . . . . . . 12 |- ( m = 1 -> ( m - 1 ) = ( 1 - 1 ) )
23		1m1e0 10700	. . . . . . . . . . . 12 |- ( 1 - 1 ) = 0
24	22, 23	syl6eq 2521	. . . . . . . . . . 11 |- ( m = 1 -> ( m - 1 ) = 0 )
25	24	oveq1d 6323	. . . . . . . . . 10 |- ( m = 1 -> ( ( m - 1 ) / 2 ) = ( 0 / 2 ) )
26		2cn 10702	. . . . . . . . . . 11 |- 2 e. CC
27		2ne0 10724	. . . . . . . . . . 11 |- 2 =/= 0
28	26, 27	div0i 10363	. . . . . . . . . 10 |- ( 0 / 2 ) = 0
29	25, 28	syl6eq 2521	. . . . . . . . 9 |- ( m = 1 -> ( ( m - 1 ) / 2 ) = 0 )
30	29	oveq1d 6323	. . . . . . . 8 |- ( m = 1 -> ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( 0 x. ( ( N - 1 ) / 2 ) ) )
31	30	oveq2d 6324	. . . . . . 7 |- ( m = 1 -> ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) )
32	21, 31	eqeq12d 2486	. . . . . 6 |- ( m = 1 -> ( ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) <-> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) ) )
33	32	imbi2d 323	. . . . 5 |- ( m = 1 -> ( ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) <-> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) ) ) )
34	33	imbi2d 323	. . . 4 |- ( m = 1 -> ( ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) <-> ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
35		oveq1 6315	. . . . . . 7 |- ( m = x -> ( m gcd ( 2 x. N ) ) = ( x gcd ( 2 x. N ) ) )
36	35	eqeq1d 2473	. . . . . 6 |- ( m = x -> ( ( m gcd ( 2 x. N ) ) = 1 <-> ( x gcd ( 2 x. N ) ) = 1 ) )
37		oveq1 6315	. . . . . . . 8 |- ( m = x -> ( m /L N ) = ( x /L N ) )
38		oveq2 6316	. . . . . . . 8 |- ( m = x -> ( N /L m ) = ( N /L x ) )
39	37, 38	oveq12d 6326	. . . . . . 7 |- ( m = x -> ( ( m /L N ) x. ( N /L m ) ) = ( ( x /L N ) x. ( N /L x ) ) )
40		oveq1 6315	. . . . . . . . . 10 |- ( m = x -> ( m - 1 ) = ( x - 1 ) )
41	40	oveq1d 6323	. . . . . . . . 9 |- ( m = x -> ( ( m - 1 ) / 2 ) = ( ( x - 1 ) / 2 ) )
42	41	oveq1d 6323	. . . . . . . 8 |- ( m = x -> ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) )
43	42	oveq2d 6324	. . . . . . 7 |- ( m = x -> ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
44	39, 43	eqeq12d 2486	. . . . . 6 |- ( m = x -> ( ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) <-> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
45	36, 44	imbi12d 327	. . . . 5 |- ( m = x -> ( ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) <-> ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
46	45	imbi2d 323	. . . 4 |- ( m = x -> ( ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) <-> ( ph -> ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
47		oveq1 6315	. . . . . . 7 |- ( m = y -> ( m gcd ( 2 x. N ) ) = ( y gcd ( 2 x. N ) ) )
48	47	eqeq1d 2473	. . . . . 6 |- ( m = y -> ( ( m gcd ( 2 x. N ) ) = 1 <-> ( y gcd ( 2 x. N ) ) = 1 ) )
49		oveq1 6315	. . . . . . . 8 |- ( m = y -> ( m /L N ) = ( y /L N ) )
50		oveq2 6316	. . . . . . . 8 |- ( m = y -> ( N /L m ) = ( N /L y ) )
51	49, 50	oveq12d 6326	. . . . . . 7 |- ( m = y -> ( ( m /L N ) x. ( N /L m ) ) = ( ( y /L N ) x. ( N /L y ) ) )
52		oveq1 6315	. . . . . . . . . 10 |- ( m = y -> ( m - 1 ) = ( y - 1 ) )
53	52	oveq1d 6323	. . . . . . . . 9 |- ( m = y -> ( ( m - 1 ) / 2 ) = ( ( y - 1 ) / 2 ) )
54	53	oveq1d 6323	. . . . . . . 8 |- ( m = y -> ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) )
55	54	oveq2d 6324	. . . . . . 7 |- ( m = y -> ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
56	51, 55	eqeq12d 2486	. . . . . 6 |- ( m = y -> ( ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) <-> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
57	48, 56	imbi12d 327	. . . . 5 |- ( m = y -> ( ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) <-> ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
58	57	imbi2d 323	. . . 4 |- ( m = y -> ( ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) <-> ( ph -> ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
59		oveq1 6315	. . . . . . 7 |- ( m = ( x x. y ) -> ( m gcd ( 2 x. N ) ) = ( ( x x. y ) gcd ( 2 x. N ) ) )
60	59	eqeq1d 2473	. . . . . 6 |- ( m = ( x x. y ) -> ( ( m gcd ( 2 x. N ) ) = 1 <-> ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) )
61		oveq1 6315	. . . . . . . 8 |- ( m = ( x x. y ) -> ( m /L N ) = ( ( x x. y ) /L N ) )
62		oveq2 6316	. . . . . . . 8 |- ( m = ( x x. y ) -> ( N /L m ) = ( N /L ( x x. y ) ) )
63	61, 62	oveq12d 6326	. . . . . . 7 |- ( m = ( x x. y ) -> ( ( m /L N ) x. ( N /L m ) ) = ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) )
64		oveq1 6315	. . . . . . . . . 10 |- ( m = ( x x. y ) -> ( m - 1 ) = ( ( x x. y ) - 1 ) )
65	64	oveq1d 6323	. . . . . . . . 9 |- ( m = ( x x. y ) -> ( ( m - 1 ) / 2 ) = ( ( ( x x. y ) - 1 ) / 2 ) )
66	65	oveq1d 6323	. . . . . . . 8 |- ( m = ( x x. y ) -> ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) )
67	66	oveq2d 6324	. . . . . . 7 |- ( m = ( x x. y ) -> ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
68	63, 67	eqeq12d 2486	. . . . . 6 |- ( m = ( x x. y ) -> ( ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) <-> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
69	60, 68	imbi12d 327	. . . . 5 |- ( m = ( x x. y ) -> ( ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) <-> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
70	69	imbi2d 323	. . . 4 |- ( m = ( x x. y ) -> ( ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) <-> ( ph -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
71		oveq1 6315	. . . . . . 7 |- ( m = M -> ( m gcd ( 2 x. N ) ) = ( M gcd ( 2 x. N ) ) )
72	71	eqeq1d 2473	. . . . . 6 |- ( m = M -> ( ( m gcd ( 2 x. N ) ) = 1 <-> ( M gcd ( 2 x. N ) ) = 1 ) )
73		oveq1 6315	. . . . . . . 8 |- ( m = M -> ( m /L N ) = ( M /L N ) )
74		oveq2 6316	. . . . . . . 8 |- ( m = M -> ( N /L m ) = ( N /L M ) )
75	73, 74	oveq12d 6326	. . . . . . 7 |- ( m = M -> ( ( m /L N ) x. ( N /L m ) ) = ( ( M /L N ) x. ( N /L M ) ) )
76		oveq1 6315	. . . . . . . . . 10 |- ( m = M -> ( m - 1 ) = ( M - 1 ) )
77	76	oveq1d 6323	. . . . . . . . 9 |- ( m = M -> ( ( m - 1 ) / 2 ) = ( ( M - 1 ) / 2 ) )
78	77	oveq1d 6323	. . . . . . . 8 |- ( m = M -> ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) = ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) )
79	78	oveq2d 6324	. . . . . . 7 |- ( m = M -> ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
80	75, 79	eqeq12d 2486	. . . . . 6 |- ( m = M -> ( ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) <-> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
81	72, 80	imbi12d 327	. . . . 5 |- ( m = M -> ( ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) <-> ( ( M gcd ( 2 x. N ) ) = 1 -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
82	81	imbi2d 323	. . . 4 |- ( m = M -> ( ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) <-> ( ph -> ( ( M gcd ( 2 x. N ) ) = 1 -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
83		1t1e1 10780	. . . . . . 7 |- ( 1 x. 1 ) = 1
84		neg1cn 10735	. . . . . . . 8 |- -u 1 e. CC
85		exp0 12314	. . . . . . . 8 |- ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
86	84, 85	ax-mp 5	. . . . . . 7 |- ( -u 1 ^ 0 ) = 1
87	83, 86	eqtr4i 2496	. . . . . 6 |- ( 1 x. 1 ) = ( -u 1 ^ 0 )
88		sq1 12407	. . . . . . . . 9 |- ( 1 ^ 2 ) = 1
89	88	oveq1i 6318	. . . . . . . 8 |- ( ( 1 ^ 2 ) /L N ) = ( 1 /L N )
90		1nn 10642	. . . . . . . . . 10 |- 1 e. NN
91	90	a1i 11	. . . . . . . . 9 |- ( ph -> 1 e. NN )
92	4	nnzd 11062	. . . . . . . . 9 |- ( ph -> N e. ZZ )
93		1gcd 14580	. . . . . . . . . 10 |- ( N e. ZZ -> ( 1 gcd N ) = 1 )
94	92, 93	syl 17	. . . . . . . . 9 |- ( ph -> ( 1 gcd N ) = 1 )
95		lgssq 24342	. . . . . . . . 9 |- ( ( 1 e. NN /\ N e. ZZ /\ ( 1 gcd N ) = 1 ) -> ( ( 1 ^ 2 ) /L N ) = 1 )
96	91, 92, 94, 95	syl3anc 1292	. . . . . . . 8 |- ( ph -> ( ( 1 ^ 2 ) /L N ) = 1 )
97	89, 96	syl5eqr 2519	. . . . . . 7 |- ( ph -> ( 1 /L N ) = 1 )
98	88	oveq2i 6319	. . . . . . . 8 |- ( N /L ( 1 ^ 2 ) ) = ( N /L 1 )
99		gcd1 14575	. . . . . . . . . 10 |- ( N e. ZZ -> ( N gcd 1 ) = 1 )
100	92, 99	syl 17	. . . . . . . . 9 |- ( ph -> ( N gcd 1 ) = 1 )
101		lgssq2 24343	. . . . . . . . 9 |- ( ( N e. ZZ /\ 1 e. NN /\ ( N gcd 1 ) = 1 ) -> ( N /L ( 1 ^ 2 ) ) = 1 )
102	92, 91, 100, 101	syl3anc 1292	. . . . . . . 8 |- ( ph -> ( N /L ( 1 ^ 2 ) ) = 1 )
103	98, 102	syl5eqr 2519	. . . . . . 7 |- ( ph -> ( N /L 1 ) = 1 )
104	97, 103	oveq12d 6326	. . . . . 6 |- ( ph -> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( 1 x. 1 ) )
105		nnm1nn0 10935	. . . . . . . . . . 11 |- ( N e. NN -> ( N - 1 ) e. NN0 )
106	4, 105	syl 17	. . . . . . . . . 10 |- ( ph -> ( N - 1 ) e. NN0 )
107	106	nn0cnd 10951	. . . . . . . . 9 |- ( ph -> ( N - 1 ) e. CC )
108	107	halfcld 10880	. . . . . . . 8 |- ( ph -> ( ( N - 1 ) / 2 ) e. CC )
109	108	mul02d 9849	. . . . . . 7 |- ( ph -> ( 0 x. ( ( N - 1 ) / 2 ) ) = 0 )
110	109	oveq2d 6324	. . . . . 6 |- ( ph -> ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) = ( -u 1 ^ 0 ) )
111	87, 104, 110	3eqtr4a 2531	. . . . 5 |- ( ph -> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) )
112	111	a1d 25	. . . 4 |- ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( 1 /L N ) x. ( N /L 1 ) ) = ( -u 1 ^ ( 0 x. ( ( N - 1 ) / 2 ) ) ) ) )
113		simprl 772	. . . . . . . . 9 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> m e. Prime )
114		prmz 14705	. . . . . . . . . . . 12 |- ( m e. Prime -> m e. ZZ )
115	114	ad2antrl 742	. . . . . . . . . . 11 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> m e. ZZ )
116	6	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> 2 e. ZZ )
117	4	adantr 472	. . . . . . . . . . . . 13 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> N e. NN )
118	117	nnzd 11062	. . . . . . . . . . . 12 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> N e. ZZ )
119		zmulcl 11009	. . . . . . . . . . . 12 |- ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 x. N ) e. ZZ )
120	6, 118, 119	sylancr 676	. . . . . . . . . . 11 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( 2 x. N ) e. ZZ )
121		simprr 774	. . . . . . . . . . 11 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( m gcd ( 2 x. N ) ) = 1 )
122		dvdsmul1 14401	. . . . . . . . . . . 12 |- ( ( 2 e. ZZ /\ N e. ZZ ) -> 2 || ( 2 x. N ) )
123	6, 118, 122	sylancr 676	. . . . . . . . . . 11 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> 2 || ( 2 x. N ) )
124		rpdvds 14755	. . . . . . . . . . 11 |- ( ( ( m e. ZZ /\ 2 e. ZZ /\ ( 2 x. N ) e. ZZ ) /\ ( ( m gcd ( 2 x. N ) ) = 1 /\ 2 || ( 2 x. N ) ) ) -> ( m gcd 2 ) = 1 )
125	115, 116, 120, 121, 123, 124	syl32anc 1300	. . . . . . . . . 10 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( m gcd 2 ) = 1 )
126		prmrp 14737	. . . . . . . . . . 11 |- ( ( m e. Prime /\ 2 e. Prime ) -> ( ( m gcd 2 ) = 1 <-> m =/= 2 ) )
127	113, 10, 126	sylancl 675	. . . . . . . . . 10 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( ( m gcd 2 ) = 1 <-> m =/= 2 ) )
128	125, 127	mpbid 215	. . . . . . . . 9 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> m =/= 2 )
129		eldifsn 4088	. . . . . . . . 9 |- ( m e. ( Prime \ { 2 } ) <-> ( m e. Prime /\ m =/= 2 ) )
130	113, 128, 129	sylanbrc 677	. . . . . . . 8 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> m e. ( Prime \ { 2 } ) )
131		prmnn 14704	. . . . . . . . . . 11 |- ( m e. Prime -> m e. NN )
132	131	ad2antrl 742	. . . . . . . . . 10 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> m e. NN )
133	2	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> 2 e. NN )
134		rpmulgcd 14602	. . . . . . . . . 10 |- ( ( ( m e. NN /\ 2 e. NN /\ N e. NN ) /\ ( m gcd 2 ) = 1 ) -> ( m gcd ( 2 x. N ) ) = ( m gcd N ) )
135	132, 133, 117, 125, 134	syl31anc 1295	. . . . . . . . 9 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( m gcd ( 2 x. N ) ) = ( m gcd N ) )
136	135, 121	eqtr3d 2507	. . . . . . . 8 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( m gcd N ) = 1 )
137	130, 136	jca 541	. . . . . . 7 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) )
138		lgsquad2lem2.f	. . . . . . 7 |- ( ( ph /\ ( m e. ( Prime \ { 2 } ) /\ ( m gcd N ) = 1 ) ) -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
139	137, 138	syldan 478	. . . . . 6 |- ( ( ph /\ ( m e. Prime /\ ( m gcd ( 2 x. N ) ) = 1 ) ) -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
140	139	exp32 616	. . . . 5 |- ( ph -> ( m e. Prime -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
141	140	com12 31	. . . 4 |- ( m e. Prime -> ( ph -> ( ( m gcd ( 2 x. N ) ) = 1 -> ( ( m /L N ) x. ( N /L m ) ) = ( -u 1 ^ ( ( ( m - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
142		jcab 880	. . . . 5 |- ( ( ph -> ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) <-> ( ( ph -> ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) /\ ( ph -> ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
143		simplrl 778	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> x e. ( ZZ>= ` 2 ) )
144		eluz2nn 11221	. . . . . . . . . . . 12 |- ( x e. ( ZZ>= ` 2 ) -> x e. NN )
145	143, 144	syl 17	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> x e. NN )
146		simplrr 779	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> y e. ( ZZ>= ` 2 ) )
147		eluz2nn 11221	. . . . . . . . . . . 12 |- ( y e. ( ZZ>= ` 2 ) -> y e. NN )
148	146, 147	syl 17	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> y e. NN )
149	145, 148	nnmulcld 10679	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( x x. y ) e. NN )
150		n2dvds1 14431	. . . . . . . . . . . 12 |- -. 2 || 1
151	92	ad2antrr 740	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> N e. ZZ )
152	6, 151, 122	sylancr 676	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> 2 || ( 2 x. N ) )
153	6	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> 2 e. ZZ )
154		eluzelz 11192	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ZZ>= ` 2 ) -> x e. ZZ )
155		eluzelz 11192	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( ZZ>= ` 2 ) -> y e. ZZ )
156	154, 155	anim12i 576	. . . . . . . . . . . . . . . . 17 |- ( ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) -> ( x e. ZZ /\ y e. ZZ ) )
157	156	ad2antlr 741	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( x e. ZZ /\ y e. ZZ ) )
158		zmulcl 11009	. . . . . . . . . . . . . . . 16 |- ( ( x e. ZZ /\ y e. ZZ ) -> ( x x. y ) e. ZZ )
159	157, 158	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( x x. y ) e. ZZ )
160	6, 151, 119	sylancr 676	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( 2 x. N ) e. ZZ )
161		dvdsgcd 14590	. . . . . . . . . . . . . . 15 |- ( ( 2 e. ZZ /\ ( x x. y ) e. ZZ /\ ( 2 x. N ) e. ZZ ) -> ( ( 2 || ( x x. y ) /\ 2 || ( 2 x. N ) ) -> 2 || ( ( x x. y ) gcd ( 2 x. N ) ) ) )
162	153, 159, 160, 161	syl3anc 1292	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( 2 || ( x x. y ) /\ 2 || ( 2 x. N ) ) -> 2 || ( ( x x. y ) gcd ( 2 x. N ) ) ) )
163	152, 162	mpan2d 688	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( 2 || ( x x. y ) -> 2 || ( ( x x. y ) gcd ( 2 x. N ) ) ) )
164		simpr 468	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( x x. y ) gcd ( 2 x. N ) ) = 1 )
165	164	breq2d 4407	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( 2 || ( ( x x. y ) gcd ( 2 x. N ) ) <-> 2 || 1 ) )
166	163, 165	sylibd 222	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( 2 || ( x x. y ) -> 2 || 1 ) )
167	150, 166	mtoi 183	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> -. 2 || ( x x. y ) )
168	167	adantrr 731	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> -. 2 || ( x x. y ) )
169	4	ad2antrr 740	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> N e. NN )
170		lgsquad2.4	. . . . . . . . . . 11 |- ( ph -> -. 2 || N )
171	170	ad2antrr 740	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> -. 2 || N )
172		dvdsmul2 14402	. . . . . . . . . . . . 13 |- ( ( 2 e. ZZ /\ N e. ZZ ) -> N || ( 2 x. N ) )
173	6, 151, 172	sylancr 676	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> N || ( 2 x. N ) )
174		rpdvds 14755	. . . . . . . . . . . 12 |- ( ( ( ( x x. y ) e. ZZ /\ N e. ZZ /\ ( 2 x. N ) e. ZZ ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ N || ( 2 x. N ) ) ) -> ( ( x x. y ) gcd N ) = 1 )
175	159, 151, 160, 164, 173, 174	syl32anc 1300	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( x x. y ) gcd N ) = 1 )
176	175	adantrr 731	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( x x. y ) gcd N ) = 1 )
177		eqidd 2472	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( x x. y ) = ( x x. y ) )
178	157	simpld 466	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> x e. ZZ )
179		gcdcom 14563	. . . . . . . . . . . . . 14 |- ( ( x e. ZZ /\ ( 2 x. N ) e. ZZ ) -> ( x gcd ( 2 x. N ) ) = ( ( 2 x. N ) gcd x ) )
180	178, 160, 179	syl2anc 673	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( x gcd ( 2 x. N ) ) = ( ( 2 x. N ) gcd x ) )
181		gcdcom 14563	. . . . . . . . . . . . . . . 16 |- ( ( ( 2 x. N ) e. ZZ /\ ( x x. y ) e. ZZ ) -> ( ( 2 x. N ) gcd ( x x. y ) ) = ( ( x x. y ) gcd ( 2 x. N ) ) )
182	160, 159, 181	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( 2 x. N ) gcd ( x x. y ) ) = ( ( x x. y ) gcd ( 2 x. N ) ) )
183	182, 164	eqtrd 2505	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( 2 x. N ) gcd ( x x. y ) ) = 1 )
184		dvdsmul1 14401	. . . . . . . . . . . . . . 15 |- ( ( x e. ZZ /\ y e. ZZ ) -> x || ( x x. y ) )
185	157, 184	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> x || ( x x. y ) )
186		rpdvds 14755	. . . . . . . . . . . . . 14 |- ( ( ( ( 2 x. N ) e. ZZ /\ x e. ZZ /\ ( x x. y ) e. ZZ ) /\ ( ( ( 2 x. N ) gcd ( x x. y ) ) = 1 /\ x || ( x x. y ) ) ) -> ( ( 2 x. N ) gcd x ) = 1 )
187	160, 178, 159, 183, 185, 186	syl32anc 1300	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( 2 x. N ) gcd x ) = 1 )
188	180, 187	eqtrd 2505	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( x gcd ( 2 x. N ) ) = 1 )
189	188	adantrr 731	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( x gcd ( 2 x. N ) ) = 1 )
190		simprrl 782	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
191	189, 190	mpd 15	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
192	157	simprd 470	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> y e. ZZ )
193		gcdcom 14563	. . . . . . . . . . . . . 14 |- ( ( y e. ZZ /\ ( 2 x. N ) e. ZZ ) -> ( y gcd ( 2 x. N ) ) = ( ( 2 x. N ) gcd y ) )
194	192, 160, 193	syl2anc 673	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( y gcd ( 2 x. N ) ) = ( ( 2 x. N ) gcd y ) )
195		dvdsmul2 14402	. . . . . . . . . . . . . . 15 |- ( ( x e. ZZ /\ y e. ZZ ) -> y || ( x x. y ) )
196	157, 195	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> y || ( x x. y ) )
197		rpdvds 14755	. . . . . . . . . . . . . 14 |- ( ( ( ( 2 x. N ) e. ZZ /\ y e. ZZ /\ ( x x. y ) e. ZZ ) /\ ( ( ( 2 x. N ) gcd ( x x. y ) ) = 1 /\ y || ( x x. y ) ) ) -> ( ( 2 x. N ) gcd y ) = 1 )
198	160, 192, 159, 183, 196, 197	syl32anc 1300	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( ( 2 x. N ) gcd y ) = 1 )
199	194, 198	eqtrd 2505	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( x x. y ) gcd ( 2 x. N ) ) = 1 ) -> ( y gcd ( 2 x. N ) ) = 1 )
200	199	adantrr 731	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( y gcd ( 2 x. N ) ) = 1 )
201		simprrr 783	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
202	200, 201	mpd 15	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
203	149, 168, 169, 171, 176, 145, 148, 177, 191, 202	lgsquad2lem1 24365	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) /\ ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 /\ ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) ) -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )
204	203	exp32 616	. . . . . . . 8 |- ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
205	204	com23 80	. . . . . . 7 |- ( ( ph /\ ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) ) -> ( ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
206	205	expcom 442	. . . . . 6 |- ( ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) -> ( ph -> ( ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
207	206	a2d 28	. . . . 5 |- ( ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) -> ( ( ph -> ( ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) /\ ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) -> ( ph -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
208	142, 207	syl5bir 226	. . . 4 |- ( ( x e. ( ZZ>= ` 2 ) /\ y e. ( ZZ>= ` 2 ) ) -> ( ( ( ph -> ( ( x gcd ( 2 x. N ) ) = 1 -> ( ( x /L N ) x. ( N /L x ) ) = ( -u 1 ^ ( ( ( x - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) /\ ( ph -> ( ( y gcd ( 2 x. N ) ) = 1 -> ( ( y /L N ) x. ( N /L y ) ) = ( -u 1 ^ ( ( ( y - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) -> ( ph -> ( ( ( x x. y ) gcd ( 2 x. N ) ) = 1 -> ( ( ( x x. y ) /L N ) x. ( N /L ( x x. y ) ) ) = ( -u 1 ^ ( ( ( ( x x. y ) - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) ) )
209	34, 46, 58, 70, 82, 112, 141, 208	prmind 14715	. . 3 |- ( M e. NN -> ( ph -> ( ( M gcd ( 2 x. N ) ) = 1 -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) ) )
210	1, 209	mpcom 36	. 2 |- ( ph -> ( ( M gcd ( 2 x. N ) ) = 1 -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) ) )
211	18, 210	mpd 15	1 |- ( ph -> ( ( M /L N ) x. ( N /L M ) ) = ( -u 1 ^ ( ( ( M - 1 ) / 2 ) x. ( ( N - 1 ) / 2 ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 376   = wceq 1452   e. wcel 1904   =/= wne 2641   A.wral 2756   \ cdif 3387   {csn 3959   class class class wbr 4395   ` cfv 5589  (class class class)co 6308   CCcc 9555   0cc0 9557   1c1 9558   x. cmul 9562   - cmin 9880   -ucneg 9881   / cdiv 10291   NNcn 10631   2c2 10681   NN0cn0 10893   ZZcz 10961   ZZ>=cuz 11182   ...cfz 11810   ^cexp 12310   || cdvds 14382   gcd cgcd 14547   Primecprime 14701   /Lclgs 24301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-sup 7974  df-inf 7975  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-n0 10894  df-z 10962  df-uz 11183  df-q 11288  df-rp 11326  df-fz 11811  df-fzo 11943  df-fl 12061  df-mod 12130  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-dvds 14383  df-gcd 14548  df-prm 14702  df-phi 14793  df-pc 14866  df-lgs 24302

This theorem is referenced by:  lgsquad2  24367