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

Theorem prmreclem2 14297
Description: Lemma for prmrec 14302. There are at most  2 ^ K squarefree numbers which divide no primes larger than  K. (We could strengthen this to  2 ^ # ( Prime  i^i  ( 1 ... K ) ) but there's no reason to.) We establish the inequality by showing that the prime counts of the number up to  K completely determine it because all higher prime counts are zero, and they are all at most  1 because no square divides the number, so there are at most  2 ^ K possibilities. (Contributed by Mario Carneiro, 5-Aug-2014.)
Hypotheses
Ref Expression
prmrec.1  |-  F  =  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( 1  /  n
) ,  0 ) )
prmrec.2  |-  ( ph  ->  K  e.  NN )
prmrec.3  |-  ( ph  ->  N  e.  NN )
prmrec.4  |-  M  =  { n  e.  ( 1 ... N )  |  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  n }
prmreclem2.5  |-  Q  =  ( n  e.  NN  |->  sup ( { r  e.  NN  |  ( r ^ 2 )  ||  n } ,  RR ,  <  ) )
Assertion
Ref Expression
prmreclem2  |-  ( ph  ->  ( # `  {
x  e.  M  | 
( Q `  x
)  =  1 } )  <_  ( 2 ^ K ) )
Distinct variable groups:    n, p, r, x, F    n, K, p, x    n, M, p, x    ph, n, p, x    Q, n, p, r, x   
n, N, p, x
Allowed substitution hints:    ph( r)    K( r)    M( r)    N( r)

Proof of Theorem prmreclem2
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovex 6310 . . . 4  |-  ( { 0 ,  1 }  ^m  ( 1 ... K ) )  e. 
_V
2 fveq2 5866 . . . . . . . 8  |-  ( x  =  y  ->  ( Q `  x )  =  ( Q `  y ) )
32eqeq1d 2469 . . . . . . 7  |-  ( x  =  y  ->  (
( Q `  x
)  =  1  <->  ( Q `  y )  =  1 ) )
43elrab 3261 . . . . . 6  |-  ( y  e.  { x  e.  M  |  ( Q `
 x )  =  1 }  <->  ( y  e.  M  /\  ( Q `  y )  =  1 ) )
5 prmrec.4 . . . . . . . . . . . . . . . . . . . 20  |-  M  =  { n  e.  ( 1 ... N )  |  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  n }
6 ssrab2 3585 . . . . . . . . . . . . . . . . . . . 20  |-  { n  e.  ( 1 ... N
)  |  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  n }  C_  ( 1 ... N )
75, 6eqsstri 3534 . . . . . . . . . . . . . . . . . . 19  |-  M  C_  ( 1 ... N
)
8 simprl 755 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( y  e.  M  /\  ( Q `  y )  =  1 ) )  ->  y  e.  M
)
98ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  y  e.  M )
107, 9sseldi 3502 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  y  e.  ( 1 ... N
) )
11 elfznn 11715 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 ... N )  ->  y  e.  NN )
1210, 11syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  y  e.  NN )
13 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  n  e.  Prime )
14 prmuz2 14097 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  Prime  ->  n  e.  ( ZZ>= `  2 )
)
1513, 14syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  n  e.  ( ZZ>= `  2 )
)
16 prmreclem2.5 . . . . . . . . . . . . . . . . . . 19  |-  Q  =  ( n  e.  NN  |->  sup ( { r  e.  NN  |  ( r ^ 2 )  ||  n } ,  RR ,  <  ) )
1716prmreclem1 14296 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
( Q `  y
)  e.  NN  /\  ( ( Q `  y ) ^ 2 )  ||  y  /\  ( n  e.  ( ZZ>=
`  2 )  ->  -.  ( n ^ 2 )  ||  ( y  /  ( ( Q `
 y ) ^
2 ) ) ) ) )
1817simp3d 1010 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
n  e.  ( ZZ>= ` 
2 )  ->  -.  ( n ^ 2 )  ||  ( y  /  ( ( Q `
 y ) ^
