Theorem lgsquadlem1 15191

Description: Lemma for Quadratic Reciprocity. Count the members of S with odd coordinates. (Contributed by Mario Carneiro, 19-Jun-2015.)

Hypotheses

Ref	Expression
lgseisen.1	|- ( ph -> P e. ( Prime \ { 2 } ) )
lgseisen.2	|- ( ph -> Q e. ( Prime \ { 2 } ) )
lgseisen.3	|- ( ph -> P =/= Q )
lgsquad.4	|- M = ( ( P - 1 ) / 2 )
lgsquad.5	|- N = ( ( Q - 1 ) / 2 )
lgsquad.6	|- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }

Assertion

Ref	Expression
lgsquadlem1	|- ( ph -> ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) )

Distinct variable groups:   x, u, y, z, P   ph, u, x, y, z   u, M, y, z   u, N, x, y, z   u, Q, x, y, z   u, S, x, z   x, M   y, S

Proof of Theorem lgsquadlem1

Dummy variables n v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		neg1cn 9087	. . . 4 |- -u 1 e. CC
2	1	a1i 9	. . 3 |- ( ph -> -u 1 e. CC )
3		neg1ap0 9091	. . . 4 |- -u 1 # 0
4	3	a1i 9	. . 3 |- ( ph -> -u 1 # 0 )
5		lgseisen.1	. . . . . . . . . 10 |- ( ph -> P e. ( Prime \ { 2 } ) )
6		lgsquad.4	. . . . . . . . . 10 |- M = ( ( P - 1 ) / 2 )
7	5, 6	gausslemma2dlem0b 15166	. . . . . . . . 9 |- ( ph -> M e. NN )
8	7	nnzd 9438	. . . . . . . 8 |- ( ph -> M e. ZZ )
9		2nn 9143	. . . . . . . 8 |- 2 e. NN
10		znq 9689	. . . . . . . 8 |- ( ( M e. ZZ /\ 2 e. NN ) -> ( M / 2 ) e. QQ )
11	8, 9, 10	sylancl 413	. . . . . . 7 |- ( ph -> ( M / 2 ) e. QQ )
12	11	flqcld 10346	. . . . . 6 |- ( ph -> ( |_ ` ( M / 2 ) ) e. ZZ )
13	12	peano2zd 9442	. . . . 5 |- ( ph -> ( ( |_ ` ( M / 2 ) ) + 1 ) e. ZZ )
14	13, 8	fzfigd 10502	. . . 4 |- ( ph -> ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) e. Fin )
15		lgseisen.2	. . . . . . . . 9 |- ( ph -> Q e. ( Prime \ { 2 } ) )
16	15	gausslemma2dlem0a 15165	. . . . . . . 8 |- ( ph -> Q e. NN )
17	16	nnzd 9438	. . . . . . 7 |- ( ph -> Q e. ZZ )
18	5	gausslemma2dlem0a 15165	. . . . . . . 8 |- ( ph -> P e. NN )
19	18	adantr 276	. . . . . . 7 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. NN )
20		znq 9689	. . . . . . 7 |- ( ( Q e. ZZ /\ P e. NN ) -> ( Q / P ) e. QQ )
21	17, 19, 20	syl2an2r 595	. . . . . 6 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q / P ) e. QQ )
22		2z 9345	. . . . . . . 8 |- 2 e. ZZ
23		elfzelz 10091	. . . . . . . . 9 |- ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) -> u e. ZZ )
24	23	adantl 277	. . . . . . . 8 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u e. ZZ )
25		zmulcl 9370	. . . . . . . 8 |- ( ( 2 e. ZZ /\ u e. ZZ ) -> ( 2 x. u ) e. ZZ )
26	22, 24, 25	sylancr 414	. . . . . . 7 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) e. ZZ )
27		zq 9691	. . . . . . 7 |- ( ( 2 x. u ) e. ZZ -> ( 2 x. u ) e. QQ )
28	26, 27	syl 14	. . . . . 6 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) e. QQ )
29		qmulcl 9702	. . . . . 6 |- ( ( ( Q / P ) e. QQ /\ ( 2 x. u ) e. QQ ) -> ( ( Q / P ) x. ( 2 x. u ) ) e. QQ )
30	21, 28, 29	syl2anc 411	. . . . 5 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / P ) x. ( 2 x. u ) ) e. QQ )
31	30	flqcld 10346	. . . 4 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ )
32	14, 31	fsumzcl 11545	. . 3 |- ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ )
33	2, 4, 32	expclzapd 10749	. 2 |- ( ph -> ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. CC )
34		lgsquad.6	. . . . . 6 |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }
35		1zzd 9344	. . . . . . 7 |- ( ph -> 1 e. ZZ )
36	35, 8	fzfigd 10502	. . . . . 6 |- ( ph -> ( 1 ... M ) e. Fin )
37		lgsquad.5	. . . . . . . . 9 |- N = ( ( Q - 1 ) / 2 )
38	15, 37	gausslemma2dlem0b 15166	. . . . . . . 8 |- ( ph -> N e. NN )
39	38	nnzd 9438	. . . . . . 7 |- ( ph -> N e. ZZ )
40	35, 39	fzfigd 10502	. . . . . 6 |- ( ph -> ( 1 ... N ) e. Fin )
41		elfznn 10120	. . . . . . . . . . 11 |- ( y e. ( 1 ... N ) -> y e. NN )
42	41	ad2antll 491	. . . . . . . . . 10 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. NN )
43	18	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. NN )
44	42, 43	nnmulcld 9031	. . . . . . . . 9 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. NN )
45	44	nnzd 9438	. . . . . . . 8 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. ZZ )
46		elfznn 10120	. . . . . . . . . . 11 |- ( x e. ( 1 ... M ) -> x e. NN )
47	46	ad2antrl 490	. . . . . . . . . 10 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> x e. NN )
48	16	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. NN )
49	47, 48	nnmulcld 9031	. . . . . . . . 9 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. NN )
50	49	nnzd 9438	. . . . . . . 8 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. ZZ )
51		zdclt 9394	. . . . . . . 8 |- ( ( ( y x. P ) e. ZZ /\ ( x x. Q ) e. ZZ ) -> DECID ( y x. P ) < ( x x. Q ) )
52	45, 50, 51	syl2anc 411	. . . . . . 7 |- ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> DECID ( y x. P ) < ( x x. Q ) )
53	52	ralrimivva 2576	. . . . . 6 |- ( ph -> A. x e. ( 1 ... M ) A. y e. ( 1 ... N )DECID ( y x. P ) < ( x x. Q ) )
54	34, 36, 40, 53	opabfi 6992	. . . . 5 |- ( ph -> S e. Fin )
55		opabssxp 4733	. . . . . . . . . . . . 13 |- { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } C_ ( ( 1 ... M ) X. ( 1 ... N ) )
56	34, 55	eqsstri 3211	. . . . . . . . . . . 12 |- S C_ ( ( 1 ... M ) X. ( 1 ... N ) )
57	56	sseli 3175	. . . . . . . . . . 11 |- ( z e. S -> z e. ( ( 1 ... M ) X. ( 1 ... N ) ) )
58		xp1st 6218	. . . . . . . . . . 11 |- ( z e. ( ( 1 ... M ) X. ( 1 ... N ) ) -> ( 1st ` z ) e. ( 1 ... M ) )
59	57, 58	syl 14	. . . . . . . . . 10 |- ( z e. S -> ( 1st ` z ) e. ( 1 ... M ) )
60	59	elfzelzd 10092	. . . . . . . . 9 |- ( z e. S -> ( 1st ` z ) e. ZZ )
61	60	adantl 277	. . . . . . . 8 |- ( ( ph /\ z e. S ) -> ( 1st ` z ) e. ZZ )
62		dvdsdc 11941	. . . . . . . 8 |- ( ( 2 e. NN /\ ( 1st ` z ) e. ZZ ) -> DECID 2 || ( 1st ` z ) )
63	9, 61, 62	sylancr 414	. . . . . . 7 |- ( ( ph /\ z e. S ) -> DECID 2 || ( 1st ` z ) )
64		dcn 843	. . . . . . 7 |- (DECID 2 || ( 1st ` z ) -> DECID -. 2 || ( 1st ` z ) )
65	63, 64	syl 14	. . . . . 6 |- ( ( ph /\ z e. S ) -> DECID -. 2 || ( 1st ` z ) )
66	65	ralrimiva 2567	. . . . 5 |- ( ph -> A. z e. S DECID -. 2 || ( 1st ` z ) )
67	54, 66	ssfirab 6990	. . . 4 |- ( ph -> { z e. S | -. 2 || ( 1st ` z ) } e. Fin )
68		hashcl 10852	. . . 4 |- ( { z e. S | -. 2 || ( 1st ` z ) } e. Fin -> (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) e. NN0 )
69	67, 68	syl 14	. . 3 |- ( ph -> (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) e. NN0 )
70		expcl 10628	. . 3 |- ( ( -u 1 e. CC /\ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) e. NN0 ) -> ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) e. CC )
71	1, 69, 70	sylancr 414	. 2 |- ( ph -> ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) e. CC )
72	69	nn0zd 9437	. . 3 |- ( ph -> (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) e. ZZ )
73	2, 4, 72	expap0d 10750	. 2 |- ( ph -> ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) # 0 )
74	71, 73	recidapd 8802	. . . 4 |- ( ph -> ( ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) x. ( 1 / ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) ) = 1 )
75		1div1e1 8723	. . . . . . . . 9 |- ( 1 / 1 ) = 1
76	75	negeqi 8213	. . . . . . . 8 |- -u ( 1 / 1 ) = -u 1
77		ax-1cn 7965	. . . . . . . . 9 |- 1 e. CC
78		1ap0 8609	. . . . . . . . 9 |- 1 # 0
79		divneg2ap 8755	. . . . . . . . 9 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 # 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) )
80	77, 77, 78, 79	mp3an 1348	. . . . . . . 8 |- -u ( 1 / 1 ) = ( 1 / -u 1 )
81	76, 80	eqtr3i 2216	. . . . . . 7 |- -u 1 = ( 1 / -u 1 )
82	81	oveq1i 5928	. . . . . 6 |- ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( ( 1 / -u 1 ) ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) )
83	2, 4, 72	exprecapd 10752	. . . . . 6 |- ( ph -> ( ( 1 / -u 1 ) ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( 1 / ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
84	82, 83	eqtrid 2238	. . . . 5 |- ( ph -> ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( 1 / ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
85	84	oveq2d 5934	. . . 4 |- ( ph -> ( ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) x. ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) x. ( 1 / ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) ) )
86	54	adantr 276	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> S e. Fin )
87	19	nnzd 9438	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. ZZ )
88	87, 26	zsubcld 9444	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - ( 2 x. u ) ) e. ZZ )
89		zdceq 9392	. . . . . . . . . . . . . 14 |- ( ( ( 1st ` z ) e. ZZ /\ ( P - ( 2 x. u ) ) e. ZZ ) -> DECID ( 1st ` z ) = ( P - ( 2 x. u ) ) )
90	60, 88, 89	syl2anr 290	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ z e. S ) -> DECID ( 1st ` z ) = ( P - ( 2 x. u ) ) )
91	90	ralrimiva 2567	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> A. z e. S DECID ( 1st ` z ) = ( P - ( 2 x. u ) ) )
92	86, 91	ssfirab 6990	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } e. Fin )
93		fveqeq2 5563	. . . . . . . . . . . . . . . . . . . 20 |- ( z = v -> ( ( 1st ` z ) = ( P - ( 2 x. u ) ) <-> ( 1st ` v ) = ( P - ( 2 x. u ) ) ) )
94	93	elrab 2916	. . . . . . . . . . . . . . . . . . 19 |- ( v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } <-> ( v e. S /\ ( 1st ` v ) = ( P - ( 2 x. u ) ) ) )
95	94	simprbi 275	. . . . . . . . . . . . . . . . . 18 |- ( v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } -> ( 1st ` v ) = ( P - ( 2 x. u ) ) )
96	95	ad2antll 491	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( 1st ` v ) = ( P - ( 2 x. u ) ) )
97	96	oveq2d 5934	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( P - ( 1st ` v ) ) = ( P - ( P - ( 2 x. u ) ) ) )
98	19	nncnd 8996	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. CC )
99	98	adantrr 479	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> P e. CC )
100	26	zcnd 9440	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) e. CC )
101	100	adantrr 479	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( 2 x. u ) e. CC )
102	99, 101	nncand 8335	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( P - ( P - ( 2 x. u ) ) ) = ( 2 x. u ) )
103	97, 102	eqtrd 2226	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( P - ( 1st ` v ) ) = ( 2 x. u ) )
104	103	oveq1d 5933	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( ( P - ( 1st ` v ) ) / 2 ) = ( ( 2 x. u ) / 2 ) )
105	24	zcnd 9440	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u e. CC )
106	105	adantrr 479	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> u e. CC )
107		2cnd 9055	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> 2 e. CC )
108		2ap0 9075	. . . . . . . . . . . . . . . 16 |- 2 # 0
109	108	a1i 9	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> 2 # 0 )
110	106, 107, 109	divcanap3d 8814	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( ( 2 x. u ) / 2 ) = u )
111	104, 110	eqtrd 2226	. . . . . . . . . . . . 13 |- ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( ( P - ( 1st ` v ) ) / 2 ) = u )
112	111	ralrimivva 2576	. . . . . . . . . . . 12 |- ( ph -> A. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) A. v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ( ( P - ( 1st ` v ) ) / 2 ) = u )
113		invdisj 4023	. . . . . . . . . . . 12 |- ( A. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) A. v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ( ( P - ( 1st ` v ) ) / 2 ) = u -> Disj u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } )
114	112, 113	syl 14	. . . . . . . . . . 11 |- ( ph -> Disj u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } )
115	14, 92, 114	hashiun 11621	. . . . . . . . . 10 |- ( ph -> (♯ ` U_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) = sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) (♯ ` { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) )
116		iunrab 3960	. . . . . . . . . . . 12 |- U_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } = { z e. S | E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) }
117		eldifsni 3747	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( P e. ( Prime \ { 2 } ) -> P =/= 2 )
118	5, 117	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> P =/= 2 )
119	118	necomd 2450	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 2 =/= P )
120	119	neneqd 2385	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> -. 2 = P )
121	120	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> -. 2 = P )
122		uzid 9606	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
123	22, 122	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. ( ZZ>= ` 2 )
124	5	eldifad 3164	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> P e. Prime )
125	124	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. Prime )
126		dvdsprm 12275	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( 2 || P <-> 2 = P ) )
127	123, 125, 126	sylancr 414	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 || P <-> 2 = P ) )
128	121, 127	mtbird 674	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> -. 2 || P )
129	18	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. NN )
130	129	nncnd 8996	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. CC )
131	26	adantlr 477	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) e. ZZ )
132	131	zcnd 9440	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) e. CC )
133	130, 132	npcand 8334	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) = P )
134	133	breq2d 4041	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 || ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) <-> 2 || P ) )
135	128, 134	mtbird 674	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> -. 2 || ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) )
136	23	adantl 277	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u e. ZZ )
137		dvdsmul1 11956	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 e. ZZ /\ u e. ZZ ) -> 2 || ( 2 x. u ) )
138	22, 136, 137	sylancr 414	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 2 || ( 2 x. u ) )
139	22	a1i 9	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 2 e. ZZ )
140	129	nnzd 9438	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. ZZ )
141	140, 131	zsubcld 9444	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - ( 2 x. u ) ) e. ZZ )
142		dvds2add 11968	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 e. ZZ /\ ( P - ( 2 x. u ) ) e. ZZ /\ ( 2 x. u ) e. ZZ ) -> ( ( 2 || ( P - ( 2 x. u ) ) /\ 2 || ( 2 x. u ) ) -> 2 || ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) ) )
143	139, 141, 131, 142	syl3anc 1249	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 || ( P - ( 2 x. u ) ) /\ 2 || ( 2 x. u ) ) -> 2 || ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) ) )
144	138, 143	mpan2d 428	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 || ( P - ( 2 x. u ) ) -> 2 || ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) ) )
145	135, 144	mtod 664	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> -. 2 || ( P - ( 2 x. u ) ) )
146		breq2 4033	. . . . . . . . . . . . . . . . 17 |- ( ( 1st ` z ) = ( P - ( 2 x. u ) ) -> ( 2 || ( 1st ` z ) <-> 2 || ( P - ( 2 x. u ) ) ) )
147	146	notbid 668	. . . . . . . . . . . . . . . 16 |- ( ( 1st ` z ) = ( P - ( 2 x. u ) ) -> ( -. 2 || ( 1st ` z ) <-> -. 2 || ( P - ( 2 x. u ) ) ) )
148	145, 147	syl5ibrcom 157	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 1st ` z ) = ( P - ( 2 x. u ) ) -> -. 2 || ( 1st ` z ) ) )
149	148	rexlimdva 2611	. . . . . . . . . . . . . 14 |- ( ( ph /\ z e. S ) -> ( E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) -> -. 2 || ( 1st ` z ) ) )
150		simpr 110	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. S ) -> z e. S )
151	56, 150	sselid 3177	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. S ) -> z e. ( ( 1 ... M ) X. ( 1 ... N ) ) )
152	151, 58	syl 14	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. S ) -> ( 1st ` z ) e. ( 1 ... M ) )
153		elfzelz 10091	. . . . . . . . . . . . . . . 16 |- ( ( 1st ` z ) e. ( 1 ... M ) -> ( 1st ` z ) e. ZZ )
154		odd2np1 12014	. . . . . . . . . . . . . . . 16 |- ( ( 1st ` z ) e. ZZ -> ( -. 2 || ( 1st ` z ) <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) )
155	152, 153, 154	3syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. S ) -> ( -. 2 || ( 1st ` z ) <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) )
156	11	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M / 2 ) e. QQ )
157	156	flqcld 10346	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( |_ ` ( M / 2 ) ) e. ZZ )
158	157	peano2zd 9442	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( |_ ` ( M / 2 ) ) + 1 ) e. ZZ )
159	7	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> M e. NN )
160	159	nnzd 9438	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> M e. ZZ )
161		simprl 529	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> n e. ZZ )
162	160, 161	zsubcld 9444	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M - n ) e. ZZ )
163	157	zred 9439	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( |_ ` ( M / 2 ) ) e. RR )
164	7	nnred 8995	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> M e. RR )
165	164	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> M e. RR )
166	165	rehalfcld 9229	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M / 2 ) e. RR )
167	162	zred 9439	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M - n ) e. RR )
168		flqle 10347	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( M / 2 ) e. QQ -> ( |_ ` ( M / 2 ) ) <_ ( M / 2 ) )
169	156, 168	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( |_ ` ( M / 2 ) ) <_ ( M / 2 ) )
170		zre 9321	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. ZZ -> n e. RR )
171	170	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> n e. RR )
172		simprr 531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) + 1 ) = ( 1st ` z ) )
173	152	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 1st ` z ) e. ( 1 ... M ) )
174	172, 173	eqeltrd 2270	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) + 1 ) e. ( 1 ... M ) )
175		elfzle2 10094	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 2 x. n ) + 1 ) e. ( 1 ... M ) -> ( ( 2 x. n ) + 1 ) <_ M )
176	174, 175	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) + 1 ) <_ M )
177		zmulcl 9370	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 2 e. ZZ /\ n e. ZZ ) -> ( 2 x. n ) e. ZZ )
178	22, 161, 177	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. n ) e. ZZ )
179		zltp1le 9371	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 2 x. n ) e. ZZ /\ M e. ZZ ) -> ( ( 2 x. n ) < M <-> ( ( 2 x. n ) + 1 ) <_ M ) )
180	178, 160, 179	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) < M <-> ( ( 2 x. n ) + 1 ) <_ M ) )
181	176, 180	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. n ) < M )
182		2re 9052	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 2 e. RR
183	182	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 2 e. RR )
184		2pos 9073	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 0 < 2
185	184	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 0 < 2 )
186		ltmuldiv2 8894	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( n e. RR /\ M e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. n ) < M <-> n < ( M / 2 ) ) )
187	171, 165, 183, 185, 186	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) < M <-> n < ( M / 2 ) ) )
188	181, 187	mpbid 147	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> n < ( M / 2 ) )
189	166	recnd 8048	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M / 2 ) e. CC )
190	7	nncnd 8996	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> M e. CC )
191	190	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> M e. CC )
192	191	2halvesd 9228	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( M / 2 ) + ( M / 2 ) ) = M )
193	189, 189, 192	mvlraddd 8383	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M / 2 ) = ( M - ( M / 2 ) ) )
194	188, 193	breqtrd 4055	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> n < ( M - ( M / 2 ) ) )
195	171, 165, 166, 194	ltsub13d 8570	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M / 2 ) < ( M - n ) )
196	163, 166, 167, 169, 195	lelttrd 8144	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( |_ ` ( M / 2 ) ) < ( M - n ) )
197		zltp1le 9371	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( |_ ` ( M / 2 ) ) e. ZZ /\ ( M - n ) e. ZZ ) -> ( ( |_ ` ( M / 2 ) ) < ( M - n ) <-> ( ( |_ ` ( M / 2 ) ) + 1 ) <_ ( M - n ) ) )
198	157, 162, 197	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( |_ ` ( M / 2 ) ) < ( M - n ) <-> ( ( |_ ` ( M / 2 ) ) + 1 ) <_ ( M - n ) ) )
199	196, 198	mpbid 147	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( |_ ` ( M / 2 ) ) + 1 ) <_ ( M - n ) )
200		2t0e0 9141	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 x. 0 ) = 0
201		2cn 9053	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 2 e. CC
202		zcn 9322	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( n e. ZZ -> n e. CC )
203	202	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> n e. CC )
204		mulcl 7999	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 2 e. CC /\ n e. CC ) -> ( 2 x. n ) e. CC )
205	201, 203, 204	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. n ) e. CC )
206		pncan 8225	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 2 x. n ) e. CC /\ 1 e. CC ) -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
207	205, 77, 206	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
208		elfznn 10120	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 2 x. n ) + 1 ) e. ( 1 ... M ) -> ( ( 2 x. n ) + 1 ) e. NN )
209		nnm1nn0 9281	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 2 x. n ) + 1 ) e. NN -> ( ( ( 2 x. n ) + 1 ) - 1 ) e. NN0 )
210	174, 208, 209	3syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( ( 2 x. n ) + 1 ) - 1 ) e. NN0 )
211	207, 210	eqeltrrd 2271	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. n ) e. NN0 )
212	211	nn0ge0d 9296	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 0 <_ ( 2 x. n ) )
213	200, 212	eqbrtrid 4064	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. 0 ) <_ ( 2 x. n ) )
214		0red 8020	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 0 e. RR )
215		lemul2 8876	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 0 e. RR /\ n e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 0 <_ n <-> ( 2 x. 0 ) <_ ( 2 x. n ) ) )
216	214, 171, 183, 185, 215	syl112anc 1253	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 0 <_ n <-> ( 2 x. 0 ) <_ ( 2 x. n ) ) )
217	213, 216	mpbird 167	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 0 <_ n )
218	165, 171	subge02d 8556	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 0 <_ n <-> ( M - n ) <_ M ) )
219	217, 218	mpbid 147	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M - n ) <_ M )
220	158, 160, 162, 199, 219	elfzd 10082	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M - n ) e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) )
221	124	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> P e. Prime )
222		prmnn 12248	. . . . . . . . . . . . . . . . . . . . 21 |- ( P e. Prime -> P e. NN )
223	221, 222	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> P e. NN )
224	223	nncnd 8996	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> P e. CC )
225		peano2cn 8154	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 x. n ) e. CC -> ( ( 2 x. n ) + 1 ) e. CC )
226	205, 225	syl 14	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) + 1 ) e. CC )
227	224, 226	nncand 8335	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( P - ( P - ( ( 2 x. n ) + 1 ) ) ) = ( ( 2 x. n ) + 1 ) )
228		1cnd 8035	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 1 e. CC )
229	224, 205, 228	sub32d 8362	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( P - ( 2 x. n ) ) - 1 ) = ( ( P - 1 ) - ( 2 x. n ) ) )
230	224, 205, 228	subsub4d 8361	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( P - ( 2 x. n ) ) - 1 ) = ( P - ( ( 2 x. n ) + 1 ) ) )
231		2cnd 9055	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 2 e. CC )
232	231, 191, 203	subdid 8433	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. ( M - n ) ) = ( ( 2 x. M ) - ( 2 x. n ) ) )
233	6	oveq2i 5929	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 2 x. M ) = ( 2 x. ( ( P - 1 ) / 2 ) )
234	18	nnzd 9438	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> P e. ZZ )
235	234	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> P e. ZZ )
236		peano2zm 9355	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( P e. ZZ -> ( P - 1 ) e. ZZ )
237	235, 236	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( P - 1 ) e. ZZ )
238	237	zcnd 9440	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( P - 1 ) e. CC )
239	183, 185	gt0ap0d 8648	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 2 # 0 )
240	238, 231, 239	divcanap2d 8811	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. ( ( P - 1 ) / 2 ) ) = ( P - 1 ) )
241	233, 240	eqtrid 2238	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. M ) = ( P - 1 ) )
242	241	oveq1d 5933	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. M ) - ( 2 x. n ) ) = ( ( P - 1 ) - ( 2 x. n ) ) )
243	232, 242	eqtr2d 2227	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( P - 1 ) - ( 2 x. n ) ) = ( 2 x. ( M - n ) ) )
244	229, 230, 243	3eqtr3d 2234	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( P - ( ( 2 x. n ) + 1 ) ) = ( 2 x. ( M - n ) ) )
245	244	oveq2d 5934	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( P - ( P - ( ( 2 x. n ) + 1 ) ) ) = ( P - ( 2 x. ( M - n ) ) ) )
246	227, 245, 172	3eqtr3rd 2235	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 1st ` z ) = ( P - ( 2 x. ( M - n ) ) ) )
247		oveq2 5926	. . . . . . . . . . . . . . . . . . 19 |- ( u = ( M - n ) -> ( 2 x. u ) = ( 2 x. ( M - n ) ) )
248	247	oveq2d 5934	. . . . . . . . . . . . . . . . . 18 |- ( u = ( M - n ) -> ( P - ( 2 x. u ) ) = ( P - ( 2 x. ( M - n ) ) ) )
249	248	rspceeqv 2882	. . . . . . . . . . . . . . . . 17 |- ( ( ( M - n ) e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ ( 1st ` z ) = ( P - ( 2 x. ( M - n ) ) ) ) -> E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) )
250	220, 246, 249	syl2anc 411	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) )
251	250	rexlimdvaa 2612	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. S ) -> ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) -> E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) ) )
252	155, 251	sylbid 150	. . . . . . . . . . . . . 14 |- ( ( ph /\ z e. S ) -> ( -. 2 || ( 1st ` z ) -> E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) ) )
253	149, 252	impbid 129	. . . . . . . . . . . . 13 |- ( ( ph /\ z e. S ) -> ( E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) <-> -. 2 || ( 1st ` z ) ) )
254	253	rabbidva 2748	. . . . . . . . . . . 12 |- ( ph -> { z e. S | E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) } = { z e. S | -. 2 || ( 1st ` z ) } )
255	116, 254	eqtrid 2238	. . . . . . . . . . 11 |- ( ph -> U_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } = { z e. S | -. 2 || ( 1st ` z ) } )
256	255	fveq2d 5558	. . . . . . . . . 10 |- ( ph -> (♯ ` U_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) = (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) )
257		ssrab2 3264	. . . . . . . . . . . . . . 15 |- { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } C_ S
258	34	relopabiv 4785	. . . . . . . . . . . . . . 15 |- Rel S
259		relss 4746	. . . . . . . . . . . . . . 15 |- ( { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } C_ S -> ( Rel S -> Rel { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) )
260	257, 258, 259	mp2 16	. . . . . . . . . . . . . 14 |- Rel { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) }
261		relxp 4768	. . . . . . . . . . . . . 14 |- Rel ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
262	34	eleq2i 2260	. . . . . . . . . . . . . . . . . 18 |- ( <. x , y >. e. S <-> <. x , y >. e. { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } )
263		opabidw 4287	. . . . . . . . . . . . . . . . . 18 |- ( <. x , y >. e. { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } <-> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) )
264	262, 263	bitri 184	. . . . . . . . . . . . . . . . 17 |- ( <. x , y >. e. S <-> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) )
265		anass 401	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. NN /\ y <_ N ) /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) <-> ( y e. NN /\ ( y <_ N /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) ) )
266	31	peano2zd 9442	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) e. ZZ )
267	266	zred 9439	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) e. RR )
268	267	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) e. RR )
269	16	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> Q e. RR )
270	269	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> Q e. RR )
271		nnre 8989	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. NN -> y e. RR )
272	271	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> y e. RR )
273		lesub 8460	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) e. RR /\ Q e. RR /\ y e. RR ) -> ( ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) <_ ( Q - y ) <-> y <_ ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) ) )
274	268, 270, 272, 273	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) <_ ( Q - y ) <-> y <_ ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) ) )
275	269	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> Q e. RR )
276	275	recnd 8048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> Q e. CC )
277	98, 276	mulcomd 8041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P x. Q ) = ( Q x. P ) )
278	100, 276	mulcomd 8041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. u ) x. Q ) = ( Q x. ( 2 x. u ) ) )
279	19	nnap0d 9028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P # 0 )
280	276, 98, 279	divcanap1d 8810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / P ) x. P ) = Q )
281	280	oveq1d 5933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( Q / P ) x. P ) x. ( 2 x. u ) ) = ( Q x. ( 2 x. u ) ) )
282	269, 18	nndivred 9032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> ( Q / P ) e. RR )
283	282	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q / P ) e. RR )
284	283	recnd 8048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q / P ) e. CC )
285	284, 98, 100	mul32d 8172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( Q / P ) x. P ) x. ( 2 x. u ) ) = ( ( ( Q / P ) x. ( 2 x. u ) ) x. P ) )
286	278, 281, 285	3eqtr2d 2232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. u ) x. Q ) = ( ( ( Q / P ) x. ( 2 x. u ) ) x. P ) )
287	277, 286	oveq12d 5936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P x. Q ) - ( ( 2 x. u ) x. Q ) ) = ( ( Q x. P ) - ( ( ( Q / P ) x. ( 2 x. u ) ) x. P ) ) )
288	98, 100, 276	subdird 8434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) x. Q ) = ( ( P x. Q ) - ( ( 2 x. u ) x. Q ) ) )
289	26	zred 9439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) e. RR )
290	283, 289	remulcld 8050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / P ) x. ( 2 x. u ) ) e. RR )
291	290	recnd 8048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / P ) x. ( 2 x. u ) ) e. CC )
292	276, 291, 98	subdird 8434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) = ( ( Q x. P ) - ( ( ( Q / P ) x. ( 2 x. u ) ) x. P ) ) )
293	287, 288, 292	3eqtr4d 2236	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) x. Q ) = ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) )
294	293	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( P - ( 2 x. u ) ) x. Q ) = ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) )
295	294	breq2d 4041	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) <-> ( y x. P ) < ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) ) )
296	290	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( Q / P ) x. ( 2 x. u ) ) e. RR )
297	270, 296	resubcld 8400	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) e. RR )
298	19	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> P e. NN )
299	298	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> P e. RR )
300	298	nngt0d 9026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> 0 < P )
301		ltmul1 8611	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( y e. RR /\ ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( y < ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) <-> ( y x. P ) < ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) ) )
302	272, 297, 299, 300, 301	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( y < ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) <-> ( y x. P ) < ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) ) )
303		ltsub13 8462	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( y e. RR /\ Q e. RR /\ ( ( Q / P ) x. ( 2 x. u ) ) e. RR ) -> ( y < ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) <-> ( ( Q / P ) x. ( 2 x. u ) ) < ( Q - y ) ) )
304	272, 270, 296, 303	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( y < ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) <-> ( ( Q / P ) x. ( 2 x. u ) ) < ( Q - y ) ) )
305	295, 302, 304	3bitr2d 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) <-> ( ( Q / P ) x. ( 2 x. u ) ) < ( Q - y ) ) )
306	16	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> Q e. NN )
307	306	nnzd 9438	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> Q e. ZZ )
308		nnz 9336	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y e. NN -> y e. ZZ )
309		zsubcl 9358	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( Q e. ZZ /\ y e. ZZ ) -> ( Q - y ) e. ZZ )
310	307, 308, 309	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( Q - y ) e. ZZ )
311		flqlt 10352	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( Q / P ) x. ( 2 x. u ) ) e. QQ /\ ( Q - y ) e. ZZ ) -> ( ( ( Q / P ) x. ( 2 x. u ) ) < ( Q - y ) <-> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < ( Q - y ) ) )
312	30, 310, 311	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( ( Q / P ) x. ( 2 x. u ) ) < ( Q - y ) <-> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < ( Q - y ) ) )
313		zltp1le 9371	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ /\ ( Q - y ) e. ZZ ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < ( Q - y ) <-> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) <_ ( Q - y ) ) )
314	31, 310, 313	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < ( Q - y ) <-> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) <_ ( Q - y ) ) )
315	305, 312, 314	3bitrd 214	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) <-> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) <_ ( Q - y ) ) )
316	37	oveq2i 5929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( 2 x. N ) = ( 2 x. ( ( Q - 1 ) / 2 ) )
317		peano2rem 8286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( Q e. RR -> ( Q - 1 ) e. RR )
318	275, 317	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q - 1 ) e. RR )
319	318	recnd 8048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q - 1 ) e. CC )
320		2cnd 9055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 2 e. CC )
321	108	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 2 # 0 )
322	319, 320, 321	divcanap2d 8811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. ( ( Q - 1 ) / 2 ) ) = ( Q - 1 ) )
323	316, 322	eqtrid 2238	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) = ( Q - 1 ) )
324	323	oveq1d 5933	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( ( Q - 1 ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
325		1cnd 8035	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 1 e. CC )
326	31	zcnd 9440	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. CC )
327	276, 325, 326	sub32d 8362	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q - 1 ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( ( Q - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) - 1 ) )
328	276, 326, 325	subsub4d 8361	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) - 1 ) = ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) )
329	324, 327, 328	3eqtrd 2230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) )
330	329	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) )
331	330	breq2d 4041	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <-> y <_ ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) ) )
332	274, 315, 331	3bitr4d 220	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) <-> y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
333	332	anbi2d 464	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y <_ N /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) <-> ( y <_ N /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
334		nnmulcl 9003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
335	9, 38, 334	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( 2 x. N ) e. NN )
336	335	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) e. NN )
337	336	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) e. RR )
338	38	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N e. NN )
339	338	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N e. RR )
340	31	zred 9439	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. RR )
341	38	nncnd 8996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> N e. CC )
342	341	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N e. CC )
343	342	2timesd 9225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) = ( N + N ) )
344	342, 342, 343	mvrladdd 8386	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - N ) = N )
345	275	rehalfcld 9229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q / 2 ) e. RR )
346	275	ltm1d 8951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q - 1 ) < Q )
347	182	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 2 e. RR )
348	184	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 0 < 2 )
349		ltdiv1 8887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( Q - 1 ) e. RR /\ Q e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( Q - 1 ) < Q <-> ( ( Q - 1 ) / 2 ) < ( Q / 2 ) ) )
350	318, 275, 347, 348, 349	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q - 1 ) < Q <-> ( ( Q - 1 ) / 2 ) < ( Q / 2 ) ) )
351	346, 350	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q - 1 ) / 2 ) < ( Q / 2 ) )
352	37, 351	eqbrtrid 4064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N < ( Q / 2 ) )
353	339, 345, 352	ltled 8138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N <_ ( Q / 2 ) )
354	276, 320, 98, 321	div32apd 8833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / 2 ) x. P ) = ( Q x. ( P / 2 ) ) )
355	164	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> M e. RR )
356	355	rehalfcld 9229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( M / 2 ) e. RR )
357	13	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( |_ ` ( M / 2 ) ) + 1 ) e. ZZ )
358	357	zred 9439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( |_ ` ( M / 2 ) ) + 1 ) e. RR )
359	24	zred 9439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u e. RR )
360	11	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( M / 2 ) e. QQ )
361		flqltp1 10348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( M / 2 ) e. QQ -> ( M / 2 ) < ( ( |_ ` ( M / 2 ) ) + 1 ) )
362	360, 361	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( M / 2 ) < ( ( |_ ` ( M / 2 ) ) + 1 ) )
363		elfzle1 10093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) -> ( ( |_ ` ( M / 2 ) ) + 1 ) <_ u )
364	363	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( |_ ` ( M / 2 ) ) + 1 ) <_ u )
365	356, 358, 359, 362, 364	ltletrd 8442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( M / 2 ) < u )
366		ltdivmul 8895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( M e. RR /\ u e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( M / 2 ) < u <-> M < ( 2 x. u ) ) )
367	355, 359, 347, 348, 366	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( M / 2 ) < u <-> M < ( 2 x. u ) ) )
368	365, 367	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> M < ( 2 x. u ) )
369	6, 368	eqbrtrrid 4065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - 1 ) / 2 ) < ( 2 x. u ) )
370	19	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. RR )
371		peano2rem 8286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( P e. RR -> ( P - 1 ) e. RR )
372	370, 371	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - 1 ) e. RR )
373		ltdivmul 8895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( P - 1 ) e. RR /\ ( 2 x. u ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( P - 1 ) / 2 ) < ( 2 x. u ) <-> ( P - 1 ) < ( 2 x. ( 2 x. u ) ) ) )
374	372, 289, 347, 348, 373	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( P - 1 ) / 2 ) < ( 2 x. u ) <-> ( P - 1 ) < ( 2 x. ( 2 x. u ) ) ) )
375	369, 374	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - 1 ) < ( 2 x. ( 2 x. u ) ) )
376		zmulcl 9370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( 2 e. ZZ /\ ( 2 x. u ) e. ZZ ) -> ( 2 x. ( 2 x. u ) ) e. ZZ )
377	22, 26, 376	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. ( 2 x. u ) ) e. ZZ )
378		zlem1lt 9373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( P e. ZZ /\ ( 2 x. ( 2 x. u ) ) e. ZZ ) -> ( P <_ ( 2 x. ( 2 x. u ) ) <-> ( P - 1 ) < ( 2 x. ( 2 x. u ) ) ) )
379	234, 377, 378	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P <_ ( 2 x. ( 2 x. u ) ) <-> ( P - 1 ) < ( 2 x. ( 2 x. u ) ) ) )
380	375, 379	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P <_ ( 2 x. ( 2 x. u ) ) )
381		ledivmul 8896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( P e. RR /\ ( 2 x. u ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( P / 2 ) <_ ( 2 x. u ) <-> P <_ ( 2 x. ( 2 x. u ) ) ) )
382	370, 289, 347, 348, 381	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P / 2 ) <_ ( 2 x. u ) <-> P <_ ( 2 x. ( 2 x. u ) ) ) )
383	380, 382	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P / 2 ) <_ ( 2 x. u ) )
384	370	rehalfcld 9229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P / 2 ) e. RR )
385	306	nngt0d 9026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 0 < Q )
386		lemul2 8876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( P / 2 ) e. RR /\ ( 2 x. u ) e. RR /\ ( Q e. RR /\ 0 < Q ) ) -> ( ( P / 2 ) <_ ( 2 x. u ) <-> ( Q x. ( P / 2 ) ) <_ ( Q x. ( 2 x. u ) ) ) )
387	384, 289, 275, 385, 386	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P / 2 ) <_ ( 2 x. u ) <-> ( Q x. ( P / 2 ) ) <_ ( Q x. ( 2 x. u ) ) ) )
388	383, 387	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q x. ( P / 2 ) ) <_ ( Q x. ( 2 x. u ) ) )
389	354, 388	eqbrtrd 4051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / 2 ) x. P ) <_ ( Q x. ( 2 x. u ) ) )
390	275, 289	remulcld 8050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q x. ( 2 x. u ) ) e. RR )
391	19	nngt0d 9026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 0 < P )
392		lemuldiv 8900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( Q / 2 ) e. RR /\ ( Q x. ( 2 x. u ) ) e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( ( ( Q / 2 ) x. P ) <_ ( Q x. ( 2 x. u ) ) <-> ( Q / 2 ) <_ ( ( Q x. ( 2 x. u ) ) / P ) ) )
393	345, 390, 370, 391, 392	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( Q / 2 ) x. P ) <_ ( Q x. ( 2 x. u ) ) <-> ( Q / 2 ) <_ ( ( Q x. ( 2 x. u ) ) / P ) ) )
394	389, 393	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q / 2 ) <_ ( ( Q x. ( 2 x. u ) ) / P ) )
395	276, 100, 98, 279	div23apd 8847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q x. ( 2 x. u ) ) / P ) = ( ( Q / P ) x. ( 2 x. u ) ) )
396	394, 395	breqtrd 4055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q / 2 ) <_ ( ( Q / P ) x. ( 2 x. u ) ) )
397	339, 345, 290, 353, 396	letrd 8143	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N <_ ( ( Q / P ) x. ( 2 x. u ) ) )
398	39	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N e. ZZ )
399		flqge 10351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( Q / P ) x. ( 2 x. u ) ) e. QQ /\ N e. ZZ ) -> ( N <_ ( ( Q / P ) x. ( 2 x. u ) ) <-> N <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
400	30, 398, 399	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( N <_ ( ( Q / P ) x. ( 2 x. u ) ) <-> N <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
401	397, 400	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) )
402	344, 401	eqbrtrd 4051	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - N ) <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) )
403	337, 339, 340, 402	subled 8567	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <_ N )
404	403	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <_ N )
405	336	nnzd 9438	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) e. ZZ )
406	405, 31	zsubcld 9444	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. ZZ )
407	406	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. ZZ )
408	407	zred 9439	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. RR )
409	38	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> N e. NN )
410	409	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> N e. RR )
411		letr 8102	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y e. RR /\ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. RR /\ N e. RR ) -> ( ( y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) /\ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <_ N ) -> y <_ N ) )
412	272, 408, 410, 411	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) /\ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <_ N ) -> y <_ N ) )
413	404, 412	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) -> y <_ N ) )
414	413	pm4.71rd 394	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <-> ( y <_ N /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
415	333, 414	bitr4d 191	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y <_ N /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) <-> y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
416	415	pm5.32da 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( y e. NN /\ ( y <_ N /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) ) <-> ( y e. NN /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
417	416	adantr 276	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( y e. NN /\ ( y <_ N /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) ) <-> ( y e. NN /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
418	265, 417	bitrid 192	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( ( y e. NN /\ y <_ N ) /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) <-> ( y e. NN /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
419		simpr 110	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> x = ( P - ( 2 x. u ) ) )
420	234	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. ZZ )
421	420, 26	zsubcld 9444	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - ( 2 x. u ) ) e. ZZ )
422		elfzle2 10094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) -> u <_ M )
423	422	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u <_ M )
424	423, 6	breqtrdi 4070	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u <_ ( ( P - 1 ) / 2 ) )
425		lemuldiv2 8901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( u e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. u ) <_ ( P - 1 ) <-> u <_ ( ( P - 1 ) / 2 ) ) )
426	359, 372, 347, 348, 425	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. u ) <_ ( P - 1 ) <-> u <_ ( ( P - 1 ) / 2 ) ) )
427	424, 426	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) <_ ( P - 1 ) )
428	370	ltm1d 8951	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - 1 ) < P )
429	289, 372, 370, 427, 428	lelttrd 8144	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) < P )
430	289, 370	posdifd 8551	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. u ) < P <-> 0 < ( P - ( 2 x. u ) ) ) )
431	429, 430	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 0 < ( P - ( 2 x. u ) ) )
432		elnnz 9327	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( P - ( 2 x. u ) ) e. NN <-> ( ( P - ( 2 x. u ) ) e. ZZ /\ 0 < ( P - ( 2 x. u ) ) ) )
433	421, 431, 432	sylanbrc 417	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - ( 2 x. u ) ) e. NN )
434	98, 100, 325	sub32d 8362	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) - 1 ) = ( ( P - 1 ) - ( 2 x. u ) ) )
435	6, 6	oveq12i 5930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( M + M ) = ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) )
436	87, 236	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - 1 ) e. ZZ )
437	436	zcnd 9440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - 1 ) e. CC )
438	437	2halvesd 9228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) ) = ( P - 1 ) )
439	435, 438	eqtrid 2238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( M + M ) = ( P - 1 ) )
440	439	oveq1d 5933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( M + M ) - M ) = ( ( P - 1 ) - M ) )
441	190	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> M e. CC )
442	441, 441	pncan2d 8332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( M + M ) - M ) = M )
443	440, 442	eqtr3d 2228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - 1 ) - M ) = M )
444	443, 368	eqbrtrd 4051	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - 1 ) - M ) < ( 2 x. u ) )
445	372, 355, 289, 444	ltsub23d 8569	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - 1 ) - ( 2 x. u ) ) < M )
446	434, 445	eqbrtrd 4051	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) - 1 ) < M )
447	7	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> M e. NN )
448	447	nnzd 9438	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> M e. ZZ )
449		zlem1lt 9373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( P - ( 2 x. u ) ) e. ZZ /\ M e. ZZ ) -> ( ( P - ( 2 x. u ) ) <_ M <-> ( ( P - ( 2 x. u ) ) - 1 ) < M ) )
450	421, 448, 449	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) <_ M <-> ( ( P - ( 2 x. u ) ) - 1 ) < M ) )
451	446, 450	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - ( 2 x. u ) ) <_ M )
452		fznn 10155	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( M e. ZZ -> ( ( P - ( 2 x. u ) ) e. ( 1 ... M ) <-> ( ( P - ( 2 x. u ) ) e. NN /\ ( P - ( 2 x. u ) ) <_ M ) ) )
453	448, 452	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) e. ( 1 ... M ) <-> ( ( P - ( 2 x. u ) ) e. NN /\ ( P - ( 2 x. u ) ) <_ M ) ) )
454	433, 451, 453	mpbir2and 946	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - ( 2 x. u ) ) e. ( 1 ... M ) )
455	454	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( P - ( 2 x. u ) ) e. ( 1 ... M ) )
456	419, 455	eqeltrd 2270	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> x e. ( 1 ... M ) )
457	456	biantrurd 305	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( y e. ( 1 ... N ) <-> ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) )
458	39	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> N e. ZZ )
459		fznn 10155	. . . . . . . . . . . . . . . . . . . . 21 |- ( N e. ZZ -> ( y e. ( 1 ... N ) <-> ( y e. NN /\ y <_ N ) ) )
460	458, 459	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( y e. ( 1 ... N ) <-> ( y e. NN /\ y <_ N ) ) )
461	457, 460	bitr3d 190	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) <-> ( y e. NN /\ y <_ N ) ) )
462	419	oveq1d 5933	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( x x. Q ) = ( ( P - ( 2 x. u ) ) x. Q ) )
463	462	breq2d 4041	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( y x. P ) < ( x x. Q ) <-> ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) )
464	461, 463	anbi12d 473	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) <-> ( ( y e. NN /\ y <_ N ) /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) ) )
465	406	adantr 276	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. ZZ )
466		fznn 10155	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. ZZ -> ( y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) <-> ( y e. NN /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
467	465, 466	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) <-> ( y e. NN /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
468	418, 464, 467	3bitr4d 220	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) <-> y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
469	264, 468	bitrid 192	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( <. x , y >. e. S <-> y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
470	469	pm5.32da 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( x = ( P - ( 2 x. u ) ) /\ <. x , y >. e. S ) <-> ( x = ( P - ( 2 x. u ) ) /\ y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ) )
471		vex 2763	. . . . . . . . . . . . . . . . . . 19 |- x e. _V
472		vex 2763	. . . . . . . . . . . . . . . . . . 19 |- y e. _V
473	471, 472	op1std 6201	. . . . . . . . . . . . . . . . . 18 |- ( z = <. x , y >. -> ( 1st ` z ) = x )
474	473	eqeq1d 2202	. . . . . . . . . . . . . . . . 17 |- ( z = <. x , y >. -> ( ( 1st ` z ) = ( P - ( 2 x. u ) ) <-> x = ( P - ( 2 x. u ) ) ) )
475	474	elrab 2916	. . . . . . . . . . . . . . . 16 |- ( <. x , y >. e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } <-> ( <. x , y >. e. S /\ x = ( P - ( 2 x. u ) ) ) )
476	475	biancomi 270	. . . . . . . . . . . . . . 15 |- ( <. x , y >. e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } <-> ( x = ( P - ( 2 x. u ) ) /\ <. x , y >. e. S ) )
477		opelxp 4689	. . . . . . . . . . . . . . . 16 |- ( <. x , y >. e. ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) <-> ( x e. { ( P - ( 2 x. u ) ) } /\ y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
478		velsn 3635	. . . . . . . . . . . . . . . . 17 |- ( x e. { ( P - ( 2 x. u ) ) } <-> x = ( P - ( 2 x. u ) ) )
479	478	anbi1i 458	. . . . . . . . . . . . . . . 16 |- ( ( x e. { ( P - ( 2 x. u ) ) } /\ y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) <-> ( x = ( P - ( 2 x. u ) ) /\ y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
480	477, 479	bitri 184	. . . . . . . . . . . . . . 15 |- ( <. x , y >. e. ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) <-> ( x = ( P - ( 2 x. u ) ) /\ y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
481	470, 476, 480	3bitr4g 223	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( <. x , y >. e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } <-> <. x , y >. e. ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ) )
482	260, 261, 481	eqrelrdv 4755	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } = ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
483	482	fveq2d 5558	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> (♯ ` { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) = (♯ ` ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ) )
484		1zzd 9344	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 1 e. ZZ )
485	484, 406	fzfigd 10502	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) e. Fin )
486		xpsnen2g 6883	. . . . . . . . . . . . . 14 |- ( ( ( P - ( 2 x. u ) ) e. ZZ /\ ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) e. Fin ) -> ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ~~ ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
487	421, 485, 486	syl2anc 411	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ~~ ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
488	482, 92	eqeltrrd 2271	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) e. Fin )
489		hashen 10855	. . . . . . . . . . . . . 14 |- ( ( ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) e. Fin /\ ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) e. Fin ) -> ( (♯ ` ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ) = (♯ ` ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) <-> ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ~~ ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
490	488, 485, 489	syl2anc 411	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( (♯ ` ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ) = (♯ ` ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) <-> ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ~~ ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
491	487, 490	mpbird 167	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> (♯ ` ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ) = (♯ ` ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
492		ltmul2 8875	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 2 x. u ) e. RR /\ P e. RR /\ ( Q e. RR /\ 0 < Q ) ) -> ( ( 2 x. u ) < P <-> ( Q x. ( 2 x. u ) ) < ( Q x. P ) ) )
493	289, 370, 275, 385, 492	syl112anc 1253	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. u ) < P <-> ( Q x. ( 2 x. u ) ) < ( Q x. P ) ) )
494	429, 493	mpbid 147	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q x. ( 2 x. u ) ) < ( Q x. P ) )
495		ltdivmul2 8897	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Q x. ( 2 x. u ) ) e. RR /\ Q e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( ( ( Q x. ( 2 x. u ) ) / P ) < Q <-> ( Q x. ( 2 x. u ) ) < ( Q x. P ) ) )
496	390, 275, 370, 391, 495	syl112anc 1253	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( Q x. ( 2 x. u ) ) / P ) < Q <-> ( Q x. ( 2 x. u ) ) < ( Q x. P ) ) )
497	494, 496	mpbird 167	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q x. ( 2 x. u ) ) / P ) < Q )
498	395, 497	eqbrtrrd 4053	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / P ) x. ( 2 x. u ) ) < Q )
499		flqlt 10352	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( Q / P ) x. ( 2 x. u ) ) e. QQ /\ Q e. ZZ ) -> ( ( ( Q / P ) x. ( 2 x. u ) ) < Q <-> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < Q ) )
500	30, 307, 499	syl2anc 411	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( Q / P ) x. ( 2 x. u ) ) < Q <-> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < Q ) )
501	498, 500	mpbid 147	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < Q )
502		zltlem1 9374	. . . . . . . . . . . . . . . . 17 |- ( ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ /\ Q e. ZZ ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < Q <-> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) <_ ( Q - 1 ) ) )
503	31, 307, 502	syl2anc 411	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < Q <-> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) <_ ( Q - 1 ) ) )
504	501, 503	mpbid 147	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) <_ ( Q - 1 ) )
505	504, 323	breqtrrd 4057	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) <_ ( 2 x. N ) )
506		eluz2 9598	. . . . . . . . . . . . . 14 |- ( ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <-> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ /\ ( 2 x. N ) e. ZZ /\ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) <_ ( 2 x. N ) ) )
507	31, 405, 505, 506	syl3anbrc 1183	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
508		uznn0sub 9624	. . . . . . . . . . . . 13 |- ( ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. NN0 )
509		hashfz1 10854	. . . . . . . . . . . . 13 |- ( ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. NN0 -> (♯ ` ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) = ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
510	507, 508, 509	3syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> (♯ ` ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) = ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
511	483, 491, 510	3eqtrd 2230	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> (♯ ` { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) = ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
512	511	sumeq2dv 11511	. . . . . . . . . 10 |- ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) (♯ ` { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) = sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
513	115, 256, 512	3eqtr3rd 2235	. . . . . . . . 9 |- ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) )
514	335	nncnd 8996	. . . . . . . . . . 11 |- ( ph -> ( 2 x. N ) e. CC )
515	514	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) e. CC )
516	14, 515, 326	fsumsub 11595	. . . . . . . . 9 |- ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) - sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
517	513, 516	eqtr3d 2228	. . . . . . . 8 |- ( ph -> (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) = ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) - sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
518	517	oveq2d 5934	. . . . . . 7 |- ( ph -> ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) - sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
519	32	zcnd 9440	. . . . . . . 8 |- ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. CC )
520	14, 405	fsumzcl 11545	. . . . . . . . 9 |- ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) e. ZZ )
521	520	zcnd 9440	. . . . . . . 8 |- ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) e. CC )
522	519, 521	pncan3d 8333	. . . . . . 7 |- ( ph -> ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) - sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) = sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) )
523		fsumconst 11597	. . . . . . . . 9 |- ( ( ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) e. Fin /\ ( 2 x. N ) e. CC ) -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) = ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. ( 2 x. N ) ) )
524	14, 514, 523	syl2anc 411	. . . . . . . 8 |- ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) = ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. ( 2 x. N ) ) )
525		hashcl 10852	. . . . . . . . . . 11 |- ( ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) e. Fin -> (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) e. NN0 )
526	14, 525	syl 14	. . . . . . . . . 10 |- ( ph -> (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) e. NN0 )
527	526	nn0cnd 9295	. . . . . . . . 9 |- ( ph -> (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) e. CC )
528		2cnd 9055	. . . . . . . . 9 |- ( ph -> 2 e. CC )
529	527, 528, 341	mul12d 8171	. . . . . . . 8 |- ( ph -> ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. ( 2 x. N ) ) = ( 2 x. ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) )
530	524, 529	eqtrd 2226	. . . . . . 7 |- ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) = ( 2 x. ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) )
531	518, 522, 530	3eqtrd 2230	. . . . . 6 |- ( ph -> ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( 2 x. ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) )
532	531	oveq2d 5934	. . . . 5 |- ( ph -> ( -u 1 ^ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( -u 1 ^ ( 2 x. ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) ) )
533	22	a1i 9	. . . . . 6 |- ( ph -> 2 e. ZZ )
534	526	nn0zd 9437	. . . . . . 7 |- ( ph -> (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) e. ZZ )
535	534, 39	zmulcld 9445	. . . . . 6 |- ( ph -> ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) e. ZZ )
536		expmulzap 10656	. . . . . 6 |- ( ( ( -u 1 e. CC /\ -u 1 # 0 ) /\ ( 2 e. ZZ /\ ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) e. ZZ ) ) -> ( -u 1 ^ ( 2 x. ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) ) = ( ( -u 1 ^ 2 ) ^ ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) )
537	2, 4, 533, 535, 536	syl22anc 1250	. . . . 5 |- ( ph -> ( -u 1 ^ ( 2 x. ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) ) = ( ( -u 1 ^ 2 ) ^ ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) )
538		neg1sqe1 10705	. . . . . . 7 |- ( -u 1 ^ 2 ) = 1
539	538	oveq1i 5928	. . . . . 6 |- ( ( -u 1 ^ 2 ) ^ ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) = ( 1 ^ ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) )
540		1exp 10639	. . . . . . 7 |- ( ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) e. ZZ -> ( 1 ^ ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) = 1 )
541	535, 540	syl 14	. . . . . 6 |- ( ph -> ( 1 ^ ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) = 1 )
542	539, 541	eqtrid 2238	. . . . 5 |- ( ph -> ( ( -u 1 ^ 2 ) ^ ( (♯ ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) = 1 )
543	532, 537, 542	3eqtrd 2230	. . . 4 |- ( ph -> ( -u 1 ^ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = 1 )
544	74, 85, 543	3eqtr4d 2236	. . 3 |- ( ph -> ( ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) x. ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( -u 1 ^ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
545		expaddzap 10654	. . . 4 |- ( ( ( -u 1 e. CC /\ -u 1 # 0 ) /\ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ /\ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) e. ZZ ) ) -> ( -u 1 ^ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) x. ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
546	2, 4, 32, 72, 545	syl22anc 1250	. . 3 |- ( ph -> ( -u 1 ^ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) x. ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
547	544, 546	eqtr2d 2227	. 2 |- ( ph -> ( ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) x. ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) x. ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
548	33, 71, 71, 73, 547	mulcanap2ad 8683	1 |- ( ph -> ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( -u 1 ^ (♯ ` { z e. S | -. 2 || ( 1st ` z ) } ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105  DECID wdc 835   = wceq 1364   e. wcel 2164   =/= wne 2364   A.wral 2472   E.wrex 2473   {crab 2476   \ cdif 3150   C_ wss 3153   {csn 3618   <.cop 3621   U_ciun 3912  Disj wdisj 4006   class class class wbr 4029   {copab 4089   X. cxp 4657   Rel wrel 4664   ` cfv 5254  (class class class)co 5918   1stc1st 6191   ~~ cen 6792   Fincfn 6794   CCcc 7870   RRcr 7871   0cc0 7872   1c1 7873   + caddc 7875   x. cmul 7877   < clt 8054   <_ cle 8055   - cmin 8190   -ucneg 8191   # cap 8600   / cdiv 8691   NNcn 8982   2c2 9033   NN0cn0 9240   ZZcz 9317   ZZ>=cuz 9592   QQcq 9684   ...cfz 10074   |_cfl 10337   ^cexp 10609  ♯chash 10846   sum_csu 11496   || cdvds 11930   Primecprime 12245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-iinf 4620  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-mulrcl 7971  ax-addcom 7972  ax-mulcom 7973  ax-addass 7974  ax-mulass 7975  ax-distr 7976  ax-i2m1 7977  ax-0lt1 7978  ax-1rid 7979  ax-0id 7980  ax-rnegex 7981  ax-precex 7982  ax-cnre 7983  ax-pre-ltirr 7984  ax-pre-ltwlin 7985  ax-pre-lttrn 7986  ax-pre-apti 7987  ax-pre-ltadd 7988  ax-pre-mulgt0 7989  ax-pre-mulext 7990  ax-arch 7991  ax-caucvg 7992

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-xor 1387  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-if 3558  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-disj 4007  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-id 4324  df-po 4327  df-iso 4328  df-iord 4397  df-on 4399  df-ilim 4400  df-suc 4402  df-iom 4623  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-isom 5263  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-1st 6193  df-2nd 6194  df-recs 6358  df-irdg 6423  df-frec 6444  df-1o 6469  df-2o 6470  df-oadd 6473  df-er 6587  df-en 6795  df-dom 6796  df-fin 6797  df-pnf 8056  df-mnf 8057  df-xr 8058  df-ltxr 8059  df-le 8060  df-sub 8192  df-neg 8193  df-reap 8594  df-ap 8601  df-div 8692  df-inn 8983  df-2 9041  df-3 9042  df-4 9043  df-n0 9241  df-z 9318  df-uz 9593  df-q 9685  df-rp 9720  df-fz 10075  df-fzo 10209  df-fl 10339  df-mod 10394  df-seqfrec 10519  df-exp 10610  df-ihash 10847  df-cj 10986  df-re 10987  df-im 10988  df-rsqrt 11142  df-abs 11143  df-clim 11422  df-sumdc 11497  df-dvds 11931  df-prm 12246

This theorem is referenced by: (None)