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

Theorem prmreclem2 14435
Description: Lemma for prmrec 14440. There are at most squarefree numbers which divide no primes larger than . (We could strengthen this to 2 ( i^i(1 )) but there's no reason to.) We establish the inequality by showing that the prime counts of the number up to completely determine it because all higher prime counts are zero, and they are all at most because no square divides the number, so there are at most possibilities. (Contributed by Mario Carneiro, 5-Aug-2014.)
Hypotheses
Ref Expression
prmrec.1
prmrec.2
prmrec.3
prmrec.4
prmreclem2.5
Assertion
Ref Expression
prmreclem2
Distinct variable groups:   , , , ,   , , ,   ,M, ,   , , ,   Q, , , ,   ,N, ,

Proof of Theorem prmreclem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovex 6324 . . . 4
2 fveq2 5871 . . . . . . . 8
32eqeq1d 2459 . . . . . . 7
43elrab 3257 . . . . . 6
5 prmrec.4 . . . . . . . . . . . . . . . . . . . 20
6 ssrab2 3584 . . . . . . . . . . . . . . . . . . . 20
75, 6eqsstri 3533 . . . . . . . . . . . . . . . . . . 19
8 simprl 756 . . . . . . . . . . . . . . . . . . . 20
98ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
107, 9sseldi 3501 . . . . . . . . . . . . . . . . . 18
11 elfznn 11743 . . . . . . . . . . . . . . . . . 18
1210, 11syl 16 . . . . . . . . . . . . . . . . 17
13 simpr 461 . . . . . . . . . . . . . . . . . 18
14 prmuz2 14235 . . . . . . . . . . . . . . . . . 18
1513, 14syl 16 . . . . . . . . . . . . . . . . 17
16 prmreclem2.5 . . . . . . . . . . . . . . . . . . 19
1716prmreclem1 14434 . . . . . . . . . . . . . . . . . 18
1817simp3d 1010 . . . . . . . . . . . . . . . . 17
1912, 15, 18sylc 60 . . . . . . . . . . . . . . . 16
20 simprr 757 . . . . . . . . . . . . . . . . . . . . . . 23
2120ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22
2221oveq1d 6311 . . . . . . . . . . . . . . . . . . . . 21
23 sq1 12262 . . . . . . . . . . . . . . . . . . . . 21
2422, 23syl6eq 2514 . . . . . . . . . . . . . . . . . . . 20
2524oveq2d 6312 . . . . . . . . . . . . . . . . . . 19
2612nncnd 10577 . . . . . . . . . . . . . . . . . . . 20
2726div1d 10337 . . . . . . . . . . . . . . . . . . 19
2825, 27eqtrd 2498 . . . . . . . . . . . . . . . . . 18
2928breq2d 4464 . . . . . . . . . . . . . . . . 17
3012nnzd 10993 . . . . . . . . . . . . . . . . . 18
31 2nn0 10837 . . . . . . . . . . . . . . . . . . 19
3231a1i 11 . . . . . . . . . . . . . . . . . 18
33 pcdvdsb 14392 . . . . . . . . . . . . . . . . . 18
3413, 30, 32, 33syl3anc 1228 . . . . . . . . . . . . . . . . 17
3529, 34bitr4d 256 . . . . . . . . . . . . . . . 16
3619, 35mtbid 300 . . . . . . . . . . . . . . 15
3713, 12pccld 14374 . . . . . . . . . . . . . . . . 17
3837nn0red 10878 . . . . . . . . . . . . . . . 16
39 2re 10630 . . . . . . . . . . . . . . . 16
40 ltnle 9685 . . . . . . . . . . . . . . . 16
4138, 39, 40sylancl 662 . . . . . . . . . . . . . . 15
4236, 41mpbird 232 . . . . . . . . . . . . . 14
43 df-2 10619 . . . . . . . . . . . . . 14
4442, 43syl6breq 4491 . . . . . . . . . . . . 13
4537nn0zd 10992 . . . . . . . . . . . . . 14
46 1z 10919 . . . . . . . . . . . . . 14
47 zleltp1 10939 . . . . . . . . . . . . . 14
4845, 46, 47sylancl 662 . . . . . . . . . . . . 13
4944, 48mpbird 232 . . . . . . . . . . . 12
50 nn0uz 11144 . . . . . . . . . . . . . 14
5137, 50syl6eleq 2555 . . . . . . . . . . . . 13
52 elfz5 11709 . . . . . . . . . . . . 13
5351, 46, 52sylancl 662 . . . . . . . . . . . 12
5449, 53mpbird 232 . . . . . . . . . . 11
55 0z 10900 . . . . . . . . . . . . 13
56 fzpr 11764 . . . . . . . . . . . . 13
5755, 56ax-mp 5 . . . . . . . . . . . 12
58 1e0p1 11032 . . . . . . . . . . . . 13
5958oveq2i 6307 . . . . . . . . . . . 12
6058preq2i 4113 . . . . . . . . . . . 12
6157, 59, 603eqtr4i 2496 . . . . . . . . . . 11
6254, 61syl6eleq 2555 . . . . . . . . . 10
63 c0ex 9611 . . . . . . . . . . . 12
6463prid1 4138 . . . . . . . . . . 11
6564a1i 11 . . . . . . . . . 10
6662, 65ifclda 3973 . . . . . . . . 9
67 eqid 2457 . . . . . . . . 9
6866, 67fmptd 6055 . . . . . . . 8
69 prex 4694 . . . . . . . . 9
70 ovex 6324 . . . . . . . . 9
7169, 70elmap 7467 . . . . . . . 8
7268, 71sylibr 212 . . . . . . 7
7372ex 434 . . . . . 6
744, 73syl5bi 217 . . . . 5
75 fveq2 5871 . . . . . . . . 9
7675eqeq1d 2459 . . . . . . . 8
7776elrab 3257 . . . . . . 7
784, 77anbi12i 697 . . . . . 6
79 ovex 6324 . . . . . . . . . . . 12
8079, 63ifex 4010 . . . . . . . . . . 11
8180, 67fnmpti 5714 . . . . . . . . . 10
82 ovex 6324 . . . . . . . . . . . 12
8382, 63ifex 4010 . . . . . . . . . . 11
84 eqid 2457 . . . . . . . . . . 11
8583, 84fnmpti 5714 . . . . . . . . . 10
86 eqfnfv 5981 . . . . . . . . . 10
8781, 85, 86mp2an 672 . . . . . . . . 9
88 eleq1 2529 . . . . . . . . . . . . 13
89 oveq1 6303 . . . . . . . . . . . . 13
9088, 89ifbieq1d 3964 . . . . . . . . . . . 12
91 ovex 6324 . . . . . . . . . . . . 13
9291, 63ifex 4010 . . . . . . . . . . . 12
9390, 67, 92fvmpt 5956 . . . . . . . . . . 11
94 oveq1 6303 . . . . . . . . . . . . 13
9588, 94ifbieq1d 3964 . . . . . . . . . . . 12
96 ovex 6324 . . . . . . . . . . . . 13
9796, 63ifex 4010 . . . . . . . . . . . 12
9895, 84, 97fvmpt 5956 . . . . . . . . . . 11
9993, 98eqeq12d 2479 . . . . . . . . . 10
10099ralbiia 2887 . . . . . . . . 9
10187, 100bitri 249 . . . . . . . 8
102 simprll 763 . . . . . . . . . . . . 13
103 breq2 4456 . . . . . . . . . . . . . . . . 17
104103notbid 294 . . . . . . . . . . . . . . . 16
105104ralbidv 2896 . . . . . . . . . . . . . . 15
106105, 5elrab2 3259 . . . . . . . . . . . . . 14
107106simprbi 464 . . . . . . . . . . . . 13
108102, 107syl 16 . . . . . . . . . . . 12
109 simprrl 765 . . . . . . . . . . . . 13
110 breq2 4456 . . . . . . . . . . . . . . . . 17
111110notbid 294 . . . . . . . . . . . . . . . 16
112111ralbidv 2896 . . . . . . . . . . . . . . 15
113112, 5elrab2 3259 . . . . . . . . . . . . . 14
114113simprbi 464 . . . . . . . . . . . . 13
115109, 114syl 16 . . . . . . . . . . . 12
116 r19.26 2984 . . . . . . . . . . . . 13
117 eldifi 3625 . . . . . . . . . . . . . . . . 17
11811ssriv 3507 . . . . . . . . . . . . . . . . . . 19
1197, 118sstri 3512 . . . . . . . . . . . . . . . . . 18
120119, 102sseldi 3501 . . . . . . . . . . . . . . . . 17
121 pceq0 14394 . . . . . . . . . . . . . . . . 17
122117, 120, 121syl2anr 478 . . . . . . . . . . . . . . . 16
123119, 109sseldi 3501 . . . . . . . . . . . . . . . . 17
124 pceq0 14394 . . . . . . . . . . . . . . . . 17
125117, 123, 124syl2anr 478 . . . . . . . . . . . . . . . 16
126122, 125anbi12d 710 . . . . . . . . . . . . . . 15
127 eqtr3 2485 . . . . . . . . . . . . . . 15
128126, 127syl6bir 229 . . . . . . . . . . . . . 14
129128ralimdva 2865 . . . . . . . . . . . . 13
130116, 129syl5bir 218 . . . . . . . . . . . 12
131108, 115, 130mp2and 679 . . . . . . . . . . 11
132131biantrud 507 . . . . . . . . . 10
133 incom 3690 . . . . . . . . . . . . . . 15
134133uneq1i 3653 . . . . . . . . . . . . . 14
135 inundif 3906 . . . . . . . . . . . . . 14
136134, 135eqtri 2486 . . . . . . . . . . . . 13
137136raleqi 3058 . . . . . . . . . . . 12
138 ralunb 3684 . . . . . . . . . . . 12
139137, 138bitr3i 251 . . . . . . . . . . 11
140 eldifn 3626 . . . . . . . . . . . . . . 15
141 iffalse 3950 . . . . . . . . . . . . . . . 16
142 iffalse 3950 . . . . . . . . . . . . . . . 16
143141, 142eqtr4d 2501 . . . . . . . . . . . . . . 15
144140, 143syl 16 . . . . . . . . . . . . . 14
145144rgen 2817 . . . . . . . . . . . . 13
146145biantru 505 . . . . . . . . . . . 12
147 inss1 3717 . . . . . . . . . . . . . . 15
148147sseli 3499 . . . . . . . . . . . . . 14
149 iftrue 3947 . . . . . . . . . . . . . . 15
150 iftrue 3947 . . . . . . . . . . . . . . 15
151149, 150eqeq12d 2479 . . . . . . . . . . . . . 14
152148, 151syl 16 . . . . . . . . . . . . 13
153152ralbiia 2887 . . . . . . . . . . . 12
154146, 153bitr3i 251 . . . . . . . . . . 11
155139, 154bitri 249 . . . . . . . . . 10
156 inundif 3906 . . . . . . . . . . . 12
157156raleqi 3058 . . . . . . . . . . 11
158 ralunb 3684 . . . . . . . . . . 11
159157, 158bitr3i 251 . . . . . . . . . 10
160132, 155, 1593bitr4g 288 . . . . . . . . 9
161120nnnn0d 10877 . . . . . . . . . 10
162123nnnn0d 10877 . . . . . . . . . 10
163 pc11 14403 . . . . . . . . . 10
164161, 162, 163syl2anc 661 . . . . . . . . 9
165160, 164bitr4d 256 . . . . . . . 8
166101, 165syl5bb 257 . . . . . . 7
167166ex 434 . . . . . 6
16878, 167syl5bi 217 . . . . 5