Theorem prmreclem2 13981

Description: Lemma for prmrec 13986. 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 6119	. . . 4 |- ( { 0 , 1 } ^m ( 1 ... K ) ) e. _V
2		fveq2 5694	. . . . . . . 8 |- ( x = y -> ( Q ` x ) = ( Q ` y ) )
3	2	eqeq1d 2451	. . . . . . 7 |- ( x = y -> ( ( Q ` x ) = 1 <-> ( Q ` y ) = 1 ) )
4	3	elrab 3120	. . . . . 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 3440	. . . . . . . . . . . . . . . . . . . 20 |- { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n } C_ ( 1 ... N )
7	5, 6	eqsstri 3389	. . . . . . . . . . . . . . . . . . 19 |- M C_ ( 1 ... N )
8		simprl 755	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) -> y e. M )
9	8	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. M )
10	7, 9	sseldi 3357	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ( 1 ... N ) )
11		elfznn 11481	. . . . . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> n e. Prime )
14		prmuz2 13784	. . . . . . . . . . . . . . . . . 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 13980	. . . . . . . . . . . . . . . . . 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 1002	. . . . . . . . . . . . . . . . 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 756	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) -> ( Q ` y ) = 1 )
21	20	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( Q ` y ) = 1 )
22	21	oveq1d 6109	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = ( 1 ^ 2 ) )
23		sq1 11963	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 ^ 2 ) = 1
24	22, 23	syl6eq 2491	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = 1 )
25	24	oveq2d 6110	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = ( y / 1 ) )
26	12	nncnd 10341	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. CC )
27	26	div1d 10102	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / 1 ) = y )
28	25, 27	eqtrd 2475	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = y )
29	28	breq2d 4307	. . . . . . . . . . . . . . . . 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 10749	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ZZ )
31		2nn0 10599	. . . . . . . . . . . . . . . . . . 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 13938	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. Prime /\ y e. ZZ /\ 2 e. NN0 ) -> ( 2 <_ ( n pCnt y ) <-> ( n ^ 2 ) || y ) )
34	13, 30, 32, 33	syl3anc 1218	. . . . . . . . . . . . . . . . 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 300	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> -. 2 <_ ( n pCnt y ) )
37	13, 12	pccld 13920	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. NN0 )
38	37	nn0red 10640	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. RR )
39		2re 10394	. . . . . . . . . . . . . . . 16 |- 2 e. RR
40		ltnle 9457	. . . . . . . . . . . . . . . 16 |- ( ( ( n pCnt y ) e. RR /\ 2 e. RR ) -> ( ( n pCnt y ) < 2 <-> -. 2 <_ ( n pCnt y ) ) )
41	38, 39, 40	sylancl 662	. . . . . . . . . . . . . . 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 10383	. . . . . . . . . . . . . 14 |- 2 = ( 1 + 1 )
44	42, 43	syl6breq 4334	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) < ( 1 + 1 ) )
45	37	nn0zd 10748	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ZZ )
46		1z 10679	. . . . . . . . . . . . . 14 |- 1 e. ZZ
47		zleltp1 10698	. . . . . . . . . . . . . 14 |- ( ( ( n pCnt y ) e. ZZ /\ 1 e. ZZ ) -> ( ( n pCnt y ) <_ 1 <-> ( n pCnt y ) < ( 1 + 1 ) ) )
48	45, 46, 47	sylancl 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 ) ) )
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 10898	. . . . . . . . . . . . . 14 |- NN0 = ( ZZ>= ` 0 )
51	37, 50	syl6eleq 2533	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ( ZZ>= ` 0 ) )
52		elfz5 11448	. . . . . . . . . . . . 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 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 ) )
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 10660	. . . . . . . . . . . . 13 |- 0 e. ZZ
56		fzpr 11514	. . . . . . . . . . . . 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 10786	. . . . . . . . . . . . 13 |- 1 = ( 0 + 1 )
59	58	oveq2i 6105	. . . . . . . . . . . 12 |- ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
60	58	preq2i 3961	. . . . . . . . . . . 12 |- { 0 , 1 } = { 0 , ( 0 + 1 ) }
61	57, 59, 60	3eqtr4i 2473	. . . . . . . . . . 11 |- ( 0 ... 1 ) = { 0 , 1 }
62	54, 61	syl6eleq 2533	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. { 0 , 1 } )
63		c0ex 9383	. . . . . . . . . . . 12 |- 0 e. _V
64	63	prid1 3986	. . . . . . . . . . 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 3824	. . . . . . . . 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 2443	. . . . . . . . 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 5870	. . . . . . . 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 4537	. . . . . . . . 9 |- { 0 , 1 } e. _V
70		ovex 6119	. . . . . . . . 9 |- ( 1 ... K ) e. _V
71	69, 70	elmap 7244	. . . . . . . 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 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 ) ) ) )
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 5694	. . . . . . . . 9 |- ( x = z -> ( Q ` x ) = ( Q ` z ) )
76	75	eqeq1d 2451	. . . . . . . 8 |- ( x = z -> ( ( Q ` x ) = 1 <-> ( Q ` z ) = 1 ) )
77	76	elrab 3120	. . . . . . 7 |- ( z e. { x e. M | ( Q ` x ) = 1 } <-> ( z e. M /\ ( Q ` z ) = 1 ) )
78	4, 77	anbi12i 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 6119	. . . . . . . . . . . 12 |- ( n pCnt y ) e. _V
80	79, 63	ifex 3861	. . . . . . . . . . 11 |- if ( n e. Prime , ( n pCnt y ) , 0 ) e. _V
81	80, 67	fnmpti 5542	. . . . . . . . . 10 |- ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt y ) , 0 ) ) Fn ( 1 ... K )
82		ovex 6119	. . . . . . . . . . . 12 |- ( n pCnt z ) e. _V
83	82, 63	ifex 3861	. . . . . . . . . . 11 |- if ( n e. Prime , ( n pCnt z ) , 0 ) e. _V
84		eqid 2443	. . . . . . . . . . 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 5542	. . . . . . . . . 10 |- ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt z ) , 0 ) ) Fn ( 1 ... K )
86		eqfnfv 5800	. . . . . . . . . 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 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 2503	. . . . . . . . . . . . 13 |- ( n = p -> ( n e. Prime <-> p e. Prime ) )
89		oveq1 6101	. . . . . . . . . . . . 13 |- ( n = p -> ( n pCnt y ) = ( p pCnt y ) )
90	88, 89	ifbieq1d 3815	. . . . . . . . . . . 12 |- ( n = p -> if ( n e. Prime , ( n pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt y ) , 0 ) )
91		ovex 6119	. . . . . . . . . . . . 13 |- ( p pCnt y ) e. _V
92	91, 63	ifex 3861	. . . . . . . . . . . 12 |- if ( p e. Prime , ( p pCnt y ) , 0 ) e. _V
93	90, 67, 92	fvmpt 5777	. . . . . . . . . . 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 6101	. . . . . . . . . . . . 13 |- ( n = p -> ( n pCnt z ) = ( p pCnt z ) )
95	88, 94	ifbieq1d 3815	. . . . . . . . . . . 12 |- ( n = p -> if ( n e. Prime , ( n pCnt z ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
96		ovex 6119	. . . . . . . . . . . . 13 |- ( p pCnt z ) e. _V
97	96, 63	ifex 3861	. . . . . . . . . . . 12 |- if ( p e. Prime , ( p pCnt z ) , 0 ) e. _V
98	95, 84, 97	fvmpt 5777	. . . . . . . . . . 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 2457	. . . . . . . . . 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 2750	. . . . . . . . 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 4299	. . . . . . . . . . . . . . . . 17 |- ( n = y -> ( p || n <-> p || y ) )
104	103	notbid 294	. . . . . . . . . . . . . . . 16 |- ( n = y -> ( -. p || n <-> -. p || y ) )
105	104	ralbidv 2738	. . . . . . . . . . . . . . 15 |- ( n = y -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
106	105, 5	elrab2 3122	. . . . . . . . . . . . . 14 |- ( y e. M <-> ( y e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
107	106	simprbi 464	. . . . . . . . . . . . 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 4299	. . . . . . . . . . . . . . . . 17 |- ( n = z -> ( p || n <-> p || z ) )
111	110	notbid 294	. . . . . . . . . . . . . . . 16 |- ( n = z -> ( -. p || n <-> -. p || z ) )
112	111	ralbidv 2738	. . . . . . . . . . . . . . 15 |- ( n = z -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
113	112, 5	elrab2 3122	. . . . . . . . . . . . . 14 |- ( z e. M <-> ( z e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
114	113	simprbi 464	. . . . . . . . . . . . 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 2852	. . . . . . . . . . . . 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 3481	. . . . . . . . . . . . . . . . 17 |- ( p e. ( Prime \ ( 1 ... K ) ) -> p e. Prime )
118	11	ssriv 3363	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ... N ) C_ NN
119	7, 118	sstri 3368	. . . . . . . . . . . . . . . . . 18 |- M C_ NN
120	119, 102	sseldi 3357	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN )
121		pceq0 13940	. . . . . . . . . . . . . . . . 17 |- ( ( p e. Prime /\ y e. NN ) -> ( ( p pCnt y ) = 0 <-> -. p || y ) )
122	117, 120, 121	syl2anr 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 ) )
123	119, 109	sseldi 3357	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN )
124		pceq0 13940	. . . . . . . . . . . . . . . . 17 |- ( ( p e. Prime /\ z e. NN ) -> ( ( p pCnt z ) = 0 <-> -. p || z ) )
125	117, 123, 124	syl2anr 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 ) )
126	122, 125	anbi12d 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 2462	. . . . . . . . . . . . . . 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 2797	. . . . . . . . . . . . 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 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 ) )
132	131	biantrud 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 3546	. . . . . . . . . . . . . . 15 |- ( Prime i^i ( 1 ... K ) ) = ( ( 1 ... K ) i^i Prime )
134	133	uneq1i 3509	. . . . . . . . . . . . . 14 |- ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) )
135		inundif 3760	. . . . . . . . . . . . . 14 |- ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
136	134, 135	eqtri 2463	. . . . . . . . . . . . 13 |- ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
137	136	raleqi 2924	. . . . . . . . . . . 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 3540	. . . . . . . . . . . 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 3482	. . . . . . . . . . . . . . 15 |- ( p e. ( ( 1 ... K ) \ Prime ) -> -. p e. Prime )
141		iffalse 3802	. . . . . . . . . . . . . . . 16 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = 0 )
142		iffalse 3802	. . . . . . . . . . . . . . . 16 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = 0 )
143	141, 142	eqtr4d 2478	. . . . . . . . . . . . . . 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 2784	. . . . . . . . . . . . 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 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 3573	. . . . . . . . . . . . . . 15 |- ( Prime i^i ( 1 ... K ) ) C_ Prime
148	147	sseli 3355	. . . . . . . . . . . . . 14 |- ( p e. ( Prime i^i ( 1 ... K ) ) -> p e. Prime )
149		iftrue 3800	. . . . . . . . . . . . . . 15 |- ( p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = ( p pCnt y ) )
150		iftrue 3800	. . . . . . . . . . . . . . 15 |- ( p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = ( p pCnt z ) )
151	149, 150	eqeq12d 2457	. . . . . . . . . . . . . 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 2750	. . . . . . . . . . . 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 3760	. . . . . . . . . . . 12 |- ( ( Prime i^i ( 1 ... K ) ) u. ( Prime \ ( 1 ... K ) ) ) = Prime
157	156	raleqi 2924	. . . . . . . . . . 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 3540	. . . . . . . . . . 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 10639	. . . . . . . . . 10 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN0 )
162	123	nnnn0d 10639	. . . . . . . . . 10 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN0 )
163		pc11 13949	. . . . . . . . . 10 |- ( ( y e. NN0 /\ z e. NN0 ) -> ( y = z <-> A. p e. Prime ( p pCnt y ) = ( p pCnt z ) ) )
164	161, 162, 163	syl2anc 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 ) ) )
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 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 ) ) )
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 7353	. . . 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 11797	. . . . . . 7 |- ( 1 ... N ) e. Fin
172		ssfi 7536	. . . . . . 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 672	. . . . . 6 |- { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n } e. Fin
174	5, 173	eqeltri 2513	. . . . 5 |- M e. Fin
175		ssrab2 3440	. . . . 5 |- { x e. M | ( Q ` x ) = 1 } C_ M
176		ssfi 7536	. . . . 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 672	. . . 4 |- { x e. M | ( Q ` x ) = 1 } e. Fin
178		prfi 7589	. . . . 5 |- { 0 , 1 } e. Fin
179		fzfid 11798	. . . . 5 |- ( ph -> ( 1 ... K ) e. Fin )
180		mapfi 7610	. . . . 5 |- ( ( { 0 , 1 } e. Fin /\ ( 1 ... K ) e. Fin ) -> ( { 0 , 1 } ^m ( 1 ... K ) ) e. Fin )
181	178, 179, 180	sylancr 663	. . . 4 |- ( ph -> ( { 0 , 1 } ^m ( 1 ... K ) ) e. Fin )
182		hashdom 12145	. . . 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 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 ) ) ) )
184	170, 183	mpbird 232	. 2 |- ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
185		hashmap 12200	. . . 4 |- ( ( { 0 , 1 } e. Fin /\ ( 1 ... K ) e. Fin ) -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
186	178, 179, 185	sylancr 663	. . 3 |- ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
187		0ne1 10392	. . . . . 6 |- 0 =/= 1
188		0cn 9381	. . . . . . 7 |- 0 e. CC
189		ax-1cn 9343	. . . . . . 7 |- 1 e. CC
190		hashprg 12158	. . . . . . 7 |- ( ( 0 e. CC /\ 1 e. CC ) -> ( 0 =/= 1 <-> ( # ` { 0 , 1 } ) = 2 ) )
191	188, 189, 190	mp2an 672	. . . . . 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 10639	. . . . 5 |- ( ph -> K e. NN0 )
196		hashfz1 12120	. . . . 5 |- ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
197	195, 196	syl 16	. . . 4 |- ( ph -> ( # ` ( 1 ... K ) ) = K )
198	193, 197	oveq12d 6112	. . 3 |- ( ph -> ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) = ( 2 ^ K ) )
199	186, 198	eqtrd 2475	. 2 |- ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( 2 ^ K ) )
200	184, 199	breqtrd 4319	1 |- ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( 2 ^ K ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   =/= wne 2609   A.wral 2718   {crab 2722   _Vcvv 2975   \ cdif 3328   u. cun 3329   i^i cin 3330   C_ wss 3331   ifcif 3794   {cpr 3882   class class class wbr 4295   e. cmpt 4353   Fn wfn 5416   -->wf 5417   ` cfv 5421  (class class class)co 6094   ^m cmap 7217   ~<_ cdom 7311   Fincfn 7313   supcsup 7693   CCcc 9283   RRcr 9284   0cc0 9285   1c1 9286   + caddc 9288   < clt 9421   <_ cle 9422   / cdiv 9996   NNcn 10325   2c2 10374   NN0cn0 10582   ZZcz 10649   ZZ>=cuz 10864   ...cfz 11440   ^cexp 11868   #chash 12106   || cdivides 13538   Primecprime 13766   pCnt cpc 13906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4406  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-cnex 9341  ax-resscn 9342  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-mulcom 9349  ax-addass 9350  ax-mulass 9351  ax-distr 9352  ax-i2m1 9353  ax-1ne0 9354  ax-1rid 9355  ax-rnegex 9356  ax-rrecex 9357  ax-cnre 9358  ax-pre-lttri 9359  ax-pre-lttrn 9360  ax-pre-ltadd 9361  ax-pre-mulgt0 9362  ax-pre-sup 9363

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-nel 2612  df-ral 2723  df-rex 2724  df-reu 2725  df-rmo 2726  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-pss 3347  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-tp 3885  df-op 3887  df-uni 4095  df-int 4132  df-iun 4176  df-br 4296  df-opab 4354  df-mpt 4355  df-tr 4389  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-riota 6055  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-om 6480  df-1st 6580  df-2nd 6581  df-recs 6835  df-rdg 6869  df-1o 6923  df-2o 6924  df-oadd 6927  df-er 7104  df-map 7219  df-pm 7220  df-en 7314  df-dom 7315  df-sdom 7316  df-fin 7317  df-sup 7694  df-card 8112  df-cda 8340  df-pnf 9423  df-mnf 9424  df-xr 9425  df-ltxr 9426  df-le 9427  df-sub 9600  df-neg 9601  df-div 9997  df-nn 10326  df-2 10383  df-3 10384  df-n0 10583  df-z 10650  df-uz 10865  df-q 10957  df-rp 10995  df-fz 11441  df-fl 11645  df-mod 11712  df-seq 11810  df-exp 11869  df-hash 12107  df-cj 12591  df-re 12592  df-im 12593  df-sqr 12727  df-abs 12728  df-dvds 13539  df-gcd 13694  df-prm 13767  df-pc 13907

This theorem is referenced by:  prmreclem3  13982