Metamath Proof Explorer

Theorem prmreclem2

Description: Lemma for prmrec . 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)

Ref Expression
Hypotheses 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 prmreclem2 
|- ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( 2 ^ K ) )

Proof

Step Hyp Ref Expression
1 prmrec.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )
2 prmrec.2 
 |-  ( ph -> K e. NN )
3 prmrec.3 
 |-  ( ph -> N e. NN )
4 prmrec.4 
 |-  M = { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n }
5 prmreclem2.5 
 |-  Q = ( n e. NN |-> sup ( { r e. NN | ( r ^ 2 ) || n } , RR , < ) )
6 ovex 
 |-  ( { 0 , 1 } ^m ( 1 ... K ) ) e. _V
7 fveqeq2 
 |-  ( x = y -> ( ( Q ` x ) = 1 <-> ( Q ` y ) = 1 ) )
8 7 elrab 
 |-  ( y e. { x e. M | ( Q ` x ) = 1 } <-> ( y e. M /\ ( Q ` y ) = 1 ) )
9 4 ssrab3 
 |-  M C_ ( 1 ... N )
10 simprl 
 |-  ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) -> y e. M )
11 10 ad2antrr 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. M )
12 9 11 sseldi 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ( 1 ... N ) )
13 elfznn 
 |-  ( y e. ( 1 ... N ) -> y e. NN )
14 12 13 syl 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. NN )
15 simpr 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> n e. Prime )
16 prmuz2 
 |-  ( n e. Prime -> n e. ( ZZ>= ` 2 ) )
17 15 16 syl 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> n e. ( ZZ>= ` 2 ) )
18 5 prmreclem1 
 |-  ( y e. NN -> ( ( Q ` y ) e. NN /\ ( ( Q ` y ) ^ 2 ) || y /\ ( n e. ( ZZ>= ` 2 ) -> -. ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) ) ) )
19 18 simp3d 
 |-  ( y e. NN -> ( n e. ( ZZ>= ` 2 ) -> -. ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) ) )
20 14 17 19 sylc 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> -. ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) )
21 simprr 
 |-  ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) -> ( Q ` y ) = 1 )
22 21 ad2antrr 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( Q ` y ) = 1 )
23 22 oveq1d 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = ( 1 ^ 2 ) )
24 sq1 
 |-  ( 1 ^ 2 ) = 1
25 23 24 eqtrdi 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = 1 )
26 25 oveq2d 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = ( y / 1 ) )
27 14 nncnd 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. CC )
28 27 div1d 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / 1 ) = y )
29 26 28 eqtrd 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = y )
30 29 breq2d 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) <-> ( n ^ 2 ) || y ) )
31 14 nnzd 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ZZ )
32 2nn0 
 |-  2 e. NN0
33 32 a1i 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> 2 e. NN0 )
34 pcdvdsb 
 |-  ( ( n e. Prime /\ y e. ZZ /\ 2 e. NN0 ) -> ( 2 <_ ( n pCnt y ) <-> ( n ^ 2 ) || y ) )
35 15 31 33 34 syl3anc 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( 2 <_ ( n pCnt y ) <-> ( n ^ 2 ) || y ) )
36 30 35 bitr4d 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) <-> 2 <_ ( n pCnt y ) ) )
37 20 36 mtbid 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> -. 2 <_ ( n pCnt y ) )
38 15 14 pccld 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. NN0 )
39 38 nn0red 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. RR )
40 2re 
 |-  2 e. RR
41 ltnle 
 |-  ( ( ( n pCnt y ) e. RR /\ 2 e. RR ) -> ( ( n pCnt y ) < 2 <-> -. 2 <_ ( n pCnt y ) ) )
42 39 40 41 sylancl 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( n pCnt y ) < 2 <-> -. 2 <_ ( n pCnt y ) ) )
43 37 42 mpbird 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) < 2 )
44 df-2 
 |-  2 = ( 1 + 1 )
45 43 44 breqtrdi 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) < ( 1 + 1 ) )
46 38 nn0zd 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ZZ )
47 1z 
 |-  1 e. ZZ
