MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4sqlem12 Unicode version

Theorem 4sqlem12 14474
Description: Lemma for 4sq 14482. For any odd prime , there is a such that P 1 is a sum of two squares. (Contributed by Mario Carneiro, 15-Jul-2014.)
Hypotheses
Ref Expression
4sq.1
4sq.2
4sq.3
4sq.4
4sqlem11.5
4sqlem11.6
Assertion
Ref Expression
4sqlem12
Distinct variable groups:   , , , ,   , , ,   ,   , , , ,N,   P, , , , ,   , , , , ,   S, , , , ,

Proof of Theorem 4sqlem12
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 4sq.1 . . . 4
2 4sq.2 . . . 4
3 4sq.3 . . . 4
4 4sq.4 . . . 4
5 4sqlem11.5 . . . 4
6 4sqlem11.6 . . . 4
71, 2, 3, 4, 5, 64sqlem11 14473 . . 3
8 n0 3794 . . 3
97, 8sylib 196 . 2
10 vex 3112 . . . . . . 7
11 eqeq1 2461 . . . . . . . 8
1211rexbidv 2968 . . . . . . 7
1310, 12, 5elab2 3249 . . . . . 6
14 abid 2444 . . . . . . . . 9
155rexeqi 3059 . . . . . . . . 9
16 oveq1 6303 . . . . . . . . . . . . . 14
1716oveq1d 6311 . . . . . . . . . . . . 13
1817eqeq2d 2471 . . . . . . . . . . . 12
1918cbvrexv 3085 . . . . . . . . . . 11
20 eqeq1 2461 . . . . . . . . . . . 12
2120rexbidv 2968 . . . . . . . . . . 11
2219, 21syl5bb 257 . . . . . . . . . 10
2322rexab 3262 . . . . . . . . 9
2414, 15, 233bitri 271 . . . . . . . 8
256rnmpt 5253 . . . . . . . . 9
2625eleq2i 2535 . . . . . . . 8
27 rexcom4 3129 . . . . . . . . 9
28 r19.41v 3009 . . . . . . . . . 10
2928exbii 1667 . . . . . . . . 9
3027, 29bitri 249 . . . . . . . 8
3124, 26, 303bitr4i 277 . . . . . . 7
32 ovex 6324 . . . . . . . . 9
33 oveq2 6304 . . . . . . . . . 10
3433eqeq2d 2471 . . . . . . . . 9
3532, 34ceqsexv 3146 . . . . . . . 8
3635rexbii 2959 . . . . . . 7
3731, 36bitri 249 . . . . . 6
3813, 37anbi12i 697 . . . . 5
39 elin 3686 . . . . 5
40 reeanv 3025 . . . . 5
4138, 39, 403bitr4i 277 . . . 4
42 eqtr2 2484 . . . . . 6
4343ad2ant1 1017 . . . . . . . . . . . . . . . . . . 19
44 prmnn 14220 . . . . . . . . . . . . . . . . . . 19
4543, 44syl 16 . . . . . . . . . . . . . . . . . 18
46 nnm1nn0 10862 . . . . . . . . . . . . . . . . . 18
4745, 46syl 16 . . . . . . . . . . . . . . . . 17
4847nn0red 10878 . . . . . . . . . . . . . . . 16
4945nnrpd 11284 . . . . . . . . . . . . . . . 16
5047nn0ge0d 10880 . . . . . . . . . . . . . . . 16
5145nnred 10576 . . . . . . . . . . . . . . . . 17
5251ltm1d 10503 . . . . . . . . . . . . . . . 16
53 modid 12020 . . . . . . . . . . . . . . . 16
5448, 49, 50, 52, 53syl22anc 1229 . . . . . . . . . . . . . . 15
5554oveq1d 6311 . . . . . . . . . . . . . 14
56 simp2r 1023 . . . . . . . . . . . . . . . . . . . . 21
57 elfzelz 11717 . . . . . . . . . . . . . . . . . . . . 21
5856, 57syl 16 . . . . . . . . . . . . . . . . . . . 20
59 zsqcl2 12245 . . . . . . . . . . . . . . . . . . . 20
6058, 59syl 16 . . . . . . . . . . . . . . . . . . 19
6160nn0red 10878 . . . . . . . . . . . . . . . . . 18
62 modlt 12006 . . . . . . . . . . . . . . . . . 18
6361, 49, 62syl2anc 661 . . . . . . . . . . . . . . . . 17
64 zsqcl 12238 . . . . . . . . . . . . . . . . . . . . 21
6558, 64syl 16 . . . . . . . . . . . . . . . . . . . 20
6665, 45zmodcld 12016 . . . . . . . . . . . . . . . . . . 19
6766nn0zd 10992 . . . . . . . . . . . . . . . . . 18
68 prmz 14221 . . . . . . . . . . . . . . . . . . 19
6943, 68syl 16 . . . . . . . . . . . . . . . . . 18
70 zltlem1 10941 . . . . . . . . . . . . . . . . . 18
7167, 69, 70syl2anc 661 . . . . . . . . . . . . . . . . 17
7263, 71mpbid 210 . . . . . . . . . . . . . . . 16
7372, 54breqtrrd 4478 . . . . . . . . . . . . . . 15
74 modsubdir 12055 . . . . . . . . . . . . . . . 16
7548, 61, 49, 74syl3anc 1228 . . . . . . . . . . . . . . 15
7673, 75mpbid 210 . . . . . . . . . . . . . 14
77 simp3 998 . . . . . . . . . . . . . 14
7855, 76, 773eqtr4rd 2509 . . . . . . . . . . . . 13
79 simp2l 1022 . . . . . . . . . . . . . . . 16
80 elfzelz 11717 . . . . . . . . . . . . . . . 16
8179, 80syl 16 . . . . . . . . . . . . . . 15
82 zsqcl 12238 . . . . . . . . . . . . . . 15
8381, 82syl 16 . . . . . . . . . . . . . 14
8447nn0zd 10992 . . . . . . . . . . . . . . 15
8584, 65zsubcld 10999 . . . . . . . . . . . . . 14
86 moddvds 13993 . . . . . . . . . . . . . 14
8745, 83, 85, 86syl3anc 1228 . . . . . . . . . . . . 13
8878, 87mpbid 210 . . . . . . . . . . . 12
89 zsqcl2 12245 . . . . . . . . . . . . . . . 16
9081, 89syl 16 . . . . . . . . . . . . . . 15
9190nn0cnd 10879 . . . . . . . . . . . . . 14
9247nn0cnd 10879 . . . . . . . . . . . . . 14
9360nn0cnd 10879 . . . . . . . . . . . . . 14
9491, 92, 93subsub3d 9984 . . . . . . . . . . . . 13
9590, 60nn0addcld 10881 . . . . . . . . . . . . . . 15
9695nn0cnd 10879 . . . . . . . . . . . . . 14
9745nncnd 10577 . . . . . . . . . . . . . 14
98 1cnd 9633 . . . . . . . . . . . . . 14
9996, 97, 98subsub3d 9984 . . . . . . . . . . . . 13
10094, 99eqtrd 2498 . . . . . . . . . . . 12
10188, 100breqtrd 4476 . . . . . . . . . . 11
102 nn0p1nn 10860 . . . . . . . . . . . . . 14
10395, 102syl 16 . . . . . . . . . . . . 13
104103nnzd 10993 . . . . . . . . . . . 12
105 dvdssubr 14027 . . . . . . . . . . . 12
10669, 104, 105syl2anc 661 . . . . . . . . . . 11
107101, 106mpbird 232 . . . . . . . . . 10
10845nnne0d 10605 . . . . . . . . . . 11
109 dvdsval2 13989 . . . . . . . . . . 11
11069, 108, 104, 109syl3anc 1228 . . . . . . . . . 10
111107, 110mpbid 210 . . . . . . . . 9
112 nnrp 11258 . . . . . . . . . . . . . 14
113 nnrp 11258 . . . . . . . . . . . . . 14
114 rpdivcl 11271 . . . . . . . . . . . . . 14
115112, 113, 114syl2an 477 . . . . . . . . . . . . 13
116103, 45, 115syl2anc 661 . . . . . . . . . . . 12
117116rpgt0d 11288 . . . . . . . . . . 11
118 elnnz 10899 . . . . . . . . . . 11
119111, 117, 118sylanbrc 664 . . . . . . . . . 10
120119nnge1d 10603 . . . . . . . . 9
12195nn0red 10878 . . . . . . . . . . . 12
122 2nn 10718 . . . . . . . . . . . . . . . 16
12323ad2ant1 1017 . . . . . . . . . . . . . . . 16
124 nnmulcl 10584 . . . . . . . . . . . . . . . 16
125122, 123, 124sylancr 663 . . . . . . . . . . . . . . 15
126125nnred 10576 . . . . . . . . . . . . . 14
127126resqcld 12336 . . . . . . . . . . . . 13
128 nnmulcl 10584 . . . . . . . . . . . . . . 15
129122, 125, 128sylancr 663 . . . . . . . . . . . . . 14
130129nnred 10576 . . . . . . . . . . . . 13
131127, 130readdcld 9644 . . . . . . . . . . . 12
132 1red 9632 . . . . . . . . . . . 12
133123nnsqcld 12330 . . . . . . . . . . . . . . . 16
134 nnmulcl 10584 . . . . . . . . . . . . . . . 16
135122, 133, 134sylancr 663 . . . . . . . . . . . . . . 15
136135nnred 10576 . . . . . . . . . . . . . 14
13790nn0red 10878 . . . . . . . . . . . . . . . 16
138133nnred 10576 . . . . . . . . . . . . . . . 16
13981zred 10994 . . . . . . . . . . . . . . . . 17
140 elfzle1 11718 . . . . . . . . . . . . . . . . . 18
14179, 140syl 16 . . . . . . . . . . . . . . . . 17
142123nnred 10576 . . . . . . . . . . . . . . . . 17
143 elfzle2 11719 . . . . . . . . . . . . . . . . . 18
14479, 143syl 16 . . . . . . . . . . . . . . . . 17
145 le2sq2 12243 . . . . . . . . . . . . . . . . 17
146139, 141, 142, 144, 145syl22anc 1229 . . . . . . . . . . . . . . . 16
14758zred 10994 . . . . . . . . . . . . . . . . 17
148 elfzle1 11718 . . . . . . . . . . . . . . . . . 18
14956, 148syl 16 . . . . . . . . . . . . . . . . 17
150 elfzle2 11719 . . . . . . . . . . . . . . . . . 18
15156, 150syl 16 . . . . . . . . . . . . . . . . 17
152 le2sq2 12243 . . . . . . . . . . . . . . . . 17
153147, 149, 142, 151, 152syl22anc 1229 . . . . . . . . . . . . . . . 16
154137, 61, 138, 138, 146, 153le2addd 10195 . . . . . . . . . . . . . . 15
155133nncnd 10577 . . . . . . . . . . . . . . . 16
1561552timesd 10806 . . . . . . . . . . . . . . 15
157154, 156breqtrrd 4478 . . . . . . . . . . . . . 14
158 2lt4 10731 . . . . . . . . . . . . . . . 16
159 2re 10630 . . . . . . . . . . . . . . . . . 18
160159a1i 11 . . . . . . . . . . . . . . . . 17
161 4re 10637 . . . . . . . . . . . . . . . . . 18
162161a1i 11 . . . . . . . . . . . . . . . . 17
163133nngt0d 10604 . . . . . . . . . . . . . . . . 17
164 ltmul1 10417 . . . . . . . . . . . . . . . . 17
165160, 162, 138, 163, 164syl112anc 1232 . . . . . . . . . . . . . . . 16
166158, 165mpbii 211 . . . . . . . . . . . . . . 15
167 2cn 10631 . . . . . . . . . . . . . . . . 17
168123nncnd 10577 . . . . . . . . . . . . . . . . 17
169 sqmul 12231 . . . . . . . . . . . . . . . . 17
170167, 168, 169sylancr 663 . . . . . . . . . . . . . . . 16
171 sq2 12264 . . . . . . . . . . . . . . . . 17
172171oveq1i 6306 . . . . . . . . . . . . . . . 16
173170, 172syl6eq 2514 . . . . . . . . . . . . . . 15
174166, 173breqtrrd 4478 . . . . . . . . . . . . . 14
175121, 136, 127, 157, 174lelttrd 9761 . . . . . . . . . . . . 13
176129nnrpd 11284 . . . . . . . . . . . . . 14
177127, 176ltaddrpd 11314 . . . . . . . . . . . . 13