2 ) ) ) )
1912, 15, 18sylc 60 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  -.  ( n ^ 2 )  ||  ( y  /  ( ( Q `
 y ) ^
2 ) ) )
20 simprr 756 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( y  e.  M  /\  ( Q `  y )  =  1 ) )  ->  ( Q `  y )  =  1 )
2120ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  ( Q `  y )  =  1 )
2221oveq1d 6300 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
( Q `  y
) ^ 2 )  =  ( 1 ^ 2 ) )
23 sq1 12231 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1 ^ 2 )  =  1
2422, 23syl6eq 2524 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
( Q `  y
) ^ 2 )  =  1 )
2524oveq2d 6301 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
y  /  ( ( Q `  y ) ^ 2 ) )  =  ( y  / 
1 ) )
2612nncnd 10553 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  y  e.  CC )
2726div1d 10313 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
y  /  1 )  =  y )
2825, 27eqtrd 2508 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
y  /  ( ( Q `  y ) ^ 2 ) )  =  y )
2928breq2d 4459 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
( n ^ 2 )  ||  ( y  /  ( ( Q `
 y ) ^
2 ) )  <->  ( n ^ 2 )  ||  y ) )
3012nnzd 10966 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  y  e.  ZZ )
31 2nn0 10813 . . . . . . . . . . . . . . . . . . 19  |-  2  e.  NN0
3231a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  2  e.  NN0 )
33 pcdvdsb 14254 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  Prime  /\  y  e.  ZZ  /\  2  e. 
NN0 )  ->  (
2  <_  ( n  pCnt  y )  <->  ( n ^ 2 )  ||  y ) )
3413, 30, 32, 33syl3anc 1228 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
2  <_  ( n  pCnt  y )  <->  ( n ^ 2 )  ||  y ) )
3529, 34bitr4d 256 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
( n ^ 2 )  ||  ( y  /  ( ( Q `
 y ) ^
2 ) )  <->  2  <_  ( n  pCnt  y )
) )
3619, 35mtbid 300 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  -.  2  <_  ( n  pCnt  y ) )
3713, 12pccld 14236 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
n  pCnt  y )  e.  NN0 )
3837nn0red 10854 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
n  pCnt  y )  e.  RR )
39 2re 10606 . . . . . . . . . . . . . . . 16  |-  2  e.  RR
40 ltnle 9665 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  pCnt  y
)  e.  RR  /\  2  e.  RR )  ->  ( ( n  pCnt  y )  <  2  <->  -.  2  <_  ( n  pCnt  y ) ) )
4138, 39, 40sylancl 662 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
( n  pCnt  y
)  <  2  <->  -.  2  <_  ( n  pCnt  y
) ) )
4236, 41mpbird 232 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
n  pCnt  y )  <  2 )
43 df-2 10595 . . . . . . . . . . . . . 14  |-  2  =  ( 1  +  1 )
4442, 43syl6breq 4486 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
n  pCnt  y )  <  ( 1  +  1 ) )
4537nn0zd 10965 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
n  pCnt  y )  e.  ZZ )
46 1z 10895 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
47 zleltp1 10914 . . . . . . . . . . . . . 14  |-  ( ( ( n  pCnt  y
)  e.  ZZ  /\  1  e.  ZZ )  ->  ( ( n  pCnt  y )  <_  1  <->  ( n  pCnt  y )  <  (
1  +  1 ) ) )
4845, 46, 47sylancl 662 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
( n  pCnt  y
)  <_  1  <->  ( n  pCnt  y )  <  (
1  +  1 ) ) )
4944, 48mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
n  pCnt  y )  <_  1 )
50 nn0uz 11117 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  0 )
5137, 50syl6eleq 2565 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
n  pCnt  y )  e.  ( ZZ>= `  0 )
)
52 elfz5 11681 . . . . . . . . . . . . 13  |-  ( ( ( n  pCnt  y
)  e.  ( ZZ>= ` 
0 )  /\  1  e.  ZZ )  ->  (
( n  pCnt  y
)  e.  ( 0 ... 1 )  <->  ( n  pCnt  y )  <_  1
) )
5351, 46, 52sylancl 662 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
( n  pCnt  y
)  e.  ( 0 ... 1 )  <->  ( n  pCnt  y )  <_  1
) )
5449, 53mpbird 232 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
n  pCnt  y )  e.  ( 0 ... 1
) )
55 0z 10876 . . . . . . . . . . . . 13  |-  0  e.  ZZ
56 fzpr 11736 . . . . . . . . . . . . 13  |-  ( 0  e.  ZZ  ->  (
0 ... ( 0  +  1 ) )  =  { 0 ,  ( 0  +  1 ) } )
5755, 56ax-mp 5 . . . . . . . . . . . 12  |-  ( 0 ... ( 0  +  1 ) )  =  { 0 ,  ( 0  +  1 ) }
58 1e0p1 11005 . . . . . . . . . . . . 13  |-  1  =  ( 0  +  1 )
5958oveq2i 6296 . . . . . . . . . . . 12  |-  ( 0 ... 1 )  =  ( 0 ... (
0  +  1 ) )
6058preq2i 4110 . . . . . . . . . . . 12  |-  { 0 ,  1 }  =  { 0 ,  ( 0  +  1 ) }
6157, 59, 603eqtr4i 2506 . . . . . . . . . . 11  |-  ( 0 ... 1 )  =  { 0 ,  1 }
6254, 61syl6eleq 2565 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  n  e.  Prime )  ->  (
n  pCnt  y )  e.  { 0 ,  1 } )
63 c0ex 9591 . . . . . . . . . . . 12  |-  0  e.  _V
6463prid1 4135 . . . . . . . . . . 11  |-  0  e.  { 0 ,  1 }
6564a1i 11 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( y  e.  M  /\  ( Q `  y
)  =  1 ) )  /\  n  e.  ( 1 ... K
) )  /\  -.  n  e.  Prime )  -> 
0  e.  { 0 ,  1 } )
6662, 65ifclda 3971 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  M  /\  ( Q `  y )  =  1 ) )  /\  n  e.  ( 1 ... K ) )  ->  if (
n  e.  Prime ,  ( n  pCnt  y ) ,  0 )  e. 
{ 0 ,  1 } )
67 eqid 2467 . . . . . . . . 9  |-  ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  y ) ,  0 ) )  =  ( n  e.  ( 1 ... K
)  |->  if ( n  e.  Prime ,  ( n 
pCnt  y ) ,  0 ) )
6866, 67fmptd 6046 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  M  /\  ( Q `  y )  =  1 ) )  ->  ( n  e.  ( 1 ... K
)  |->  if ( n  e.  Prime ,  ( n 
pCnt  y ) ,  0 ) ) : ( 1 ... K
) --> { 0 ,  1 } )
69 prex 4689 . . . . . . . . 9  |-  { 0 ,  1 }  e.  _V
70 ovex 6310 . . . . . . . . 9  |-  ( 1 ... K )  e. 
_V
7169, 70elmap 7448 . . . . . . . 8  |-  ( ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  y
) ,  0 ) )  e.  ( { 0 ,  1 }  ^m  ( 1 ... K ) )  <->  ( n  e.  ( 1 ... K
)  |->  if ( n  e.  Prime ,  ( n 
pCnt  y ) ,  0 ) ) : ( 1 ... K
) --> { 0 ,  1 } )
7268, 71sylibr 212 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  M  /\  ( Q `  y )  =  1 ) )  ->  ( n  e.  ( 1 ... K
)  |->  if ( n  e.  Prime ,  ( n 
pCnt  y ) ,  0 ) )  e.  ( { 0 ,  1 }  ^m  (
1 ... K ) ) )
7372ex 434 . . . . . 6  |-  ( ph  ->  ( ( y  e.  M  /\  ( Q `
 y )  =  1 )  ->  (
n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  y
) ,  0 ) )  e.  ( { 0 ,  1 }  ^m  ( 1 ... K ) ) ) )
744, 73syl5bi 217 . . . . 5  |-  ( ph  ->  ( y  e.  {
x  e.  M  | 
( Q `  x
)  =  1 }  ->  ( n  e.  ( 1 ... K
)  |->  if ( n  e.  Prime ,  ( n 
pCnt  y ) ,  0 ) )  e.  ( { 0 ,  1 }  ^m  (
1 ... K ) ) ) )
75 fveq2 5866 . . . . . . . . 9  |-  ( x  =  z  ->  ( Q `  x )  =  ( Q `  z ) )
7675eqeq1d 2469 . . . . . . . 8  |-  ( x  =  z  ->  (
( Q `  x
)  =  1  <->  ( Q `  z )  =  1 ) )
7776elrab 3261 . . . . . . 7  |-  ( z  e.  { x  e.  M  |  ( Q `
 x )  =  1 }  <->  ( z  e.  M  /\  ( Q `  z )  =  1 ) )