48 zleltp1 
 |-  ( ( ( n pCnt y ) e. ZZ /\ 1 e. ZZ ) -> ( ( n pCnt y ) <_ 1 <-> ( n pCnt y ) < ( 1 + 1 ) ) )
49 46 47 48 sylancl 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( n pCnt y ) <_ 1 <-> ( n pCnt y ) < ( 1 + 1 ) ) )
50 45 49 mpbird 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) <_ 1 )
51 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
52 38 51 eleqtrdi 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ( ZZ>= ` 0 ) )
53 elfz5 
 |-  ( ( ( n pCnt y ) e. ( ZZ>= ` 0 ) /\ 1 e. ZZ ) -> ( ( n pCnt y ) e. ( 0 ... 1 ) <-> ( n pCnt y ) <_ 1 ) )
54 52 47 53 sylancl 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( n pCnt y ) e. ( 0 ... 1 ) <-> ( n pCnt y ) <_ 1 ) )
55 50 54 mpbird 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ( 0 ... 1 ) )
56 0z 
 |-  0 e. ZZ
57 fzpr 
 |-  ( 0 e. ZZ -> ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
58 56 57 ax-mp 
 |-  ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
59 1e0p1 
 |-  1 = ( 0 + 1 )
60 59 oveq2i 
 |-  ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
61 59 preq2i 
 |-  { 0 , 1 } = { 0 , ( 0 + 1 ) }
62 58 60 61 3eqtr4i 
 |-  ( 0 ... 1 ) = { 0 , 1 }
63 55 62 eleqtrdi 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. { 0 , 1 } )
64 c0ex 
 |-  0 e. _V
65 64 prid1 
 |-  0 e. { 0 , 1 }
66 65 a1i 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ -. n e. Prime ) -> 0 e. { 0 , 1 } )
67 63 66 ifclda 
 |-  ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) -> if ( n e. Prime , ( n pCnt y ) , 0 ) e. { 0 , 1 } )
68 67 fmpttd 
 |-  ( ( 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 
 |-  { 0 , 1 } e. _V
70 ovex 
 |-  ( 1 ... K ) e. _V
71 69 70 elmap 
 |-  ( ( 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 } )
72 68 71 sylibr 
 |-  ( ( 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 ) ) )
73 72 ex 
 |-  ( 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 ) ) ) )
74 8 73 syl5bi 
 |-  ( 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 fveqeq2 
 |-  ( x = z -> ( ( Q ` x ) = 1 <-> ( Q ` z ) = 1 ) )
76 75 elrab 
 |-  ( z e. { x e. M | ( Q ` x ) = 1 } <-> ( z e. M /\ ( Q ` z ) = 1 ) )
77 8 76 anbi12i 
 |-  ( ( 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 ) ) )
78 ovex 
 |-  ( n pCnt y ) e. _V
79 78 64 ifex 
 |-  if ( n e. Prime , ( n pCnt y ) , 0 ) e. _V
80 eqid 
 |-  ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt y ) , 0 ) ) = ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt y ) , 0 ) )
81 79 80 fnmpti 
 |-  ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt y ) , 0 ) ) Fn ( 1 ... K )
82 ovex 
 |-  ( n pCnt z ) e. _V
83 82 64 ifex 
 |-  if ( n e. Prime , ( n pCnt z ) , 0 ) e. _V
84 eqid 
 |-  ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt z ) , 0 ) ) = ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt z ) , 0 ) )
85 83 84 fnmpti 
 |-  ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt z ) , 0 ) ) Fn ( 1 ... K )
86 eqfnfv 
 |-  ( ( ( 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 ) ) )
