Theorem lgseisenlem2 15961

Description: Lemma for lgseisen 15964. The function M is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 17-Jun-2015.)

Hypotheses

Ref	Expression
lgseisen.1	|- ( ph -> P e. ( Prime \ { 2 } ) )
lgseisen.2	|- ( ph -> Q e. ( Prime \ { 2 } ) )
lgseisen.3	|- ( ph -> P =/= Q )
lgseisen.4	|- R = ( ( Q x. ( 2 x. x ) ) mod P )
lgseisen.5	|- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
lgseisen.6	|- S = ( ( Q x. ( 2 x. y ) ) mod P )

Assertion

Ref	Expression
lgseisenlem2	|- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) )

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

Allowed substitution hints:   R( x, y)   S( y)   M( x)

Proof of Theorem lgseisenlem2

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lgseisen.1	. . . 4 |- ( ph -> P e. ( Prime \ { 2 } ) )
2		lgseisen.2	. . . 4 |- ( ph -> Q e. ( Prime \ { 2 } ) )
3		lgseisen.3	. . . 4 |- ( ph -> P =/= Q )
4		lgseisen.4	. . . 4 |- R = ( ( Q x. ( 2 x. x ) ) mod P )
5		lgseisen.5	. . . 4 |- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
6	1, 2, 3, 4, 5	lgseisenlem1 15960	. . 3 |- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) )
7		oveq2 6060	. . . . . . . . . . . . . . 15 |- ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
8	7	oveq2d 6068	. . . . . . . . . . . . . 14 |- ( x = y -> ( Q x. ( 2 x. x ) ) = ( Q x. ( 2 x. y ) ) )
9	8	oveq1d 6067	. . . . . . . . . . . . 13 |- ( x = y -> ( ( Q x. ( 2 x. x ) ) mod P ) = ( ( Q x. ( 2 x. y ) ) mod P ) )
10		lgseisen.6	. . . . . . . . . . . . 13 |- S = ( ( Q x. ( 2 x. y ) ) mod P )
11	9, 4, 10	3eqtr4g 2292	. . . . . . . . . . . 12 |- ( x = y -> R = S )
12	11	oveq2d 6068	. . . . . . . . . . 11 |- ( x = y -> ( -u 1 ^ R ) = ( -u 1 ^ S ) )
13	12, 11	oveq12d 6070	. . . . . . . . . 10 |- ( x = y -> ( ( -u 1 ^ R ) x. R ) = ( ( -u 1 ^ S ) x. S ) )
14	13	oveq1d 6067	. . . . . . . . 9 |- ( x = y -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = ( ( ( -u 1 ^ S ) x. S ) mod P ) )
15	14	oveq1d 6067	. . . . . . . 8 |- ( x = y -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) = ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) )
16		simprl 531	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. ( 1 ... ( ( P - 1 ) / 2 ) ) )
17		neg1z 9611	. . . . . . . . . . . . 13 |- -u 1 e. ZZ
18	2	eldifad 3224	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> Q e. Prime )
19		prmnn 12811	. . . . . . . . . . . . . . . . . . 19 |- ( Q e. Prime -> Q e. NN )
20	18, 19	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( ph -> Q e. NN )
21	20	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. NN )
22		2nn 9401	. . . . . . . . . . . . . . . . . . 19 |- 2 e. NN
23	22	a1i 9	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 e. NN )
24		elfznn 10391	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y e. NN )
25	24	ad2antrl 490	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. NN )
26	23, 25	nnmulcld 9288	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. NN )
27	21, 26	nnmulcld 9288	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. y ) ) e. NN )
28	27	nnzd 9702	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. y ) ) e. ZZ )
29	1	eldifad 3224	. . . . . . . . . . . . . . . . 17 |- ( ph -> P e. Prime )
30		prmnn 12811	. . . . . . . . . . . . . . . . 17 |- ( P e. Prime -> P e. NN )
31	29, 30	syl 14	. . . . . . . . . . . . . . . 16 |- ( ph -> P e. NN )
32	31	adantr 276	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. NN )
33	28, 32	zmodcld 10711	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( Q x. ( 2 x. y ) ) mod P ) e. NN0 )
34	10, 33	eqeltrid 2321	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> S e. NN0 )
35		zexpcl 10920	. . . . . . . . . . . . 13 |- ( ( -u 1 e. ZZ /\ S e. NN0 ) -> ( -u 1 ^ S ) e. ZZ )
36	17, 34, 35	sylancr 414	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ S ) e. ZZ )
37	34	nn0zd 9701	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> S e. ZZ )
38	36, 37	zmulcld 9709	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) x. S ) e. ZZ )
39	38, 32	zmodcld 10711	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ S ) x. S ) mod P ) e. NN0 )
40	39	nn0zd 9701	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ S ) x. S ) mod P ) e. ZZ )
41		znq 9959	. . . . . . . . 9 |- ( ( ( ( ( -u 1 ^ S ) x. S ) mod P ) e. ZZ /\ 2 e. NN ) -> ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) e. QQ )
42	40, 22, 41	sylancl 413	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) e. QQ )
43	5, 15, 16, 42	fvmptd3 5773	. . . . . . 7 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( M ` y ) = ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) )
44		simprr 533	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. ( 1 ... ( ( P - 1 ) / 2 ) ) )
45		elfznn 10391	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. NN )
46	45	ad2antll 491	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. NN )
47	23, 46	nnmulcld 9288	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. NN )
48	21, 47	nnmulcld 9288	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. x ) ) e. NN )
49	48	nnzd 9702	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. x ) ) e. ZZ )
50	49, 32	zmodcld 10711	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( Q x. ( 2 x. x ) ) mod P ) e. NN0 )
51	4, 50	eqeltrid 2321	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> R e. NN0 )
52		zexpcl 10920	. . . . . . . . . . . . . 14 |- ( ( -u 1 e. ZZ /\ R e. NN0 ) -> ( -u 1 ^ R ) e. ZZ )
53	17, 51, 52	sylancr 414	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) e. ZZ )
54	51	nn0zd 9701	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> R e. ZZ )
55	53, 54	zmulcld 9709	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. R ) e. ZZ )
56	55, 32	zmodcld 10711	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN0 )
57	56	nn0zd 9701	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. ZZ )
58		znq 9959	. . . . . . . . . 10 |- ( ( ( ( ( -u 1 ^ R ) x. R ) mod P ) e. ZZ /\ 2 e. NN ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. QQ )
59	57, 22, 58	sylancl 413	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. QQ )
60	59	elexd 2829	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. _V )
61	5	fvmpt2 5763	. . . . . . . 8 |- ( ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. _V ) -> ( M ` x ) = ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
62	44, 60, 61	syl2anc 411	. . . . . . 7 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( M ` x ) = ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
63	43, 62	eqeq12d 2249	. . . . . 6 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( M ` y ) = ( M ` x ) <-> ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) = ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) )
64	2	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. ( Prime \ { 2 } ) )
65	64	eldifad 3224	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. Prime )
66		prmz 12812	. . . . . . . . . . . . . . . . 17 |- ( Q e. Prime -> Q e. ZZ )
67	65, 66	syl 14	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. ZZ )
68		2z 9607	. . . . . . . . . . . . . . . . 17 |- 2 e. ZZ
69		elfzelz 10362	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y e. ZZ )
70	69	ad2antrl 490	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. ZZ )
71		zmulcl 9633	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. ZZ /\ y e. ZZ ) -> ( 2 x. y ) e. ZZ )
72	68, 70, 71	sylancr 414	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. ZZ )
73	67, 72	zmulcld 9709	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. y ) ) e. ZZ )
74	1	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. ( Prime \ { 2 } ) )
75	74	eldifad 3224	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. Prime )
76	75, 30	syl 14	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. NN )
77	73, 76	zmodcld 10711	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( Q x. ( 2 x. y ) ) mod P ) e. NN0 )
78	10, 77	eqeltrid 2321	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> S e. NN0 )
79	78	nn0zd 9701	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> S e. ZZ )
80		m1expcl 10928	. . . . . . . . . . . 12 |- ( S e. ZZ -> ( -u 1 ^ S ) e. ZZ )
81	79, 80	syl 14	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ S ) e. ZZ )
82	81, 79	zmulcld 9709	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) x. S ) e. ZZ )
83	82, 76	zmodcld 10711	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ S ) x. S ) mod P ) e. NN0 )
84	83	nn0cnd 9557	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ S ) x. S ) mod P ) e. CC )
85		elfzelz 10362	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. ZZ )
86	85	ad2antll 491	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. ZZ )
87		zmulcl 9633	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. ZZ /\ x e. ZZ ) -> ( 2 x. x ) e. ZZ )
88	68, 86, 87	sylancr 414	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. ZZ )
89	67, 88	zmulcld 9709	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. x ) ) e. ZZ )
90	89, 76	zmodcld 10711	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( Q x. ( 2 x. x ) ) mod P ) e. NN0 )
91	4, 90	eqeltrid 2321	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> R e. NN0 )
92	91	nn0zd 9701	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> R e. ZZ )
93		m1expcl 10928	. . . . . . . . . . . 12 |- ( R e. ZZ -> ( -u 1 ^ R ) e. ZZ )
94	92, 93	syl 14	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) e. ZZ )
95	94, 92	zmulcld 9709	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. R ) e. ZZ )
96	95, 76	zmodcld 10711	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN0 )
97	96	nn0cnd 9557	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. CC )
98		2cnd 9312	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 e. CC )
99	23	nnap0d 9285	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 # 0 )
100		div11ap 8976	. . . . . . . 8 |- ( ( ( ( ( -u 1 ^ S ) x. S ) mod P ) e. CC /\ ( ( ( -u 1 ^ R ) x. R ) mod P ) e. CC /\ ( 2 e. CC /\ 2 # 0 ) ) -> ( ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) = ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) <-> ( ( ( -u 1 ^ S ) x. S ) mod P ) = ( ( ( -u 1 ^ R ) x. R ) mod P ) ) )
101	84, 97, 98, 99, 100	syl112anc 1278	. . . . . . 7 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) = ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) <-> ( ( ( -u 1 ^ S ) x. S ) mod P ) = ( ( ( -u 1 ^ R ) x. R ) mod P ) ) )
102		nnq 9968	. . . . . . . . . . 11 |- ( P e. NN -> P e. QQ )
103	32, 102	syl 14	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. QQ )
104	32	nngt0d 9283	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 < P )
105		eqidd 2235	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) mod P ) = ( ( -u 1 ^ S ) mod P ) )
106	10	oveq1i 6062	. . . . . . . . . . 11 |- ( S mod P ) = ( ( ( Q x. ( 2 x. y ) ) mod P ) mod P )
107		nnq 9968	. . . . . . . . . . . . 13 |- ( ( Q x. ( 2 x. y ) ) e. NN -> ( Q x. ( 2 x. y ) ) e. QQ )
108	27, 107	syl 14	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. y ) ) e. QQ )
109	31, 102	syl 14	. . . . . . . . . . . . 13 |- ( ph -> P e. QQ )
110	109	adantr 276	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. QQ )
111		modqabs2 10724	. . . . . . . . . . . 12 |- ( ( ( Q x. ( 2 x. y ) ) e. QQ /\ P e. QQ /\ 0 < P ) -> ( ( ( Q x. ( 2 x. y ) ) mod P ) mod P ) = ( ( Q x. ( 2 x. y ) ) mod P ) )
112	108, 110, 104, 111	syl3anc 1274	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( Q x. ( 2 x. y ) ) mod P ) mod P ) = ( ( Q x. ( 2 x. y ) ) mod P ) )
113	106, 112	eqtrid 2279	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( S mod P ) = ( ( Q x. ( 2 x. y ) ) mod P ) )
114	36, 36, 37, 28, 103, 104, 105, 113	modqmul12d 10744	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ S ) x. S ) mod P ) = ( ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) mod P ) )
115		eqidd 2235	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) mod P ) = ( ( -u 1 ^ R ) mod P ) )
116	4	oveq1i 6062	. . . . . . . . . . 11 |- ( R mod P ) = ( ( ( Q x. ( 2 x. x ) ) mod P ) mod P )
117		nnq 9968	. . . . . . . . . . . . 13 |- ( ( Q x. ( 2 x. x ) ) e. NN -> ( Q x. ( 2 x. x ) ) e. QQ )
118	48, 117	syl 14	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. x ) ) e. QQ )
119		modqabs2 10724	. . . . . . . . . . . 12 |- ( ( ( Q x. ( 2 x. x ) ) e. QQ /\ P e. QQ /\ 0 < P ) -> ( ( ( Q x. ( 2 x. x ) ) mod P ) mod P ) = ( ( Q x. ( 2 x. x ) ) mod P ) )
120	118, 110, 104, 119	syl3anc 1274	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( Q x. ( 2 x. x ) ) mod P ) mod P ) = ( ( Q x. ( 2 x. x ) ) mod P ) )
121	116, 120	eqtrid 2279	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( R mod P ) = ( ( Q x. ( 2 x. x ) ) mod P ) )
122	53, 53, 54, 49, 110, 104, 115, 121	modqmul12d 10744	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = ( ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) mod P ) )
123	114, 122	eqeq12d 2249	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( ( -u 1 ^ S ) x. S ) mod P ) = ( ( ( -u 1 ^ R ) x. R ) mod P ) <-> ( ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) mod P ) = ( ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) mod P ) ) )
124	81, 73	zmulcld 9709	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) e. ZZ )
125	94, 89	zmulcld 9709	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) e. ZZ )
126		moddvds 12489	. . . . . . . . . 10 |- ( ( P e. NN /\ ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) e. ZZ /\ ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) e. ZZ ) -> ( ( ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) mod P ) = ( ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) mod P ) <-> P || ( ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) - ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) ) ) )
127	76, 124, 125, 126	syl3anc 1274	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) mod P ) = ( ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) mod P ) <-> P || ( ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) - ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) ) ) )
128	67	zcnd 9704	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. CC )
129	81, 72	zmulcld 9709	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) x. ( 2 x. y ) ) e. ZZ )
130	129	zcnd 9704	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) x. ( 2 x. y ) ) e. CC )
131	94, 88	zmulcld 9709	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( 2 x. x ) ) e. ZZ )
132	131	zcnd 9704	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( 2 x. x ) ) e. CC )
133	128, 130, 132	subdid 8689	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) = ( ( Q x. ( ( -u 1 ^ S ) x. ( 2 x. y ) ) ) - ( Q x. ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) )
134	81	zcnd 9704	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ S ) e. CC )
135	72	zcnd 9704	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. CC )
136	128, 134, 135	mul12d 8427	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( ( -u 1 ^ S ) x. ( 2 x. y ) ) ) = ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) )
137	94	zcnd 9704	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) e. CC )
138	88	zcnd 9704	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. CC )
139	128, 137, 138	mul12d 8427	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) = ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) )
140	136, 139	oveq12d 6070	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( Q x. ( ( -u 1 ^ S ) x. ( 2 x. y ) ) ) - ( Q x. ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) = ( ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) - ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) ) )
141	133, 140	eqtrd 2267	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) = ( ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) - ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) ) )
142	141	breq2d 4123	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( Q x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) <-> P || ( ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) - ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) ) ) )
143	3	adantr 276	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P =/= Q )
144		prmrp 12846	. . . . . . . . . . . . . 14 |- ( ( P e. Prime /\ Q e. Prime ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )
145	75, 65, 144	syl2anc 411	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )
146	143, 145	mpbird 167	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P gcd Q ) = 1 )
147		prmz 12812	. . . . . . . . . . . . . 14 |- ( P e. Prime -> P e. ZZ )
148	75, 147	syl 14	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. ZZ )
149	129, 131	zsubcld 9708	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) e. ZZ )
150		coprmdvds 12793	. . . . . . . . . . . . 13 |- ( ( P e. ZZ /\ Q e. ZZ /\ ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) e. ZZ ) -> ( ( P || ( Q x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) /\ ( P gcd Q ) = 1 ) -> P || ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) )
151	148, 67, 149, 150	syl3anc 1274	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P || ( Q x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) /\ ( P gcd Q ) = 1 ) -> P || ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) )
152	146, 151	mpan2d 428	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( Q x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) -> P || ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) )
153		dvdsmultr2 12523	. . . . . . . . . . . 12 |- ( ( P e. ZZ /\ ( -u 1 ^ R ) e. ZZ /\ ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) e. ZZ ) -> ( P || ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) -> P || ( ( -u 1 ^ R ) x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) ) )
154	148, 94, 149, 153	syl3anc 1274	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) -> P || ( ( -u 1 ^ R ) x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) ) )
155	137, 130, 132	subdid 8689	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) = ( ( ( -u 1 ^ R ) x. ( ( -u 1 ^ S ) x. ( 2 x. y ) ) ) - ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) )
156		neg1cn 9344	. . . . . . . . . . . . . . . . . . 19 |- -u 1 e. CC
157	156	a1i 9	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -u 1 e. CC )
158	157, 78, 91	expaddd 11041	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ ( R + S ) ) = ( ( -u 1 ^ R ) x. ( -u 1 ^ S ) ) )
159	158	oveq1d 6067	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) = ( ( ( -u 1 ^ R ) x. ( -u 1 ^ S ) ) x. ( 2 x. y ) ) )
160	137, 134, 135	mulassd 8299	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. ( -u 1 ^ S ) ) x. ( 2 x. y ) ) = ( ( -u 1 ^ R ) x. ( ( -u 1 ^ S ) x. ( 2 x. y ) ) ) )
161	159, 160	eqtr2d 2268	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( ( -u 1 ^ S ) x. ( 2 x. y ) ) ) = ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) )
162		ax-1cn 8222	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. CC
163		1ap0 8866	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 # 0
164		divneg2ap 9012	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 # 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) )
165	162, 162, 163, 164	mp3an 1374	. . . . . . . . . . . . . . . . . . . . . 22 |- -u ( 1 / 1 ) = ( 1 / -u 1 )
166		1div1e1 8980	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 1 / 1 ) = 1
167	166	negeqi 8469	. . . . . . . . . . . . . . . . . . . . . 22 |- -u ( 1 / 1 ) = -u 1
168	165, 167	eqtr3i 2257	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 / -u 1 ) = -u 1
169	168	oveq1i 6062	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 1 / -u 1 ) ^ R ) = ( -u 1 ^ R )
170		neg1ap0 9348	. . . . . . . . . . . . . . . . . . . . . 22 |- -u 1 # 0
171	170	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -u 1 # 0 )
172	157, 171, 54	exprecapd 11047	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 1 / -u 1 ) ^ R ) = ( 1 / ( -u 1 ^ R ) ) )
173	169, 172	eqtr3id 2281	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) = ( 1 / ( -u 1 ^ R ) ) )
174	173	oveq2d 6068	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) = ( ( -u 1 ^ R ) x. ( 1 / ( -u 1 ^ R ) ) ) )
175	157, 171, 54	expap0d 11045	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) # 0 )
176	137, 175	recidapd 9059	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( 1 / ( -u 1 ^ R ) ) ) = 1 )
177	174, 176	eqtrd 2267	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) = 1 )
178	177	oveq1d 6067	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) x. ( 2 x. x ) ) = ( 1 x. ( 2 x. x ) ) )
179	137, 137, 138	mulassd 8299	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) x. ( 2 x. x ) ) = ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) )
180	138	mullidd 8294	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 1 x. ( 2 x. x ) ) = ( 2 x. x ) )
181	178, 179, 180	3eqtr3d 2275	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) = ( 2 x. x ) )
182	161, 181	oveq12d 6070	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. ( ( -u 1 ^ S ) x. ( 2 x. y ) ) ) - ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) = ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) - ( 2 x. x ) ) )
183	155, 182	eqtrd 2267	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) = ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) - ( 2 x. x ) ) )
184	183	breq2d 4123	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( ( -u 1 ^ R ) x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) <-> P || ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) - ( 2 x. x ) ) ) )
185		eqcom 2236	. . . . . . . . . . . . . . . . 17 |- ( ( ( -u 1 x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) <-> ( ( 2 x. x ) mod P ) = ( ( -u 1 x. ( 2 x. y ) ) mod P ) )
186	135	mulm1d 8685	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 x. ( 2 x. y ) ) = -u ( 2 x. y ) )
187	186	oveq1d 6067	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 x. ( 2 x. y ) ) mod P ) = ( -u ( 2 x. y ) mod P ) )
188	187	eqeq2d 2246	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( 2 x. x ) mod P ) = ( ( -u 1 x. ( 2 x. y ) ) mod P ) <-> ( ( 2 x. x ) mod P ) = ( -u ( 2 x. y ) mod P ) ) )
189	185, 188	bitrid 192	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) <-> ( ( 2 x. x ) mod P ) = ( -u ( 2 x. y ) mod P ) ) )
190	72	znegcld 9705	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -u ( 2 x. y ) e. ZZ )
191		moddvds 12489	. . . . . . . . . . . . . . . . . 18 |- ( ( P e. NN /\ ( 2 x. x ) e. ZZ /\ -u ( 2 x. y ) e. ZZ ) -> ( ( ( 2 x. x ) mod P ) = ( -u ( 2 x. y ) mod P ) <-> P || ( ( 2 x. x ) - -u ( 2 x. y ) ) ) )
192	76, 88, 190, 191	syl3anc 1274	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( 2 x. x ) mod P ) = ( -u ( 2 x. y ) mod P ) <-> P || ( ( 2 x. x ) - -u ( 2 x. y ) ) ) )
193	46, 25	nnaddcld 9287	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) e. NN )
194	46	nnred 9252	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. RR )
195	70	zred 9703	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. RR )
196		oddprm 12961	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
197	74, 196	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P - 1 ) / 2 ) e. NN )
198	197	nnred 9252	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P - 1 ) / 2 ) e. RR )
199		elfzle2 10365	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x <_ ( ( P - 1 ) / 2 ) )
200	199	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x <_ ( ( P - 1 ) / 2 ) )
201		elfzle2 10365	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y <_ ( ( P - 1 ) / 2 ) )
202	201	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y <_ ( ( P - 1 ) / 2 ) )
203	194, 195, 198, 198, 200, 202	le2addd 8839	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) <_ ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) ) )
204	76	nnred 9252	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. RR )
205		peano2rem 8542	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( P e. RR -> ( P - 1 ) e. RR )
206	204, 205	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) e. RR )
207	206	recnd 8304	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) e. CC )
208	207	2halvesd 9486	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) ) = ( P - 1 ) )
209	203, 208	breqtrd 4137	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) <_ ( P - 1 ) )
210		peano2zm 9617	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( P e. ZZ -> ( P - 1 ) e. ZZ )
211		fznn 10427	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( P - 1 ) e. ZZ -> ( ( x + y ) e. ( 1 ... ( P - 1 ) ) <-> ( ( x + y ) e. NN /\ ( x + y ) <_ ( P - 1 ) ) ) )
212	148, 210, 211	3syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( x + y ) e. ( 1 ... ( P - 1 ) ) <-> ( ( x + y ) e. NN /\ ( x + y ) <_ ( P - 1 ) ) ) )
213	193, 209, 212	mpbir2and 953	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) e. ( 1 ... ( P - 1 ) ) )
214		fzm1ndvds 12546	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( P e. NN /\ ( x + y ) e. ( 1 ... ( P - 1 ) ) ) -> -. P || ( x + y ) )
215	76, 213, 214	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -. P || ( x + y ) )
216		eldifsni 3824	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( P e. ( Prime \ { 2 } ) -> P =/= 2 )
217	74, 216	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P =/= 2 )
218		2prm 12828	. . . . . . . . . . . . . . . . . . . . . . 23 |- 2 e. Prime
219		prmrp 12846	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( P e. Prime /\ 2 e. Prime ) -> ( ( P gcd 2 ) = 1 <-> P =/= 2 ) )
220	75, 218, 219	sylancl 413	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P gcd 2 ) = 1 <-> P =/= 2 ) )
221	217, 220	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P gcd 2 ) = 1 )
222	68	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 e. ZZ )
223	193	nnzd 9702	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) e. ZZ )
224		coprmdvds 12793	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( P e. ZZ /\ 2 e. ZZ /\ ( x + y ) e. ZZ ) -> ( ( P || ( 2 x. ( x + y ) ) /\ ( P gcd 2 ) = 1 ) -> P || ( x + y ) ) )
225	148, 222, 223, 224	syl3anc 1274	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P || ( 2 x. ( x + y ) ) /\ ( P gcd 2 ) = 1 ) -> P || ( x + y ) ) )
226	221, 225	mpan2d 428	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( 2 x. ( x + y ) ) -> P || ( x + y ) ) )
227	215, 226	mtod 669	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -. P || ( 2 x. ( x + y ) ) )
228	138, 135	subnegd 8593	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. x ) - -u ( 2 x. y ) ) = ( ( 2 x. x ) + ( 2 x. y ) ) )
229	86	zcnd 9704	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. CC )
230	70	zcnd 9704	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. CC )
231	98, 229, 230	adddid 8300	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. ( x + y ) ) = ( ( 2 x. x ) + ( 2 x. y ) ) )
232	228, 231	eqtr4d 2270	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. x ) - -u ( 2 x. y ) ) = ( 2 x. ( x + y ) ) )
233	232	breq2d 4123	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( ( 2 x. x ) - -u ( 2 x. y ) ) <-> P || ( 2 x. ( x + y ) ) ) )
234	227, 233	mtbird 680	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -. P || ( ( 2 x. x ) - -u ( 2 x. y ) ) )
235	234	pm2.21d 624	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( ( 2 x. x ) - -u ( 2 x. y ) ) -> ( 2 x. y ) = ( 2 x. x ) ) )
236	192, 235	sylbid 150	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( 2 x. x ) mod P ) = ( -u ( 2 x. y ) mod P ) -> ( 2 x. y ) = ( 2 x. x ) ) )
237	189, 236	sylbid 150	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) -> ( 2 x. y ) = ( 2 x. x ) ) )
238		oveq1 6059	. . . . . . . . . . . . . . . . . 18 |- ( ( -u 1 ^ ( R + S ) ) = -u 1 -> ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) = ( -u 1 x. ( 2 x. y ) ) )
239	238	oveq1d 6067	. . . . . . . . . . . . . . . . 17 |- ( ( -u 1 ^ ( R + S ) ) = -u 1 -> ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( -u 1 x. ( 2 x. y ) ) mod P ) )
240	239	eqeq1d 2243	. . . . . . . . . . . . . . . 16 |- ( ( -u 1 ^ ( R + S ) ) = -u 1 -> ( ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) <-> ( ( -u 1 x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) ) )
241	240	imbi1d 231	. . . . . . . . . . . . . . 15 |- ( ( -u 1 ^ ( R + S ) ) = -u 1 -> ( ( ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) -> ( 2 x. y ) = ( 2 x. x ) ) <-> ( ( ( -u 1 x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) -> ( 2 x. y ) = ( 2 x. x ) ) ) )
242	237, 241	syl5ibrcom 157	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ ( R + S ) ) = -u 1 -> ( ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) -> ( 2 x. y ) = ( 2 x. x ) ) ) )
243	135	mullidd 8294	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 1 x. ( 2 x. y ) ) = ( 2 x. y ) )
244	243	oveq1d 6067	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 1 x. ( 2 x. y ) ) mod P ) = ( ( 2 x. y ) mod P ) )
245		nnq 9968	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 x. y ) e. NN -> ( 2 x. y ) e. QQ )
246	26, 245	syl 14	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. QQ )
247		nnmulcl 9260	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 e. NN /\ y e. NN ) -> ( 2 x. y ) e. NN )
248	22, 25, 247	sylancr 414	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. NN )
249	248	nnnn0d 9555	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. NN0 )
250	249	nn0ge0d 9558	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 <_ ( 2 x. y ) )
251		2re 9309	. . . . . . . . . . . . . . . . . . . . . . 23 |- 2 e. RR
252	251	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 e. RR )
253		2pos 9330	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 < 2
254	253	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 < 2 )
255		lemuldiv2 9158	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. y ) <_ ( P - 1 ) <-> y <_ ( ( P - 1 ) / 2 ) ) )
256	195, 206, 252, 254, 255	syl112anc 1278	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. y ) <_ ( P - 1 ) <-> y <_ ( ( P - 1 ) / 2 ) ) )
257	202, 256	mpbird 167	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) <_ ( P - 1 ) )
258		zltlem1 9637	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 2 x. y ) e. ZZ /\ P e. ZZ ) -> ( ( 2 x. y ) < P <-> ( 2 x. y ) <_ ( P - 1 ) ) )
259	72, 148, 258	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. y ) < P <-> ( 2 x. y ) <_ ( P - 1 ) ) )
260	257, 259	mpbird 167	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) < P )
261		modqid 10715	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 2 x. y ) e. QQ /\ P e. QQ ) /\ ( 0 <_ ( 2 x. y ) /\ ( 2 x. y ) < P ) ) -> ( ( 2 x. y ) mod P ) = ( 2 x. y ) )
262	246, 110, 250, 260, 261	syl22anc 1275	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. y ) mod P ) = ( 2 x. y ) )
263	244, 262	eqtrd 2267	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 1 x. ( 2 x. y ) ) mod P ) = ( 2 x. y ) )
264		nnq 9968	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 x. x ) e. NN -> ( 2 x. x ) e. QQ )
265	47, 264	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. QQ )
266		nnmulcl 9260	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 e. NN /\ x e. NN ) -> ( 2 x. x ) e. NN )
267	22, 46, 266	sylancr 414	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. NN )
268	267	nnnn0d 9555	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. NN0 )
269	268	nn0ge0d 9558	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 <_ ( 2 x. x ) )
270		lemuldiv2 9158	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. x ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
271	194, 206, 252, 254, 270	syl112anc 1278	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. x ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
272	200, 271	mpbird 167	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) <_ ( P - 1 ) )
273		zltlem1 9637	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 2 x. x ) e. ZZ /\ P e. ZZ ) -> ( ( 2 x. x ) < P <-> ( 2 x. x ) <_ ( P - 1 ) ) )
274	88, 148, 273	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. x ) < P <-> ( 2 x. x ) <_ ( P - 1 ) ) )
275	272, 274	mpbird 167	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) < P )
276		modqid 10715	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 2 x. x ) e. QQ /\ P e. QQ ) /\ ( 0 <_ ( 2 x. x ) /\ ( 2 x. x ) < P ) ) -> ( ( 2 x. x ) mod P ) = ( 2 x. x ) )
277	265, 110, 269, 275, 276	syl22anc 1275	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. x ) mod P ) = ( 2 x. x ) )
278	263, 277	eqeq12d 2249	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( 1 x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) <-> ( 2 x. y ) = ( 2 x. x ) ) )
279	278	biimpd 144	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( 1 x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) -> ( 2 x. y ) = ( 2 x. x ) ) )
280		oveq1 6059	. . . . . . . . . . . . . . . . . 18 |- ( ( -u 1 ^ ( R + S ) ) = 1 -> ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) = ( 1 x. ( 2 x. y ) ) )
281	280	oveq1d 6067	. . . . . . . . . . . . . . . . 17 |- ( ( -u 1 ^ ( R + S ) ) = 1 -> ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( 1 x. ( 2 x. y ) ) mod P ) )
282	281	eqeq1d 2243	. . . . . . . . . . . . . . . 16 |- ( ( -u 1 ^ ( R + S ) ) = 1 -> ( ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) <-> ( ( 1 x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) ) )
283	282	imbi1d 231	. . . . . . . . . . . . . . 15 |- ( ( -u 1 ^ ( R + S ) ) = 1 -> ( ( ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) -> ( 2 x. y ) = ( 2 x. x ) ) <-> ( ( ( 1 x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) -> ( 2 x. y ) = ( 2 x. x ) ) ) )
284	279, 283	syl5ibrcom 157	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ ( R + S ) ) = 1 -> ( ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) -> ( 2 x. y ) = ( 2 x. x ) ) ) )
285	91, 78	nn0addcld 9559	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( R + S ) e. NN0 )
286	285	nn0zd 9701	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( R + S ) e. ZZ )
287		m1expcl2 10927	. . . . . . . . . . . . . . 15 |- ( ( R + S ) e. ZZ -> ( -u 1 ^ ( R + S ) ) e. { -u 1 , 1 } )
288		elpri 3714	. . . . . . . . . . . . . . 15 |- ( ( -u 1 ^ ( R + S ) ) e. { -u 1 , 1 } -> ( ( -u 1 ^ ( R + S ) ) = -u 1 \/ ( -u 1 ^ ( R + S ) ) = 1 ) )
289	286, 287, 288	3syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ ( R + S ) ) = -u 1 \/ ( -u 1 ^ ( R + S ) ) = 1 ) )
290	242, 284, 289	mpjaod 726	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) -> ( 2 x. y ) = ( 2 x. x ) ) )
291		zexpcl 10920	. . . . . . . . . . . . . . . 16 |- ( ( -u 1 e. ZZ /\ ( R + S ) e. NN0 ) -> ( -u 1 ^ ( R + S ) ) e. ZZ )
292	17, 285, 291	sylancr 414	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ ( R + S ) ) e. ZZ )
293	292, 72	zmulcld 9709	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) e. ZZ )
294		moddvds 12489	. . . . . . . . . . . . . 14 |- ( ( P e. NN /\ ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) e. ZZ /\ ( 2 x. x ) e. ZZ ) -> ( ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) <-> P || ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) - ( 2 x. x ) ) ) )
295	76, 293, 88, 294	syl3anc 1274	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( 2 x. x ) mod P ) <-> P || ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) - ( 2 x. x ) ) ) )
296	230, 229, 98, 99	mulcanapd 8937	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. y ) = ( 2 x. x ) <-> y = x ) )
297	290, 295, 296	3imtr3d 202	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) - ( 2 x. x ) ) -> y = x ) )
298	184, 297	sylbid 150	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( ( -u 1 ^ R ) x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) -> y = x ) )
299	152, 154, 298	3syld 57	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( Q x. ( ( ( -u 1 ^ S ) x. ( 2 x. y ) ) - ( ( -u 1 ^ R ) x. ( 2 x. x ) ) ) ) -> y = x ) )
300	142, 299	sylbird 170	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) - ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) ) -> y = x ) )
301	127, 300	sylbid 150	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( ( -u 1 ^ S ) x. ( Q x. ( 2 x. y ) ) ) mod P ) = ( ( ( -u 1 ^ R ) x. ( Q x. ( 2 x. x ) ) ) mod P ) -> y = x ) )
302	123, 301	sylbid 150	. . . . . . 7 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( ( -u 1 ^ S ) x. S ) mod P ) = ( ( ( -u 1 ^ R ) x. R ) mod P ) -> y = x ) )
303	101, 302	sylbid 150	. . . . . 6 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) = ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) -> y = x ) )
304	63, 303	sylbid 150	. . . . 5 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( M ` y ) = ( M ` x ) -> y = x ) )
305	304	ralrimivva 2626	. . . 4 |- ( ph -> A. y e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( M ` y ) = ( M ` x ) -> y = x ) )
306		nfmpt1 4205	. . . . . . . . . 10 |- F/_ x ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
307	5, 306	nfcxfr 2383	. . . . . . . . 9 |- F/_ x M
308		nfcv 2386	. . . . . . . . 9 |- F/_ x y
309	307, 308	nffv 5682	. . . . . . . 8 |- F/_ x ( M ` y )
310		nfcv 2386	. . . . . . . . 9 |- F/_ x z
311	307, 310	nffv 5682	. . . . . . . 8 |- F/_ x ( M ` z )
312	309, 311	nfeq 2394	. . . . . . 7 |- F/ x ( M ` y ) = ( M ` z )
313		nfv 1577	. . . . . . 7 |- F/ x y = z
314	312, 313	nfim 1621	. . . . . 6 |- F/ x ( ( M ` y ) = ( M ` z ) -> y = z )
315		nfv 1577	. . . . . 6 |- F/ z ( ( M ` y ) = ( M ` x ) -> y = x )
316		fveq2 5672	. . . . . . . 8 |- ( z = x -> ( M ` z ) = ( M ` x ) )
317	316	eqeq2d 2246	. . . . . . 7 |- ( z = x -> ( ( M ` y ) = ( M ` z ) <-> ( M ` y ) = ( M ` x ) ) )
318		equequ2 1761	. . . . . . 7 |- ( z = x -> ( y = z <-> y = x ) )
319	317, 318	imbi12d 234	. . . . . 6 |- ( z = x -> ( ( ( M ` y ) = ( M ` z ) -> y = z ) <-> ( ( M ` y ) = ( M ` x ) -> y = x ) ) )
320	314, 315, 319	cbvralw 2773	. . . . 5 |- ( A. z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( M ` y ) = ( M ` z ) -> y = z ) <-> A. x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( M ` y ) = ( M ` x ) -> y = x ) )
321	320	ralbii 2550	. . . 4 |- ( A. y e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( M ` y ) = ( M ` z ) -> y = z ) <-> A. y e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( M ` y ) = ( M ` x ) -> y = x ) )
322	305, 321	sylibr 134	. . 3 |- ( ph -> A. y e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( M ` y ) = ( M ` z ) -> y = z ) )
323		dff13 5943	. . 3 |- ( M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( 1 ... ( ( P - 1 ) / 2 ) ) <-> ( M : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) /\ A. y e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( M ` y ) = ( M ` z ) -> y = z ) ) )
324	6, 322, 323	sylanbrc 417	. 2 |- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( 1 ... ( ( P - 1 ) / 2 ) ) )
325		1zzd 9606	. . . . 5 |- ( ph -> 1 e. ZZ )
326	1, 196	syl 14	. . . . . 6 |- ( ph -> ( ( P - 1 ) / 2 ) e. NN )
327	326	nnzd 9702	. . . . 5 |- ( ph -> ( ( P - 1 ) / 2 ) e. ZZ )
328	325, 327	fzfigd 10797	. . . 4 |- ( ph -> ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin )
329		enrefg 7005	. . . 4 |- ( ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin -> ( 1 ... ( ( P - 1 ) / 2 ) ) ~~ ( 1 ... ( ( P - 1 ) / 2 ) ) )
330	328, 329	syl 14	. . 3 |- ( ph -> ( 1 ... ( ( P - 1 ) / 2 ) ) ~~ ( 1 ... ( ( P - 1 ) / 2 ) ) )
331		f1finf1o 7219	. . 3 |- ( ( ( 1 ... ( ( P - 1 ) / 2 ) ) ~~ ( 1 ... ( ( P - 1 ) / 2 ) ) /\ ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin ) -> ( M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( 1 ... ( ( P - 1 ) / 2 ) ) <-> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) ) )
332	330, 328, 331	syl2anc 411	. 2 |- ( ph -> ( M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( 1 ... ( ( P - 1 ) / 2 ) ) <-> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) ) )
333	324, 332	mpbid 147	1 |- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 716   = wceq 1398   e. wcel 2205   =/= wne 2414   A.wral 2522   _Vcvv 2815   \ cdif 3210   {csn 3691   {cpr 3692   class class class wbr 4111   |-> cmpt 4173   -->wf 5350   -1-1->wf1 5351   -1-1-onto->wf1o 5353   ` cfv 5354  (class class class)co 6052   ~~ cen 6975   Fincfn 6977   CCcc 8127   RRcr 8128   0cc0 8129   1c1 8130   + caddc 8132   x. cmul 8134   < clt 8310   <_ cle 8311   - cmin 8446   -ucneg 8447   # cap 8857   / cdiv 8948   NNcn 9239   2c2 9290   NN0cn0 9498   ZZcz 9579   QQcq 9954   ...cfz 10345   mod cmo 10688   ^cexp 10904   || cdvds 12477   gcd cgcd 12653   Primecprime 12808

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-coll 4227  ax-sep 4230  ax-nul 4238  ax-pow 4289  ax-pr 4324  ax-un 4556  ax-setind 4661  ax-iinf 4712  ax-cnex 8220  ax-resscn 8221  ax-1cn 8222  ax-1re 8223  ax-icn 8224  ax-addcl 8225  ax-addrcl 8226  ax-mulcl 8227  ax-mulrcl 8228  ax-addcom 8229  ax-mulcom 8230  ax-addass 8231  ax-mulass 8232  ax-distr 8233  ax-i2m1 8234  ax-0lt1 8235  ax-1rid 8236  ax-0id 8237  ax-rnegex 8238  ax-precex 8239  ax-cnre 8240  ax-pre-ltirr 8241  ax-pre-ltwlin 8242  ax-pre-lttrn 8243  ax-pre-apti 8244  ax-pre-ltadd 8245  ax-pre-mulgt0 8246  ax-pre-mulext 8247  ax-arch 8248  ax-caucvg 8249

This theorem depends on definitions:  df-bi 117  df-stab 839  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-xor 1421  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-reu 2529  df-rmo 2530  df-rab 2531  df-v 2817  df-sbc 3045  df-csb 3141  df-dif 3215  df-un 3217  df-in 3219  df-ss 3226  df-nul 3511  df-if 3623  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-int 3952  df-iun 3995  df-br 4112  df-opab 4174  df-mpt 4175  df-tr 4211  df-id 4416  df-po 4419  df-iso 4420  df-iord 4489  df-on 4491  df-ilim 4492  df-suc 4494  df-iom 4715  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-rn 4762  df-res 4763  df-ima 4764  df-iota 5314  df-fun 5356  df-fn 5357  df-f 5358  df-f1 5359  df-fo 5360  df-f1o 5361  df-fv 5362  df-riota 6005  df-ov 6055  df-oprab 6056  df-mpo 6057  df-1st 6336  df-2nd 6337  df-recs 6538  df-frec 6624  df-1o 6649  df-2o 6650  df-er 6769  df-en 6978  df-fin 6980  df-sup 7277  df-pnf 8312  df-mnf 8313  df-xr 8314  df-ltxr 8315  df-le 8316  df-sub 8448  df-neg 8449  df-reap 8851  df-ap 8858  df-div 8949  df-inn 9240  df-2 9298  df-3 9299  df-4 9300  df-n0 9499  df-z 9580  df-uz 9857  df-q 9955  df-rp 9990  df-fz 10346  df-fzo 10481  df-fl 10634  df-mod 10689  df-seqfrec 10814  df-exp 10905  df-cj 11531  df-re 11532  df-im 11533  df-rsqrt 11687  df-abs 11688  df-dvds 12478  df-gcd 12654  df-prm 12809

This theorem is referenced by:  lgseisenlem3  15962