Theorem lgseisenlem1 15960

Description: Lemma for lgseisen 15964. If R ( u ) = ( Q x. u ) mod P and M ( u ) = ( -u 1 ^ R ( u ) ) x. R ( u ), then for any even 1 <_ u <_ P - 1, M ( u ) is also an even integer 1 <_ M ( u ) <_ P - 1. To simplify these statements, we divide all the even numbers by 2, so that it becomes the statement that M ( x / 2 ) = ( -u 1 ^ R ( x / 2 ) ) x. R ( x / 2 ) / 2 is an integer between 1 and ( P - 1 ) / 2. (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 ) )

Assertion

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

Distinct variable groups:   x, P   ph, x   x, Q

Allowed substitution hints:   R( x)   M( x)

Proof of Theorem lgseisenlem1

Step	Hyp	Ref	Expression
1		1zzd 9606	. . 3 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 1 e. ZZ )
2		lgseisen.1	. . . . . 6 |- ( ph -> P e. ( Prime \ { 2 } ) )
3	2	adantr 276	. . . . 5 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. ( Prime \ { 2 } ) )
4		oddprm 12961	. . . . 5 |- ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
5	3, 4	syl 14	. . . 4 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P - 1 ) / 2 ) e. NN )
6	5	nnzd 9702	. . 3 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P - 1 ) / 2 ) e. ZZ )
7		neg1cn 9344	. . . . . . . . . . . . 13 |- -u 1 e. CC
8	7	a1i 9	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> -u 1 e. CC )
9		neg1ap0 9348	. . . . . . . . . . . . 13 |- -u 1 # 0
10	9	a1i 9	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> -u 1 # 0 )
11		2z 9607	. . . . . . . . . . . . 13 |- 2 e. ZZ
12	11	a1i 9	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> 2 e. ZZ )
13		simpr 110	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( R / 2 ) e. ZZ )
14		expmulzap 10951	. . . . . . . . . . . 12 |- ( ( ( -u 1 e. CC /\ -u 1 # 0 ) /\ ( 2 e. ZZ /\ ( R / 2 ) e. ZZ ) ) -> ( -u 1 ^ ( 2 x. ( R / 2 ) ) ) = ( ( -u 1 ^ 2 ) ^ ( R / 2 ) ) )
15	8, 10, 12, 13, 14	syl22anc 1275	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( -u 1 ^ ( 2 x. ( R / 2 ) ) ) = ( ( -u 1 ^ 2 ) ^ ( R / 2 ) ) )
16		lgseisen.4	. . . . . . . . . . . . . . . . . 18 |- R = ( ( Q x. ( 2 x. x ) ) mod P )
17		lgseisen.2	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> Q e. ( Prime \ { 2 } ) )
18	17	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. ( Prime \ { 2 } ) )
19	18	eldifad 3224	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. Prime )
20		prmz 12812	. . . . . . . . . . . . . . . . . . . . 21 |- ( Q e. Prime -> Q e. ZZ )
21	19, 20	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. ZZ )
22		elfzelz 10362	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. ZZ )
23	22	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. ZZ )
24		zmulcl 9633	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 e. ZZ /\ x e. ZZ ) -> ( 2 x. x ) e. ZZ )
25	11, 23, 24	sylancr 414	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. ZZ )
26	21, 25	zmulcld 9709	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. ZZ )
27	3	eldifad 3224	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. Prime )
28		prmnn 12811	. . . . . . . . . . . . . . . . . . . 20 |- ( P e. Prime -> P e. NN )
29	27, 28	syl 14	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. NN )
30		zmodfz 10712	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Q x. ( 2 x. x ) ) e. ZZ /\ P e. NN ) -> ( ( Q x. ( 2 x. x ) ) mod P ) e. ( 0 ... ( P - 1 ) ) )
31	26, 29, 30	syl2anc 411	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q x. ( 2 x. x ) ) mod P ) e. ( 0 ... ( P - 1 ) ) )
32	16, 31	eqeltrid 2321	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. ( 0 ... ( P - 1 ) ) )
33		elfznn0 10452	. . . . . . . . . . . . . . . . 17 |- ( R e. ( 0 ... ( P - 1 ) ) -> R e. NN0 )
34	32, 33	syl 14	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. NN0 )
35	34	nn0zd 9701	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. ZZ )
36	35	zcnd 9704	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. CC )
37	36	adantr 276	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> R e. CC )
38		2cnd 9312	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> 2 e. CC )
39		2ap0 9332	. . . . . . . . . . . . . 14 |- 2 # 0
40	39	a1i 9	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> 2 # 0 )
41	37, 38, 40	divcanap2d 9068	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( 2 x. ( R / 2 ) ) = R )
42	41	oveq2d 6068	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( -u 1 ^ ( 2 x. ( R / 2 ) ) ) = ( -u 1 ^ R ) )
43		neg1sqe1 11000	. . . . . . . . . . . . 13 |- ( -u 1 ^ 2 ) = 1
44	43	oveq1i 6062	. . . . . . . . . . . 12 |- ( ( -u 1 ^ 2 ) ^ ( R / 2 ) ) = ( 1 ^ ( R / 2 ) )
45		1exp 10934	. . . . . . . . . . . . 13 |- ( ( R / 2 ) e. ZZ -> ( 1 ^ ( R / 2 ) ) = 1 )
46	45	adantl 277	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( 1 ^ ( R / 2 ) ) = 1 )
47	44, 46	eqtrid 2279	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( -u 1 ^ 2 ) ^ ( R / 2 ) ) = 1 )
48	15, 42, 47	3eqtr3d 2275	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( -u 1 ^ R ) = 1 )
49	48	oveq1d 6067	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( -u 1 ^ R ) x. R ) = ( 1 x. R ) )
50	37	mullidd 8294	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( 1 x. R ) = R )
51	49, 50	eqtrd 2267	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( -u 1 ^ R ) x. R ) = R )
52	51	oveq1d 6067	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = ( R mod P ) )
53		zq 9961	. . . . . . . . . 10 |- ( R e. ZZ -> R e. QQ )
54	35, 53	syl 14	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. QQ )
55		nnq 9968	. . . . . . . . . 10 |- ( P e. NN -> P e. QQ )
56	29, 55	syl 14	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. QQ )
57	34	nn0ge0d 9558	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 <_ R )
58		zq 9961	. . . . . . . . . . . 12 |- ( ( Q x. ( 2 x. x ) ) e. ZZ -> ( Q x. ( 2 x. x ) ) e. QQ )
59	26, 58	syl 14	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. QQ )
60	29	nngt0d 9283	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 < P )
61		modqlt 10699	. . . . . . . . . . 11 |- ( ( ( Q x. ( 2 x. x ) ) e. QQ /\ P e. QQ /\ 0 < P ) -> ( ( Q x. ( 2 x. x ) ) mod P ) < P )
62	59, 56, 60, 61	syl3anc 1274	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q x. ( 2 x. x ) ) mod P ) < P )
63	16, 62	eqbrtrid 4146	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R < P )
64		modqid 10715	. . . . . . . . 9 |- ( ( ( R e. QQ /\ P e. QQ ) /\ ( 0 <_ R /\ R < P ) ) -> ( R mod P ) = R )
65	54, 56, 57, 63, 64	syl22anc 1275	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( R mod P ) = R )
66	65	adantr 276	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( R mod P ) = R )
67	52, 66	eqtrd 2267	. . . . . 6 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = R )
68	67	oveq1d 6067	. . . . 5 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) = ( R / 2 ) )
69	68, 13	eqeltrd 2311	. . . 4 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( R / 2 ) e. ZZ ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ZZ )
70	29	nncnd 9253	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. CC )
71	70	mullidd 8294	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 1 x. P ) = P )
72	71	oveq2d 6068	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u R + ( 1 x. P ) ) = ( -u R + P ) )
73	34	nn0red 9556	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. RR )
74	73	renegcld 8655	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u R e. RR )
75	74	recnd 8304	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u R e. CC )
76	70, 75	addcomd 8426	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P + -u R ) = ( -u R + P ) )
77	70, 36	negsubd 8592	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P + -u R ) = ( P - R ) )
78	72, 76, 77	3eqtr2d 2273	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u R + ( 1 x. P ) ) = ( P - R ) )
79	78	oveq1d 6067	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u R + ( 1 x. P ) ) mod P ) = ( ( P - R ) mod P ) )
80		qnegcl 9971	. . . . . . . . . . . 12 |- ( R e. QQ -> -u R e. QQ )
81	54, 80	syl 14	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u R e. QQ )
82		modqcyc 10725	. . . . . . . . . . 11 |- ( ( ( -u R e. QQ /\ 1 e. ZZ ) /\ ( P e. QQ /\ 0 < P ) ) -> ( ( -u R + ( 1 x. P ) ) mod P ) = ( -u R mod P ) )
83	81, 1, 56, 60, 82	syl22anc 1275	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u R + ( 1 x. P ) ) mod P ) = ( -u R mod P ) )
84		qsubcl 9973	. . . . . . . . . . . 12 |- ( ( P e. QQ /\ R e. QQ ) -> ( P - R ) e. QQ )
85	56, 54, 84	syl2anc 411	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - R ) e. QQ )
86	29	nnred 9252	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. RR )
87	73, 86, 63	ltled 8394	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R <_ P )
88	86, 73	subge0d 8811	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 0 <_ ( P - R ) <-> R <_ P ) )
89	87, 88	mpbird 167	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 <_ ( P - R ) )
90		2nn 9401	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 e. NN
91		elfznn 10391	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. NN )
92	91	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. NN )
93		nnmulcl 9260	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 e. NN /\ x e. NN ) -> ( 2 x. x ) e. NN )
94	90, 92, 93	sylancr 414	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. NN )
95		elfzle2 10365	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x <_ ( ( P - 1 ) / 2 ) )
96	95	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x <_ ( ( P - 1 ) / 2 ) )
97	92	nnred 9252	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. RR )
98		prmuz2 12832	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
99		uz2m1nn 9940	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( P e. ( ZZ>= ` 2 ) -> ( P - 1 ) e. NN )
100	27, 98, 99	3syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. NN )
101	100	nnred 9252	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. RR )
102		2re 9309	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 2 e. RR
103	102	a1i 9	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 2 e. RR )
104		2pos 9330	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 < 2
105	104	a1i 9	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 < 2 )
106		lemuldiv2 9158	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. x ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
107	97, 101, 103, 105, 106	syl112anc 1278	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( 2 x. x ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
108	96, 107	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) <_ ( P - 1 ) )
109		prmz 12812	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( P e. Prime -> P e. ZZ )
110	27, 109	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. ZZ )
111		peano2zm 9617	. . . . . . . . . . . . . . . . . . . . . 22 |- ( P e. ZZ -> ( P - 1 ) e. ZZ )
112		fznn 10427	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( P - 1 ) e. ZZ -> ( ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) <-> ( ( 2 x. x ) e. NN /\ ( 2 x. x ) <_ ( P - 1 ) ) ) )
113	110, 111, 112	3syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) <-> ( ( 2 x. x ) e. NN /\ ( 2 x. x ) <_ ( P - 1 ) ) ) )
114	94, 108, 113	mpbir2and 953	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) )
115		fzm1ndvds 12546	. . . . . . . . . . . . . . . . . . . 20 |- ( ( P e. NN /\ ( 2 x. x ) e. ( 1 ... ( P - 1 ) ) ) -> -. P || ( 2 x. x ) )
116	29, 114, 115	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || ( 2 x. x ) )
117		lgseisen.3	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> P =/= Q )
118	117	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P =/= Q )
119		prmrp 12846	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( P e. Prime /\ Q e. Prime ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )
120	27, 19, 119	syl2anc 411	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )
121	118, 120	mpbird 167	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P gcd Q ) = 1 )
122		coprmdvds 12793	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( P e. ZZ /\ Q e. ZZ /\ ( 2 x. x ) e. ZZ ) -> ( ( P || ( Q x. ( 2 x. x ) ) /\ ( P gcd Q ) = 1 ) -> P || ( 2 x. x ) ) )
123	110, 21, 25, 122	syl3anc 1274	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P || ( Q x. ( 2 x. x ) ) /\ ( P gcd Q ) = 1 ) -> P || ( 2 x. x ) ) )
124	121, 123	mpan2d 428	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P || ( Q x. ( 2 x. x ) ) -> P || ( 2 x. x ) ) )
125	116, 124	mtod 669	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || ( Q x. ( 2 x. x ) ) )
126		dvdsval3 12481	. . . . . . . . . . . . . . . . . . 19 |- ( ( P e. NN /\ ( Q x. ( 2 x. x ) ) e. ZZ ) -> ( P || ( Q x. ( 2 x. x ) ) <-> ( ( Q x. ( 2 x. x ) ) mod P ) = 0 ) )
127	29, 26, 126	syl2anc 411	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P || ( Q x. ( 2 x. x ) ) <-> ( ( Q x. ( 2 x. x ) ) mod P ) = 0 ) )
128	125, 127	mtbid 679	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. ( ( Q x. ( 2 x. x ) ) mod P ) = 0 )
129	16	eqeq1i 2242	. . . . . . . . . . . . . . . . 17 |- ( R = 0 <-> ( ( Q x. ( 2 x. x ) ) mod P ) = 0 )
130	128, 129	sylnibr 684	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. R = 0 )
131	100	nnnn0d 9555	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. NN0 )
132		nn0uz 9892	. . . . . . . . . . . . . . . . . . . 20 |- NN0 = ( ZZ>= ` 0 )
133	131, 132	eleqtrdi 2327	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. ( ZZ>= ` 0 ) )
134		elfzp12 10437	. . . . . . . . . . . . . . . . . . 19 |- ( ( P - 1 ) e. ( ZZ>= ` 0 ) -> ( R e. ( 0 ... ( P - 1 ) ) <-> ( R = 0 \/ R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) ) )
135	133, 134	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( R e. ( 0 ... ( P - 1 ) ) <-> ( R = 0 \/ R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) ) )
136	32, 135	mpbid 147	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( R = 0 \/ R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) )
137	136	ord 732	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -. R = 0 -> R e. ( ( 0 + 1 ) ... ( P - 1 ) ) ) )
138	130, 137	mpd 13	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. ( ( 0 + 1 ) ... ( P - 1 ) ) )
139		1e0p1 9753	. . . . . . . . . . . . . . . 16 |- 1 = ( 0 + 1 )
140	139	oveq1i 6062	. . . . . . . . . . . . . . 15 |- ( 1 ... ( P - 1 ) ) = ( ( 0 + 1 ) ... ( P - 1 ) )
141	138, 140	eleqtrrdi 2328	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. ( 1 ... ( P - 1 ) ) )
142		elfznn 10391	. . . . . . . . . . . . . 14 |- ( R e. ( 1 ... ( P - 1 ) ) -> R e. NN )
143	141, 142	syl 14	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. NN )
144	143	nnrpd 10030	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. RR+ )
145	86, 144	ltsubrpd 10065	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - R ) < P )
146		modqid 10715	. . . . . . . . . . 11 |- ( ( ( ( P - R ) e. QQ /\ P e. QQ ) /\ ( 0 <_ ( P - R ) /\ ( P - R ) < P ) ) -> ( ( P - R ) mod P ) = ( P - R ) )
147	85, 56, 89, 145, 146	syl22anc 1275	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P - R ) mod P ) = ( P - R ) )
148	79, 83, 147	3eqtr3d 2275	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u R mod P ) = ( P - R ) )
149	148	adantr 276	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( -u R mod P ) = ( P - R ) )
150		ax-1cn 8222	. . . . . . . . . . . . . 14 |- 1 e. CC
151	150	a1i 9	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 1 e. CC )
152	143	adantr 276	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> R e. NN )
153		2ne0 9331	. . . . . . . . . . . . . . . 16 |- 2 =/= 0
154	35	peano2zd 9706	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( R + 1 ) e. ZZ )
155		dvdsval2 12480	. . . . . . . . . . . . . . . 16 |- ( ( 2 e. ZZ /\ 2 =/= 0 /\ ( R + 1 ) e. ZZ ) -> ( 2 || ( R + 1 ) <-> ( ( R + 1 ) / 2 ) e. ZZ ) )
156	11, 153, 154, 155	mp3an12i 1378	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 || ( R + 1 ) <-> ( ( R + 1 ) / 2 ) e. ZZ ) )
157	156	biimpar 297	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 2 || ( R + 1 ) )
158	35	adantr 276	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> R e. ZZ )
159	90	a1i 9	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 2 e. NN )
160		1lt2 9409	. . . . . . . . . . . . . . . 16 |- 1 < 2
161	160	a1i 9	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 1 < 2 )
162		ndvdsp1 12622	. . . . . . . . . . . . . . 15 |- ( ( R e. ZZ /\ 2 e. NN /\ 1 < 2 ) -> ( 2 || R -> -. 2 || ( R + 1 ) ) )
163	158, 159, 161, 162	syl3anc 1274	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( 2 || R -> -. 2 || ( R + 1 ) ) )
164	157, 163	mt2d 630	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> -. 2 || R )
165		oexpneg 12567	. . . . . . . . . . . . 13 |- ( ( 1 e. CC /\ R e. NN /\ -. 2 || R ) -> ( -u 1 ^ R ) = -u ( 1 ^ R ) )
166	151, 152, 164, 165	syl3anc 1274	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( -u 1 ^ R ) = -u ( 1 ^ R ) )
167		1exp 10934	. . . . . . . . . . . . . 14 |- ( R e. ZZ -> ( 1 ^ R ) = 1 )
168	158, 167	syl 14	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( 1 ^ R ) = 1 )
169	168	negeqd 8470	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> -u ( 1 ^ R ) = -u 1 )
170	166, 169	eqtrd 2267	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( -u 1 ^ R ) = -u 1 )
171	170	oveq1d 6067	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( -u 1 ^ R ) x. R ) = ( -u 1 x. R ) )
172	36	adantr 276	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> R e. CC )
173	172	mulm1d 8685	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( -u 1 x. R ) = -u R )
174	171, 173	eqtrd 2267	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( -u 1 ^ R ) x. R ) = -u R )
175	174	oveq1d 6067	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = ( -u R mod P ) )
176	70	adantr 276	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> P e. CC )
177	176, 172, 151	pnpcan2d 8624	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P + 1 ) - ( R + 1 ) ) = ( P - R ) )
178	149, 175, 177	3eqtr4d 2277	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = ( ( P + 1 ) - ( R + 1 ) ) )
179	178	oveq1d 6067	. . . . . 6 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) = ( ( ( P + 1 ) - ( R + 1 ) ) / 2 ) )
180		peano2cn 8410	. . . . . . . 8 |- ( P e. CC -> ( P + 1 ) e. CC )
181	176, 180	syl 14	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( P + 1 ) e. CC )
182		peano2cn 8410	. . . . . . . 8 |- ( R e. CC -> ( R + 1 ) e. CC )
183	172, 182	syl 14	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( R + 1 ) e. CC )
184		2cnd 9312	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 2 e. CC )
185	39	a1i 9	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> 2 # 0 )
186	181, 183, 184, 185	divsubdirapd 9106	. . . . . 6 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( P + 1 ) - ( R + 1 ) ) / 2 ) = ( ( ( P + 1 ) / 2 ) - ( ( R + 1 ) / 2 ) ) )
187	179, 186	eqtrd 2267	. . . . 5 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) = ( ( ( P + 1 ) / 2 ) - ( ( R + 1 ) / 2 ) ) )
188	176, 151, 184	subadd23d 8608	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P - 1 ) + 2 ) = ( P + ( 2 - 1 ) ) )
189		2m1e1 9357	. . . . . . . . . . 11 |- ( 2 - 1 ) = 1
190	189	oveq2i 6063	. . . . . . . . . 10 |- ( P + ( 2 - 1 ) ) = ( P + 1 )
191	188, 190	eqtr2di 2284	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( P + 1 ) = ( ( P - 1 ) + 2 ) )
192	191	oveq1d 6067	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P + 1 ) / 2 ) = ( ( ( P - 1 ) + 2 ) / 2 ) )
193	100	nncnd 9253	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P - 1 ) e. CC )
194	193	adantr 276	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( P - 1 ) e. CC )
195	194, 184, 184, 185	divdirapd 9105	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( P - 1 ) + 2 ) / 2 ) = ( ( ( P - 1 ) / 2 ) + ( 2 / 2 ) ) )
196		2div2e1 9372	. . . . . . . . . 10 |- ( 2 / 2 ) = 1
197	196	oveq2i 6063	. . . . . . . . 9 |- ( ( ( P - 1 ) / 2 ) + ( 2 / 2 ) ) = ( ( ( P - 1 ) / 2 ) + 1 )
198	195, 197	eqtrdi 2283	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( P - 1 ) + 2 ) / 2 ) = ( ( ( P - 1 ) / 2 ) + 1 ) )
199	192, 198	eqtrd 2267	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P + 1 ) / 2 ) = ( ( ( P - 1 ) / 2 ) + 1 ) )
200	6	adantr 276	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P - 1 ) / 2 ) e. ZZ )
201	200	peano2zd 9706	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( P - 1 ) / 2 ) + 1 ) e. ZZ )
202	199, 201	eqeltrd 2311	. . . . . 6 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( P + 1 ) / 2 ) e. ZZ )
203		simpr 110	. . . . . 6 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( R + 1 ) / 2 ) e. ZZ )
204	202, 203	zsubcld 9708	. . . . 5 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( P + 1 ) / 2 ) - ( ( R + 1 ) / 2 ) ) e. ZZ )
205	187, 204	eqeltrd 2311	. . . 4 |- ( ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) /\ ( ( R + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ZZ )
206		zeo 9686	. . . . 5 |- ( R e. ZZ -> ( ( R / 2 ) e. ZZ \/ ( ( R + 1 ) / 2 ) e. ZZ ) )
207	35, 206	syl 14	. . . 4 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( R / 2 ) e. ZZ \/ ( ( R + 1 ) / 2 ) e. ZZ ) )
208	69, 205, 207	mpjaodan 806	. . 3 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ZZ )
209		m1expcl 10928	. . . . . . . . . 10 |- ( R e. ZZ -> ( -u 1 ^ R ) e. ZZ )
210	35, 209	syl 14	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) e. ZZ )
211	210, 35	zmulcld 9709	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. R ) e. ZZ )
212	211, 29	zmodcld 10711	. . . . . . 7 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN0 )
213	212	nn0red 9556	. . . . . 6 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. RR )
214		fzm1ndvds 12546	. . . . . . . . . . . 12 |- ( ( P e. NN /\ R e. ( 1 ... ( P - 1 ) ) ) -> -. P || R )
215	29, 141, 214	syl2anc 411	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || R )
216		1ap0 8866	. . . . . . . . . . . . . . . . . . . 20 |- 1 # 0
217		divneg2ap 9012	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 # 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) )
218	150, 150, 216, 217	mp3an 1374	. . . . . . . . . . . . . . . . . . 19 |- -u ( 1 / 1 ) = ( 1 / -u 1 )
219		1div1e1 8980	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 / 1 ) = 1
220	219	negeqi 8469	. . . . . . . . . . . . . . . . . . 19 |- -u ( 1 / 1 ) = -u 1
221	218, 220	eqtr3i 2257	. . . . . . . . . . . . . . . . . 18 |- ( 1 / -u 1 ) = -u 1
222	221	oveq1i 6062	. . . . . . . . . . . . . . . . 17 |- ( ( 1 / -u 1 ) ^ R ) = ( -u 1 ^ R )
223	7	a1i 9	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u 1 e. CC )
224	9	a1i 9	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u 1 # 0 )
225	223, 224, 35	exprecapd 11047	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( 1 / -u 1 ) ^ R ) = ( 1 / ( -u 1 ^ R ) ) )
226	222, 225	eqtr3id 2281	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) = ( 1 / ( -u 1 ^ R ) ) )
227	226	oveq2d 6068	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) = ( ( -u 1 ^ R ) x. ( 1 / ( -u 1 ^ R ) ) ) )
228	210	zcnd 9704	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) e. CC )
229	223, 224, 35	expap0d 11045	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) # 0 )
230	228, 229	recidapd 9059	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. ( 1 / ( -u 1 ^ R ) ) ) = 1 )
231	227, 230	eqtrd 2267	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) = 1 )
232	231	oveq1d 6067	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) x. R ) = ( 1 x. R ) )
233	228, 228, 36	mulassd 8299	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) x. R ) = ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) )
234	36	mullidd 8294	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 1 x. R ) = R )
235	232, 233, 234	3eqtr3d 2275	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) = R )
236	235	breq2d 4123	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P || ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) <-> P || R ) )
237	215, 236	mtbird 680	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) )
238		dvdsmultr2 12523	. . . . . . . . . . 11 |- ( ( P e. ZZ /\ ( -u 1 ^ R ) e. ZZ /\ ( ( -u 1 ^ R ) x. R ) e. ZZ ) -> ( P || ( ( -u 1 ^ R ) x. R ) -> P || ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) ) )
239	110, 210, 211, 238	syl3anc 1274	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P || ( ( -u 1 ^ R ) x. R ) -> P || ( ( -u 1 ^ R ) x. ( ( -u 1 ^ R ) x. R ) ) ) )
240	237, 239	mtod 669	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || ( ( -u 1 ^ R ) x. R ) )
241		dvdsval3 12481	. . . . . . . . . 10 |- ( ( P e. NN /\ ( ( -u 1 ^ R ) x. R ) e. ZZ ) -> ( P || ( ( -u 1 ^ R ) x. R ) <-> ( ( ( -u 1 ^ R ) x. R ) mod P ) = 0 ) )
242	29, 211, 241	syl2anc 411	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P || ( ( -u 1 ^ R ) x. R ) <-> ( ( ( -u 1 ^ R ) x. R ) mod P ) = 0 ) )
243	240, 242	mtbid 679	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. ( ( ( -u 1 ^ R ) x. R ) mod P ) = 0 )
244		elnn0 9500	. . . . . . . . 9 |- ( ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN0 <-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN \/ ( ( ( -u 1 ^ R ) x. R ) mod P ) = 0 ) )
245	212, 244	sylib 122	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN \/ ( ( ( -u 1 ^ R ) x. R ) mod P ) = 0 ) )
246	243, 245	ecased 1386	. . . . . . 7 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN )
247	246	nngt0d 9283	. . . . . 6 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 < ( ( ( -u 1 ^ R ) x. R ) mod P ) )
248	213, 103, 247, 105	divgt0d 9211	. . . . 5 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 0 < ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
249		elnnz 9589	. . . . 5 |- ( ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. NN <-> ( ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ZZ /\ 0 < ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) )
250	208, 248, 249	sylanbrc 417	. . . 4 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. NN )
251	250	nnge1d 9282	. . 3 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 1 <_ ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
252		zmodfz 10712	. . . . . 6 |- ( ( ( ( -u 1 ^ R ) x. R ) e. ZZ /\ P e. NN ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. ( 0 ... ( P - 1 ) ) )
253	211, 29, 252	syl2anc 411	. . . . 5 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. ( 0 ... ( P - 1 ) ) )
254		elfzle2 10365	. . . . 5 |- ( ( ( ( -u 1 ^ R ) x. R ) mod P ) e. ( 0 ... ( P - 1 ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) <_ ( P - 1 ) )
255	253, 254	syl 14	. . . 4 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) <_ ( P - 1 ) )
256		lediv1 9145	. . . . 5 |- ( ( ( ( ( -u 1 ^ R ) x. R ) mod P ) e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) <_ ( P - 1 ) <-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) <_ ( ( P - 1 ) / 2 ) ) )
257	213, 101, 103, 105, 256	syl112anc 1278	. . . 4 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) <_ ( P - 1 ) <-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) <_ ( ( P - 1 ) / 2 ) ) )
258	255, 257	mpbid 147	. . 3 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) <_ ( ( P - 1 ) / 2 ) )
259	1, 6, 208, 251, 258	elfzd 10353	. 2 |- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) )
260		lgseisen.5	. 2 |- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
261	259, 260	fmptd 5833	1 |- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 716   = wceq 1398   e. wcel 2205   =/= wne 2414   \ cdif 3210   {csn 3691   class class class wbr 4111   |-> cmpt 4173   -->wf 5350   ` cfv 5354  (class class class)co 6052   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   ZZ>=cuz 9856   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-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-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:  lgseisenlem2  15961  lgseisenlem3  15962