Theorem lgseisenlem2 25101

Description: Lemma for lgseisen 25104. 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 25100	. . 3 |- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) )
7		oveq2 6658	. . . . . . . . . . . . . . . 16 |- ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
8	7	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( x = y -> ( Q x. ( 2 x. x ) ) = ( Q x. ( 2 x. y ) ) )
9	8	oveq1d 6665	. . . . . . . . . . . . . 14 |- ( x = y -> ( ( Q x. ( 2 x. x ) ) mod P ) = ( ( Q x. ( 2 x. y ) ) mod P ) )
10		lgseisen.6	. . . . . . . . . . . . . 14 |- S = ( ( Q x. ( 2 x. y ) ) mod P )
11	9, 4, 10	3eqtr4g 2681	. . . . . . . . . . . . 13 |- ( x = y -> R = S )
12	11	oveq2d 6666	. . . . . . . . . . . 12 |- ( x = y -> ( -u 1 ^ R ) = ( -u 1 ^ S ) )
13	12, 11	oveq12d 6668	. . . . . . . . . . 11 |- ( x = y -> ( ( -u 1 ^ R ) x. R ) = ( ( -u 1 ^ S ) x. S ) )
14	13	oveq1d 6665	. . . . . . . . . 10 |- ( x = y -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = ( ( ( -u 1 ^ S ) x. S ) mod P ) )
15	14	oveq1d 6665	. . . . . . . . 9 |- ( x = y -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) = ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) )
16		ovex 6678	. . . . . . . . 9 |- ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) e. _V
17	15, 5, 16	fvmpt 6282	. . . . . . . 8 |- ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( M ` y ) = ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) )
18	17	ad2antrl 764	. . . . . . 7 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( M ` y ) = ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) )
19		ovex 6678	. . . . . . . . 9 |- ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. _V
20	5	fvmpt2 6291	. . . . . . . . 9 |- ( ( 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 ) )
21	19, 20	mpan2 707	. . . . . . . 8 |- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( M ` x ) = ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
22	21	ad2antll 765	. . . . . . 7 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( M ` x ) = ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
23	18, 22	eqeq12d 2637	. . . . . 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 ) ) )
24	2	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. ( Prime \ { 2 } ) )
25	24	eldifad 3586	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. Prime )
26		prmz 15389	. . . . . . . . . . . . . . . . 17 |- ( Q e. Prime -> Q e. ZZ )
27	25, 26	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. ZZ )
28		2z 11409	. . . . . . . . . . . . . . . . 17 |- 2 e. ZZ
29		elfzelz 12342	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y e. ZZ )
30	29	ad2antrl 764	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. ZZ )
31		zmulcl 11426	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. ZZ /\ y e. ZZ ) -> ( 2 x. y ) e. ZZ )
32	28, 30, 31	sylancr 695	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. ZZ )
33	27, 32	zmulcld 11488	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. y ) ) e. ZZ )
34	1	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. ( Prime \ { 2 } ) )
35	34	eldifad 3586	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. Prime )
36		prmnn 15388	. . . . . . . . . . . . . . . 16 |- ( P e. Prime -> P e. NN )
37	35, 36	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. NN )
38	33, 37	zmodcld 12691	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( Q x. ( 2 x. y ) ) mod P ) e. NN0 )
39	10, 38	syl5eqel 2705	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> S e. NN0 )
40	39	nn0zd 11480	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> S e. ZZ )
41		m1expcl 12883	. . . . . . . . . . . 12 |- ( S e. ZZ -> ( -u 1 ^ S ) e. ZZ )
42	40, 41	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ S ) e. ZZ )
43	42, 40	zmulcld 11488	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) x. S ) e. ZZ )
44	43, 37	zmodcld 12691	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ S ) x. S ) mod P ) e. NN0 )
45	44	nn0cnd 11353	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ S ) x. S ) mod P ) e. CC )
46		elfzelz 12342	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. ZZ )
47	46	ad2antll 765	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. ZZ )
48		zmulcl 11426	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. ZZ /\ x e. ZZ ) -> ( 2 x. x ) e. ZZ )
49	28, 47, 48	sylancr 695	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. ZZ )
50	27, 49	zmulcld 11488	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. x ) ) e. ZZ )
51	50, 37	zmodcld 12691	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( Q x. ( 2 x. x ) ) mod P ) e. NN0 )
52	4, 51	syl5eqel 2705	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> R e. NN0 )
53	52	nn0zd 11480	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> R e. ZZ )
54		m1expcl 12883	. . . . . . . . . . . 12 |- ( R e. ZZ -> ( -u 1 ^ R ) e. ZZ )
55	53, 54	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) e. ZZ )
56	55, 53	zmulcld 11488	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. R ) e. ZZ )
57	56, 37	zmodcld 12691	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. NN0 )
58	57	nn0cnd 11353	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. CC )
59		2cnd 11093	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 e. CC )
60		2ne0 11113	. . . . . . . . 9 |- 2 =/= 0
61	60	a1i 11	. . . . . . . 8 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 =/= 0 )
62		div11 10713	. . . . . . . 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 ) ) )
63	45, 58, 59, 61, 62	syl112anc 1330	. . . . . . 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 ) ) )
64	37	nnrpd 11870	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. RR+ )
65		eqidd 2623	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) mod P ) = ( ( -u 1 ^ S ) mod P ) )
66	10	oveq1i 6660	. . . . . . . . . . 11 |- ( S mod P ) = ( ( ( Q x. ( 2 x. y ) ) mod P ) mod P )
67	33	zred 11482	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. y ) ) e. RR )
68		modabs2 12704	. . . . . . . . . . . 12 |- ( ( ( Q x. ( 2 x. y ) ) e. RR /\ P e. RR+ ) -> ( ( ( Q x. ( 2 x. y ) ) mod P ) mod P ) = ( ( Q x. ( 2 x. y ) ) mod P ) )
69	67, 64, 68	syl2anc 693	. . . . . . . . . . 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 ) )
70	66, 69	syl5eq 2668	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( S mod P ) = ( ( Q x. ( 2 x. y ) ) mod P ) )
71	42, 42, 40, 33, 64, 65, 70	modmul12d 12724	. . . . . . . . 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 ) )
72		eqidd 2623	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) mod P ) = ( ( -u 1 ^ R ) mod P ) )
73	4	oveq1i 6660	. . . . . . . . . . 11 |- ( R mod P ) = ( ( ( Q x. ( 2 x. x ) ) mod P ) mod P )
74	50	zred 11482	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. x ) ) e. RR )
75		modabs2 12704	. . . . . . . . . . . 12 |- ( ( ( Q x. ( 2 x. x ) ) e. RR /\ P e. RR+ ) -> ( ( ( Q x. ( 2 x. x ) ) mod P ) mod P ) = ( ( Q x. ( 2 x. x ) ) mod P ) )
76	74, 64, 75	syl2anc 693	. . . . . . . . . . 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 ) )
77	73, 76	syl5eq 2668	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( R mod P ) = ( ( Q x. ( 2 x. x ) ) mod P ) )
78	55, 55, 53, 50, 64, 72, 77	modmul12d 12724	. . . . . . . . 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 ) )
79	71, 78	eqeq12d 2637	. . . . . . . 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 ) ) )
80	42, 33	zmulcld 11488	. . . . . . . . . 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 )
81	55, 50	zmulcld 11488	. . . . . . . . . 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 )
82		moddvds 14991	. . . . . . . . . 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 ) ) ) ) ) )
83	37, 80, 81, 82	syl3anc 1326	. . . . . . . . 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 ) ) ) ) ) )
84	27	zcnd 11483	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. CC )
85	42, 32	zmulcld 11488	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) x. ( 2 x. y ) ) e. ZZ )
86	85	zcnd 11483	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) x. ( 2 x. y ) ) e. CC )
87	55, 49	zmulcld 11488	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( 2 x. x ) ) e. ZZ )
88	87	zcnd 11483	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( 2 x. x ) ) e. CC )
89	84, 86, 88	subdid 10486	. . . . . . . . . . . 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 ) ) ) ) )
90	42	zcnd 11483	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ S ) e. CC )
91	32	zcnd 11483	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. CC )
92	84, 90, 91	mul12d 10245	. . . . . . . . . . . . 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 ) ) ) )
93	55	zcnd 11483	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) e. CC )
94	49	zcnd 11483	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. CC )
95	84, 93, 94	mul12d 10245	. . . . . . . . . . . . 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 ) ) ) )
96	92, 95	oveq12d 6668	. . . . . . . . . . . 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 ) ) ) ) )
97	89, 96	eqtrd 2656	. . . . . . . . . . 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 ) ) ) ) )
98	97	breq2d 4665	. . . . . . . . . 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 ) ) ) ) ) )
99	3	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P =/= Q )
100		prmrp 15424	. . . . . . . . . . . . . 14 |- ( ( P e. Prime /\ Q e. Prime ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )
101	35, 25, 100	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) )
102	99, 101	mpbird 247	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P gcd Q ) = 1 )
103		prmz 15389	. . . . . . . . . . . . . 14 |- ( P e. Prime -> P e. ZZ )
104	35, 103	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. ZZ )
105	85, 87	zsubcld 11487	. . . . . . . . . . . . 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 )
106		coprmdvds 15366	. . . . . . . . . . . . 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 ) ) ) ) )
107	104, 27, 105, 106	syl3anc 1326	. . . . . . . . . . . 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 ) ) ) ) )
108	102, 107	mpan2d 710	. . . . . . . . . . 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 ) ) ) ) )
109		dvdsmultr2 15021	. . . . . . . . . . . 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 ) ) ) ) ) )
110	104, 55, 105, 109	syl3anc 1326	. . . . . . . . . . 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 ) ) ) ) ) )
111	93, 86, 88	subdid 10486	. . . . . . . . . . . . . 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 ) ) ) ) )
112		neg1cn 11124	. . . . . . . . . . . . . . . . . . 19 |- -u 1 e. CC
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -u 1 e. CC )
114	113, 39, 52	expaddd 13010	. . . . . . . . . . . . . . . . 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 ) ) )
115	114	oveq1d 6665	. . . . . . . . . . . . . . . 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 ) ) )
116	93, 90, 91	mulassd 10063	. . . . . . . . . . . . . . . 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 ) ) ) )
117	115, 116	eqtr2d 2657	. . . . . . . . . . . . . . 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 ) ) )
118		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. CC
119		ax-1ne0 10005	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 =/= 0
120		divneg2 10749	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 1 e. CC /\ 1 e. CC /\ 1 =/= 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) )
121	118, 118, 119, 120	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . 22 |- -u ( 1 / 1 ) = ( 1 / -u 1 )
122		1div1e1 10717	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 1 / 1 ) = 1
123	122	negeqi 10274	. . . . . . . . . . . . . . . . . . . . . 22 |- -u ( 1 / 1 ) = -u 1
124	121, 123	eqtr3i 2646	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 / -u 1 ) = -u 1
125	124	oveq1i 6660	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 1 / -u 1 ) ^ R ) = ( -u 1 ^ R )
126		neg1ne0 11126	. . . . . . . . . . . . . . . . . . . . . 22 |- -u 1 =/= 0
127	126	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -u 1 =/= 0 )
128	113, 127, 53	exprecd 13016	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 1 / -u 1 ) ^ R ) = ( 1 / ( -u 1 ^ R ) ) )
129	125, 128	syl5eqr 2670	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) = ( 1 / ( -u 1 ^ R ) ) )
130	129	oveq2d 6666	. . . . . . . . . . . . . . . . . 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 ) ) ) )
131	113, 127, 53	expne0d 13014	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) =/= 0 )
132	93, 131	recidd 10796	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( 1 / ( -u 1 ^ R ) ) ) = 1 )
133	130, 132	eqtrd 2656	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) = 1 )
134	133	oveq1d 6665	. . . . . . . . . . . . . . . 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 ) ) )
135	93, 93, 94	mulassd 10063	. . . . . . . . . . . . . . . 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 ) ) ) )
136	94	mulid2d 10058	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 1 x. ( 2 x. x ) ) = ( 2 x. x ) )
137	134, 135, 136	3eqtr3d 2664	. . . . . . . . . . . . . . 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 ) )
138	117, 137	oveq12d 6668	. . . . . . . . . . . . . 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 ) ) )
139	111, 138	eqtrd 2656	. . . . . . . . . . . . 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 ) ) )
140	139	breq2d 4665	. . . . . . . . . . . 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 ) ) ) )
141		eqcom 2629	. . . . . . . . . . . . . . . . 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 ) )
142	91	mulm1d 10482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 x. ( 2 x. y ) ) = -u ( 2 x. y ) )
143	142	oveq1d 6665	. . . . . . . . . . . . . . . . . 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 ) )
144	143	eqeq2d 2632	. . . . . . . . . . . . . . . . 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 ) ) )
145	141, 144	syl5bb 272	. . . . . . . . . . . . . . . 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 ) ) )
146	32	znegcld 11484	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -u ( 2 x. y ) e. ZZ )
147		moddvds 14991	. . . . . . . . . . . . . . . . . 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 ) ) ) )
148	37, 49, 146, 147	syl3anc 1326	. . . . . . . . . . . . . . . . 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 ) ) ) )
149		elfznn 12370	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. NN )
150	149	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. NN )
151		elfznn 12370	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y e. NN )
152	151	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. NN )
153	150, 152	nnaddcld 11067	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) e. NN )
154	150	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. RR )
155	30	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. RR )
156		oddprm 15515	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
157	34, 156	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P - 1 ) / 2 ) e. NN )
158	157	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P - 1 ) / 2 ) e. RR )
159		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x <_ ( ( P - 1 ) / 2 ) )
160	159	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x <_ ( ( P - 1 ) / 2 ) )
161		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y <_ ( ( P - 1 ) / 2 ) )
162	161	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y <_ ( ( P - 1 ) / 2 ) )
163	154, 155, 158, 158, 160, 162	le2addd 10646	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) <_ ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) ) )
164	37	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. RR )
165		peano2rem 10348	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( P e. RR -> ( P - 1 ) e. RR )
166	164, 165	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) e. RR )
167	166	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) e. CC )
168	167	2halvesd 11278	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) ) = ( P - 1 ) )
169	163, 168	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) <_ ( P - 1 ) )
170		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( P e. ZZ -> ( P - 1 ) e. ZZ )
171		fznn 12408	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( P - 1 ) e. ZZ -> ( ( x + y ) e. ( 1 ... ( P - 1 ) ) <-> ( ( x + y ) e. NN /\ ( x + y ) <_ ( P - 1 ) ) ) )
172	104, 170, 171	3syl 18	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
173	153, 169, 172	mpbir2and 957	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) e. ( 1 ... ( P - 1 ) ) )
174		fzm1ndvds 15044	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( P e. NN /\ ( x + y ) e. ( 1 ... ( P - 1 ) ) ) -> -. P || ( x + y ) )
175	37, 173, 174	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -. P || ( x + y ) )
176		eldifsni 4320	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( P e. ( Prime \ { 2 } ) -> P =/= 2 )
177	34, 176	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P =/= 2 )
178		2prm 15405	. . . . . . . . . . . . . . . . . . . . . . 23 |- 2 e. Prime
179		prmrp 15424	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( P e. Prime /\ 2 e. Prime ) -> ( ( P gcd 2 ) = 1 <-> P =/= 2 ) )
180	35, 178, 179	sylancl 694	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P gcd 2 ) = 1 <-> P =/= 2 ) )
181	177, 180	mpbird 247	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P gcd 2 ) = 1 )
182	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 e. ZZ )
183	153	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) e. ZZ )
184		coprmdvds 15366	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( P e. ZZ /\ 2 e. ZZ /\ ( x + y ) e. ZZ ) -> ( ( P || ( 2 x. ( x + y ) ) /\ ( P gcd 2 ) = 1 ) -> P || ( x + y ) ) )
185	104, 182, 183, 184	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
186	181, 185	mpan2d 710	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( 2 x. ( x + y ) ) -> P || ( x + y ) ) )
187	175, 186	mtod 189	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -. P || ( 2 x. ( x + y ) ) )
188	94, 91	subnegd 10399	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
189	47	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. CC )
190	30	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. CC )
191	59, 189, 190	adddid 10064	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. ( x + y ) ) = ( ( 2 x. x ) + ( 2 x. y ) ) )
192	188, 191	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . 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 ) ) )
193	192	breq2d 4665	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
194	187, 193	mtbird 315	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -. P || ( ( 2 x. x ) - -u ( 2 x. y ) ) )
195	194	pm2.21d 118	. . . . . . . . . . . . . . . . 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 ) ) )
196	148, 195	sylbid 230	. . . . . . . . . . . . . . . 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 ) ) )
197	145, 196	sylbid 230	. . . . . . . . . . . . . . 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 ) ) )
198		oveq1 6657	. . . . . . . . . . . . . . . . . 18 |- ( ( -u 1 ^ ( R + S ) ) = -u 1 -> ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) = ( -u 1 x. ( 2 x. y ) ) )
199	198	oveq1d 6665	. . . . . . . . . . . . . . . . 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 ) )
200	199	eqeq1d 2624	. . . . . . . . . . . . . . . 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 ) ) )
201	200	imbi1d 331	. . . . . . . . . . . . . . 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 ) ) ) )
202	197, 201	syl5ibrcom 237	. . . . . . . . . . . . . 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 ) ) ) )
203	91	mulid2d 10058	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 1 x. ( 2 x. y ) ) = ( 2 x. y ) )
204	203	oveq1d 6665	. . . . . . . . . . . . . . . . . 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 ) )
205	32	zred 11482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. RR )
206		2nn 11185	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 e. NN
207		nnmulcl 11043	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 e. NN /\ y e. NN ) -> ( 2 x. y ) e. NN )
208	206, 152, 207	sylancr 695	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. NN )
209	208	nnnn0d 11351	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. NN0 )
210	209	nn0ge0d 11354	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 <_ ( 2 x. y ) )
211		2re 11090	. . . . . . . . . . . . . . . . . . . . . . 23 |- 2 e. RR
212	211	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 e. RR )
213		2pos 11112	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 < 2
214	213	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 < 2 )
215		lemuldiv2 10904	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. y ) <_ ( P - 1 ) <-> y <_ ( ( P - 1 ) / 2 ) ) )
216	155, 166, 212, 214, 215	syl112anc 1330	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. y ) <_ ( P - 1 ) <-> y <_ ( ( P - 1 ) / 2 ) ) )
217	162, 216	mpbird 247	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) <_ ( P - 1 ) )
218		zltlem1 11430	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 2 x. y ) e. ZZ /\ P e. ZZ ) -> ( ( 2 x. y ) < P <-> ( 2 x. y ) <_ ( P - 1 ) ) )
219	32, 104, 218	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. y ) < P <-> ( 2 x. y ) <_ ( P - 1 ) ) )
220	217, 219	mpbird 247	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) < P )
221		modid 12695	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 2 x. y ) e. RR /\ P e. RR+ ) /\ ( 0 <_ ( 2 x. y ) /\ ( 2 x. y ) < P ) ) -> ( ( 2 x. y ) mod P ) = ( 2 x. y ) )
222	205, 64, 210, 220, 221	syl22anc 1327	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. y ) mod P ) = ( 2 x. y ) )
223	204, 222	eqtrd 2656	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 1 x. ( 2 x. y ) ) mod P ) = ( 2 x. y ) )
224	49	zred 11482	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. RR )
225		nnmulcl 11043	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 e. NN /\ x e. NN ) -> ( 2 x. x ) e. NN )
226	206, 150, 225	sylancr 695	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. NN )
227	226	nnnn0d 11351	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. NN0 )
228	227	nn0ge0d 11354	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 <_ ( 2 x. x ) )
229		lemuldiv2 10904	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. x ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
230	154, 166, 212, 214, 229	syl112anc 1330	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. x ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
231	160, 230	mpbird 247	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) <_ ( P - 1 ) )
232		zltlem1 11430	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 2 x. x ) e. ZZ /\ P e. ZZ ) -> ( ( 2 x. x ) < P <-> ( 2 x. x ) <_ ( P - 1 ) ) )
233	49, 104, 232	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. x ) < P <-> ( 2 x. x ) <_ ( P - 1 ) ) )
234	231, 233	mpbird 247	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) < P )
235		modid 12695	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 2 x. x ) e. RR /\ P e. RR+ ) /\ ( 0 <_ ( 2 x. x ) /\ ( 2 x. x ) < P ) ) -> ( ( 2 x. x ) mod P ) = ( 2 x. x ) )
236	224, 64, 228, 234, 235	syl22anc 1327	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. x ) mod P ) = ( 2 x. x ) )
237	223, 236	eqeq12d 2637	. . . . . . . . . . . . . . . 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 ) ) )
238	237	biimpd 219	. . . . . . . . . . . . . . 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 ) ) )
239		oveq1 6657	. . . . . . . . . . . . . . . . . 18 |- ( ( -u 1 ^ ( R + S ) ) = 1 -> ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) = ( 1 x. ( 2 x. y ) ) )
240	239	oveq1d 6665	. . . . . . . . . . . . . . . . 17 |- ( ( -u 1 ^ ( R + S ) ) = 1 -> ( ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) mod P ) = ( ( 1 x. ( 2 x. y ) ) mod P ) )
241	240	eqeq1d 2624	. . . . . . . . . . . . . . . 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 ) ) )
242	241	imbi1d 331	. . . . . . . . . . . . . . 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 ) ) ) )
243	238, 242	syl5ibrcom 237	. . . . . . . . . . . . . 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 ) ) ) )
244	52, 39	nn0addcld 11355	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( R + S ) e. NN0 )
245	244	nn0zd 11480	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( R + S ) e. ZZ )
246		m1expcl2 12882	. . . . . . . . . . . . . . 15 |- ( ( R + S ) e. ZZ -> ( -u 1 ^ ( R + S ) ) e. { -u 1 , 1 } )
247		elpri 4197	. . . . . . . . . . . . . . 15 |- ( ( -u 1 ^ ( R + S ) ) e. { -u 1 , 1 } -> ( ( -u 1 ^ ( R + S ) ) = -u 1 \/ ( -u 1 ^ ( R + S ) ) = 1 ) )
248	245, 246, 247	3syl 18	. . . . . . . . . . . . . 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 ) )
249	202, 243, 248	mpjaod 396	. . . . . . . . . . . . 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 ) ) )
250		neg1z 11413	. . . . . . . . . . . . . . . 16 |- -u 1 e. ZZ
251		zexpcl 12875	. . . . . . . . . . . . . . . 16 |- ( ( -u 1 e. ZZ /\ ( R + S ) e. NN0 ) -> ( -u 1 ^ ( R + S ) ) e. ZZ )
252	250, 244, 251	sylancr 695	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ ( R + S ) ) e. ZZ )
253	252, 32	zmulcld 11488	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) e. ZZ )
254		moddvds 14991	. . . . . . . . . . . . . 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 ) ) ) )
255	37, 253, 49, 254	syl3anc 1326	. . . . . . . . . . . . 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 ) ) ) )
256	190, 189, 59, 61	mulcand 10660	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 2 x. y ) = ( 2 x. x ) <-> y = x ) )
257	249, 255, 256	3imtr3d 282	. . . . . . . . . . . 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 ) )
258	140, 257	sylbid 230	. . . . . . . . . . 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 ) )
259	108, 110, 258	3syld 60	. . . . . . . . . 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 ) )
260	98, 259	sylbird 250	. . . . . . . . 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 ) )
261	83, 260	sylbid 230	. . . . . . . 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 ) )
262	79, 261	sylbid 230	. . . . . . 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 ) )
263	63, 262	sylbid 230	. . . . . 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 ) )
264	23, 263	sylbid 230	. . . . 5 |- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( M ` y ) = ( M ` x ) -> y = x ) )
265	264	ralrimivva 2971	. . . 4 |- ( ph -> A. y e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( M ` y ) = ( M ` x ) -> y = x ) )
266		nfmpt1 4747	. . . . . . . . . 10 |- F/_ x ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) )
267	5, 266	nfcxfr 2762	. . . . . . . . 9 |- F/_ x M
268		nfcv 2764	. . . . . . . . 9 |- F/_ x y
269	267, 268	nffv 6198	. . . . . . . 8 |- F/_ x ( M ` y )
270		nfcv 2764	. . . . . . . . 9 |- F/_ x z
271	267, 270	nffv 6198	. . . . . . . 8 |- F/_ x ( M ` z )
272	269, 271	nfeq 2776	. . . . . . 7 |- F/ x ( M ` y ) = ( M ` z )
273		nfv 1843	. . . . . . 7 |- F/ x y = z
274	272, 273	nfim 1825	. . . . . 6 |- F/ x ( ( M ` y ) = ( M ` z ) -> y = z )
275		nfv 1843	. . . . . 6 |- F/ z ( ( M ` y ) = ( M ` x ) -> y = x )
276		fveq2 6191	. . . . . . . 8 |- ( z = x -> ( M ` z ) = ( M ` x ) )
277	276	eqeq2d 2632	. . . . . . 7 |- ( z = x -> ( ( M ` y ) = ( M ` z ) <-> ( M ` y ) = ( M ` x ) ) )
278		equequ2 1953	. . . . . . 7 |- ( z = x -> ( y = z <-> y = x ) )
279	277, 278	imbi12d 334	. . . . . 6 |- ( z = x -> ( ( ( M ` y ) = ( M ` z ) -> y = z ) <-> ( ( M ` y ) = ( M ` x ) -> y = x ) ) )
280	274, 275, 279	cbvral 3167	. . . . 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 ) )
281	280	ralbii 2980	. . . 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 ) )
282	265, 281	sylibr 224	. . 3 |- ( ph -> A. y e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( M ` y ) = ( M ` z ) -> y = z ) )
283		dff13 6512	. . 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 ) ) )
284	6, 282, 283	sylanbrc 698	. 2 |- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( 1 ... ( ( P - 1 ) / 2 ) ) )
285		ovex 6678	. . . 4 |- ( 1 ... ( ( P - 1 ) / 2 ) ) e. _V
286	285	enref 7988	. . 3 |- ( 1 ... ( ( P - 1 ) / 2 ) ) ~~ ( 1 ... ( ( P - 1 ) / 2 ) )
287		fzfi 12771	. . 3 |- ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin
288		f1finf1o 8187	. . 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 ) ) ) )
289	286, 287, 288	mp2an 708	. 2 |- ( M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( 1 ... ( ( P - 1 ) / 2 ) ) <-> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) )
290	284, 289	sylib 208	1 |- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   _Vcvv 3200   \ cdif 3571   {csn 4177   {cpr 4179   class class class wbr 4653   |-> cmpt 4729   -->wf 5884   -1-1->wf1 5885   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   ~~ cen 7952   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   - cmin 10266   -ucneg 10267   / cdiv 10684   NNcn 11020   2c2 11070   NN0cn0 11292   ZZcz 11377   RR+crp 11832   ...cfz 12326   mod cmo 12668   ^cexp 12860   || cdvds 14983   gcd cgcd 15216   Primecprime 15385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-fz 12327  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-dvds 14984  df-gcd 15217  df-prm 15386

This theorem is referenced by:  lgseisenlem3  25102