87 81 85 86 mp2an 
 |-  ( ( 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 eleq1w 
 |-  ( n = p -> ( n e. Prime <-> p e. Prime ) )
89 oveq1 
 |-  ( n = p -> ( n pCnt y ) = ( p pCnt y ) )
90 88 89 ifbieq1d 
 |-  ( n = p -> if ( n e. Prime , ( n pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt y ) , 0 ) )
91 ovex 
 |-  ( p pCnt y ) e. _V
92 91 64 ifex 
 |-  if ( p e. Prime , ( p pCnt y ) , 0 ) e. _V
93 90 80 92 fvmpt 
 |-  ( 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 
 |-  ( n = p -> ( n pCnt z ) = ( p pCnt z ) )
95 88 94 ifbieq1d 
 |-  ( n = p -> if ( n e. Prime , ( n pCnt z ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
96 ovex 
 |-  ( p pCnt z ) e. _V
97 96 64 ifex 
 |-  if ( p e. Prime , ( p pCnt z ) , 0 ) e. _V
98 95 84 97 fvmpt 
 |-  ( 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 ) )
99 93 98 eqeq12d 
 |-  ( 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 ) ) )
100 99 ralbiia 
 |-  ( 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 ) )
101 87 100 bitri 
 |-  ( ( 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 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. M )
103 breq2 
 |-  ( n = y -> ( p || n <-> p || y ) )
104 103 notbid 
 |-  ( n = y -> ( -. p || n <-> -. p || y ) )
105 104 ralbidv 
 |-  ( n = y -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
106 105 4 elrab2 
 |-  ( y e. M <-> ( y e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
107 106 simprbi 
 |-  ( y e. M -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y )
108 102 107 syl 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y )
109 simprrl 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. M )
110 breq2 
 |-  ( n = z -> ( p || n <-> p || z ) )
111 110 notbid 
 |-  ( n = z -> ( -. p || n <-> -. p || z ) )
112 111 ralbidv 
 |-  ( n = z -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
113 112 4 elrab2 
 |-  ( z e. M <-> ( z e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
114 113 simprbi 
 |-  ( z e. M -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z )
115 109 114 syl 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z )
116 r19.26 
 |-  ( 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 
 |-  ( p e. ( Prime \ ( 1 ... K ) ) -> p e. Prime )
118 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
119 9 118 sstri 
 |-  M C_ NN
120 119 102 sseldi 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN )
121 pceq0 
 |-  ( ( p e. Prime /\ y e. NN ) -> ( ( p pCnt y ) = 0 <-> -. p || y ) )
122 117 120 121 syl2anr 
 |-  ( ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) /\ p e. ( Prime \ ( 1 ... K ) ) ) -> ( ( p pCnt y ) = 0 <-> -. p || y ) )
123 119 109 sseldi 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN )
124 pceq0 
 |-  ( ( p e. Prime /\ z e. NN ) -> ( ( p pCnt z ) = 0 <-> -. p || z ) )
125 117 123 124 syl2anr 
 |-  ( ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) /\ p e. ( Prime \ ( 1 ... K ) ) ) -> ( ( p pCnt z ) = 0 <-> -. p || z ) )
126 122 125 anbi12d 
 |-  ( ( ( 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 
 |-  ( ( ( p pCnt y ) = 0 /\ ( p pCnt z ) = 0 ) -> ( p pCnt y ) = ( p pCnt z ) )
128 126 127 syl6bir 
 |-  ( ( ( 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 ) ) )
129 128 ralimdva 
 |-  ( ( 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 ) ) )
130 116 129 syl5bir 
 |-  ( ( 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 ) ) )
131 108 115 130 mp2and 
 |-  ( ( 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 ) )
132 131 biantrud 
 |-  ( ( 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 
 |-  ( Prime i^i ( 1 ... K ) ) = ( ( 1 ... K ) i^i Prime )
134 133 uneq1i 
 |-  ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) )
135 inundif 
 |-  ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
136 134 135 eqtri 
 |-  ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
137 136 raleqi 
 |-  ( 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 
 |-  ( 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 ) ) )
139 137 138 bitr3i 
 |-  ( 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 
 |-  ( p e. ( ( 1 ... K ) \ Prime ) -> -. p e. Prime )
141 iffalse 
 |-  ( -. p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = 0 )
142 iffalse 
 |-  ( -. p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = 0 )
143 141 142 eqtr4d 
 |-  ( -. p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
144 140 143 syl 
 |-  ( p e. ( ( 1 ... K ) \ Prime ) -> if ( p e. Prime , ( p pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
145 144 rgen 
 |-  A. p e. ( ( 1 ... K ) \ Prime ) if ( p e. Prime , ( p pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 )
146 145 biantru 
 |-  ( 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 elinel1 
 |-  ( p e. ( Prime i^i ( 1 ... K ) ) -> p e. Prime )
148 iftrue 
 |-  ( p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = ( p pCnt y ) )
149 iftrue 
 |-  ( p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = ( p pCnt z ) )
150 148 149 eqeq12d 
 |-  ( 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 ) ) )
151 147 150 syl 
 |-  ( 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 ) ) )
152 151 ralbiia 
 |-  ( 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 ) )
153 146 152 bitr3i 
 |-  ( ( 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 ) )
154 139 153 bitri 
 |-  ( 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 ) )
155 inundif 
 |-  ( ( Prime i^i ( 1 ... K ) ) u. ( Prime \ ( 1 ... K ) ) ) = Prime
156 155 raleqi 
 |-  ( 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 ) )
157 ralunb 
 |-  ( 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 ) ) )
