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) (Proof shortened by Timothy J. O'Malley, 9-Oct-2026)

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 sselid 
 |-  ( ( ( ( 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 fz01pr 
 |-  ( 0 ... 1 ) = { 0 , 1 }
57 55 56 eleqtrdi 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. { 0 , 1 } )
58 0elpr01 
 |-  0 e. { 0 , 1 }
59 58 a1i 
 |-  ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ -. n e. Prime ) -> 0 e. { 0 , 1 } )
60 57 59 ifclda 
 |-  ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) -> if ( n e. Prime , ( n pCnt y ) , 0 ) e. { 0 , 1 } )
61 60 fmpttd 
 |-  ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) -> ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt y ) , 0 ) ) : ( 1 ... K ) --> { 0 , 1 } )
62 prex 
 |-  { 0 , 1 } e. _V
63 ovex 
 |-  ( 1 ... K ) e. _V
64 62 63 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 } )
65 61 64 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 ) ) )
66 65 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 ) ) ) )
67 8 66 biimtrid 
 |-  ( 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 ) ) ) )
68 fveqeq2 
 |-  ( x = z -> ( ( Q ` x ) = 1 <-> ( Q ` z ) = 1 ) )
69 68 elrab 
 |-  ( z e. { x e. M | ( Q ` x ) = 1 } <-> ( z e. M /\ ( Q ` z ) = 1 ) )
70 8 69 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 ) ) )
71 ovex 
 |-  ( n pCnt y ) e. _V
72 c0ex 
 |-  0 e. _V
73 71 72 ifex 
 |-  if ( n e. Prime , ( n pCnt y ) , 0 ) e. _V
74 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 ) )
75 73 74 fnmpti 
 |-  ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt y ) , 0 ) ) Fn ( 1 ... K )
76 ovex 
 |-  ( n pCnt z ) e. _V
77 76 72 ifex 
 |-  if ( n e. Prime , ( n pCnt z ) , 0 ) e. _V
78 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 ) )
79 77 78 fnmpti 
 |-  ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt z ) , 0 ) ) Fn ( 1 ... K )
80 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 ) ) )
81 75 79 80 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 ) )
82 eleq1w 
 |-  ( n = p -> ( n e. Prime <-> p e. Prime ) )
83 oveq1 
 |-  ( n = p -> ( n pCnt y ) = ( p pCnt y ) )
84 82 83 ifbieq1d 
 |-  ( n = p -> if ( n e. Prime , ( n pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt y ) , 0 ) )
85 ovex 
 |-  ( p pCnt y ) e. _V
86 85 72 ifex 
 |-  if ( p e. Prime , ( p pCnt y ) , 0 ) e. _V
87 84 74 86 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 ) )
88 oveq1 
 |-  ( n = p -> ( n pCnt z ) = ( p pCnt z ) )
89 82 88 ifbieq1d 
 |-  ( n = p -> if ( n e. Prime , ( n pCnt z ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
90 ovex 
 |-  ( p pCnt z ) e. _V
91 90 72 ifex 
 |-  if ( p e. Prime , ( p pCnt z ) , 0 ) e. _V
92 89 78 91 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 ) )
93 87 92 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 ) ) )
94 93 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 ) )
95 81 94 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 ) )
96 simprll 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. M )
97 breq2 
 |-  ( n = y -> ( p || n <-> p || y ) )
98 97 notbid 
 |-  ( n = y -> ( -. p || n <-> -. p || y ) )
99 98 ralbidv 
 |-  ( n = y -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
100 99 4 elrab2 
 |-  ( y e. M <-> ( y e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
101 100 simprbi 
 |-  ( y e. M -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y )
102 96 101 syl 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y )
103 simprrl 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. M )
104 breq2 
 |-  ( n = z -> ( p || n <-> p || z ) )
105 104 notbid 
 |-  ( n = z -> ( -. p || n <-> -. p || z ) )
106 105 ralbidv 
 |-  ( n = z -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
107 106 4 elrab2 
 |-  ( z e. M <-> ( z e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
108 107 simprbi 
 |-  ( z e. M -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z )
109 103 108 syl 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z )
110 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 ) )
111 eldifi 
 |-  ( p e. ( Prime \ ( 1 ... K ) ) -> p e. Prime )
112 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
113 9 112 sstri 
 |-  M C_ NN
114 113 96 sselid 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN )
115 pceq0 
 |-  ( ( p e. Prime /\ y e. NN ) -> ( ( p pCnt y ) = 0 <-> -. p || y ) )
