Theorem lgsquadlem2

Description: Lemma for lgsquad . Count the members of S with even coordinates, and combine with lgsquadlem1 to get the total count of lattice points in S (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Hypotheses	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	lgsquadlem2	|- ( ph -> ( Q /L P ) = ( -u 1 ^ ( # ` S ) ) )

Proof

Step	Hyp	Ref	Expression
1		lgseisen.1	|- ( ph -> P e. ( Prime \ { 2 } ) )
2		lgseisen.2	|- ( ph -> Q e. ( Prime \ { 2 } ) )
3		lgseisen.3	|- ( ph -> P =/= Q )
4		lgsquad.4	|- M = ( ( P - 1 ) / 2 )
5		lgsquad.5	|- N = ( ( Q - 1 ) / 2 )
6		lgsquad.6	|- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }
7	1 2 3	lgseisen	|- ( ph -> ( Q /L P ) = ( -u 1 ^ sum_ u e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
8	4	oveq2i	|- ( 1 ... M ) = ( 1 ... ( ( P - 1 ) / 2 ) )
9	8	sumeq1i	|- sum_ u e. ( 1 ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) = sum_ u e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) )
10	1 4	gausslemma2dlem0b	|- ( ph -> M e. NN )
11	10	nnred	|- ( ph -> M e. RR )
12	11	rehalfcld	|- ( ph -> ( M / 2 ) e. RR )
13	12	flcld	|- ( ph -> ( |_ ` ( M / 2 ) ) e. ZZ )
14	13	zred	|- ( ph -> ( |_ ` ( M / 2 ) ) e. RR )
15	14	ltp1d	|- ( ph -> ( |_ ` ( M / 2 ) ) < ( ( |_ ` ( M / 2 ) ) + 1 ) )
16		fzdisj	|- ( ( |_ ` ( M / 2 ) ) < ( ( |_ ` ( M / 2 ) ) + 1 ) -> ( ( 1 ... ( |_ ` ( M / 2 ) ) ) i^i ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) = (/) )
17	15 16	syl	|- ( ph -> ( ( 1 ... ( |_ ` ( M / 2 ) ) ) i^i ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) = (/) )
18	10	nnrpd	|- ( ph -> M e. RR+ )
19	18	rphalfcld	|- ( ph -> ( M / 2 ) e. RR+ )
20	19	rpge0d	|- ( ph -> 0 <_ ( M / 2 ) )
21		flge0nn0	|- ( ( ( M / 2 ) e. RR /\ 0 <_ ( M / 2 ) ) -> ( |_ ` ( M / 2 ) ) e. NN0 )
22	12 20 21	syl2anc	|- ( ph -> ( |_ ` ( M / 2 ) ) e. NN0 )
23	10	nnnn0d	|- ( ph -> M e. NN0 )
24		rphalflt	|- ( M e. RR+ -> ( M / 2 ) < M )
25	18 24	syl	|- ( ph -> ( M / 2 ) < M )
26	10	nnzd	|- ( ph -> M e. ZZ )
27		fllt	|- ( ( ( M / 2 ) e. RR /\ M e. ZZ ) -> ( ( M / 2 ) < M <-> ( |_ ` ( M / 2 ) ) < M ) )
28	12 26 27	syl2anc	|- ( ph -> ( ( M / 2 ) < M <-> ( |_ ` ( M / 2 ) ) < M ) )
29	25 28	mpbid	|- ( ph -> ( |_ ` ( M / 2 ) ) < M )
30	14 11 29	ltled	|- ( ph -> ( |_ ` ( M / 2 ) ) <_ M )
31		elfz2nn0	|- ( ( |_ ` ( M / 2 ) ) e. ( 0 ... M ) <-> ( ( |_ ` ( M / 2 ) ) e. NN0 /\ M e. NN0 /\ ( |_ ` ( M / 2 ) ) <_ M ) )
32	22 23 30 31	syl3anbrc	|- ( ph -> ( |_ ` ( M / 2 ) ) e. ( 0 ... M ) )
33		nn0uz	|- NN0 = ( ZZ>= ` 0 )
34	23 33	eleqtrdi	|- ( ph -> M e. ( ZZ>= ` 0 ) )
35		elfzp12	|- ( M e. ( ZZ>= ` 0 ) -> ( ( |_ ` ( M / 2 ) ) e. ( 0 ... M ) <-> ( ( |_ ` ( M / 2 ) ) = 0 \/ ( |_ ` ( M / 2 ) ) e. ( ( 0 + 1 ) ... M ) ) ) )
36	34 35	syl	|- ( ph -> ( ( |_ ` ( M / 2 ) ) e. ( 0 ... M ) <-> ( ( |_ ` ( M / 2 ) ) = 0 \/ ( |_ ` ( M / 2 ) ) e. ( ( 0 + 1 ) ... M ) ) ) )
37	32 36	mpbid	|- ( ph -> ( ( |_ ` ( M / 2 ) ) = 0 \/ ( |_ ` ( M / 2 ) ) e. ( ( 0 + 1 ) ... M ) ) )
38		un0	|- ( ( 1 ... M ) u. (/) ) = ( 1 ... M )
39		uncom	|- ( ( 1 ... M ) u. (/) ) = ( (/) u. ( 1 ... M ) )
40	38 39	eqtr3i	|- ( 1 ... M ) = ( (/) u. ( 1 ... M ) )
41		oveq2	|- ( ( |_ ` ( M / 2 ) ) = 0 -> ( 1 ... ( |_ ` ( M / 2 ) ) ) = ( 1 ... 0 ) )
42		fz10	|- ( 1 ... 0 ) = (/)
43	41 42	eqtrdi	|- ( ( |_ ` ( M / 2 ) ) = 0 -> ( 1 ... ( |_ ` ( M / 2 ) ) ) = (/) )
44		oveq1	|- ( ( |_ ` ( M / 2 ) ) = 0 -> ( ( |_ ` ( M / 2 ) ) + 1 ) = ( 0 + 1 ) )
45		0p1e1	|- ( 0 + 1 ) = 1
46	44 45	eqtrdi	|- ( ( |_ ` ( M / 2 ) ) = 0 -> ( ( |_ ` ( M / 2 ) ) + 1 ) = 1 )
47	46	oveq1d	|- ( ( |_ ` ( M / 2 ) ) = 0 -> ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) = ( 1 ... M ) )
48	43 47	uneq12d	|- ( ( |_ ` ( M / 2 ) ) = 0 -> ( ( 1 ... ( |_ ` ( M / 2 ) ) ) u. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) = ( (/) u. ( 1 ... M ) ) )
49	40 48	eqtr4id	|- ( ( |_ ` ( M / 2 ) ) = 0 -> ( 1 ... M ) = ( ( 1 ... ( |_ ` ( M / 2 ) ) ) u. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) )
50		fzsplit	|- ( ( |_ ` ( M / 2 ) ) e. ( 1 ... M ) -> ( 1 ... M ) = ( ( 1 ... ( |_ ` ( M / 2 ) ) ) u. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) )
51	45	oveq1i	|- ( ( 0 + 1 ) ... M ) = ( 1 ... M )
52	50 51	eleq2s	|- ( ( |_ ` ( M / 2 ) ) e. ( ( 0 + 1 ) ... M ) -> ( 1 ... M ) = ( ( 1 ... ( |_ ` ( M / 2 ) ) ) u. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) )
53	49 52	jaoi	|- ( ( ( |_ ` ( M / 2 ) ) = 0 \/ ( |_ ` ( M / 2 ) ) e. ( ( 0 + 1 ) ... M ) ) -> ( 1 ... M ) = ( ( 1 ... ( |_ ` ( M / 2 ) ) ) u. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) )
54	37 53	syl	|- ( ph -> ( 1 ... M ) = ( ( 1 ... ( |_ ` ( M / 2 ) ) ) u. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) )
55		fzfid	|- ( ph -> ( 1 ... M ) e. Fin )
56	2	gausslemma2dlem0a	|- ( ph -> Q e. NN )
57	56	nnred	|- ( ph -> Q e. RR )
58	1	gausslemma2dlem0a	|- ( ph -> P e. NN )
59	57 58	nndivred	|- ( ph -> ( Q / P ) e. RR )
60	59	adantr	|- ( ( ph /\ u e. ( 1 ... M ) ) -> ( Q / P ) e. RR )
61		2nn	|- 2 e. NN
62		elfznn	|- ( u e. ( 1 ... M ) -> u e. NN )
63	62	adantl	|- ( ( ph /\ u e. ( 1 ... M ) ) -> u e. NN )
64		nnmulcl	|- ( ( 2 e. NN /\ u e. NN ) -> ( 2 x. u ) e. NN )
65	61 63 64	sylancr	|- ( ( ph /\ u e. ( 1 ... M ) ) -> ( 2 x. u ) e. NN )
66	65	nnred	|- ( ( ph /\ u e. ( 1 ... M ) ) -> ( 2 x. u ) e. RR )
67	60 66	remulcld	|- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( Q / P ) x. ( 2 x. u ) ) e. RR )
68	56	nnrpd	|- ( ph -> Q e. RR+ )
69	58	nnrpd	|- ( ph -> P e. RR+ )
70	68 69	rpdivcld	|- ( ph -> ( Q / P ) e. RR+ )
71	70	adantr	|- ( ( ph /\ u e. ( 1 ... M ) ) -> ( Q / P ) e. RR+ )
72	65	nnrpd	|- ( ( ph /\ u e. ( 1 ... M ) ) -> ( 2 x. u ) e. RR+ )
73	71 72	rpmulcld	|- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( Q / P ) x. ( 2 x. u ) ) e. RR+ )
74	73	rpge0d	|- ( ( ph /\ u e. ( 1 ... M ) ) -> 0 <_ ( ( Q / P ) x. ( 2 x. u ) ) )
75		flge0nn0	|- ( ( ( ( Q / P ) x. ( 2 x. u ) ) e. RR /\ 0 <_ ( ( Q / P ) x. ( 2 x. u ) ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. NN0 )
76	67 74 75	syl2anc	|- ( ( ph /\ u e. ( 1 ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. NN0 )
77	76	nn0cnd	|- ( ( ph /\ u e. ( 1 ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. CC )
78	17 54 55 77	fsumsplit	|- ( ph -> sum_ u e. ( 1 ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) = ( sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
79	9 78	eqtr3id	|- ( ph -> sum_ u e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) = ( sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
80	79	oveq2d	|- ( ph -> ( -u 1 ^ sum_ u e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( -u 1 ^ ( sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
81		neg1cn	|- -u 1 e. CC
82	81	a1i	|- ( ph -> -u 1 e. CC )
83		fzfid	|- ( ph -> ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) e. Fin )
84		ssun2	|- ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) C_ ( ( 1 ... ( |_ ` ( M / 2 ) ) ) u. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) )
85	84 54	sseqtrrid	|- ( ph -> ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) C_ ( 1 ... M ) )
86	85	sselda	|- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u e. ( 1 ... M ) )
87	86 76	syldan	|- ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. NN0 )
88	83 87	fsumnn0cl	|- ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. NN0 )
89		fzfid	|- ( ph -> ( 1 ... ( |_ ` ( M / 2 ) ) ) e. Fin )
90		ssun1	|- ( 1 ... ( |_ ` ( M / 2 ) ) ) C_ ( ( 1 ... ( |_ ` ( M / 2 ) ) ) u. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) )
91	90 54	sseqtrrid	|- ( ph -> ( 1 ... ( |_ ` ( M / 2 ) ) ) C_ ( 1 ... M ) )
92	91	sselda	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> u e. ( 1 ... M ) )
93	92 76	syldan	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. NN0 )
94	89 93	fsumnn0cl	|- ( ph -> sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. NN0 )
95	82 88 94	expaddd	|- ( ph -> ( -u 1 ^ ( sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) = ( ( -u 1 ^ sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) x. ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
96		fzfid	|- ( ph -> ( 1 ... N ) e. Fin )
97		xpfi	|- ( ( ( 1 ... M ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( 1 ... M ) X. ( 1 ... N ) ) e. Fin )
98	55 96 97	syl2anc	|- ( ph -> ( ( 1 ... M ) X. ( 1 ... N ) ) e. Fin )
99		opabssxp	|- { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } C_ ( ( 1 ... M ) X. ( 1 ... N ) )
100	6 99	eqsstri	|- S C_ ( ( 1 ... M ) X. ( 1 ... N ) )
101		ssfi	|- ( ( ( ( 1 ... M ) X. ( 1 ... N ) ) e. Fin /\ S C_ ( ( 1 ... M ) X. ( 1 ... N ) ) ) -> S e. Fin )
102	98 100 101	sylancl	|- ( ph -> S e. Fin )
103		ssrab2	|- { z e. S | -. 2 || ( 1st ` z ) } C_ S
104		ssfi	|- ( ( S e. Fin /\ { z e. S | -. 2 || ( 1st ` z ) } C_ S ) -> { z e. S | -. 2 || ( 1st ` z ) } e. Fin )
105	102 103 104	sylancl	|- ( ph -> { z e. S | -. 2 || ( 1st ` z ) } e. Fin )
106		hashcl	|- ( { z e. S | -. 2 || ( 1st ` z ) } e. Fin -> ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) e. NN0 )
107	105 106	syl	|- ( ph -> ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) e. NN0 )
108		ssrab2	|- { z e. S | 2 || ( 1st ` z ) } C_ S
109		ssfi	|- ( ( S e. Fin /\ { z e. S | 2 || ( 1st ` z ) } C_ S ) -> { z e. S | 2 || ( 1st ` z ) } e. Fin )
110	102 108 109	sylancl	|- ( ph -> { z e. S | 2 || ( 1st ` z ) } e. Fin )
111		hashcl	|- ( { z e. S | 2 || ( 1st ` z ) } e. Fin -> ( # ` { z e. S | 2 || ( 1st ` z ) } ) e. NN0 )
112	110 111	syl	|- ( ph -> ( # ` { z e. S | 2 || ( 1st ` z ) } ) e. NN0 )
113	82 107 112	expaddd	|- ( ph -> ( -u 1 ^ ( ( # ` { z e. S | 2 || ( 1st ` z ) } ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( ( -u 1 ^ ( # ` { z e. S | 2 || ( 1st ` z ) } ) ) x. ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
114	92 65	syldan	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( 2 x. u ) e. NN )
115		fzfid	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. Fin )
116		xpsnen2g	|- ( ( ( 2 x. u ) e. NN /\ ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. Fin ) -> ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ~~ ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
117	114 115 116	syl2anc	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ~~ ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
118		hasheni	|- ( ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ~~ ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) -> ( # ` ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) = ( # ` ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
119	117 118	syl	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( # ` ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) = ( # ` ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
120		ssrab2	|- { z e. S | ( 2 x. u ) = ( 1st ` z ) } C_ S
121	6	relopabiv	|- Rel S
122		relss	|- ( { z e. S | ( 2 x. u ) = ( 1st ` z ) } C_ S -> ( Rel S -> Rel { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) )
123	120 121 122	mp2	|- Rel { z e. S | ( 2 x. u ) = ( 1st ` z ) }
124		relxp	|- Rel ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
125	6	eleq2i	|- ( <. x , y >. e. S <-> <. x , y >. e. { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } )
126		opabidw	|- ( <. 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 ) ) )
127	125 126	bitri	|- ( <. x , y >. e. S <-> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) )
128		anass	|- ( ( ( y e. NN /\ y <_ N ) /\ ( y x. P ) < ( Q x. ( 2 x. u ) ) ) <-> ( y e. NN /\ ( y <_ N /\ ( y x. P ) < ( Q x. ( 2 x. u ) ) ) ) )
129	114	adantr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( 2 x. u ) e. NN )
130	129	nnred	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( 2 x. u ) e. RR )
131	58	ad2antrr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> P e. NN )
132	131	nnred	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> P e. RR )
133	132	rehalfcld	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( P / 2 ) e. RR )
134	11	adantr	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> M e. RR )
135	134	adantr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> M e. RR )
136		elfzle2	|- ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) -> u <_ ( |_ ` ( M / 2 ) ) )
137	136	adantl	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> u <_ ( |_ ` ( M / 2 ) ) )
138	134	rehalfcld	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( M / 2 ) e. RR )
139		elfzelz	|- ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) -> u e. ZZ )
140	139	adantl	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> u e. ZZ )
141		flge	|- ( ( ( M / 2 ) e. RR /\ u e. ZZ ) -> ( u <_ ( M / 2 ) <-> u <_ ( |_ ` ( M / 2 ) ) ) )
142	138 140 141	syl2anc	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( u <_ ( M / 2 ) <-> u <_ ( |_ ` ( M / 2 ) ) ) )
143	137 142	mpbird	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> u <_ ( M / 2 ) )
144		elfznn	|- ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) -> u e. NN )
145	144	adantl	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> u e. NN )
146	145	nnred	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> u e. RR )
147		2re	|- 2 e. RR
148	147	a1i	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> 2 e. RR )
149		2pos	|- 0 < 2
150	149	a1i	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> 0 < 2 )
151		lemuldiv2	|- ( ( u e. RR /\ M e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. u ) <_ M <-> u <_ ( M / 2 ) ) )
152	146 134 148 150 151	syl112anc	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( ( 2 x. u ) <_ M <-> u <_ ( M / 2 ) ) )
153	143 152	mpbird	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( 2 x. u ) <_ M )
154	153	adantr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( 2 x. u ) <_ M )
155	132	ltm1d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( P - 1 ) < P )
156		peano2rem	|- ( P e. RR -> ( P - 1 ) e. RR )
157	132 156	syl	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( P - 1 ) e. RR )
158	147	a1i	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> 2 e. RR )
159	149	a1i	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> 0 < 2 )
160		ltdiv1	|- ( ( ( P - 1 ) e. RR /\ P e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( P - 1 ) < P <-> ( ( P - 1 ) / 2 ) < ( P / 2 ) ) )
161	157 132 158 159 160	syl112anc	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( P - 1 ) < P <-> ( ( P - 1 ) / 2 ) < ( P / 2 ) ) )
162	155 161	mpbid	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( P - 1 ) / 2 ) < ( P / 2 ) )
163	4 162	eqbrtrid	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> M < ( P / 2 ) )
164	130 135 133 154 163	lelttrd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( 2 x. u ) < ( P / 2 ) )
165	131	nnrpd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> P e. RR+ )
166		rphalflt	|- ( P e. RR+ -> ( P / 2 ) < P )
167	165 166	syl	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( P / 2 ) < P )
168	130 133 132 164 167	lttrd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( 2 x. u ) < P )
169	130 132	ltnled	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( 2 x. u ) < P <-> -. P <_ ( 2 x. u ) ) )
170	168 169	mpbid	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> -. P <_ ( 2 x. u ) )
171	1	eldifad	|- ( ph -> P e. Prime )
172	171	ad2antrr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> P e. Prime )
173		prmz	|- ( P e. Prime -> P e. ZZ )
174	172 173	syl	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> P e. ZZ )
175		dvdsle	|- ( ( P e. ZZ /\ ( 2 x. u ) e. NN ) -> ( P || ( 2 x. u ) -> P <_ ( 2 x. u ) ) )
176	174 129 175	syl2anc	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( P || ( 2 x. u ) -> P <_ ( 2 x. u ) ) )
177	170 176	mtod	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> -. P || ( 2 x. u ) )
178	2	eldifad	|- ( ph -> Q e. Prime )
179		prmrp	|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )
180	171 178 179	syl2anc	|- ( ph -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )
181	3 180	mpbird	|- ( ph -> ( P gcd Q ) = 1 )
182	181	ad2antrr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( P gcd Q ) = 1 )
183	178	ad2antrr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> Q e. Prime )
184		prmz	|- ( Q e. Prime -> Q e. ZZ )
185	183 184	syl	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> Q e. ZZ )
186	129	nnzd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( 2 x. u ) e. ZZ )
187		coprmdvds	|- ( ( P e. ZZ /\ Q e. ZZ /\ ( 2 x. u ) e. ZZ ) -> ( ( P || ( Q x. ( 2 x. u ) ) /\ ( P gcd Q ) = 1 ) -> P || ( 2 x. u ) ) )
188	174 185 186 187	syl3anc	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( P || ( Q x. ( 2 x. u ) ) /\ ( P gcd Q ) = 1 ) -> P || ( 2 x. u ) ) )
189	182 188	mpan2d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( P || ( Q x. ( 2 x. u ) ) -> P || ( 2 x. u ) ) )
190	177 189	mtod	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> -. P || ( Q x. ( 2 x. u ) ) )
191		nnz	|- ( y e. NN -> y e. ZZ )
192	191	adantl	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> y e. ZZ )
193		dvdsmul2	|- ( ( y e. ZZ /\ P e. ZZ ) -> P || ( y x. P ) )
194	192 174 193	syl2anc	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> P || ( y x. P ) )
195		breq2	|- ( ( Q x. ( 2 x. u ) ) = ( y x. P ) -> ( P || ( Q x. ( 2 x. u ) ) <-> P || ( y x. P ) ) )
196	194 195	syl5ibrcom	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( Q x. ( 2 x. u ) ) = ( y x. P ) -> P || ( Q x. ( 2 x. u ) ) ) )
197	196	necon3bd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( -. P || ( Q x. ( 2 x. u ) ) -> ( Q x. ( 2 x. u ) ) =/= ( y x. P ) ) )
198	190 197	mpd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( Q x. ( 2 x. u ) ) =/= ( y x. P ) )
199		simpr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> y e. NN )
200	199 131	nnmulcld	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( y x. P ) e. NN )
201	200	nnred	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( y x. P ) e. RR )
202	56	adantr	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> Q e. NN )
203	202 114	nnmulcld	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( Q x. ( 2 x. u ) ) e. NN )
204	203	adantr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( Q x. ( 2 x. u ) ) e. NN )
205	204	nnred	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( Q x. ( 2 x. u ) ) e. RR )
206	201 205	ltlend	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( y x. P ) < ( Q x. ( 2 x. u ) ) <-> ( ( y x. P ) <_ ( Q x. ( 2 x. u ) ) /\ ( Q x. ( 2 x. u ) ) =/= ( y x. P ) ) ) )
207	198 206	mpbiran2d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( y x. P ) < ( Q x. ( 2 x. u ) ) <-> ( y x. P ) <_ ( Q x. ( 2 x. u ) ) ) )
208		nnre	|- ( y e. NN -> y e. RR )
209	208	adantl	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> y e. RR )
210	131	nngt0d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> 0 < P )
211		lemuldiv	|- ( ( y e. RR /\ ( Q x. ( 2 x. u ) ) e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( ( y x. P ) <_ ( Q x. ( 2 x. u ) ) <-> y <_ ( ( Q x. ( 2 x. u ) ) / P ) ) )
212	209 205 132 210 211	syl112anc	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( y x. P ) <_ ( Q x. ( 2 x. u ) ) <-> y <_ ( ( Q x. ( 2 x. u ) ) / P ) ) )
213	202	adantr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> Q e. NN )
214	213	nncnd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> Q e. CC )
215	129	nncnd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( 2 x. u ) e. CC )
216	131	nncnd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> P e. CC )
217	131	nnne0d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> P =/= 0 )
218	214 215 216 217	div23d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( Q x. ( 2 x. u ) ) / P ) = ( ( Q / P ) x. ( 2 x. u ) ) )
219	218	breq2d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( y <_ ( ( Q x. ( 2 x. u ) ) / P ) <-> y <_ ( ( Q / P ) x. ( 2 x. u ) ) ) )
220	207 212 219	3bitrd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( y x. P ) < ( Q x. ( 2 x. u ) ) <-> y <_ ( ( Q / P ) x. ( 2 x. u ) ) ) )
221	213	nnred	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> Q e. RR )
222	213	nngt0d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> 0 < Q )
223		ltmul2	|- ( ( ( 2 x. u ) e. RR /\ ( P / 2 ) e. RR /\ ( Q e. RR /\ 0 < Q ) ) -> ( ( 2 x. u ) < ( P / 2 ) <-> ( Q x. ( 2 x. u ) ) < ( Q x. ( P / 2 ) ) ) )
224	130 133 221 222 223	syl112anc	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( 2 x. u ) < ( P / 2 ) <-> ( Q x. ( 2 x. u ) ) < ( Q x. ( P / 2 ) ) ) )
225	164 224	mpbid	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( Q x. ( 2 x. u ) ) < ( Q x. ( P / 2 ) ) )
226		2cnd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> 2 e. CC )
227		2ne0	|- 2 =/= 0
228	227	a1i	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> 2 =/= 0 )
229		divass	|- ( ( Q e. CC /\ P e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( Q x. P ) / 2 ) = ( Q x. ( P / 2 ) ) )
230		div23	|- ( ( Q e. CC /\ P e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( Q x. P ) / 2 ) = ( ( Q / 2 ) x. P ) )
231	229 230	eqtr3d	|- ( ( Q e. CC /\ P e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( Q x. ( P / 2 ) ) = ( ( Q / 2 ) x. P ) )
232	214 216 226 228 231	syl112anc	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( Q x. ( P / 2 ) ) = ( ( Q / 2 ) x. P ) )
233	225 232	breqtrd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( Q x. ( 2 x. u ) ) < ( ( Q / 2 ) x. P ) )
234	221	rehalfcld	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( Q / 2 ) e. RR )
235	234 132	remulcld	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( Q / 2 ) x. P ) e. RR )
236		lttr	|- ( ( ( y x. P ) e. RR /\ ( Q x. ( 2 x. u ) ) e. RR /\ ( ( Q / 2 ) x. P ) e. RR ) -> ( ( ( y x. P ) < ( Q x. ( 2 x. u ) ) /\ ( Q x. ( 2 x. u ) ) < ( ( Q / 2 ) x. P ) ) -> ( y x. P ) < ( ( Q / 2 ) x. P ) ) )
237	201 205 235 236	syl3anc	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( ( y x. P ) < ( Q x. ( 2 x. u ) ) /\ ( Q x. ( 2 x. u ) ) < ( ( Q / 2 ) x. P ) ) -> ( y x. P ) < ( ( Q / 2 ) x. P ) ) )
238	233 237	mpan2d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( y x. P ) < ( Q x. ( 2 x. u ) ) -> ( y x. P ) < ( ( Q / 2 ) x. P ) ) )
239		ltmul1	|- ( ( y e. RR /\ ( Q / 2 ) e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( y < ( Q / 2 ) <-> ( y x. P ) < ( ( Q / 2 ) x. P ) ) )
240	209 234 132 210 239	syl112anc	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( y < ( Q / 2 ) <-> ( y x. P ) < ( ( Q / 2 ) x. P ) ) )
241	238 240	sylibrd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( y x. P ) < ( Q x. ( 2 x. u ) ) -> y < ( Q / 2 ) ) )
242		peano2rem	|- ( Q e. RR -> ( Q - 1 ) e. RR )
243	221 242	syl	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( Q - 1 ) e. RR )
244	243	recnd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( Q - 1 ) e. CC )
245	214 244 226 228	divsubdird	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( Q - ( Q - 1 ) ) / 2 ) = ( ( Q / 2 ) - ( ( Q - 1 ) / 2 ) ) )
246	5	oveq2i	|- ( ( Q / 2 ) - N ) = ( ( Q / 2 ) - ( ( Q - 1 ) / 2 ) )
247	245 246	eqtr4di	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( Q - ( Q - 1 ) ) / 2 ) = ( ( Q / 2 ) - N ) )
248		ax-1cn	|- 1 e. CC
249		nncan	|- ( ( Q e. CC /\ 1 e. CC ) -> ( Q - ( Q - 1 ) ) = 1 )
250	214 248 249	sylancl	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( Q - ( Q - 1 ) ) = 1 )
251	250	oveq1d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( Q - ( Q - 1 ) ) / 2 ) = ( 1 / 2 ) )
252		halflt1	|- ( 1 / 2 ) < 1
253	251 252	eqbrtrdi	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( Q - ( Q - 1 ) ) / 2 ) < 1 )
254	247 253	eqbrtrrd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( Q / 2 ) - N ) < 1 )
255	2 5	gausslemma2dlem0b	|- ( ph -> N e. NN )
256	255	ad2antrr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> N e. NN )
257	256	nnred	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> N e. RR )
258		1red	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> 1 e. RR )
259	234 257 258	ltsubadd2d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( ( Q / 2 ) - N ) < 1 <-> ( Q / 2 ) < ( N + 1 ) ) )
260	254 259	mpbid	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( Q / 2 ) < ( N + 1 ) )
261		peano2re	|- ( N e. RR -> ( N + 1 ) e. RR )
262	257 261	syl	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( N + 1 ) e. RR )
263		lttr	|- ( ( y e. RR /\ ( Q / 2 ) e. RR /\ ( N + 1 ) e. RR ) -> ( ( y < ( Q / 2 ) /\ ( Q / 2 ) < ( N + 1 ) ) -> y < ( N + 1 ) ) )
264	209 234 262 263	syl3anc	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( y < ( Q / 2 ) /\ ( Q / 2 ) < ( N + 1 ) ) -> y < ( N + 1 ) ) )
265	260 264	mpan2d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( y < ( Q / 2 ) -> y < ( N + 1 ) ) )
266	241 265	syld	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( y x. P ) < ( Q x. ( 2 x. u ) ) -> y < ( N + 1 ) ) )
267		nnleltp1	|- ( ( y e. NN /\ N e. NN ) -> ( y <_ N <-> y < ( N + 1 ) ) )
268	199 256 267	syl2anc	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( y <_ N <-> y < ( N + 1 ) ) )
269	266 268	sylibrd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( y x. P ) < ( Q x. ( 2 x. u ) ) -> y <_ N ) )
270	269	pm4.71rd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( y x. P ) < ( Q x. ( 2 x. u ) ) <-> ( y <_ N /\ ( y x. P ) < ( Q x. ( 2 x. u ) ) ) ) )
271	92 67	syldan	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( ( Q / P ) x. ( 2 x. u ) ) e. RR )
272		flge	|- ( ( ( ( Q / P ) x. ( 2 x. u ) ) e. RR /\ y e. ZZ ) -> ( y <_ ( ( Q / P ) x. ( 2 x. u ) ) <-> y <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
273	271 191 272	syl2an	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( y <_ ( ( Q / P ) x. ( 2 x. u ) ) <-> y <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
274	220 270 273	3bitr3d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ y e. NN ) -> ( ( y <_ N /\ ( y x. P ) < ( Q x. ( 2 x. u ) ) ) <-> y <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
275	274	pm5.32da	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( ( y e. NN /\ ( y <_ N /\ ( y x. P ) < ( Q x. ( 2 x. u ) ) ) ) <-> ( y e. NN /\ y <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
276	128 275	syl5bb	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( ( ( y e. NN /\ y <_ N ) /\ ( y x. P ) < ( Q x. ( 2 x. u ) ) ) <-> ( y e. NN /\ y <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
277	276	adantr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> ( ( ( y e. NN /\ y <_ N ) /\ ( y x. P ) < ( Q x. ( 2 x. u ) ) ) <-> ( y e. NN /\ y <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
278		simpr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> x = ( 2 x. u ) )
279		nnuz	|- NN = ( ZZ>= ` 1 )
280	114 279	eleqtrdi	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( 2 x. u ) e. ( ZZ>= ` 1 ) )
281	26	adantr	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> M e. ZZ )
282		elfz5	|- ( ( ( 2 x. u ) e. ( ZZ>= ` 1 ) /\ M e. ZZ ) -> ( ( 2 x. u ) e. ( 1 ... M ) <-> ( 2 x. u ) <_ M ) )
283	280 281 282	syl2anc	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( ( 2 x. u ) e. ( 1 ... M ) <-> ( 2 x. u ) <_ M ) )
284	153 283	mpbird	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( 2 x. u ) e. ( 1 ... M ) )
285	284	adantr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> ( 2 x. u ) e. ( 1 ... M ) )
286	278 285	eqeltrd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> x e. ( 1 ... M ) )
287	286	biantrurd	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> ( y e. ( 1 ... N ) <-> ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) )
288	255	nnzd	|- ( ph -> N e. ZZ )
289	288	ad2antrr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> N e. ZZ )
290		fznn	|- ( N e. ZZ -> ( y e. ( 1 ... N ) <-> ( y e. NN /\ y <_ N ) ) )
291	289 290	syl	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> ( y e. ( 1 ... N ) <-> ( y e. NN /\ y <_ N ) ) )
292	287 291	bitr3d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) <-> ( y e. NN /\ y <_ N ) ) )
293		oveq1	|- ( x = ( 2 x. u ) -> ( x x. Q ) = ( ( 2 x. u ) x. Q ) )
294	114	nncnd	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( 2 x. u ) e. CC )
295	202	nncnd	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> Q e. CC )
296	294 295	mulcomd	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( ( 2 x. u ) x. Q ) = ( Q x. ( 2 x. u ) ) )
297	293 296	sylan9eqr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> ( x x. Q ) = ( Q x. ( 2 x. u ) ) )
298	297	breq2d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> ( ( y x. P ) < ( x x. Q ) <-> ( y x. P ) < ( Q x. ( 2 x. u ) ) ) )
299	292 298	anbi12d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 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 ) < ( Q x. ( 2 x. u ) ) ) ) )
300	271	flcld	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ )
301		fznn	|- ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ -> ( y e. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <-> ( y e. NN /\ y <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
302	300 301	syl	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( y e. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <-> ( y e. NN /\ y <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
303	302	adantr	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> ( y e. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <-> ( y e. NN /\ y <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
304	277 299 303	3bitr4d	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) <-> y e. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
305	127 304	syl5bb	|- ( ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) /\ x = ( 2 x. u ) ) -> ( <. x , y >. e. S <-> y e. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
306	305	pm5.32da	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( ( x = ( 2 x. u ) /\ <. x , y >. e. S ) <-> ( x = ( 2 x. u ) /\ y e. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
307		vex	|- x e. _V
308		vex	|- y e. _V
309	307 308	op1std	|- ( z = <. x , y >. -> ( 1st ` z ) = x )
310	309	eqeq2d	|- ( z = <. x , y >. -> ( ( 2 x. u ) = ( 1st ` z ) <-> ( 2 x. u ) = x ) )
311		eqcom	|- ( ( 2 x. u ) = x <-> x = ( 2 x. u ) )
312	310 311	bitrdi	|- ( z = <. x , y >. -> ( ( 2 x. u ) = ( 1st ` z ) <-> x = ( 2 x. u ) ) )
313	312	elrab	|- ( <. x , y >. e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } <-> ( <. x , y >. e. S /\ x = ( 2 x. u ) ) )
314	313	biancomi	|- ( <. x , y >. e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } <-> ( x = ( 2 x. u ) /\ <. x , y >. e. S ) )
315		opelxp	|- ( <. x , y >. e. ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) <-> ( x e. { ( 2 x. u ) } /\ y e. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
316		velsn	|- ( x e. { ( 2 x. u ) } <-> x = ( 2 x. u ) )
317	316	anbi1i	|- ( ( x e. { ( 2 x. u ) } /\ y e. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) <-> ( x = ( 2 x. u ) /\ y e. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
318	315 317	bitri	|- ( <. x , y >. e. ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) <-> ( x = ( 2 x. u ) /\ y e. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
319	306 314 318	3bitr4g	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( <. x , y >. e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } <-> <. x , y >. e. ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
320	123 124 319	eqrelrdv	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> { z e. S | ( 2 x. u ) = ( 1st ` z ) } = ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
321	320	eqcomd	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) = { z e. S | ( 2 x. u ) = ( 1st ` z ) } )
322	321	fveq2d	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( # ` ( { ( 2 x. u ) } X. ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) = ( # ` { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) )
323		hashfz1	|- ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. NN0 -> ( # ` ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) = ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) )
324	93 323	syl	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( # ` ( 1 ... ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) = ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) )
325	119 322 324	3eqtr3rd	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) = ( # ` { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) )
326	325	sumeq2dv	|- ( ph -> sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) = sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( # ` { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) )
327	102	adantr	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> S e. Fin )
328		ssfi	|- ( ( S e. Fin /\ { z e. S | ( 2 x. u ) = ( 1st ` z ) } C_ S ) -> { z e. S | ( 2 x. u ) = ( 1st ` z ) } e. Fin )
329	327 120 328	sylancl	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> { z e. S | ( 2 x. u ) = ( 1st ` z ) } e. Fin )
330		fveq2	|- ( z = v -> ( 1st ` z ) = ( 1st ` v ) )
331	330	eqeq2d	|- ( z = v -> ( ( 2 x. u ) = ( 1st ` z ) <-> ( 2 x. u ) = ( 1st ` v ) ) )
332	331	elrab	|- ( v e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } <-> ( v e. S /\ ( 2 x. u ) = ( 1st ` v ) ) )
333	332	simprbi	|- ( v e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } -> ( 2 x. u ) = ( 1st ` v ) )
334	333	ad2antll	|- ( ( ph /\ ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) /\ v e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) ) -> ( 2 x. u ) = ( 1st ` v ) )
335	334	oveq1d	|- ( ( ph /\ ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) /\ v e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) ) -> ( ( 2 x. u ) / 2 ) = ( ( 1st ` v ) / 2 ) )
336	145	nncnd	|- ( ( ph /\ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ) -> u e. CC )
337	336	adantrr	|- ( ( ph /\ ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) /\ v e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) ) -> u e. CC )
338		2cnd	|- ( ( ph /\ ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) /\ v e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) ) -> 2 e. CC )
339	227	a1i	|- ( ( ph /\ ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) /\ v e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) ) -> 2 =/= 0 )
340	337 338 339	divcan3d	|- ( ( ph /\ ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) /\ v e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) ) -> ( ( 2 x. u ) / 2 ) = u )
341	335 340	eqtr3d	|- ( ( ph /\ ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) /\ v e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) ) -> ( ( 1st ` v ) / 2 ) = u )
342	341	ralrimivva	|- ( ph -> A. u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) A. v e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } ( ( 1st ` v ) / 2 ) = u )
343		invdisj	|- ( A. u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) A. v e. { z e. S | ( 2 x. u ) = ( 1st ` z ) } ( ( 1st ` v ) / 2 ) = u -> Disj_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) { z e. S | ( 2 x. u ) = ( 1st ` z ) } )
344	342 343	syl	|- ( ph -> Disj_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) { z e. S | ( 2 x. u ) = ( 1st ` z ) } )
345	89 329 344	hashiun	|- ( ph -> ( # ` U_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) = sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( # ` { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) )
346		iunrab	|- U_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) { z e. S | ( 2 x. u ) = ( 1st ` z ) } = { z e. S | E. u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( 2 x. u ) = ( 1st ` z ) }
347		2cn	|- 2 e. CC
348		zcn	|- ( u e. ZZ -> u e. CC )
349	348	adantl	|- ( ( ( ph /\ z e. S ) /\ u e. ZZ ) -> u e. CC )
350		mulcom	|- ( ( 2 e. CC /\ u e. CC ) -> ( 2 x. u ) = ( u x. 2 ) )
351	347 349 350	sylancr	|- ( ( ( ph /\ z e. S ) /\ u e. ZZ ) -> ( 2 x. u ) = ( u x. 2 ) )
352	351	eqeq1d	|- ( ( ( ph /\ z e. S ) /\ u e. ZZ ) -> ( ( 2 x. u ) = ( 1st ` z ) <-> ( u x. 2 ) = ( 1st ` z ) ) )
353	352	rexbidva	|- ( ( ph /\ z e. S ) -> ( E. u e. ZZ ( 2 x. u ) = ( 1st ` z ) <-> E. u e. ZZ ( u x. 2 ) = ( 1st ` z ) ) )
354	139	anim1i	|- ( ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) /\ ( 2 x. u ) = ( 1st ` z ) ) -> ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) )
355	354	reximi2	|- ( E. u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( 2 x. u ) = ( 1st ` z ) -> E. u e. ZZ ( 2 x. u ) = ( 1st ` z ) )
356		simprr	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( 2 x. u ) = ( 1st ` z ) )
357		simpr	|- ( ( ph /\ z e. S ) -> z e. S )
358	100 357	sselid	|- ( ( ph /\ z e. S ) -> z e. ( ( 1 ... M ) X. ( 1 ... N ) ) )
359		xp1st	|- ( z e. ( ( 1 ... M ) X. ( 1 ... N ) ) -> ( 1st ` z ) e. ( 1 ... M ) )
360	358 359	syl	|- ( ( ph /\ z e. S ) -> ( 1st ` z ) e. ( 1 ... M ) )
361	360	adantr	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( 1st ` z ) e. ( 1 ... M ) )
362		elfzle2	|- ( ( 1st ` z ) e. ( 1 ... M ) -> ( 1st ` z ) <_ M )
363	361 362	syl	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( 1st ` z ) <_ M )
364	356 363	eqbrtrd	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( 2 x. u ) <_ M )
365		zre	|- ( u e. ZZ -> u e. RR )
366	365	ad2antrl	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> u e. RR )
367	11	ad2antrr	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> M e. RR )
368	147	a1i	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> 2 e. RR )
369	149	a1i	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> 0 < 2 )
370	366 367 368 369 151	syl112anc	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( ( 2 x. u ) <_ M <-> u <_ ( M / 2 ) ) )
371	364 370	mpbid	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> u <_ ( M / 2 ) )
372	12	ad2antrr	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( M / 2 ) e. RR )
373		simprl	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> u e. ZZ )
374	372 373 141	syl2anc	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( u <_ ( M / 2 ) <-> u <_ ( |_ ` ( M / 2 ) ) ) )
375	371 374	mpbid	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> u <_ ( |_ ` ( M / 2 ) ) )
376		2t0e0	|- ( 2 x. 0 ) = 0
377		elfznn	|- ( ( 1st ` z ) e. ( 1 ... M ) -> ( 1st ` z ) e. NN )
378	361 377	syl	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( 1st ` z ) e. NN )
379	356 378	eqeltrd	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( 2 x. u ) e. NN )
380	379	nngt0d	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> 0 < ( 2 x. u ) )
381	376 380	eqbrtrid	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( 2 x. 0 ) < ( 2 x. u ) )
382		0red	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> 0 e. RR )
383		ltmul2	|- ( ( 0 e. RR /\ u e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 0 < u <-> ( 2 x. 0 ) < ( 2 x. u ) ) )
384	382 366 368 369 383	syl112anc	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( 0 < u <-> ( 2 x. 0 ) < ( 2 x. u ) ) )
385	381 384	mpbird	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> 0 < u )
386		elnnz	|- ( u e. NN <-> ( u e. ZZ /\ 0 < u ) )
387	373 385 386	sylanbrc	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> u e. NN )
388	387 279	eleqtrdi	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> u e. ( ZZ>= ` 1 ) )
389	13	ad2antrr	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( |_ ` ( M / 2 ) ) e. ZZ )
390		elfz5	|- ( ( u e. ( ZZ>= ` 1 ) /\ ( |_ ` ( M / 2 ) ) e. ZZ ) -> ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) <-> u <_ ( |_ ` ( M / 2 ) ) ) )
391	388 389 390	syl2anc	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) <-> u <_ ( |_ ` ( M / 2 ) ) ) )
392	375 391	mpbird	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) )
393	392 356	jca	|- ( ( ( ph /\ z e. S ) /\ ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) ) -> ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) /\ ( 2 x. u ) = ( 1st ` z ) ) )
394	393	ex	|- ( ( ph /\ z e. S ) -> ( ( u e. ZZ /\ ( 2 x. u ) = ( 1st ` z ) ) -> ( u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) /\ ( 2 x. u ) = ( 1st ` z ) ) ) )
395	394	reximdv2	|- ( ( ph /\ z e. S ) -> ( E. u e. ZZ ( 2 x. u ) = ( 1st ` z ) -> E. u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( 2 x. u ) = ( 1st ` z ) ) )
396	355 395	impbid2	|- ( ( ph /\ z e. S ) -> ( E. u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( 2 x. u ) = ( 1st ` z ) <-> E. u e. ZZ ( 2 x. u ) = ( 1st ` z ) ) )
397		2z	|- 2 e. ZZ
398	360	elfzelzd	|- ( ( ph /\ z e. S ) -> ( 1st ` z ) e. ZZ )
399		divides	|- ( ( 2 e. ZZ /\ ( 1st ` z ) e. ZZ ) -> ( 2 || ( 1st ` z ) <-> E. u e. ZZ ( u x. 2 ) = ( 1st ` z ) ) )
400	397 398 399	sylancr	|- ( ( ph /\ z e. S ) -> ( 2 || ( 1st ` z ) <-> E. u e. ZZ ( u x. 2 ) = ( 1st ` z ) ) )
401	353 396 400	3bitr4d	|- ( ( ph /\ z e. S ) -> ( E. u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( 2 x. u ) = ( 1st ` z ) <-> 2 || ( 1st ` z ) ) )
402	401	rabbidva	|- ( ph -> { z e. S | E. u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( 2 x. u ) = ( 1st ` z ) } = { z e. S | 2 || ( 1st ` z ) } )
403	346 402	syl5eq	|- ( ph -> U_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) { z e. S | ( 2 x. u ) = ( 1st ` z ) } = { z e. S | 2 || ( 1st ` z ) } )
404	403	fveq2d	|- ( ph -> ( # ` U_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) { z e. S | ( 2 x. u ) = ( 1st ` z ) } ) = ( # ` { z e. S | 2 || ( 1st ` z ) } ) )
405	326 345 404	3eqtr2d	|- ( ph -> sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) = ( # ` { z e. S | 2 || ( 1st ` z ) } ) )
406	405	oveq2d	|- ( ph -> ( -u 1 ^ sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( -u 1 ^ ( # ` { z e. S | 2 || ( 1st ` z ) } ) ) )
407	1 2 3 4 5 6	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 ) } ) ) )
408	406 407	oveq12d	|- ( ph -> ( ( -u 1 ^ sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) x. ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) = ( ( -u 1 ^ ( # ` { z e. S | 2 || ( 1st ` z ) } ) ) x. ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
409	113 408	eqtr4d	|- ( ph -> ( -u 1 ^ ( ( # ` { z e. S | 2 || ( 1st ` z ) } ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( ( -u 1 ^ sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) x. ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
410		inrab	|- ( { z e. S | 2 || ( 1st ` z ) } i^i { z e. S | -. 2 || ( 1st ` z ) } ) = { z e. S | ( 2 || ( 1st ` z ) /\ -. 2 || ( 1st ` z ) ) }
411		pm3.24	|- -. ( 2 || ( 1st ` z ) /\ -. 2 || ( 1st ` z ) )
412	411	a1i	|- ( ph -> -. ( 2 || ( 1st ` z ) /\ -. 2 || ( 1st ` z ) ) )
413	412	ralrimivw	|- ( ph -> A. z e. S -. ( 2 || ( 1st ` z ) /\ -. 2 || ( 1st ` z ) ) )
414		rabeq0	|- ( { z e. S | ( 2 || ( 1st ` z ) /\ -. 2 || ( 1st ` z ) ) } = (/) <-> A. z e. S -. ( 2 || ( 1st ` z ) /\ -. 2 || ( 1st ` z ) ) )
415	413 414	sylibr	|- ( ph -> { z e. S | ( 2 || ( 1st ` z ) /\ -. 2 || ( 1st ` z ) ) } = (/) )
416	410 415	syl5eq	|- ( ph -> ( { z e. S | 2 || ( 1st ` z ) } i^i { z e. S | -. 2 || ( 1st ` z ) } ) = (/) )
417		hashun	|- ( ( { z e. S | 2 || ( 1st ` z ) } e. Fin /\ { z e. S | -. 2 || ( 1st ` z ) } e. Fin /\ ( { z e. S | 2 || ( 1st ` z ) } i^i { z e. S | -. 2 || ( 1st ` z ) } ) = (/) ) -> ( # ` ( { z e. S | 2 || ( 1st ` z ) } u. { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( ( # ` { z e. S | 2 || ( 1st ` z ) } ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) )
418	110 105 416 417	syl3anc	|- ( ph -> ( # ` ( { z e. S | 2 || ( 1st ` z ) } u. { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( ( # ` { z e. S | 2 || ( 1st ` z ) } ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) )
419		unrab	|- ( { z e. S | 2 || ( 1st ` z ) } u. { z e. S | -. 2 || ( 1st ` z ) } ) = { z e. S | ( 2 || ( 1st ` z ) \/ -. 2 || ( 1st ` z ) ) }
420		exmid	|- ( 2 || ( 1st ` z ) \/ -. 2 || ( 1st ` z ) )
421	420	rgenw	|- A. z e. S ( 2 || ( 1st ` z ) \/ -. 2 || ( 1st ` z ) )
422		rabid2	|- ( S = { z e. S | ( 2 || ( 1st ` z ) \/ -. 2 || ( 1st ` z ) ) } <-> A. z e. S ( 2 || ( 1st ` z ) \/ -. 2 || ( 1st ` z ) ) )
423	421 422	mpbir	|- S = { z e. S | ( 2 || ( 1st ` z ) \/ -. 2 || ( 1st ` z ) ) }
424	419 423	eqtr4i	|- ( { z e. S | 2 || ( 1st ` z ) } u. { z e. S | -. 2 || ( 1st ` z ) } ) = S
425	424	fveq2i	|- ( # ` ( { z e. S | 2 || ( 1st ` z ) } u. { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( # ` S )
426	418 425	eqtr3di	|- ( ph -> ( ( # ` { z e. S | 2 || ( 1st ` z ) } ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( # ` S ) )
427	426	oveq2d	|- ( ph -> ( -u 1 ^ ( ( # ` { z e. S | 2 || ( 1st ` z ) } ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( -u 1 ^ ( # ` S ) ) )
428	95 409 427	3eqtr2d	|- ( ph -> ( -u 1 ^ ( sum_ u e. ( 1 ... ( |_ ` ( M / 2 ) ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) = ( -u 1 ^ ( # ` S ) ) )
429	7 80 428	3eqtrd	|- ( ph -> ( Q /L P ) = ( -u 1 ^ ( # ` S ) ) )