158 156 157 bitr3i 
 |-  ( 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 ) ) )
159 132 154 158 3bitr4g 
 |-  ( ( 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 ) ) )
160 120 nnnn0d 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN0 )
161 123 nnnn0d 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN0 )
162 pc11 
 |-  ( ( y e. NN0 /\ z e. NN0 ) -> ( y = z <-> A. p e. Prime ( p pCnt y ) = ( p pCnt z ) ) )
163 160 161 162 syl2anc 
 |-  ( ( 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 ) ) )
164 159 163 bitr4d 
 |-  ( ( 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 ) )
165 101 164 syl5bb 
 |-  ( ( 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 ) )
166 165 ex 
 |-  ( 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 ) ) )
167 77 166 syl5bi 
 |-  ( 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 ) ) )
168 74 167 dom2d 
 |-  ( ph -> ( ( { 0 , 1 } ^m ( 1 ... K ) ) e. _V -> { x e. M | ( Q ` x ) = 1 } ~<_ ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
169 6 168 mpi 
 |-  ( ph -> { x e. M | ( Q ` x ) = 1 } ~<_ ( { 0 , 1 } ^m ( 1 ... K ) ) )
170 fzfi 
 |-  ( 1 ... N ) e. Fin
171 ssrab2 
 |-  { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n } C_ ( 1 ... N )
172 ssfi 
 |-  ( ( ( 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 )
173 170 171 172 mp2an 
 |-  { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n } e. Fin
174 4 173 eqeltri 
 |-  M e. Fin
175 ssrab2 
 |-  { x e. M | ( Q ` x ) = 1 } C_ M
176 ssfi 
 |-  ( ( M e. Fin /\ { x e. M | ( Q ` x ) = 1 } C_ M ) -> { x e. M | ( Q ` x ) = 1 } e. Fin )
177 174 175 176 mp2an 
 |-  { x e. M | ( Q ` x ) = 1 } e. Fin
178 prfi 
 |-  { 0 , 1 } e. Fin
179 fzfid 
 |-  ( ph -> ( 1 ... K ) e. Fin )
180 mapfi 
 |-  ( ( { 0 , 1 } e. Fin /\ ( 1 ... K ) e. Fin ) -> ( { 0 , 1 } ^m ( 1 ... K ) ) e. Fin )
181 178 179 180 sylancr 
 |-  ( ph -> ( { 0 , 1 } ^m ( 1 ... K ) ) e. Fin )
182 hashdom 
 |-  ( ( { 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 ) ) ) )
183 177 181 182 sylancr 
 |-  ( ph -> ( ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) <-> { x e. M | ( Q ` x ) = 1 } ~<_ ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
184 169 183 mpbird 
 |-  ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
185 hashmap 
 |-  ( ( { 0 , 1 } e. Fin /\ ( 1 ... K ) e. Fin ) -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
186 178 179 185 sylancr 
 |-  ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
187 prhash2ex 
 |-  ( # ` { 0 , 1 } ) = 2
188 187 a1i 
 |-  ( ph -> ( # ` { 0 , 1 } ) = 2 )
189 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
190 hashfz1 
 |-  ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
191 189 190 syl 
 |-  ( ph -> ( # ` ( 1 ... K ) ) = K )
192 188 191 oveq12d 
 |-  ( ph -> ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) = ( 2 ^ K ) )
193 186 192 eqtrd 
 |-  ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( 2 ^ K ) )
194 184 193 breqtrd 
 |-  ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( 2 ^ K ) )