Step |
Hyp |
Ref |
Expression |
1 |
|
lgseisen.1 |
|- ( ph -> P e. ( Prime \ { 2 } ) ) |
2 |
|
lgseisen.2 |
|- ( ph -> Q e. ( Prime \ { 2 } ) ) |
3 |
|
lgseisen.3 |
|- ( ph -> P =/= Q ) |
4 |
|
lgseisen.4 |
|- R = ( ( Q x. ( 2 x. x ) ) mod P ) |
5 |
|
lgseisen.5 |
|- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) |
6 |
|
lgseisen.6 |
|- S = ( ( Q x. ( 2 x. y ) ) mod P ) |
7 |
1 2 3 4 5
|
lgseisenlem1 |
|- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) ) |
8 |
|
oveq2 |
|- ( x = y -> ( 2 x. x ) = ( 2 x. y ) ) |
9 |
8
|
oveq2d |
|- ( x = y -> ( Q x. ( 2 x. x ) ) = ( Q x. ( 2 x. y ) ) ) |
10 |
9
|
oveq1d |
|- ( x = y -> ( ( Q x. ( 2 x. x ) ) mod P ) = ( ( Q x. ( 2 x. y ) ) mod P ) ) |
11 |
10 4 6
|
3eqtr4g |
|- ( x = y -> R = S ) |
12 |
11
|
oveq2d |
|- ( x = y -> ( -u 1 ^ R ) = ( -u 1 ^ S ) ) |
13 |
12 11
|
oveq12d |
|- ( x = y -> ( ( -u 1 ^ R ) x. R ) = ( ( -u 1 ^ S ) x. S ) ) |
14 |
13
|
oveq1d |
|- ( x = y -> ( ( ( -u 1 ^ R ) x. R ) mod P ) = ( ( ( -u 1 ^ S ) x. S ) mod P ) ) |
15 |
14
|
oveq1d |
|- ( x = y -> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) = ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) ) |
16 |
|
ovex |
|- ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) e. _V |
17 |
15 5 16
|
fvmpt |
|- ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( M ` y ) = ( ( ( ( -u 1 ^ S ) x. S ) mod P ) / 2 ) ) |
18 |
17
|
ad2antrl |
|- ( ( 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 |
|- ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) e. _V |
20 |
5
|
fvmpt2 |
|- ( ( 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 |
|- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( M ` x ) = ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) |
22 |
21
|
ad2antll |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. ( Prime \ { 2 } ) ) |
25 |
24
|
eldifad |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. Prime ) |
26 |
|
prmz |
|- ( Q e. Prime -> Q e. ZZ ) |
27 |
25 26
|
syl |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. ZZ ) |
28 |
|
2z |
|- 2 e. ZZ |
29 |
|
elfzelz |
|- ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y e. ZZ ) |
30 |
29
|
ad2antrl |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. ZZ ) |
31 |
|
zmulcl |
|- ( ( 2 e. ZZ /\ y e. ZZ ) -> ( 2 x. y ) e. ZZ ) |
32 |
28 30 31
|
sylancr |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. ZZ ) |
33 |
27 32
|
zmulcld |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. y ) ) e. ZZ ) |
34 |
1
|
adantr |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. ( Prime \ { 2 } ) ) |
35 |
34
|
eldifad |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. Prime ) |
36 |
|
prmnn |
|- ( P e. Prime -> P e. NN ) |
37 |
35 36
|
syl |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. NN ) |
38 |
33 37
|
zmodcld |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( Q x. ( 2 x. y ) ) mod P ) e. NN0 ) |
39 |
6 38
|
eqeltrid |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> S e. NN0 ) |
40 |
39
|
nn0zd |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> S e. ZZ ) |
41 |
|
m1expcl |
|- ( S e. ZZ -> ( -u 1 ^ S ) e. ZZ ) |
42 |
40 41
|
syl |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ S ) e. ZZ ) |
43 |
42 40
|
zmulcld |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) x. S ) e. ZZ ) |
44 |
43 37
|
zmodcld |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ S ) x. S ) mod P ) e. CC ) |
46 |
|
elfzelz |
|- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. ZZ ) |
47 |
46
|
ad2antll |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. ZZ ) |
48 |
|
zmulcl |
|- ( ( 2 e. ZZ /\ x e. ZZ ) -> ( 2 x. x ) e. ZZ ) |
49 |
28 47 48
|
sylancr |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. ZZ ) |
50 |
27 49
|
zmulcld |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. x ) ) e. ZZ ) |
51 |
50 37
|
zmodcld |
|- ( ( 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
|
eqeltrid |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> R e. NN0 ) |
53 |
52
|
nn0zd |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> R e. ZZ ) |
54 |
|
m1expcl |
|- ( R e. ZZ -> ( -u 1 ^ R ) e. ZZ ) |
55 |
53 54
|
syl |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) e. ZZ ) |
56 |
55 53
|
zmulcld |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. R ) e. ZZ ) |
57 |
56 37
|
zmodcld |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( -u 1 ^ R ) x. R ) mod P ) e. CC ) |
59 |
|
2cnd |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 e. CC ) |
60 |
|
2ne0 |
|- 2 =/= 0 |
61 |
60
|
a1i |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 =/= 0 ) |
62 |
|
div11 |
|- ( ( ( ( ( -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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. RR+ ) |
65 |
|
eqidd |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ S ) mod P ) = ( ( -u 1 ^ S ) mod P ) ) |
66 |
6
|
oveq1i |
|- ( S mod P ) = ( ( ( Q x. ( 2 x. y ) ) mod P ) mod P ) |
67 |
33
|
zred |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. y ) ) e. RR ) |
68 |
|
modabs2 |
|- ( ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( R mod P ) = ( ( ( Q x. ( 2 x. x ) ) mod P ) mod P ) |
74 |
50
|
zred |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( Q x. ( 2 x. x ) ) e. RR ) |
75 |
|
modabs2 |
|- ( ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> Q e. CC ) |
85 |
42 32
|
zmulcld |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ S ) e. CC ) |
91 |
32
|
zcnd |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. CC ) |
92 |
84 90 91
|
mul12d |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) e. CC ) |
94 |
49
|
zcnd |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. CC ) |
95 |
84 93 94
|
mul12d |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P =/= Q ) |
100 |
|
prmrp |
|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) ) |
101 |
35 25 100
|
syl2anc |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P gcd Q ) = 1 <-> P =/= Q ) ) |
102 |
99 101
|
mpbird |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P gcd Q ) = 1 ) |
103 |
|
prmz |
|- ( P e. Prime -> P e. ZZ ) |
104 |
35 103
|
syl |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. ZZ ) |
105 |
85 87
|
zsubcld |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- -u 1 e. CC |
113 |
112
|
a1i |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -u 1 e. CC ) |
114 |
113 39 52
|
expaddd |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- 1 e. CC |
119 |
|
ax-1ne0 |
|- 1 =/= 0 |
120 |
|
divneg2 |
|- ( ( 1 e. CC /\ 1 e. CC /\ 1 =/= 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) ) |
121 |
118 118 119 120
|
mp3an |
|- -u ( 1 / 1 ) = ( 1 / -u 1 ) |
122 |
|
1div1e1 |
|- ( 1 / 1 ) = 1 |
123 |
122
|
negeqi |
|- -u ( 1 / 1 ) = -u 1 |
124 |
121 123
|
eqtr3i |
|- ( 1 / -u 1 ) = -u 1 |
125 |
124
|
oveq1i |
|- ( ( 1 / -u 1 ) ^ R ) = ( -u 1 ^ R ) |
126 |
|
neg1ne0 |
|- -u 1 =/= 0 |
127 |
126
|
a1i |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -u 1 =/= 0 ) |
128 |
113 127 53
|
exprecd |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( 1 / -u 1 ) ^ R ) = ( 1 / ( -u 1 ^ R ) ) ) |
129 |
125 128
|
eqtr3id |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) = ( 1 / ( -u 1 ^ R ) ) ) |
130 |
129
|
oveq2d |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ R ) =/= 0 ) |
132 |
93 131
|
recidd |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( -u 1 ^ R ) x. ( -u 1 ^ R ) ) = 1 ) |
134 |
133
|
oveq1d |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( ( -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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -u ( 2 x. y ) e. ZZ ) |
147 |
|
moddvds |
|- ( ( 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 |
|- ( ( 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 |
|- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. NN ) |
150 |
149
|
ad2antll |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. NN ) |
151 |
|
elfznn |
|- ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y e. NN ) |
152 |
151
|
ad2antrl |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. NN ) |
153 |
150 152
|
nnaddcld |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) e. NN ) |
154 |
150
|
nnred |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. RR ) |
155 |
30
|
zred |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. RR ) |
156 |
|
oddprm |
|- ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN ) |
157 |
34 156
|
syl |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P - 1 ) / 2 ) e. NN ) |
158 |
157
|
nnred |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P - 1 ) / 2 ) e. RR ) |
159 |
|
elfzle2 |
|- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x <_ ( ( P - 1 ) / 2 ) ) |
160 |
159
|
ad2antll |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x <_ ( ( P - 1 ) / 2 ) ) |
161 |
|
elfzle2 |
|- ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y <_ ( ( P - 1 ) / 2 ) ) |
162 |
161
|
ad2antrl |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) <_ ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) ) ) |
164 |
37
|
nnred |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. RR ) |
165 |
|
peano2rem |
|- ( P e. RR -> ( P - 1 ) e. RR ) |
166 |
164 165
|
syl |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) e. RR ) |
167 |
166
|
recnd |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) e. CC ) |
168 |
167
|
2halvesd |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) <_ ( P - 1 ) ) |
170 |
|
peano2zm |
|- ( P e. ZZ -> ( P - 1 ) e. ZZ ) |
171 |
|
fznn |
|- ( ( P - 1 ) e. ZZ -> ( ( x + y ) e. ( 1 ... ( P - 1 ) ) <-> ( ( x + y ) e. NN /\ ( x + y ) <_ ( P - 1 ) ) ) ) |
172 |
104 170 171
|
3syl |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) e. ( 1 ... ( P - 1 ) ) ) |
174 |
|
fzm1ndvds |
|- ( ( P e. NN /\ ( x + y ) e. ( 1 ... ( P - 1 ) ) ) -> -. P || ( x + y ) ) |
175 |
37 173 174
|
syl2anc |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -. P || ( x + y ) ) |
176 |
|
eldifsni |
|- ( P e. ( Prime \ { 2 } ) -> P =/= 2 ) |
177 |
34 176
|
syl |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P =/= 2 ) |
178 |
|
2prm |
|- 2 e. Prime |
179 |
|
prmrp |
|- ( ( P e. Prime /\ 2 e. Prime ) -> ( ( P gcd 2 ) = 1 <-> P =/= 2 ) ) |
180 |
35 178 179
|
sylancl |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P gcd 2 ) = 1 <-> P =/= 2 ) ) |
181 |
177 180
|
mpbird |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P gcd 2 ) = 1 ) |
182 |
28
|
a1i |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 e. ZZ ) |
183 |
153
|
nnzd |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + y ) e. ZZ ) |
184 |
|
coprmdvds |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -. P || ( 2 x. ( x + y ) ) ) |
188 |
94 91
|
subnegd |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. CC ) |
190 |
30
|
zcnd |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> y e. CC ) |
191 |
59 189 190
|
adddid |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( -u 1 ^ ( R + S ) ) = -u 1 -> ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) = ( -u 1 x. ( 2 x. y ) ) ) |
199 |
198
|
oveq1d |
|- ( ( -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 |
|- ( ( -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 |
|- ( ( -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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 1 x. ( 2 x. y ) ) = ( 2 x. y ) ) |
204 |
203
|
oveq1d |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. RR ) |
206 |
|
2nn |
|- 2 e. NN |
207 |
|
nnmulcl |
|- ( ( 2 e. NN /\ y e. NN ) -> ( 2 x. y ) e. NN ) |
208 |
206 152 207
|
sylancr |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. NN ) |
209 |
208
|
nnnn0d |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) e. NN0 ) |
210 |
209
|
nn0ge0d |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 <_ ( 2 x. y ) ) |
211 |
|
2re |
|- 2 e. RR |
212 |
211
|
a1i |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 2 e. RR ) |
213 |
|
2pos |
|- 0 < 2 |
214 |
213
|
a1i |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 < 2 ) |
215 |
|
lemuldiv2 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) <_ ( P - 1 ) ) |
218 |
|
zltlem1 |
|- ( ( ( 2 x. y ) e. ZZ /\ P e. ZZ ) -> ( ( 2 x. y ) < P <-> ( 2 x. y ) <_ ( P - 1 ) ) ) |
219 |
32 104 218
|
syl2anc |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. y ) < P ) |
221 |
|
modid |
|- ( ( ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. RR ) |
225 |
|
nnmulcl |
|- ( ( 2 e. NN /\ x e. NN ) -> ( 2 x. x ) e. NN ) |
226 |
206 150 225
|
sylancr |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. NN ) |
227 |
226
|
nnnn0d |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) e. NN0 ) |
228 |
227
|
nn0ge0d |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 <_ ( 2 x. x ) ) |
229 |
|
lemuldiv2 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) <_ ( P - 1 ) ) |
232 |
|
zltlem1 |
|- ( ( ( 2 x. x ) e. ZZ /\ P e. ZZ ) -> ( ( 2 x. x ) < P <-> ( 2 x. x ) <_ ( P - 1 ) ) ) |
233 |
49 104 232
|
syl2anc |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( 2 x. x ) < P ) |
235 |
|
modid |
|- ( ( ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( -u 1 ^ ( R + S ) ) = 1 -> ( ( -u 1 ^ ( R + S ) ) x. ( 2 x. y ) ) = ( 1 x. ( 2 x. y ) ) ) |
240 |
239
|
oveq1d |
|- ( ( -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 |
|- ( ( -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 |
|- ( ( -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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( R + S ) e. NN0 ) |
245 |
244
|
nn0zd |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( R + S ) e. ZZ ) |
246 |
|
m1expcl2 |
|- ( ( R + S ) e. ZZ -> ( -u 1 ^ ( R + S ) ) e. { -u 1 , 1 } ) |
247 |
|
elpri |
|- ( ( -u 1 ^ ( R + S ) ) e. { -u 1 , 1 } -> ( ( -u 1 ^ ( R + S ) ) = -u 1 \/ ( -u 1 ^ ( R + S ) ) = 1 ) ) |
248 |
245 246 247
|
3syl |
|- ( ( 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 |
|- ( ( 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 |
|- -u 1 e. ZZ |
251 |
|
zexpcl |
|- ( ( -u 1 e. ZZ /\ ( R + S ) e. NN0 ) -> ( -u 1 ^ ( R + S ) ) e. ZZ ) |
252 |
250 244 251
|
sylancr |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( -u 1 ^ ( R + S ) ) e. ZZ ) |
253 |
252 32
|
zmulcld |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( 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 |
|- ( ( ph /\ ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( M ` y ) = ( M ` x ) -> y = x ) ) |
265 |
264
|
ralrimivva |
|- ( ph -> A. y e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( M ` y ) = ( M ` x ) -> y = x ) ) |
266 |
|
nfmpt1 |
|- F/_ x ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) |
267 |
5 266
|
nfcxfr |
|- F/_ x M |
268 |
|
nfcv |
|- F/_ x y |
269 |
267 268
|
nffv |
|- F/_ x ( M ` y ) |
270 |
|
nfcv |
|- F/_ x z |
271 |
267 270
|
nffv |
|- F/_ x ( M ` z ) |
272 |
269 271
|
nfeq |
|- F/ x ( M ` y ) = ( M ` z ) |
273 |
|
nfv |
|- F/ x y = z |
274 |
272 273
|
nfim |
|- F/ x ( ( M ` y ) = ( M ` z ) -> y = z ) |
275 |
|
nfv |
|- F/ z ( ( M ` y ) = ( M ` x ) -> y = x ) |
276 |
|
fveq2 |
|- ( z = x -> ( M ` z ) = ( M ` x ) ) |
277 |
276
|
eqeq2d |
|- ( z = x -> ( ( M ` y ) = ( M ` z ) <-> ( M ` y ) = ( M ` x ) ) ) |
278 |
|
equequ2 |
|- ( z = x -> ( y = z <-> y = x ) ) |
279 |
277 278
|
imbi12d |
|- ( z = x -> ( ( ( M ` y ) = ( M ` z ) -> y = z ) <-> ( ( M ` y ) = ( M ` x ) -> y = x ) ) ) |
280 |
274 275 279
|
cbvralw |
|- ( 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 |
|- ( 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 |
|- ( ph -> A. y e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( M ` y ) = ( M ` z ) -> y = z ) ) |
283 |
|
dff13 |
|- ( 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 |
7 282 283
|
sylanbrc |
|- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( 1 ... ( ( P - 1 ) / 2 ) ) ) |
285 |
|
ovex |
|- ( 1 ... ( ( P - 1 ) / 2 ) ) e. _V |
286 |
285
|
enref |
|- ( 1 ... ( ( P - 1 ) / 2 ) ) ~~ ( 1 ... ( ( P - 1 ) / 2 ) ) |
287 |
|
fzfi |
|- ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin |
288 |
|
f1finf1o |
|- ( ( ( 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 |
|- ( 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 |
|- ( ph -> M : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) ) |