116 111 114 115 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 ) )
117 113 103 sselid 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN )
118 pceq0 
 |-  ( ( p e. Prime /\ z e. NN ) -> ( ( p pCnt z ) = 0 <-> -. p || z ) )
119 111 117 118 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 ) )
120 116 119 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 ) ) )
121 eqtr3 
 |-  ( ( ( p pCnt y ) = 0 /\ ( p pCnt z ) = 0 ) -> ( p pCnt y ) = ( p pCnt z ) )
122 120 121 biimtrrdi 
 |-  ( ( ( 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 ) ) )
123 122 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 ) ) )
124 110 123 biimtrrid 
 |-  ( ( 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 ) ) )
125 102 109 124 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 ) )
126 125 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 ) ) ) )
127 incom 
 |-  ( Prime i^i ( 1 ... K ) ) = ( ( 1 ... K ) i^i Prime )
128 127 uneq1i 
 |-  ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) )
129 inundif 
 |-  ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
130 128 129 eqtri 
 |-  ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
131 130 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 ) )
132 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 ) ) )
133 131 132 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 ) ) )
134 eldifn 
 |-  ( p e. ( ( 1 ... K ) \ Prime ) -> -. p e. Prime )
135 iffalse 
 |-  ( -. p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = 0 )
136 iffalse 
 |-  ( -. p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = 0 )
137 135 136 eqtr4d 
 |-  ( -. p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
138 134 137 syl 
 |-  ( p e. ( ( 1 ... K ) \ Prime ) -> if ( p e. Prime , ( p pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
139 138 rgen 
 |-  A. p e. ( ( 1 ... K ) \ Prime ) if ( p e. Prime , ( p pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 )
140 139 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 ) ) )
141 elinel1 
 |-  ( p e. ( Prime i^i ( 1 ... K ) ) -> p e. Prime )
142 iftrue 
 |-  ( p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = ( p pCnt y ) )
143 iftrue 
 |-  ( p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = ( p pCnt z ) )
144 142 143 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 ) ) )
145 141 144 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 ) ) )
146 145 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 ) )
147 140 146 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 ) )
148 133 147 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 ) )
149 inundif 
 |-  ( ( Prime i^i ( 1 ... K ) ) u. ( Prime \ ( 1 ... K ) ) ) = Prime
150 149 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 ) )
151 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 ) ) )
152 150 151 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 ) ) )
153 126 148 152 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 ) ) )
154 114 nnnn0d 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN0 )
155 117 nnnn0d 
 |-  ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN0 )
156 pc11 
 |-  ( ( y e. NN0 /\ z e. NN0 ) -> ( y = z <-> A. p e. Prime ( p pCnt y ) = ( p pCnt z ) ) )
157 154 155 156 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 ) ) )
158 153 157 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 ) )
159 95 158 bitrid 
 |-  ( ( 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 ) )
160 159 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 ) ) )
161 70 160 biimtrid 
 |-  ( 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 ) ) )
162 67 161 dom2d 
 |-  ( ph -> ( ( { 0 , 1 } ^m ( 1 ... K ) ) e. _V -> { x e. M | ( Q ` x ) = 1 } ~<_ ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
163 6 162 mpi 
 |-  ( ph -> { x e. M | ( Q ` x ) = 1 } ~<_ ( { 0 , 1 } ^m ( 1 ... K ) ) )
164 hashdomi 
 |-  ( { x e. M | ( Q ` x ) = 1 } ~<_ ( { 0 , 1 } ^m ( 1 ... K ) ) -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
165 163 164 syl 
 |-  ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
166 prfi 
 |-  { 0 , 1 } e. Fin
167 fzfid 
 |-  ( ph -> ( 1 ... K ) e. Fin )
168 hashmap 
 |-  ( ( { 0 , 1 } e. Fin /\ ( 1 ... K ) e. Fin ) -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
169 166 167 168 sylancr 
 |-  ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
170 prhash2ex 
 |-  ( # ` { 0 , 1 } ) = 2
171 170 a1i 
 |-  ( ph -> ( # ` { 0 , 1 } ) = 2 )
172 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
173 hashfz1 
 |-  ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
174 172 173 syl 
 |-  ( ph -> ( # ` ( 1 ... K ) ) = K )
175 171 174 oveq12d 
 |-  ( ph -> ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) = ( 2 ^ K ) )
176 169 175 eqtrd 
 |-  ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( 2 ^ K ) )
177 165 176 breqtrd 
 |-  ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( 2 ^ K ) )