Theorem prmreclem2 14522

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

Step	Hyp	Ref	Expression
1		ovex 6298	. . . 4 |- ( { 0 , 1 } ^m ( 1 ... K ) ) e. _V
2		fveq2 5848	. . . . . . . 8 |- ( x = y -> ( Q ` x ) = ( Q ` y ) )
3	2	eqeq1d 2456	. . . . . . 7 |- ( x = y -> ( ( Q ` x ) = 1 <-> ( Q ` y ) = 1 ) )
4	3	elrab 3254	. . . . . 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 3571	. . . . . . . . . . . . . . . . . . . 20 |- { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n } C_ ( 1 ... N )
7	5, 6	eqsstri 3519	. . . . . . . . . . . . . . . . . . 19 |- M C_ ( 1 ... N )
8		simprl 754	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) -> y e. M )
9	8	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. M )
10	7, 9	sseldi 3487	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ( 1 ... N ) )
11		elfznn 11717	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 1 ... N ) -> y e. NN )
12	10, 11	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. NN )
13		simpr 459	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> n e. Prime )
14		prmuz2 14322	. . . . . . . . . . . . . . . . . 18 |- ( n e. Prime -> n e. ( ZZ>= ` 2 ) )
15	13, 14	syl 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 , < ) )
17	16	prmreclem1 14521	. . . . . . . . . . . . . . . . . 18 |- ( y e. NN -> ( ( Q ` y ) e. NN /\ ( ( Q ` y ) ^ 2 ) || y /\ ( n e. ( ZZ>= ` 2 ) -> -. ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) ) ) )
18	17	simp3d 1008	. . . . . . . . . . . . . . . . 17 |- ( y e. NN -> ( n e. ( ZZ>= ` 2 ) -> -. ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) ) )
19	12, 15, 18	sylc 60	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> -. ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) )
20		simprr 755	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) -> ( Q ` y ) = 1 )
21	20	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( Q ` y ) = 1 )
22	21	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = ( 1 ^ 2 ) )
23		sq1 12247	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 ^ 2 ) = 1
24	22, 23	syl6eq 2511	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = 1 )
25	24	oveq2d 6286	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = ( y / 1 ) )
26	12	nncnd 10547	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. CC )
27	26	div1d 10308	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / 1 ) = y )
28	25, 27	eqtrd 2495	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = y )
29	28	breq2d 4451	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) <-> ( n ^ 2 ) || y ) )
30	12	nnzd 10964	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ZZ )
31		2nn0 10808	. . . . . . . . . . . . . . . . . . 19 |- 2 e. NN0
32	31	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> 2 e. NN0 )
33		pcdvdsb 14479	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. Prime /\ y e. ZZ /\ 2 e. NN0 ) -> ( 2 <_ ( n pCnt y ) <-> ( n ^ 2 ) || y ) )
34	13, 30, 32, 33	syl3anc 1226	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( 2 <_ ( n pCnt y ) <-> ( n ^ 2 ) || y ) )
35	29, 34	bitr4d 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 ) ) )
36	19, 35	mtbid 298	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> -. 2 <_ ( n pCnt y ) )
37	13, 12	pccld 14461	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. NN0 )
38	37	nn0red 10849	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. RR )
39		2re 10601	. . . . . . . . . . . . . . . 16 |- 2 e. RR
40		ltnle 9653	. . . . . . . . . . . . . . . 16 |- ( ( ( n pCnt y ) e. RR /\ 2 e. RR ) -> ( ( n pCnt y ) < 2 <-> -. 2 <_ ( n pCnt y ) ) )
41	38, 39, 40	sylancl 660	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( n pCnt y ) < 2 <-> -. 2 <_ ( n pCnt y ) ) )
42	36, 41	mpbird 232	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) < 2 )
43		df-2 10590	. . . . . . . . . . . . . 14 |- 2 = ( 1 + 1 )
44	42, 43	syl6breq 4478	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) < ( 1 + 1 ) )
45	37	nn0zd 10963	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ZZ )
46		1z 10890	. . . . . . . . . . . . . 14 |- 1 e. ZZ
47		zleltp1 10910	. . . . . . . . . . . . . 14 |- ( ( ( n pCnt y ) e. ZZ /\ 1 e. ZZ ) -> ( ( n pCnt y ) <_ 1 <-> ( n pCnt y ) < ( 1 + 1 ) ) )
48	45, 46, 47	sylancl 660	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( n pCnt y ) <_ 1 <-> ( n pCnt y ) < ( 1 + 1 ) ) )
49	44, 48	mpbird 232	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) <_ 1 )
50		nn0uz 11116	. . . . . . . . . . . . . 14 |- NN0 = ( ZZ>= ` 0 )
51	37, 50	syl6eleq 2552	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ( ZZ>= ` 0 ) )
52		elfz5 11683	. . . . . . . . . . . . 13 |- ( ( ( n pCnt y ) e. ( ZZ>= ` 0 ) /\ 1 e. ZZ ) -> ( ( n pCnt y ) e. ( 0 ... 1 ) <-> ( n pCnt y ) <_ 1 ) )
53	51, 46, 52	sylancl 660	. . . . . . . . . . . 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 ) )
54	49, 53	mpbird 232	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ( 0 ... 1 ) )
55		0z 10871	. . . . . . . . . . . . 13 |- 0 e. ZZ
56		fzpr 11739	. . . . . . . . . . . . 13 |- ( 0 e. ZZ -> ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
57	55, 56	ax-mp 5	. . . . . . . . . . . 12 |- ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
58		1e0p1 11004	. . . . . . . . . . . . 13 |- 1 = ( 0 + 1 )
59	58	oveq2i 6281	. . . . . . . . . . . 12 |- ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
60	58	preq2i 4099	. . . . . . . . . . . 12 |- { 0 , 1 } = { 0 , ( 0 + 1 ) }
61	57, 59, 60	3eqtr4i 2493	. . . . . . . . . . 11 |- ( 0 ... 1 ) = { 0 , 1 }
62	54, 61	syl6eleq 2552	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. { 0 , 1 } )
63		c0ex 9579	. . . . . . . . . . . 12 |- 0 e. _V
64	63	prid1 4124	. . . . . . . . . . 11 |- 0 e. { 0 , 1 }
65	64	a1i 11	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ -. n e. Prime ) -> 0 e. { 0 , 1 } )
66	62, 65	ifclda 3961	. . . . . . . . 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 2454	. . . . . . . . 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 ) )
68	66, 67	fmptd 6031	. . . . . . . 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 4679	. . . . . . . . 9 |- { 0 , 1 } e. _V
70		ovex 6298	. . . . . . . . 9 |- ( 1 ... K ) e. _V
71	69, 70	elmap 7440	. . . . . . . 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 } )
72	68, 71	sylibr 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 ) ) )
73	72	ex 432	. . . . . 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 ) ) ) )
74	4, 73	syl5bi 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 5848	. . . . . . . . 9 |- ( x = z -> ( Q ` x ) = ( Q ` z ) )
76	75	eqeq1d 2456	. . . . . . . 8 |- ( x = z -> ( ( Q ` x ) = 1 <-> ( Q ` z ) = 1 ) )
77	76	elrab 3254	. . . . . . 7 |- ( z e. { x e. M | ( Q ` x ) = 1 } <-> ( z e. M /\ ( Q ` z ) = 1 ) )
78	4, 77	anbi12i 695	. . . . . 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 6298	. . . . . . . . . . . 12 |- ( n pCnt y ) e. _V
80	79, 63	ifex 3997	. . . . . . . . . . 11 |- if ( n e. Prime , ( n pCnt y ) , 0 ) e. _V
81	80, 67	fnmpti 5691	. . . . . . . . . 10 |- ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt y ) , 0 ) ) Fn ( 1 ... K )
82		ovex 6298	. . . . . . . . . . . 12 |- ( n pCnt z ) e. _V
83	82, 63	ifex 3997	. . . . . . . . . . 11 |- if ( n e. Prime , ( n pCnt z ) , 0 ) e. _V
84		eqid 2454	. . . . . . . . . . 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 ) )
85	83, 84	fnmpti 5691	. . . . . . . . . 10 |- ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt z ) , 0 ) ) Fn ( 1 ... K )
86		eqfnfv 5957	. . . . . . . . . 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 ) ) )
87	81, 85, 86	mp2an 670	. . . . . . . . 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 2526	. . . . . . . . . . . . 13 |- ( n = p -> ( n e. Prime <-> p e. Prime ) )
89		oveq1 6277	. . . . . . . . . . . . 13 |- ( n = p -> ( n pCnt y ) = ( p pCnt y ) )
90	88, 89	ifbieq1d 3952	. . . . . . . . . . . 12 |- ( n = p -> if ( n e. Prime , ( n pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt y ) , 0 ) )
91		ovex 6298	. . . . . . . . . . . . 13 |- ( p pCnt y ) e. _V
92	91, 63	ifex 3997	. . . . . . . . . . . 12 |- if ( p e. Prime , ( p pCnt y ) , 0 ) e. _V
93	90, 67, 92	fvmpt 5931	. . . . . . . . . . 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 6277	. . . . . . . . . . . . 13 |- ( n = p -> ( n pCnt z ) = ( p pCnt z ) )
95	88, 94	ifbieq1d 3952	. . . . . . . . . . . 12 |- ( n = p -> if ( n e. Prime , ( n pCnt z ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
96		ovex 6298	. . . . . . . . . . . . 13 |- ( p pCnt z ) e. _V
97	96, 63	ifex 3997	. . . . . . . . . . . 12 |- if ( p e. Prime , ( p pCnt z ) , 0 ) e. _V
98	95, 84, 97	fvmpt 5931	. . . . . . . . . . 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 ) )
99	93, 98	eqeq12d 2476	. . . . . . . . . 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 ) ) )
100	99	ralbiia 2884	. . . . . . . . 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 ) )
101	87, 100	bitri 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 4443	. . . . . . . . . . . . . . . . 17 |- ( n = y -> ( p || n <-> p || y ) )
104	103	notbid 292	. . . . . . . . . . . . . . . 16 |- ( n = y -> ( -. p || n <-> -. p || y ) )
105	104	ralbidv 2893	. . . . . . . . . . . . . . 15 |- ( n = y -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
106	105, 5	elrab2 3256	. . . . . . . . . . . . . 14 |- ( y e. M <-> ( y e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
107	106	simprbi 462	. . . . . . . . . . . . 13 |- ( y e. M -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y )
108	102, 107	syl 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 4443	. . . . . . . . . . . . . . . . 17 |- ( n = z -> ( p || n <-> p || z ) )
111	110	notbid 292	. . . . . . . . . . . . . . . 16 |- ( n = z -> ( -. p || n <-> -. p || z ) )
112	111	ralbidv 2893	. . . . . . . . . . . . . . 15 |- ( n = z -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
113	112, 5	elrab2 3256	. . . . . . . . . . . . . 14 |- ( z e. M <-> ( z e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
114	113	simprbi 462	. . . . . . . . . . . . 13 |- ( z e. M -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z )
115	109, 114	syl 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 2981	. . . . . . . . . . . . 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 3612	. . . . . . . . . . . . . . . . 17 |- ( p e. ( Prime \ ( 1 ... K ) ) -> p e. Prime )
118	11	ssriv 3493	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ... N ) C_ NN
119	7, 118	sstri 3498	. . . . . . . . . . . . . . . . . 18 |- M C_ NN
120	119, 102	sseldi 3487	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN )
121		pceq0 14481	. . . . . . . . . . . . . . . . 17 |- ( ( p e. Prime /\ y e. NN ) -> ( ( p pCnt y ) = 0 <-> -. p || y ) )
122	117, 120, 121	syl2anr 476	. . . . . . . . . . . . . . . 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 ) )
123	119, 109	sseldi 3487	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN )
124		pceq0 14481	. . . . . . . . . . . . . . . . 17 |- ( ( p e. Prime /\ z e. NN ) -> ( ( p pCnt z ) = 0 <-> -. p || z ) )
125	117, 123, 124	syl2anr 476	. . . . . . . . . . . . . . . 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 ) )
126	122, 125	anbi12d 708	. . . . . . . . . . . . . . 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 2482	. . . . . . . . . . . . . . 15 |- ( ( ( p pCnt y ) = 0 /\ ( p pCnt z ) = 0 ) -> ( p pCnt y ) = ( p pCnt z ) )
128	126, 127	syl6bir 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 ) ) )
129	128	ralimdva 2862	. . . . . . . . . . . . 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 ) ) )
130	116, 129	syl5bir 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 ) ) )
131	108, 115, 130	mp2and 677	. . . . . . . . . . 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 ) )
132	131	biantrud 505	. . . . . . . . . 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 3677	. . . . . . . . . . . . . . 15 |- ( Prime i^i ( 1 ... K ) ) = ( ( 1 ... K ) i^i Prime )
134	133	uneq1i 3640	. . . . . . . . . . . . . 14 |- ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) )
135		inundif 3894	. . . . . . . . . . . . . 14 |- ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
136	134, 135	eqtri 2483	. . . . . . . . . . . . 13 |- ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
137	136	raleqi 3055	. . . . . . . . . . . 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 3671	. . . . . . . . . . . 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 ) ) )
139	137, 138	bitr3i 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 3613	. . . . . . . . . . . . . . 15 |- ( p e. ( ( 1 ... K ) \ Prime ) -> -. p e. Prime )
141		iffalse 3938	. . . . . . . . . . . . . . . 16 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = 0 )
142		iffalse 3938	. . . . . . . . . . . . . . . 16 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = 0 )
143	141, 142	eqtr4d 2498	. . . . . . . . . . . . . . 15 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
144	140, 143	syl 16	. . . . . . . . . . . . . 14 |- ( p e. ( ( 1 ... K ) \ Prime ) -> if ( p e. Prime , ( p pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
145	144	rgen 2814	. . . . . . . . . . . . 13 |- 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 503	. . . . . . . . . . . 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 3704	. . . . . . . . . . . . . . 15 |- ( Prime i^i ( 1 ... K ) ) C_ Prime
148	147	sseli 3485	. . . . . . . . . . . . . 14 |- ( p e. ( Prime i^i ( 1 ... K ) ) -> p e. Prime )
149		iftrue 3935	. . . . . . . . . . . . . . 15 |- ( p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = ( p pCnt y ) )
150		iftrue 3935	. . . . . . . . . . . . . . 15 |- ( p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = ( p pCnt z ) )
151	149, 150	eqeq12d 2476	. . . . . . . . . . . . . 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 ) ) )
152	148, 151	syl 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 ) ) )
153	152	ralbiia 2884	. . . . . . . . . . . 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 ) )
154	146, 153	bitr3i 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 ) )
155	139, 154	bitri 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 3894	. . . . . . . . . . . 12 |- ( ( Prime i^i ( 1 ... K ) ) u. ( Prime \ ( 1 ... K ) ) ) = Prime
157	156	raleqi 3055	. . . . . . . . . . 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 3671	. . . . . . . . . . 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 ) ) )
159	157, 158	bitr3i 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 ) ) )
160	132, 155, 159	3bitr4g 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 ) ) )
161	120	nnnn0d 10848	. . . . . . . . . 10 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN0 )
162	123	nnnn0d 10848	. . . . . . . . . 10 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN0 )
163		pc11 14490	. . . . . . . . . 10 |- ( ( y e. NN0 /\ z e. NN0 ) -> ( y = z <-> A. p e. Prime ( p pCnt y ) = ( p pCnt z ) ) )
164	161, 162, 163	syl2anc 659	. . . . . . . . 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 ) ) )
165	160, 164	bitr4d 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 ) )
166	101, 165	syl5bb 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 ) )
167	166	ex 432	. . . . . 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 ) ) )
168	78, 167	syl5bi 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 ) ) )
169	74, 168	dom2d 7549	. . . 4 |- ( ph -> ( ( { 0 , 1 } ^m ( 1 ... K ) ) e. _V -> { x e. M | ( Q ` x ) = 1 } ~<_ ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
170	1, 169	mpi 17	. . 3 |- ( ph -> { x e. M | ( Q ` x ) = 1 } ~<_ ( { 0 , 1 } ^m ( 1 ... K ) ) )
171		fzfi 12067	. . . . . . 7 |- ( 1 ... N ) e. Fin
172		ssfi 7733	. . . . . . 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 )
173	171, 6, 172	mp2an 670	. . . . . 6 |- { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n } e. Fin
174	5, 173	eqeltri 2538	. . . . 5 |- M e. Fin
175		ssrab2 3571	. . . . 5 |- { x e. M | ( Q ` x ) = 1 } C_ M
176		ssfi 7733	. . . . 5 |- ( ( M e. Fin /\ { x e. M | ( Q ` x ) = 1 } C_ M ) -> { x e. M | ( Q ` x ) = 1 } e. Fin )
177	174, 175, 176	mp2an 670	. . . 4 |- { x e. M | ( Q ` x ) = 1 } e. Fin
178		prfi 7787	. . . . 5 |- { 0 , 1 } e. Fin
179		fzfid 12068	. . . . 5 |- ( ph -> ( 1 ... K ) e. Fin )
180		mapfi 7808	. . . . 5 |- ( ( { 0 , 1 } e. Fin /\ ( 1 ... K ) e. Fin ) -> ( { 0 , 1 } ^m ( 1 ... K ) ) e. Fin )
181	178, 179, 180	sylancr 661	. . . 4 |- ( ph -> ( { 0 , 1 } ^m ( 1 ... K ) ) e. Fin )
182		hashdom 12433	. . . 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 ) ) ) )
183	177, 181, 182	sylancr 661	. . 3 |- ( ph -> ( ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) <-> { x e. M | ( Q ` x ) = 1 } ~<_ ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
184	170, 183	mpbird 232	. 2 |- ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
185		hashmap 12480	. . . 4 |- ( ( { 0 , 1 } e. Fin /\ ( 1 ... K ) e. Fin ) -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
186	178, 179, 185	sylancr 661	. . 3 |- ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
187		0ne1 10599	. . . . . 6 |- 0 =/= 1
188		0cn 9577	. . . . . . 7 |- 0 e. CC
189		ax-1cn 9539	. . . . . . 7 |- 1 e. CC
190		hashprg 12447	. . . . . . 7 |- ( ( 0 e. CC /\ 1 e. CC ) -> ( 0 =/= 1 <-> ( # ` { 0 , 1 } ) = 2 ) )
191	188, 189, 190	mp2an 670	. . . . . 6 |- ( 0 =/= 1 <-> ( # ` { 0 , 1 } ) = 2 )
192	187, 191	mpbi 208	. . . . 5 |- ( # ` { 0 , 1 } ) = 2
193	192	a1i 11	. . . 4 |- ( ph -> ( # ` { 0 , 1 } ) = 2 )
194		prmrec.2	. . . . . 6 |- ( ph -> K e. NN )
195	194	nnnn0d 10848	. . . . 5 |- ( ph -> K e. NN0 )
196		hashfz1 12404	. . . . 5 |- ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
197	195, 196	syl 16	. . . 4 |- ( ph -> ( # ` ( 1 ... K ) ) = K )
198	193, 197	oveq12d 6288	. . 3 |- ( ph -> ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) = ( 2 ^ K ) )
199	186, 198	eqtrd 2495	. 2 |- ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( 2 ^ K ) )
200	184, 199	breqtrd 4463	1 |- ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( 2 ^ K ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1398   e. wcel 1823   =/= wne 2649   A.wral 2804   {crab 2808   _Vcvv 3106   \ cdif 3458   u. cun 3459   i^i cin 3460   C_ wss 3461   ifcif 3929   {cpr 4018   class class class wbr 4439   |-> cmpt 4497   Fn wfn 5565   -->wf 5566   ` cfv 5570  (class class class)co 6270   ^m cmap 7412   ~<_ cdom 7507   Fincfn 7509   supcsup 7892   CCcc 9479   RRcr 9480   0cc0 9481   1c1 9482   + caddc 9484   < clt 9617   <_ cle 9618   / cdiv 10202   NNcn 10531   2c2 10581   NN0cn0 10791   ZZcz 10860   ZZ>=cuz 11082   ...cfz 11675   ^cexp 12151   #chash 12390   || cdvds 14073   Primecprime 14304   pCnt cpc 14447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-1st 6773  df-2nd 6774  df-recs 7034  df-rdg 7068  df-1o 7122  df-2o 7123  df-oadd 7126  df-er 7303  df-map 7414  df-pm 7415  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-sup 7893  df-card 8311  df-cda 8539  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-div 10203  df-nn 10532  df-2 10590  df-3 10591  df-n0 10792  df-z 10861  df-uz 11083  df-q 11184  df-rp 11222  df-fz 11676  df-fl 11910  df-mod 11979  df-seq 12093  df-exp 12152  df-hash 12391  df-cj 13017  df-re 13018  df-im 13019  df-sqrt 13153  df-abs 13154  df-dvds 14074  df-gcd 14232  df-prm 14305  df-pc 14448

This theorem is referenced by:  prmreclem3  14523