784, 77anbi12i 697 . . . . . 6  |-  ( ( y  e.  { x  e.  M  |  ( Q `  x )  =  1 }  /\  z  e.  { x  e.  M  |  ( Q `  x )  =  1 } )  <-> 
( ( y  e.  M  /\  ( Q `
 y )  =  1 )  /\  (
z  e.  M  /\  ( Q `  z )  =  1 ) ) )
79 ovex 6310 . . . . . . . . . . . 12  |-  ( n 
pCnt  y )  e. 
_V
8079, 63ifex 4008 . . . . . . . . . . 11  |-  if ( n  e.  Prime ,  ( n  pCnt  y ) ,  0 )  e. 
_V
8180, 67fnmpti 5709 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  y ) ,  0 ) )  Fn  ( 1 ... K )
82 ovex 6310 . . . . . . . . . . . 12  |-  ( n 
pCnt  z )  e. 
_V
8382, 63ifex 4008 . . . . . . . . . . 11  |-  if ( n  e.  Prime ,  ( n  pCnt  z ) ,  0 )  e. 
_V
84 eqid 2467 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  z ) ,  0 ) )  =  ( n  e.  ( 1 ... K
)  |->  if ( n  e.  Prime ,  ( n 
pCnt  z ) ,  0 ) )
8583, 84fnmpti 5709 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  z ) ,  0 ) )  Fn  ( 1 ... K )
86 eqfnfv 5976 . . . . . . . . . 10  |-  ( ( ( n  e.  ( 1 ... K ) 
|->  if ( n  e. 
Prime ,  ( n  pCnt  y ) ,  0 ) )  Fn  (
1 ... K )  /\  ( n  e.  (
1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  z
) ,  0 ) )  Fn  ( 1 ... K ) )  ->  ( ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  y ) ,  0 ) )  =  ( n  e.  ( 1 ... K
)  |->  if ( n  e.  Prime ,  ( n 
pCnt  z ) ,  0 ) )  <->  A. p  e.  ( 1 ... K
) ( ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  y ) ,  0 ) ) `
 p )  =  ( ( n  e.  ( 1 ... K
)  |->  if ( n  e.  Prime ,  ( n 
pCnt  z ) ,  0 ) ) `  p ) ) )
8781, 85, 86mp2an 672 . . . . . . . . 9  |-  ( ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  y
) ,  0 ) )  =  ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  z ) ,  0 ) )  <->  A. p  e.  (
1 ... K ) ( ( n  e.  ( 1 ... K ) 
|->  if ( n  e. 
Prime ,  ( n  pCnt  y ) ,  0 ) ) `  p
)  =  ( ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  z
) ,  0 ) ) `  p ) )
88 eleq1 2539 . . . . . . . . . . . . 13  |-  ( n  =  p  ->  (
n  e.  Prime  <->  p  e.  Prime ) )
89 oveq1 6292 . . . . . . . . . . . . 13  |-  ( n  =  p  ->  (
n  pCnt  y )  =  ( p  pCnt  y ) )
9088, 89ifbieq1d 3962 . . . . . . . . . . . 12  |-  ( n  =  p  ->  if ( n  e.  Prime ,  ( n  pCnt  y
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  y ) ,  0 ) )
91 ovex 6310 . . . . . . . . . . . . 13  |-  ( p 
pCnt  y )  e. 
_V
9291, 63ifex 4008 . . . . . . . . . . . 12  |-  if ( p  e.  Prime ,  ( p  pCnt  y ) ,  0 )  e. 
_V
9390, 67, 92fvmpt 5951 . . . . . . . . . . 11  |-  ( p  e.  ( 1 ... K )  ->  (
( n  e.  ( 1 ... K ) 
|->  if ( n  e. 
Prime ,  ( n  pCnt  y ) ,  0 ) ) `  p
)  =  if ( p  e.  Prime ,  ( p  pCnt  y ) ,  0 ) )
94 oveq1 6292 . . . . . . . . . . . . 13  |-  ( n  =  p  ->  (
n  pCnt  z )  =  ( p  pCnt  z ) )
9588, 94ifbieq1d 3962 . . . . . . . . . . . 12  |-  ( n  =  p  ->  if ( n  e.  Prime ,  ( n  pCnt  z
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  z ) ,  0 ) )
96 ovex 6310 . . . . . . . . . . . . 13  |-  ( p 
pCnt  z )  e. 
_V
9796, 63ifex 4008 . . . . . . . . . . . 12  |-  if ( p  e.  Prime ,  ( p  pCnt  z ) ,  0 )  e. 
_V
9895, 84, 97fvmpt 5951 . . . . . . . . . . 11  |-  ( p  e.  ( 1 ... K )  ->  (
( n  e.  ( 1 ... K ) 
|->  if ( n  e. 
Prime ,  ( n  pCnt  z ) ,  0 ) ) `  p
)  =  if ( p  e.  Prime ,  ( p  pCnt  z ) ,  0 ) )
9993, 98eqeq12d 2489 . . . . . . . . . 10  |-  ( p  e.  ( 1 ... K )  ->  (
( ( n  e.  ( 1 ... K
)  |->  if ( n  e.  Prime ,  ( n 
pCnt  y ) ,  0 ) ) `  p )  =  ( ( n  e.  ( 1 ... K ) 
|->  if ( n  e. 
Prime ,  ( n  pCnt  z ) ,  0 ) ) `  p
)  <->  if ( p  e. 
Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e.  Prime ,  ( p  pCnt  z ) ,  0 ) ) )
10099ralbiia 2894 . . . . . . . . 9  |-  ( A. p  e.  ( 1 ... K ) ( ( n  e.  ( 1 ... K ) 
|->  if ( n  e. 
Prime ,  ( n  pCnt  y ) ,  0 ) ) `  p
)  =  ( ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  z
) ,  0 ) ) `  p )  <->  A. p  e.  (
1 ... K ) if ( p  e.  Prime ,  ( p  pCnt  y
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  z ) ,  0 ) )
10187, 100bitri 249 . . . . . . . 8  |-  ( ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  y
) ,  0 ) )  =  ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  z ) ,  0 ) )  <->  A. p  e.  (
1 ... K ) if ( p  e.  Prime ,  ( p  pCnt  y
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  z ) ,  0 ) )
102 simprll 761 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  y  e.  M )
103 breq2 4451 . . . . . . . . . . . . . . . . 17  |-  ( n  =  y  ->  (
p  ||  n  <->  p  ||  y
) )
104103notbid 294 . . . . . . . . . . . . . . . 16  |-  ( n  =  y  ->  ( -.  p  ||  n  <->  -.  p  ||  y ) )
105104ralbidv 2903 . . . . . . . . . . . . . . 15  |-  ( n  =  y  ->  ( A. p  e.  ( Prime  \  ( 1 ... K ) )  -.  p  ||  n  <->  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  y
) )
106105, 5elrab2 3263 . . . . . . . . . . . . . 14  |-  ( y  e.  M  <->  ( y  e.  ( 1 ... N
)  /\  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  y
) )
107106simprbi 464 . . . . . . . . . . . . 13  |-  ( y  e.  M  ->  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  y
)
108102, 107syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  y
)
109 simprrl 763 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  z  e.  M )
110 breq2 4451 . . . . . . . . . . . . . . . . 17  |-  ( n  =  z  ->  (
p  ||  n  <->  p  ||  z
) )
111110notbid 294 . . . . . . . . . . . . . . . 16  |-  ( n  =  z  ->  ( -.  p  ||  n  <->  -.  p  ||  z ) )
112111ralbidv 2903 . . . . . . . . . . . . . . 15  |-  ( n  =  z  ->  ( A. p  e.  ( Prime  \  ( 1 ... K ) )  -.  p  ||  n  <->  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  z
) )
113112, 5elrab2 3263 . . . . . . . . . . . . . 14  |-  ( z  e.  M  <->  ( z  e.  ( 1 ... N
)  /\  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  z
) )
114113simprbi 464 . . . . . . . . . . . . 13  |-  ( z  e.  M  ->  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  z
)
115109, 114syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  z
)
116 r19.26 2989 . . . . . . . . . . . . 13  |-  ( A. p  e.  ( Prime  \  ( 1 ... K
) ) ( -.  p  ||  y  /\  -.  p  ||  z )  <-> 
( A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  y  /\  A. p  e.  ( Prime  \  ( 1 ... K ) )  -.  p  ||  z
) )
117 eldifi 3626 . . . . . . . . . . . . . . . . 17  |-  ( p  e.  ( Prime  \  (
1 ... K ) )  ->  p  e.  Prime )
11811ssriv 3508 . . . . . . . . . . . . . . . . . . 19  |-  ( 1 ... N )  C_  NN
1197, 118sstri 3513 . . . . . . . . . . . . . . . . . 18  |-  M  C_  NN
120119, 102sseldi 3502 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  y  e.  NN )
121 pceq0 14256 . . . . . . . . . . . . . . . . 17  |-  ( ( p  e.  Prime  /\  y  e.  NN )  ->  (
( p  pCnt  y
)  =  0  <->  -.  p  ||  y ) )
122117, 120, 121syl2anr 478 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
( y  e.  M  /\  ( Q `  y
)  =  1 )  /\  ( z  e.  M  /\  ( Q `
 z )  =  1 ) ) )  /\  p  e.  ( Prime  \  ( 1 ... K ) ) )  ->  ( (
p  pCnt  y )  =  0  <->  -.  p  ||  y ) )
123119, 109sseldi 3502 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  z  e.  NN )
124 pceq0 14256 . . . . . . . . . . . . . . . . 17  |-  ( ( p  e.  Prime  /\  z  e.  NN )  ->  (
( p  pCnt  z
)  =  0  <->  -.  p  ||  z ) )
125117, 123, 124syl2anr 478 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
( y  e.  M  /\  ( Q `  y
)  =  1 )  /\  ( z  e.  M  /\  ( Q `
 z )  =  1 ) ) )  /\  p  e.  ( Prime  \  ( 1 ... K ) ) )  ->  ( (
p  pCnt  z )  =  0  <->  -.  p  ||  z ) )
126122, 125anbi12d 710 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( y  e.  M  /\  ( Q `  y
)  =  1 )  /\  ( z  e.  M  /\  ( Q `
 z )  =  1 ) ) )  /\  p  e.  ( Prime  \  ( 1 ... K ) ) )  ->  ( (
( p  pCnt  y
)  =  0  /\  ( p  pCnt  z
)  =  0 )  <-> 
( -.  p  ||  y  /\  -.  p  ||  z ) ) )
127 eqtr3 2495 . . . . . . . . . . . . . . 15  |-  ( ( ( p  pCnt  y
)  =  0  /\  ( p  pCnt  z
)  =  0 )  ->  ( p  pCnt  y )  =  ( p 
pCnt  z ) )
128126, 127syl6bir 229 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
( y  e.  M  /\  ( Q `  y
)  =  1 )  /\  ( z  e.  M  /\  ( Q `
 z )  =  1 ) ) )  /\  p  e.  ( Prime  \  ( 1 ... K ) ) )  ->  ( ( -.  p  ||  y  /\  -.  p  ||  z )  ->  ( p  pCnt  y )  =  ( p 
pCnt  z ) ) )
129128ralimdva 2872 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  ( A. p  e.  ( Prime  \  ( 1 ... K ) ) ( -.  p  ||  y  /\  -.  p  ||  z
)  ->  A. p  e.  ( Prime  \  (
1 ... K ) ) ( p  pCnt  y
)  =  ( p 
pCnt  z ) ) )
130116, 129syl5bir 218 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  (
( A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  y  /\  A. p  e.  ( Prime  \  ( 1 ... K ) )  -.  p  ||  z
)  ->  A. p  e.  ( Prime  \  (
1 ... K ) ) ( p  pCnt  y
)  =  ( p 
pCnt  z ) ) )
131108, 115, 130mp2and 679 . . . . . . . . . . 11  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  A. p  e.  ( Prime  \  (
1 ... K ) ) ( p  pCnt  y
)  =  ( p 
pCnt  z ) )
132131biantrud 507 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  ( A. p  e.  ( Prime  i^i  ( 1 ... K ) ) ( p  pCnt  y )  =  ( p  pCnt  z )  <->  ( A. p  e.  ( Prime  i^i  (
1 ... K ) ) ( p  pCnt  y
)  =  ( p 
pCnt  z )  /\  A. p  e.  ( Prime  \  ( 1 ... K ) ) ( p  pCnt  y )  =  ( p  pCnt  z ) ) ) )
133 incom 3691 . . . . . . . . . . . . . . 15  |-  ( Prime  i^i  ( 1 ... K
) )  =  ( ( 1 ... K
)  i^i  Prime )
134133uneq1i 3654 . . . . . . . . . . . . . 14  |-  ( ( Prime  i^i  ( 1 ... K ) )  u.  ( ( 1 ... K )  \  Prime ) )  =  ( ( ( 1 ... K )  i^i  Prime )  u.  ( ( 1 ... K )  \  Prime ) )
135 inundif 3905 . . . . . . . . . . . . . 14  |-  ( ( ( 1 ... K
)  i^i  Prime )  u.  ( ( 1 ... K )  \  Prime ) )  =  ( 1 ... K )
136134, 135eqtri 2496 . . . . . . . . . . . . 13  |-  ( ( Prime  i^i  ( 1 ... K ) )  u.  ( ( 1 ... K )  \  Prime ) )  =  ( 1 ... K )
137136raleqi 3062 . . . . . . . . . . . 12  |-  ( A. p  e.  ( ( Prime  i^i  ( 1 ... K ) )  u.  ( ( 1 ... K )  \  Prime ) ) if ( p  e.  Prime ,  ( p 
pCnt  y ) ,  0 )  =  if ( p  e.  Prime ,  ( p  pCnt  z
) ,  0 )  <->  A. p  e.  (
1 ... K ) if ( p  e.  Prime ,  ( p  pCnt  y
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  z ) ,  0 ) )
138 ralunb 3685 . . . . . . . . . . . 12  |-  ( A. p  e.  ( ( Prime  i^i  ( 1 ... K ) )  u.  ( ( 1 ... K )  \  Prime ) ) if ( p  e.  Prime ,  ( p 
pCnt  y ) ,  0 )  =  if ( p  e.  Prime ,  ( p  pCnt  z
) ,  0 )  <-> 
( A. p  e.  ( Prime  i^i  (
1 ... K ) ) if ( p  e. 
Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e.  Prime ,  ( p  pCnt  z ) ,  0 )  /\  A. p  e.  ( ( 1 ... K ) 
\  Prime ) if ( p  e.  Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e. 
Prime ,  ( p  pCnt  z ) ,  0 ) ) )
139137, 138bitr3i 251 . . . . . . . . . . 11  |-  ( A. p  e.  ( 1 ... K ) if ( p  e.  Prime ,  ( p  pCnt  y
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  z ) ,  0 )  <->  ( A. p  e.  ( Prime  i^i  ( 1 ... K
) ) if ( p  e.  Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e. 
Prime ,  ( p  pCnt  z ) ,  0 )  /\  A. p  e.  ( ( 1 ... K )  \  Prime ) if ( p  e. 
Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e.  Prime ,  ( p  pCnt  z ) ,  0 ) ) )
140 eldifn 3627 . . . . . . . . . . . . . . 15  |-  ( p  e.  ( ( 1 ... K )  \  Prime )  ->  -.  p  e.  Prime )
141 iffalse 3948 . . . . . . . . . . . . . . . 16  |-  ( -.  p  e.  Prime  ->  if ( p  e.  Prime ,  ( p  pCnt  y
) ,  0 )  =  0 )
142 iffalse 3948 . . . . . . . . . . . . . . . 16  |-  ( -.  p  e.  Prime  ->  if ( p  e.  Prime ,  ( p  pCnt  z
) ,  0 )  =  0 )
143141, 142eqtr4d 2511 . . . . . . . . . . . . . . 15  |-  ( -.  p  e.  Prime  ->  if ( p  e.  Prime ,  ( p  pCnt  y
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  z ) ,  0 ) )
144140, 143syl 16 . . . . . . . . . . . . . 14  |-  ( p  e.  ( ( 1 ... K )  \  Prime )  ->  if (
p  e.  Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e. 
Prime ,  ( p  pCnt  z ) ,  0 ) )
145144rgen 2824 . . . . . . . . . . . . 13  |-  A. p  e.  ( ( 1 ... K )  \  Prime ) if ( p  e. 
Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e.  Prime ,  ( p  pCnt  z ) ,  0 )
146145biantru 505 . . . . . . . . . . . 12  |-  ( A. p  e.  ( Prime  i^i  ( 1 ... K
) ) if ( p  e.  Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e. 
Prime ,  ( p  pCnt  z ) ,  0 )  <->  ( A. p  e.  ( Prime  i^i  (
1 ... K ) ) if ( p  e. 
Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e.  Prime ,  ( p  pCnt  z ) ,  0 )  /\  A. p  e.  ( ( 1 ... K ) 
\  Prime ) if ( p  e.  Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e. 
Prime ,  ( p  pCnt  z ) ,  0 ) ) )
147 inss1 3718 . . . . . . . . . . . . . . 15  |-  ( Prime  i^i  ( 1 ... K
) )  C_  Prime
148147sseli 3500 . . . . . . . . . . . . . 14  |-  ( p  e.  ( Prime  i^i  ( 1 ... K
) )  ->  p  e.  Prime )
149 iftrue 3945 . . . . . . . . . . . . . . 15  |-  ( p  e.  Prime  ->  if ( p  e.  Prime ,  ( p  pCnt  y ) ,  0 )  =  ( p  pCnt  y
) )
150 iftrue 3945 . . . . . . . . . . . . . . 15  |-  ( p  e.  Prime  ->  if ( p  e.  Prime ,  ( p  pCnt  z ) ,  0 )  =  ( p  pCnt  z
) )
151149, 150eqeq12d 2489 . . . . . . . . . . . . . 14  |-  ( p  e.  Prime  ->  ( if ( p  e.  Prime ,  ( p  pCnt  y
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  z ) ,  0 )  <->  ( p  pCnt  y )  =  ( p  pCnt  z )
) )
152148, 151syl 16 . . . . . . . . . . . . 13  |-  ( p  e.  ( Prime  i^i  ( 1 ... K
) )  ->  ( if ( p  e.  Prime ,  ( p  pCnt  y
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  z ) ,  0 )  <->  ( p  pCnt  y )  =  ( p  pCnt  z )
) )
153152ralbiia 2894 . . . . . . . . . . . 12  |-  ( A. p  e.  ( Prime  i^i  ( 1 ... K
) ) if ( p  e.  Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e. 
Prime ,  ( p  pCnt  z ) ,  0 )  <->  A. p  e.  ( Prime  i^i  ( 1 ... K ) ) ( p  pCnt  y
)  =  ( p 
pCnt  z ) )
154146, 153bitr3i 251 . . . . . . . . . . 11  |-  ( ( A. p  e.  ( Prime  i^i  ( 1 ... K ) ) if ( p  e. 
Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e.  Prime ,  ( p  pCnt  z ) ,  0 )  /\  A. p  e.  ( ( 1 ... K ) 
\  Prime ) if ( p  e.  Prime ,  ( p  pCnt  y ) ,  0 )  =  if ( p  e. 
Prime ,  ( p  pCnt  z ) ,  0 ) )  <->  A. p  e.  ( Prime  i^i  (
1 ... K ) ) ( p  pCnt  y
)  =  ( p 
pCnt  z ) )
155139, 154bitri 249 . . . . . . . . . 10  |-  ( A. p  e.  ( 1 ... K ) if ( p  e.  Prime ,  ( p  pCnt  y
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  z ) ,  0 )  <->  A. p  e.  ( Prime  i^i  (
1 ... K ) ) ( p  pCnt  y
)  =  ( p 
pCnt  z ) )
156 inundif 3905 . . . . . . . . . . . 12  |-  ( ( Prime  i^i  ( 1 ... K ) )  u.  ( Prime  \  (
1 ... K ) ) )  =  Prime
157156raleqi 3062 . . . . . . . . . . 11  |-  ( A. p  e.  ( ( Prime  i^i  ( 1 ... K ) )  u.  ( Prime  \  (
1 ... K ) ) ) ( p  pCnt  y )  =  ( p 
pCnt  z )  <->  A. p  e.  Prime  ( p  pCnt  y )  =  ( p 
pCnt  z ) )
158 ralunb 3685 . . . . . . . . . . 11  |-  ( A. p  e.  ( ( Prime  i^i  ( 1 ... K ) )  u.  ( Prime  \  (
1 ... K ) ) ) ( p  pCnt  y )  =  ( p 
pCnt  z )  <->  ( A. p  e.  ( Prime  i^i  ( 1 ... K
) ) ( p 
pCnt  y )  =  ( p  pCnt  z
)  /\  A. p  e.  ( Prime  \  (
1 ... K ) ) ( p  pCnt  y
)  =  ( p 
pCnt  z ) ) )
159157, 158bitr3i 251 . . . . . . . . . 10  |-  ( A. p  e.  Prime  ( p 
pCnt  y )  =  ( p  pCnt  z
)  <->  ( A. p  e.  ( Prime  i^i  (
1 ... K ) ) ( p  pCnt  y
)  =  ( p 
pCnt  z )  /\  A. p  e.  ( Prime  \  ( 1 ... K ) ) ( p  pCnt  y )  =  ( p  pCnt  z ) ) )
160132, 155, 1593bitr4g 288 . . . . . . . . 9  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  ( A. p  e.  (
1 ... K ) if ( p  e.  Prime ,  ( p  pCnt  y
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  z ) ,  0 )  <->  A. p  e.  Prime  ( p  pCnt  y )  =  ( p 
pCnt  z ) ) )
161120nnnn0d 10853 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  y  e.  NN0 )
162123nnnn0d 10853 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  z  e.  NN0 )
163 pc11 14265 . . . . . . . . . 10  |-  ( ( y  e.  NN0  /\  z  e.  NN0 )  -> 
( y  =  z  <->  A. p  e.  Prime  ( p  pCnt  y )  =  ( p  pCnt  z ) ) )
164161, 162, 163syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  (
y  =  z  <->  A. p  e.  Prime  ( p  pCnt  y )  =  ( p 
pCnt  z ) ) )
165160, 164bitr4d 256 . . . . . . . 8  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  ( A. p  e.  (
1 ... K ) if ( p  e.  Prime ,  ( p  pCnt  y
) ,  0 )  =  if ( p  e.  Prime ,  ( p 
pCnt  z ) ,  0 )  <->  y  =  z ) )
166101, 165syl5bb 257 . . . . . . 7  |-  ( (
ph  /\  ( (
y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) ) )  ->  (
( n  e.  ( 1 ... K ) 
|->  if ( n  e. 
Prime ,  ( n  pCnt  y ) ,  0 ) )  =  ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  z
) ,  0 ) )  <->  y  =  z ) )
167166ex 434 . . . . . 6  |-  ( ph  ->  ( ( ( y  e.  M  /\  ( Q `  y )  =  1 )  /\  ( z  e.  M  /\  ( Q `  z
)  =  1 ) )  ->  ( (
n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  y
) ,  0 ) )  =  ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  z ) ,  0 ) )  <-> 
y  =  z ) ) )
16878, 167syl5bi 217 . . . . 5  |-  ( ph  ->  ( ( y  e. 
{ x  e.  M  |  ( Q `  x )  =  1 }  /\  z  e. 
{ x  e.  M  |  ( Q `  x )  =  1 } )  ->  (
( n  e.  ( 1 ... K ) 
|->  if ( n  e. 
Prime ,  ( n  pCnt  y ) ,  0 ) )  =  ( n  e.  ( 1 ... K )  |->  if ( n  e.  Prime ,  ( n  pCnt  z
) ,  0 ) )  <->  y  =  z ) ) )
16974, 168dom2d 7557 . . . 4  |-  ( ph  ->  ( ( { 0 ,  1 }  ^m  ( 1 ... K
) )  e.  _V  ->  { x  e.  M  |  ( Q `  x )  =  1 }  ~<_  ( { 0 ,  1 }  ^m  ( 1 ... K
) ) ) )
1701, 169mpi 17 . . 3  |-  ( ph  ->  { x  e.  M  |  ( Q `  x )  =  1 }  ~<_  ( { 0 ,  1 }  ^m  ( 1 ... K
) ) )
171 fzfi 12051 . . . . . . 7  |-  ( 1 ... N )  e. 
Fin
172 ssfi 7741 . . . . . . 7  |-  ( ( ( 1 ... N
)  e.  Fin  /\  { n  e.  ( 1 ... N )  | 
A. p  e.  ( Prime  \  ( 1 ... K ) )  -.  p  ||  n }  C_  ( 1 ... N ) )  ->  { n  e.  (
1 ... N )  | 
A. p  e.  ( Prime  \  ( 1 ... K ) )  -.  p  ||  n }  e.  Fin )
173171, 6, 172mp2an 672 . . . . . 6  |-  { n  e.  ( 1 ... N
)  |  A. p  e.  ( Prime  \  (
1 ... K ) )  -.  p  ||  n }  e.  Fin
1745, 173eqeltri 2551 . . . . 5  |-  M  e. 
Fin
175 ssrab2 3585 . . . . 5  |-  { x  e.  M  |  ( Q `  x )  =  1 }  C_  M
176 ssfi 7741 . . . . 5  |-  ( ( M  e.  Fin  /\  { x  e.  M  | 
( Q `  x
)  =  1 } 
C_  M )  ->  { x  e.  M  |  ( Q `  x )  =  1 }  e.  Fin )
177174, 175, 176mp2an 672 . . . 4  |-  { x  e.  M  |  ( Q `  x )  =  1 }  e.  Fin
178 prfi 7796 . . . . 5  |-  { 0 ,  1 }  e.  Fin
179 fzfid 12052 . . . . 5  |-  ( ph  ->  ( 1 ... K
)  e.  Fin )
180 mapfi 7817 . . . . 5  |-  ( ( { 0 ,  1 }  e.  Fin  /\  ( 1 ... K
)  e.  Fin )  ->  ( { 0 ,  1 }  ^m  (
1 ... K ) )  e.  Fin )
181178, 179, 180sylancr 663 . . . 4  |-  ( ph  ->  ( { 0 ,  1 }  ^m  (
1 ... K ) )  e.  Fin )
182 hashdom 12416 . . . 4  |-  ( ( { x  e.  M  |  ( Q `  x )  =  1 }  e.  Fin  /\  ( { 0 ,  1 }  ^m  ( 1 ... K ) )  e.  Fin )  -> 
( ( # `  {
x  e.  M  | 
( Q `  x
)  =  1 } )  <_  ( # `  ( { 0 ,  1 }  ^m  ( 1 ... K ) ) )  <->  { x  e.  M  |  ( Q `  x )  =  1 }  ~<_  ( { 0 ,  1 }  ^m  ( 1 ... K
) ) ) )
183177, 181, 182sylancr 663 . . 3  |-  ( ph  ->  ( ( # `  {
x  e.  M  | 
( Q `  x
)  =  1 } )  <_  ( # `  ( { 0 ,  1 }  ^m  ( 1 ... K ) ) )  <->  { x  e.  M  |  ( Q `  x )  =  1 }  ~<_  ( { 0 ,  1 }  ^m  ( 1 ... K
) ) ) )
184170, 183mpbird 232 . 2  |-  ( ph  ->  ( # `  {
x  e.  M  | 
( Q `  x
)  =  1 } )  <_  ( # `  ( { 0 ,  1 }  ^m  ( 1 ... K ) ) ) )
185 hashmap 12460 . . . 4  |-  ( ( { 0 ,  1 }  e.  Fin  /\  ( 1 ... K
)  e.  Fin )  ->  ( # `  ( { 0 ,  1 }  ^m  ( 1 ... K ) ) )  =  ( (
# `  { 0 ,  1 } ) ^ ( # `  (
1 ... K ) ) ) )
186178, 179, 185sylancr 663 . . 3  |-  ( ph  ->  ( # `  ( { 0 ,  1 }  ^m  ( 1 ... K ) ) )  =  ( (
# `  { 0 ,  1 } ) ^ ( # `  (
1 ... K ) ) ) )
187 0ne1 10604 . . . . . 6  |-  0  =/=  1
188 0cn 9589 . . . . . . 7  |-  0  e.  CC
189 ax-1cn 9551 . . . . . . 7  |-  1  e.  CC
190 hashprg 12429 . . . . . . 7  |-  ( ( 0  e.  CC  /\  1  e.  CC )  ->  ( 0  =/=  1  <->  (
# `  { 0 ,  1 } )  =  2 ) )
191188, 189, 190mp2an 672 . . . . . 6  |-  ( 0  =/=  1  <->  ( # `  {
0 ,  1 } )  =  2 )
192187, 191mpbi 208 . . . . 5  |-  ( # `  { 0 ,  1 } )  =  2
193192a1i 11 . . . 4  |-  ( ph  ->  ( # `  {
0 ,  1 } )  =  2 )
194 prmrec.2 . . . . . 6  |-  ( ph  ->  K  e.  NN )
195194nnnn0d 10853 . . . . 5  |-  ( ph  ->  K  e.  NN0 )
196 hashfz1 12388 . . . . 5  |-  ( K  e.  NN0  ->  ( # `  ( 1 ... K
) )  =  K )
197195, 196syl 16 . . . 4  |-  ( ph  ->  ( # `  (
1 ... K ) )  =  K )
198193, 197oveq12d 6303 . . 3  |-  ( ph  ->  ( ( # `  {
0 ,  1 } ) ^ ( # `  ( 1 ... K
) ) )  =  ( 2 ^ K
) )
199186, 198eqtrd 2508 . 2  |-  ( ph  ->  ( # `  ( { 0 ,  1 }  ^m  ( 1 ... K ) ) )  =  ( 2 ^ K ) )
200184, 199breqtrd 4471 1  |-  ( ph  ->  ( # `  {
x  e.  M  | 
( Q `  x
)  =  1 } )  <_  ( 2 ^ K ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767    =/= wne 2662   A.wral 2814   {crab 2818   _Vcvv 3113    \ cdif 3473    u. cun 3474    i^i cin 3475    C_ wss 3476   ifcif 3939   {cpr 4029   class class class wbr 4447    |-> cmpt 4505    Fn wfn 5583   -->wf 5584   ` cfv 5588  (class class class)co 6285    ^m cmap 7421    ~<_ cdom 7515   Fincfn 7517   supcsup 7901   CCcc 9491   RRcr 9492   0cc0 9493   1c1 9494    + caddc 9496    < clt 9629    <_ cle 9630    / cdiv 10207   NNcn 10537   2c2 10586   NN0cn0 10796   ZZcz 10865   ZZ>=cuz 11083   ...cfz 11673   ^cexp 12135   #chash 12374    || cdivides 13850   Primecprime 14079    pCnt cpc 14222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6577  ax-cnex 9549  ax-resscn 9550  ax-1cn 9551  ax-icn 9552  ax-addcl 9553  ax-addrcl 9554  ax-mulcl 9555  ax-mulrcl 9556  ax-mulcom 9557  ax-addass 9558  ax-mulass 9559  ax-distr 9560  ax-i2m1 9561  ax-1ne0 9562  ax-1rid 9563  ax-rnegex 9564  ax-rrecex 9565  ax-cnre 9566  ax-pre-lttri 9567  ax-pre-lttrn 9568  ax-pre-ltadd 9569  ax-pre-mulgt0 9570  ax-pre-sup 9571
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6246  df-ov 6288  df-oprab 6289  df-mpt2 6290  df-om 6686  df-1st 6785  df-2nd 6786  df-recs 7043  df-rdg 7077  df-1o 7131  df-2o 7132  df-oadd 7135  df-er 7312  df-map 7423  df-pm 7424  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-sup 7902  df-card 8321  df-cda 8549  df-pnf 9631  df-mnf 9632  df-xr 9633  df-ltxr 9634  df-le 9635  df-sub 9808  df-neg 9809  df-div 10208  df-nn 10538  df-2 10595  df-3 10596  df-n0 10797  df-z 10866  df-uz 11084  df-q 11184  df-rp 11222  df-fz 11674  df-fl 11898  df-mod 11966  df-seq 12077  df-exp 12136  df-hash 12375  df-cj 12898  df-re 12899  df-im 12900  df-sqrt 13034  df-abs 13035  df-dvds 13851  df-gcd 14007  df-prm 14080  df-pc 14223
This theorem is referenced by:  prmreclem3  14298
  Copyright terms: Public domain W3C validator