Metamath Proof Explorer


Theorem lgseisenlem2

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

Ref Expression
Hypotheses lgseisen.1 φ P 2
lgseisen.2 φ Q 2
lgseisen.3 φ P Q
lgseisen.4 R = Q 2 x mod P
lgseisen.5 M = x 1 P 1 2 1 R R mod P 2
lgseisen.6 S = Q 2 y mod P
Assertion lgseisenlem2 φ M : 1 P 1 2 1-1 onto 1 P 1 2

Proof

Step Hyp Ref Expression
1 lgseisen.1 φ P 2
2 lgseisen.2 φ Q 2
3 lgseisen.3 φ P Q
4 lgseisen.4 R = Q 2 x mod P
5 lgseisen.5 M = x 1 P 1 2 1 R R mod P 2
6 lgseisen.6 S = Q 2 y mod P
7 1 2 3 4 5 lgseisenlem1 φ M : 1 P 1 2 1 P 1 2
8 oveq2 x = y 2 x = 2 y
9 8 oveq2d x = y Q 2 x = Q 2 y
10 9 oveq1d x = y Q 2 x mod P = Q 2 y mod P
11 10 4 6 3eqtr4g x = y R = S
12 11 oveq2d x = y 1 R = 1 S
13 12 11 oveq12d x = y 1 R R = 1 S S
14 13 oveq1d x = y 1 R R mod P = 1 S S mod P
15 14 oveq1d x = y 1 R R mod P 2 = 1 S S mod P 2
16 ovex 1 S S mod P 2 V
17 15 5 16 fvmpt y 1 P 1 2 M y = 1 S S mod P 2
18 17 ad2antrl φ y 1 P 1 2 x 1 P 1 2 M y = 1 S S mod P 2
19 ovex 1 R R mod P 2 V
20 5 fvmpt2 x 1 P 1 2 1 R R mod P 2 V M x = 1 R R mod P 2
21 19 20 mpan2 x 1 P 1 2 M x = 1 R R mod P 2
22 21 ad2antll φ y 1 P 1 2 x 1 P 1 2 M x = 1 R R mod P 2
23 18 22 eqeq12d φ y 1 P 1 2 x 1 P 1 2 M y = M x 1 S S mod P 2 = 1 R R mod P 2
24 2 adantr φ y 1 P 1 2 x 1 P 1 2 Q 2
25 24 eldifad φ y 1 P 1 2 x 1 P 1 2 Q
26 prmz Q Q
27 25 26 syl φ y 1 P 1 2 x 1 P 1 2 Q
28 2z 2
29 elfzelz y 1 P 1 2 y
30 29 ad2antrl φ y 1 P 1 2 x 1 P 1 2 y
31 zmulcl 2 y 2 y
32 28 30 31 sylancr φ y 1 P 1 2 x 1 P 1 2 2 y
33 27 32 zmulcld φ y 1 P 1 2 x 1 P 1 2 Q 2 y
34 1 adantr φ y 1 P 1 2 x 1 P 1 2 P 2
35 34 eldifad φ y 1 P 1 2 x 1 P 1 2 P
36 prmnn P P
37 35 36 syl φ y 1 P 1 2 x 1 P 1 2 P
38 33 37 zmodcld φ y 1 P 1 2 x 1 P 1 2 Q 2 y mod P 0
39 6 38 eqeltrid φ y 1 P 1 2 x 1 P 1 2 S 0
40 39 nn0zd φ y 1 P 1 2 x 1 P 1 2 S
41 m1expcl S 1 S
42 40 41 syl φ y 1 P 1 2 x 1 P 1 2 1 S
43 42 40 zmulcld φ y 1 P 1 2 x 1 P 1 2 1 S S
44 43 37 zmodcld φ y 1 P 1 2 x 1 P 1 2 1 S S mod P 0
45 44 nn0cnd φ y 1 P 1 2 x 1 P 1 2 1 S S mod P
46 elfzelz x 1 P 1 2 x
47 46 ad2antll φ y 1 P 1 2 x 1 P 1 2 x
48 zmulcl 2 x 2 x
49 28 47 48 sylancr φ y 1 P 1 2 x 1 P 1 2 2 x
50 27 49 zmulcld φ y 1 P 1 2 x 1 P 1 2 Q 2 x
51 50 37 zmodcld φ y 1 P 1 2 x 1 P 1 2 Q 2 x mod P 0
52 4 51 eqeltrid φ y 1 P 1 2 x 1 P 1 2 R 0
53 52 nn0zd φ y 1 P 1 2 x 1 P 1 2 R
54 m1expcl R 1 R
55 53 54 syl φ y 1 P 1 2 x 1 P 1 2 1 R
56 55 53 zmulcld φ y 1 P 1 2 x 1 P 1 2 1 R R
57 56 37 zmodcld φ y 1 P 1 2 x 1 P 1 2 1 R R mod P 0
58 57 nn0cnd φ y 1 P 1 2 x 1 P 1 2 1 R R mod P
59 2cnd φ y 1 P 1 2 x 1 P 1 2 2
60 2ne0 2 0
61 60 a1i φ y 1 P 1 2 x 1 P 1 2 2 0
62 div11 1 S S mod P 1 R R mod P 2 2 0 1 S S mod P 2 = 1 R R mod P 2 1 S S mod P = 1 R R mod P
63 45 58 59 61 62 syl112anc φ y 1 P 1 2 x 1 P 1 2 1 S S mod P 2 = 1 R R mod P 2 1 S S mod P = 1 R R mod P
64 37 nnrpd φ y 1 P 1 2 x 1 P 1 2 P +
65 eqidd φ y 1 P 1 2 x 1 P 1 2 1 S mod P = 1 S mod P
66 6 oveq1i S mod P = Q 2 y mod P mod P
67 33 zred φ y 1 P 1 2 x 1 P 1 2 Q 2 y
68 modabs2 Q 2 y P + Q 2 y mod P mod P = Q 2 y mod P
69 67 64 68 syl2anc φ y 1 P 1 2 x 1 P 1 2 Q 2 y mod P mod P = Q 2 y mod P
70 66 69 syl5eq φ y 1 P 1 2 x 1 P 1 2 S mod P = Q 2 y mod P
71 42 42 40 33 64 65 70 modmul12d φ y 1 P 1 2 x 1 P 1 2 1 S S mod P = 1 S Q 2 y mod P
72 eqidd φ y 1 P 1 2 x 1 P 1 2 1 R mod P = 1 R mod P
73 4 oveq1i R mod P = Q 2 x mod P mod P
74 50 zred φ y 1 P 1 2 x 1 P 1 2 Q 2 x
75 modabs2 Q 2 x P + Q 2 x mod P mod P = Q 2 x mod P
76 74 64 75 syl2anc φ y 1 P 1 2 x 1 P 1 2 Q 2 x mod P mod P = Q 2 x mod P
77 73 76 syl5eq φ y 1 P 1 2 x 1 P 1 2 R mod P = Q 2 x mod P
78 55 55 53 50 64 72 77 modmul12d φ y 1 P 1 2 x 1 P 1 2 1 R R mod P = 1 R Q 2 x mod P
79 71 78 eqeq12d φ y 1 P 1 2 x 1 P 1 2 1 S S mod P = 1 R R mod P 1 S Q 2 y mod P = 1 R Q 2 x mod P
80 42 33 zmulcld φ y 1 P 1 2 x 1 P 1 2 1 S Q 2 y
81 55 50 zmulcld φ y 1 P 1 2 x 1 P 1 2 1 R Q 2 x
82 moddvds P 1 S Q 2 y 1 R Q 2 x 1 S Q 2 y mod P = 1 R Q 2 x mod P P 1 S Q 2 y 1 R Q 2 x
83 37 80 81 82 syl3anc φ y 1 P 1 2 x 1 P 1 2 1 S Q 2 y mod P = 1 R Q 2 x mod P P 1 S Q 2 y 1 R Q 2 x
84 27 zcnd φ y 1 P 1 2 x 1 P 1 2 Q
85 42 32 zmulcld φ y 1 P 1 2 x 1 P 1 2 1 S 2 y
86 85 zcnd φ y 1 P 1 2 x 1 P 1 2 1 S 2 y
87 55 49 zmulcld φ y 1 P 1 2 x 1 P 1 2 1 R 2 x
88 87 zcnd φ y 1 P 1 2 x 1 P 1 2 1 R 2 x
89 84 86 88 subdid φ y 1 P 1 2 x 1 P 1 2 Q 1 S 2 y 1 R 2 x = Q 1 S 2 y Q 1 R 2 x
90 42 zcnd φ y 1 P 1 2 x 1 P 1 2 1 S
91 32 zcnd φ y 1 P 1 2 x 1 P 1 2 2 y
92 84 90 91 mul12d φ y 1 P 1 2 x 1 P 1 2 Q 1 S 2 y = 1 S Q 2 y
93 55 zcnd φ y 1 P 1 2 x 1 P 1 2 1 R
94 49 zcnd φ y 1 P 1 2 x 1 P 1 2 2 x
95 84 93 94 mul12d φ y 1 P 1 2 x 1 P 1 2 Q 1 R 2 x = 1 R Q 2 x
96 92 95 oveq12d φ y 1 P 1 2 x 1 P 1 2 Q 1 S 2 y Q 1 R 2 x = 1 S Q 2 y 1 R Q 2 x
97 89 96 eqtrd φ y 1 P 1 2 x 1 P 1 2 Q 1 S 2 y 1 R 2 x = 1 S Q 2 y 1 R Q 2 x
98 97 breq2d φ y 1 P 1 2 x 1 P 1 2 P Q 1 S 2 y 1 R 2 x P 1 S Q 2 y 1 R Q 2 x
99 3 adantr φ y 1 P 1 2 x 1 P 1 2 P Q
100 prmrp P Q P gcd Q = 1 P Q
101 35 25 100 syl2anc φ y 1 P 1 2 x 1 P 1 2 P gcd Q = 1 P Q
102 99 101 mpbird φ y 1 P 1 2 x 1 P 1 2 P gcd Q = 1
103 prmz P P
104 35 103 syl φ y 1 P 1 2 x 1 P 1 2 P
105 85 87 zsubcld φ y 1 P 1 2 x 1 P 1 2 1 S 2 y 1 R 2 x
106 coprmdvds P Q 1 S 2 y 1 R 2 x P Q 1 S 2 y 1 R 2 x P gcd Q = 1 P 1 S 2 y 1 R 2 x
107 104 27 105 106 syl3anc φ y 1 P 1 2 x 1 P 1 2 P Q 1 S 2 y 1 R 2 x P gcd Q = 1 P 1 S 2 y 1 R 2 x
108 102 107 mpan2d φ y 1 P 1 2 x 1 P 1 2 P Q 1 S 2 y 1 R 2 x P 1 S 2 y 1 R 2 x
109 dvdsmultr2 P 1 R 1 S 2 y 1 R 2 x P 1 S 2 y 1 R 2 x P 1 R 1 S 2 y 1 R 2 x
110 104 55 105 109 syl3anc φ y 1 P 1 2 x 1 P 1 2 P 1 S 2 y 1 R 2 x P 1 R 1 S 2 y 1 R 2 x
111 93 86 88 subdid φ y 1 P 1 2 x 1 P 1 2 1 R 1 S 2 y 1 R 2 x = 1 R 1 S 2 y 1 R 1 R 2 x
112 neg1cn 1
113 112 a1i φ y 1 P 1 2 x 1 P 1 2 1
114 113 39 52 expaddd φ y 1 P 1 2 x 1 P 1 2 1 R + S = 1 R 1 S
115 114 oveq1d φ y 1 P 1 2 x 1 P 1 2 1 R + S 2 y = 1 R 1 S 2 y
116 93 90 91 mulassd φ y 1 P 1 2 x 1 P 1 2 1 R 1 S 2 y = 1 R 1 S 2 y
117 115 116 eqtr2d φ y 1 P 1 2 x 1 P 1 2 1 R 1 S 2 y = 1 R + S 2 y
118 ax-1cn 1
119 ax-1ne0 1 0
120 divneg2 1 1 1 0 1 1 = 1 1
121 118 118 119 120 mp3an 1 1 = 1 1
122 1div1e1 1 1 = 1
123 122 negeqi 1 1 = 1
124 121 123 eqtr3i 1 1 = 1
125 124 oveq1i 1 1 R = 1 R
126 neg1ne0 1 0
127 126 a1i φ y 1 P 1 2 x 1 P 1 2 1 0
128 113 127 53 exprecd φ y 1 P 1 2 x 1 P 1 2 1 1 R = 1 1 R
129 125 128 eqtr3id φ y 1 P 1 2 x 1 P 1 2 1 R = 1 1 R
130 129 oveq2d φ y 1 P 1 2 x 1 P 1 2 1 R 1 R = 1 R 1 1 R
131 113 127 53 expne0d φ y 1 P 1 2 x 1 P 1 2 1 R 0
132 93 131 recidd φ y 1 P 1 2 x 1 P 1 2 1 R 1 1 R = 1
133 130 132 eqtrd φ y 1 P 1 2 x 1 P 1 2 1 R 1 R = 1
134 133 oveq1d φ y 1 P 1 2 x 1 P 1 2 1 R 1 R 2 x = 1 2 x
135 93 93 94 mulassd φ y 1 P 1 2 x 1 P 1 2 1 R 1 R 2 x = 1 R 1 R 2 x
136 94 mulid2d φ y 1 P 1 2 x 1 P 1 2 1 2 x = 2 x
137 134 135 136 3eqtr3d φ y 1 P 1 2 x 1 P 1 2 1 R 1 R 2 x = 2 x
138 117 137 oveq12d φ y 1 P 1 2 x 1 P 1 2 1 R 1 S 2 y 1 R 1 R 2 x = 1 R + S 2 y 2 x
139 111 138 eqtrd φ y 1 P 1 2 x 1 P 1 2 1 R 1 S 2 y 1 R 2 x = 1 R + S 2 y 2 x
140 139 breq2d φ y 1 P 1 2 x 1 P 1 2 P 1 R 1 S 2 y 1 R 2 x P 1 R + S 2 y 2 x
141 eqcom -1 2 y mod P = 2 x mod P 2 x mod P = -1 2 y mod P
142 91 mulm1d φ y 1 P 1 2 x 1 P 1 2 -1 2 y = 2 y
143 142 oveq1d φ y 1 P 1 2 x 1 P 1 2 -1 2 y mod P = 2 y mod P
144 143 eqeq2d φ y 1 P 1 2 x 1 P 1 2 2 x mod P = -1 2 y mod P 2 x mod P = 2 y mod P
145 141 144 syl5bb φ y 1 P 1 2 x 1 P 1 2 -1 2 y mod P = 2 x mod P 2 x mod P = 2 y mod P
146 32 znegcld φ y 1 P 1 2 x 1 P 1 2 2 y
147 moddvds P 2 x 2 y 2 x mod P = 2 y mod P P 2 x 2 y
148 37 49 146 147 syl3anc φ y 1 P 1 2 x 1 P 1 2 2 x mod P = 2 y mod P P 2 x 2 y
149 elfznn x 1 P 1 2 x
150 149 ad2antll φ y 1 P 1 2 x 1 P 1 2 x
151 elfznn y 1 P 1 2 y
152 151 ad2antrl φ y 1 P 1 2 x 1 P 1 2 y
153 150 152 nnaddcld φ y 1 P 1 2 x 1 P 1 2 x + y
154 150 nnred φ y 1 P 1 2 x 1 P 1 2 x
155 30 zred φ y 1 P 1 2 x 1 P 1 2 y
156 oddprm P 2 P 1 2
157 34 156 syl φ y 1 P 1 2 x 1 P 1 2 P 1 2
158 157 nnred φ y 1 P 1 2 x 1 P 1 2 P 1 2
159 elfzle2 x 1 P 1 2 x P 1 2
160 159 ad2antll φ y 1 P 1 2 x 1 P 1 2 x P 1 2
161 elfzle2 y 1 P 1 2 y P 1 2
162 161 ad2antrl φ y 1 P 1 2 x 1 P 1 2 y P 1 2
163 154 155 158 158 160 162 le2addd φ y 1 P 1 2 x 1 P 1 2 x + y P 1 2 + P 1 2
164 37 nnred φ y 1 P 1 2 x 1 P 1 2 P
165 peano2rem P P 1
166 164 165 syl φ y 1 P 1 2 x 1 P 1 2 P 1
167 166 recnd φ y 1 P 1 2 x 1 P 1 2 P 1
168 167 2halvesd φ y 1 P 1 2 x 1 P 1 2 P 1 2 + P 1 2 = P 1
169 163 168 breqtrd φ y 1 P 1 2 x 1 P 1 2 x + y P 1
170 peano2zm P P 1
171 fznn P 1 x + y 1 P 1 x + y x + y P 1
172 104 170 171 3syl φ y 1 P 1 2 x 1 P 1 2 x + y 1 P 1 x + y x + y P 1
173 153 169 172 mpbir2and φ y 1 P 1 2 x 1 P 1 2 x + y 1 P 1
174 fzm1ndvds P x + y 1 P 1 ¬ P x + y
175 37 173 174 syl2anc φ y 1 P 1 2 x 1 P 1 2 ¬ P x + y
176 eldifsni P 2 P 2
177 34 176 syl φ y 1 P 1 2 x 1 P 1 2 P 2
178 2prm 2
179 prmrp P 2 P gcd 2 = 1 P 2
180 35 178 179 sylancl φ y 1 P 1 2 x 1 P 1 2 P gcd 2 = 1 P 2
181 177 180 mpbird φ y 1 P 1 2 x 1 P 1 2 P gcd 2 = 1
182 28 a1i φ y 1 P 1 2 x 1 P 1 2 2
183 153 nnzd φ y 1 P 1 2 x 1 P 1 2 x + y
184 coprmdvds P 2 x + y P 2 x + y P gcd 2 = 1 P x + y
185 104 182 183 184 syl3anc φ y 1 P 1 2 x 1 P 1 2 P 2 x + y P gcd 2 = 1 P x + y
186 181 185 mpan2d φ y 1 P 1 2 x 1 P 1 2 P 2 x + y P x + y
187 175 186 mtod φ y 1 P 1 2 x 1 P 1 2 ¬ P 2 x + y
188 94 91 subnegd φ y 1 P 1 2 x 1 P 1 2 2 x 2 y = 2 x + 2 y
189 47 zcnd φ y 1 P 1 2 x 1 P 1 2 x
190 30 zcnd φ y 1 P 1 2 x 1 P 1 2 y
191 59 189 190 adddid φ y 1 P 1 2 x 1 P 1 2 2 x + y = 2 x + 2 y
192 188 191 eqtr4d φ y 1 P 1 2 x 1 P 1 2 2 x 2 y = 2 x + y
193 192 breq2d φ y 1 P 1 2 x 1 P 1 2 P 2 x 2 y P 2 x + y
194 187 193 mtbird φ y 1 P 1 2 x 1 P 1 2 ¬ P 2 x 2 y
195 194 pm2.21d φ y 1 P 1 2 x 1 P 1 2 P 2 x 2 y 2 y = 2 x
196 148 195 sylbid φ y 1 P 1 2 x 1 P 1 2 2 x mod P = 2 y mod P 2 y = 2 x
197 145 196 sylbid φ y 1 P 1 2 x 1 P 1 2 -1 2 y mod P = 2 x mod P 2 y = 2 x
198 oveq1 1 R + S = 1 1 R + S 2 y = -1 2 y
199 198 oveq1d 1 R + S = 1 1 R + S 2 y mod P = -1 2 y mod P
200 199 eqeq1d 1 R + S = 1 1 R + S 2 y mod P = 2 x mod P -1 2 y mod P = 2 x mod P
201 200 imbi1d 1 R + S = 1 1 R + S 2 y mod P = 2 x mod P 2 y = 2 x -1 2 y mod P = 2 x mod P 2 y = 2 x
202 197 201 syl5ibrcom φ y 1 P 1 2 x 1 P 1 2 1 R + S = 1 1 R + S 2 y mod P = 2 x mod P 2 y = 2 x
203 91 mulid2d φ y 1 P 1 2 x 1 P 1 2 1 2 y = 2 y
204 203 oveq1d φ y 1 P 1 2 x 1 P 1 2 1 2 y mod P = 2 y mod P
205 32 zred φ y 1 P 1 2 x 1 P 1 2 2 y
206 2nn 2
207 nnmulcl 2 y 2 y
208 206 152 207 sylancr φ y 1 P 1 2 x 1 P 1 2 2 y
209 208 nnnn0d φ y 1 P 1 2 x 1 P 1 2 2 y 0
210 209 nn0ge0d φ y 1 P 1 2 x 1 P 1 2 0 2 y
211 2re 2
212 211 a1i φ y 1 P 1 2 x 1 P 1 2 2
213 2pos 0 < 2
214 213 a1i φ y 1 P 1 2 x 1 P 1 2 0 < 2
215 lemuldiv2 y P 1 2 0 < 2 2 y P 1 y P 1 2
216 155 166 212 214 215 syl112anc φ y 1 P 1 2 x 1 P 1 2 2 y P 1 y P 1 2
217 162 216 mpbird φ y 1 P 1 2 x 1 P 1 2 2 y P 1
218 zltlem1 2 y P 2 y < P 2 y P 1
219 32 104 218 syl2anc φ y 1 P 1 2 x 1 P 1 2 2 y < P 2 y P 1
220 217 219 mpbird φ y 1 P 1 2 x 1 P 1 2 2 y < P
221 modid 2 y P + 0 2 y 2 y < P 2 y mod P = 2 y
222 205 64 210 220 221 syl22anc φ y 1 P 1 2 x 1 P 1 2 2 y mod P = 2 y
223 204 222 eqtrd φ y 1 P 1 2 x 1 P 1 2 1 2 y mod P = 2 y
224 49 zred φ y 1 P 1 2 x 1 P 1 2 2 x
225 nnmulcl 2 x 2 x
226 206 150 225 sylancr φ y 1 P 1 2 x 1 P 1 2 2 x
227 226 nnnn0d φ y 1 P 1 2 x 1 P 1 2 2 x 0
228 227 nn0ge0d φ y 1 P 1 2 x 1 P 1 2 0 2 x
229 lemuldiv2 x P 1 2 0 < 2 2 x P 1 x P 1 2
230 154 166 212 214 229 syl112anc φ y 1 P 1 2 x 1 P 1 2 2 x P 1 x P 1 2
231 160 230 mpbird φ y 1 P 1 2 x 1 P 1 2 2 x P 1
232 zltlem1 2 x P 2 x < P 2 x P 1
233 49 104 232 syl2anc φ y 1 P 1 2 x 1 P 1 2 2 x < P 2 x P 1
234 231 233 mpbird φ y 1 P 1 2 x 1 P 1 2 2 x < P
235 modid 2 x P + 0 2 x 2 x < P 2 x mod P = 2 x
236 224 64 228 234 235 syl22anc φ y 1 P 1 2 x 1 P 1 2 2 x mod P = 2 x
237 223 236 eqeq12d φ y 1 P 1 2 x 1 P 1 2 1 2 y mod P = 2 x mod P 2 y = 2 x
238 237 biimpd φ y 1 P 1 2 x 1 P 1 2 1 2 y mod P = 2 x mod P 2 y = 2 x
239 oveq1 1 R + S = 1 1 R + S 2 y = 1 2 y
240 239 oveq1d 1 R + S = 1 1 R + S 2 y mod P = 1 2 y mod P
241 240 eqeq1d 1 R + S = 1 1 R + S 2 y mod P = 2 x mod P 1 2 y mod P = 2 x mod P
242 241 imbi1d 1 R + S = 1 1 R + S 2 y mod P = 2 x mod P 2 y = 2 x 1 2 y mod P = 2 x mod P 2 y = 2 x
243 238 242 syl5ibrcom φ y 1 P 1 2 x 1 P 1 2 1 R + S = 1 1 R + S 2 y mod P = 2 x mod P 2 y = 2 x
244 52 39 nn0addcld φ y 1 P 1 2 x 1 P 1 2 R + S 0
245 244 nn0zd φ y 1 P 1 2 x 1 P 1 2 R + S
246 m1expcl2 R + S 1 R + S 1 1
247 elpri 1 R + S 1 1 1 R + S = 1 1 R + S = 1
248 245 246 247 3syl φ y 1 P 1 2 x 1 P 1 2 1 R + S = 1 1 R + S = 1
249 202 243 248 mpjaod φ y 1 P 1 2 x 1 P 1 2 1 R + S 2 y mod P = 2 x mod P 2 y = 2 x
250 neg1z 1
251 zexpcl 1 R + S 0 1 R + S
252 250 244 251 sylancr φ y 1 P 1 2 x 1 P 1 2 1 R + S
253 252 32 zmulcld φ y 1 P 1 2 x 1 P 1 2 1 R + S 2 y
254 moddvds P 1 R + S 2 y 2 x 1 R + S 2 y mod P = 2 x mod P P 1 R + S 2 y 2 x
255 37 253 49 254 syl3anc φ y 1 P 1 2 x 1 P 1 2 1 R + S 2 y mod P = 2 x mod P P 1 R + S 2 y 2 x
256 190 189 59 61 mulcand φ y 1 P 1 2 x 1 P 1 2 2 y = 2 x y = x
257 249 255 256 3imtr3d φ y 1 P 1 2 x 1 P 1 2 P 1 R + S 2 y 2 x y = x
258 140 257 sylbid φ y 1 P 1 2 x 1 P 1 2 P 1 R 1 S 2 y 1 R 2 x y = x
259 108 110 258 3syld φ y 1 P 1 2 x 1 P 1 2 P Q 1 S 2 y 1 R 2 x y = x
260 98 259 sylbird φ y 1 P 1 2 x 1 P 1 2 P 1 S Q 2 y 1 R Q 2 x y = x
261 83 260 sylbid φ y 1 P 1 2 x 1 P 1 2 1 S Q 2 y mod P = 1 R Q 2 x mod P y = x
262 79 261 sylbid φ y 1 P 1 2 x 1 P 1 2 1 S S mod P = 1 R R mod P y = x
263 63 262 sylbid φ y 1 P 1 2 x 1 P 1 2 1 S S mod P 2 = 1 R R mod P 2 y = x
264 23 263 sylbid φ y 1 P 1 2 x 1 P 1 2 M y = M x y = x
265 264 ralrimivva φ y 1 P 1 2 x 1 P 1 2 M y = M x y = x
266 nfmpt1 _ x x 1 P 1 2 1 R R mod P 2
267 5 266 nfcxfr _ x M
268 nfcv _ x y
269 267 268 nffv _ x M y
270 nfcv _ x z
271 267 270 nffv _ x M z
272 269 271 nfeq x M y = M z
273 nfv x y = z
274 272 273 nfim x M y = M z y = z
275 nfv 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 z 1 P 1 2 M y = M z y = z x 1 P 1 2 M y = M x y = x
281 280 ralbii y 1 P 1 2 z 1 P 1 2 M y = M z y = z y 1 P 1 2 x 1 P 1 2 M y = M x y = x
282 265 281 sylibr φ y 1 P 1 2 z 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 y 1 P 1 2 z 1 P 1 2 M y = M z y = z
284 7 282 283 sylanbrc φ M : 1 P 1 2 1-1 1 P 1 2
285 ovex 1 P 1 2 V
286 285 enref 1 P 1 2 1 P 1 2
287 fzfi 1 P 1 2 Fin
288 f1finf1o 1 P 1 2 1 P 1 2 1 P 1 2 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 φ M : 1 P 1 2 1-1 onto 1 P 1 2