Theorem prmreclem2 14824

Description: Lemma for prmrec 14829. 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 6333	. . . 4 |- ( { 0 , 1 } ^m ( 1 ... K ) ) e. _V
2		fveq2 5881	. . . . . . . 8 |- ( x = y -> ( Q ` x ) = ( Q ` y ) )
3	2	eqeq1d 2431	. . . . . . 7 |- ( x = y -> ( ( Q ` x ) = 1 <-> ( Q ` y ) = 1 ) )
4	3	elrab 3235	. . . . . 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 3552	. . . . . . . . . . . . . . . . . . . 20 |- { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n } C_ ( 1 ... N )
7	5, 6	eqsstri 3500	. . . . . . . . . . . . . . . . . . 19 |- M C_ ( 1 ... N )
8		simprl 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) -> y e. M )
9	8	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. M )
10	7, 9	sseldi 3468	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ( 1 ... N ) )
11		elfznn 11826	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 1 ... N ) -> y e. NN )
12	10, 11	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. NN )
13		simpr 462	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> n e. Prime )
14		prmuz2 14613	. . . . . . . . . . . . . . . . . 18 |- ( n e. Prime -> n e. ( ZZ>= ` 2 ) )
15	13, 14	syl 17	. . . . . . . . . . . . . . . . 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 14823	. . . . . . . . . . . . . . . . . 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 1019	. . . . . . . . . . . . . . . . 17 |- ( y e. NN -> ( n e. ( ZZ>= ` 2 ) -> -. ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) ) )
19	12, 15, 18	sylc 62	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> -. ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) )
20		simprr 764	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) -> ( Q ` y ) = 1 )
21	20	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( Q ` y ) = 1 )
22	21	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = ( 1 ^ 2 ) )
23		sq1 12366	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 ^ 2 ) = 1
24	22, 23	syl6eq 2486	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = 1 )
25	24	oveq2d 6321	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = ( y / 1 ) )
26	12	nncnd 10625	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. CC )
27	26	div1d 10374	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / 1 ) = y )
28	25, 27	eqtrd 2470	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = y )
29	28	breq2d 4438	. . . . . . . . . . . . . . . . 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 11039	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ZZ )
31		2nn0 10886	. . . . . . . . . . . . . . . . . . 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 14781	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. Prime /\ y e. ZZ /\ 2 e. NN0 ) -> ( 2 <_ ( n pCnt y ) <-> ( n ^ 2 ) || y ) )
34	13, 30, 32, 33	syl3anc 1264	. . . . . . . . . . . . . . . . 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 259	. . . . . . . . . . . . . . . 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 301	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> -. 2 <_ ( n pCnt y ) )
37	13, 12	pccld 14763	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. NN0 )
38	37	nn0red 10926	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. RR )
39		2re 10679	. . . . . . . . . . . . . . . 16 |- 2 e. RR
40		ltnle 9712	. . . . . . . . . . . . . . . 16 |- ( ( ( n pCnt y ) e. RR /\ 2 e. RR ) -> ( ( n pCnt y ) < 2 <-> -. 2 <_ ( n pCnt y ) ) )
41	38, 39, 40	sylancl 666	. . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) < 2 )
43		df-2 10668	. . . . . . . . . . . . . 14 |- 2 = ( 1 + 1 )
44	42, 43	syl6breq 4465	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) < ( 1 + 1 ) )
45	37	nn0zd 11038	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ZZ )
46		1z 10967	. . . . . . . . . . . . . 14 |- 1 e. ZZ
47		zleltp1 10987	. . . . . . . . . . . . . 14 |- ( ( ( n pCnt y ) e. ZZ /\ 1 e. ZZ ) -> ( ( n pCnt y ) <_ 1 <-> ( n pCnt y ) < ( 1 + 1 ) ) )
48	45, 46, 47	sylancl 666	. . . . . . . . . . . . 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 235	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) <_ 1 )
50		nn0uz 11193	. . . . . . . . . . . . . 14 |- NN0 = ( ZZ>= ` 0 )
51	37, 50	syl6eleq 2527	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ( ZZ>= ` 0 ) )
52		elfz5 11790	. . . . . . . . . . . . 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 666	. . . . . . . . . . . 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 235	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ( 0 ... 1 ) )
55		0z 10948	. . . . . . . . . . . . 13 |- 0 e. ZZ
56		fzpr 11849	. . . . . . . . . . . . 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 11079	. . . . . . . . . . . . 13 |- 1 = ( 0 + 1 )
59	58	oveq2i 6316	. . . . . . . . . . . 12 |- ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
60	58	preq2i 4086	. . . . . . . . . . . 12 |- { 0 , 1 } = { 0 , ( 0 + 1 ) }
61	57, 59, 60	3eqtr4i 2468	. . . . . . . . . . 11 |- ( 0 ... 1 ) = { 0 , 1 }
62	54, 61	syl6eleq 2527	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. { 0 , 1 } )
63		c0ex 9636	. . . . . . . . . . . 12 |- 0 e. _V
64	63	prid1 4111	. . . . . . . . . . 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 3947	. . . . . . . . 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 2429	. . . . . . . . 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 6061	. . . . . . . 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 4664	. . . . . . . . 9 |- { 0 , 1 } e. _V
70		ovex 6333	. . . . . . . . 9 |- ( 1 ... K ) e. _V
71	69, 70	elmap 7508	. . . . . . . 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 215	. . . . . . 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 435	. . . . . 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 220	. . . . 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 5881	. . . . . . . . 9 |- ( x = z -> ( Q ` x ) = ( Q ` z ) )
76	75	eqeq1d 2431	. . . . . . . 8 |- ( x = z -> ( ( Q ` x ) = 1 <-> ( Q ` z ) = 1 ) )
77	76	elrab 3235	. . . . . . 7 |- ( z e. { x e. M | ( Q ` x ) = 1 } <-> ( z e. M /\ ( Q ` z ) = 1 ) )
78	4, 77	anbi12i 701	. . . . . 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 6333	. . . . . . . . . . . 12 |- ( n pCnt y ) e. _V
80	79, 63	ifex 3983	. . . . . . . . . . 11 |- if ( n e. Prime , ( n pCnt y ) , 0 ) e. _V
81	80, 67	fnmpti 5724	. . . . . . . . . 10 |- ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt y ) , 0 ) ) Fn ( 1 ... K )
82		ovex 6333	. . . . . . . . . . . 12 |- ( n pCnt z ) e. _V
83	82, 63	ifex 3983	. . . . . . . . . . 11 |- if ( n e. Prime , ( n pCnt z ) , 0 ) e. _V
84		eqid 2429	. . . . . . . . . . 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 5724	. . . . . . . . . 10 |- ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt z ) , 0 ) ) Fn ( 1 ... K )
86		eqfnfv 5991	. . . . . . . . . 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 676	. . . . . . . . 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 2501	. . . . . . . . . . . . 13 |- ( n = p -> ( n e. Prime <-> p e. Prime ) )
89		oveq1 6312	. . . . . . . . . . . . 13 |- ( n = p -> ( n pCnt y ) = ( p pCnt y ) )
90	88, 89	ifbieq1d 3938	. . . . . . . . . . . 12 |- ( n = p -> if ( n e. Prime , ( n pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt y ) , 0 ) )
91		ovex 6333	. . . . . . . . . . . . 13 |- ( p pCnt y ) e. _V
92	91, 63	ifex 3983	. . . . . . . . . . . 12 |- if ( p e. Prime , ( p pCnt y ) , 0 ) e. _V
93	90, 67, 92	fvmpt 5964	. . . . . . . . . . 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 6312	. . . . . . . . . . . . 13 |- ( n = p -> ( n pCnt z ) = ( p pCnt z ) )
95	88, 94	ifbieq1d 3938	. . . . . . . . . . . 12 |- ( n = p -> if ( n e. Prime , ( n pCnt z ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
96		ovex 6333	. . . . . . . . . . . . 13 |- ( p pCnt z ) e. _V
97	96, 63	ifex 3983	. . . . . . . . . . . 12 |- if ( p e. Prime , ( p pCnt z ) , 0 ) e. _V
98	95, 84, 97	fvmpt 5964	. . . . . . . . . . 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 2451	. . . . . . . . . 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 2862	. . . . . . . . 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 252	. . . . . . . 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 770	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. M )
103		breq2 4430	. . . . . . . . . . . . . . . . 17 |- ( n = y -> ( p || n <-> p || y ) )
104	103	notbid 295	. . . . . . . . . . . . . . . 16 |- ( n = y -> ( -. p || n <-> -. p || y ) )
105	104	ralbidv 2871	. . . . . . . . . . . . . . 15 |- ( n = y -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
106	105, 5	elrab2 3237	. . . . . . . . . . . . . 14 |- ( y e. M <-> ( y e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
107	106	simprbi 465	. . . . . . . . . . . . 13 |- ( y e. M -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y )
108	102, 107	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y )
109		simprrl 772	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. M )
110		breq2 4430	. . . . . . . . . . . . . . . . 17 |- ( n = z -> ( p || n <-> p || z ) )
111	110	notbid 295	. . . . . . . . . . . . . . . 16 |- ( n = z -> ( -. p || n <-> -. p || z ) )
112	111	ralbidv 2871	. . . . . . . . . . . . . . 15 |- ( n = z -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
113	112, 5	elrab2 3237	. . . . . . . . . . . . . 14 |- ( z e. M <-> ( z e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
114	113	simprbi 465	. . . . . . . . . . . . 13 |- ( z e. M -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z )
115	109, 114	syl 17	. . . . . . . . . . . 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 2962	. . . . . . . . . . . . 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 3593	. . . . . . . . . . . . . . . . 17 |- ( p e. ( Prime \ ( 1 ... K ) ) -> p e. Prime )
118	11	ssriv 3474	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ... N ) C_ NN
119	7, 118	sstri 3479	. . . . . . . . . . . . . . . . . 18 |- M C_ NN
120	119, 102	sseldi 3468	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN )
121		pceq0 14783	. . . . . . . . . . . . . . . . 17 |- ( ( p e. Prime /\ y e. NN ) -> ( ( p pCnt y ) = 0 <-> -. p || y ) )
122	117, 120, 121	syl2anr 480	. . . . . . . . . . . . . . . 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 3468	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN )
124		pceq0 14783	. . . . . . . . . . . . . . . . 17 |- ( ( p e. Prime /\ z e. NN ) -> ( ( p pCnt z ) = 0 <-> -. p || z ) )
125	117, 123, 124	syl2anr 480	. . . . . . . . . . . . . . . 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 715	. . . . . . . . . . . . . . 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 2457	. . . . . . . . . . . . . . 15 |- ( ( ( p pCnt y ) = 0 /\ ( p pCnt z ) = 0 ) -> ( p pCnt y ) = ( p pCnt z ) )
128	126, 127	syl6bir 232	. . . . . . . . . . . . . 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 2840	. . . . . . . . . . . . 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 221	. . . . . . . . . . . 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 683	. . . . . . . . . . 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 509	. . . . . . . . . 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 3661	. . . . . . . . . . . . . . 15 |- ( Prime i^i ( 1 ... K ) ) = ( ( 1 ... K ) i^i Prime )
134	133	uneq1i 3622	. . . . . . . . . . . . . 14 |- ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) )
135		inundif 3879	. . . . . . . . . . . . . 14 |- ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
136	134, 135	eqtri 2458	. . . . . . . . . . . . 13 |- ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
137	136	raleqi 3036	. . . . . . . . . . . 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 3653	. . . . . . . . . . . 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 254	. . . . . . . . . . 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 3594	. . . . . . . . . . . . . . 15 |- ( p e. ( ( 1 ... K ) \ Prime ) -> -. p e. Prime )
141		iffalse 3924	. . . . . . . . . . . . . . . 16 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = 0 )
142		iffalse 3924	. . . . . . . . . . . . . . . 16 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = 0 )
143	141, 142	eqtr4d 2473	. . . . . . . . . . . . . . 15 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
144	140, 143	syl 17	. . . . . . . . . . . . . 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 2792	. . . . . . . . . . . . 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 507	. . . . . . . . . . . 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 3688	. . . . . . . . . . . . . . 15 |- ( Prime i^i ( 1 ... K ) ) C_ Prime
148	147	sseli 3466	. . . . . . . . . . . . . 14 |- ( p e. ( Prime i^i ( 1 ... K ) ) -> p e. Prime )
149		iftrue 3921	. . . . . . . . . . . . . . 15 |- ( p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = ( p pCnt y ) )
150		iftrue 3921	. . . . . . . . . . . . . . 15 |- ( p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = ( p pCnt z ) )
151	149, 150	eqeq12d 2451	. . . . . . . . . . . . . 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 17	. . . . . . . . . . . . 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 2862	. . . . . . . . . . . 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 254	. . . . . . . . . . 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 252	. . . . . . . . . 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 3879	. . . . . . . . . . . 12 |- ( ( Prime i^i ( 1 ... K ) ) u. ( Prime \ ( 1 ... K ) ) ) = Prime
157	156	raleqi 3036	. . . . . . . . . . 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 3653	. . . . . . . . . . 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 254	. . . . . . . . . 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 291	. . . . . . . . 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 10925	. . . . . . . . . 10 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN0 )
162	123	nnnn0d 10925	. . . . . . . . . 10 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN0 )
163		pc11 14792	. . . . . . . . . 10 |- ( ( y e. NN0 /\ z e. NN0 ) -> ( y = z <-> A. p e. Prime ( p pCnt y ) = ( p pCnt z ) ) )
164	161, 162, 163	syl2anc 665	. . . . . . . . 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 259	. . . . . . . 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 260	. . . . . . 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 435	. . . . . 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 220	. . . . 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 7617	. . . 4 |- ( ph -> ( ( { 0 , 1 } ^m ( 1 ... K ) ) e. _V -> { x e. M | ( Q ` x ) = 1 } ~<_ ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
170	1, 169	mpi 21	. . 3 |- ( ph -> { x e. M | ( Q ` x ) = 1 } ~<_ ( { 0 , 1 } ^m ( 1 ... K ) ) )
171		fzfi 12182	. . . . . . 7 |- ( 1 ... N ) e. Fin
172		ssfi 7798	. . . . . . 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 676	. . . . . 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 3552	. . . . 5 |- { x e. M | ( Q ` x ) = 1 } C_ M
176		ssfi 7798	. . . . 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 676	. . . 4 |- { x e. M | ( Q ` x ) = 1 } e. Fin
178		prfi 7852	. . . . 5 |- { 0 , 1 } e. Fin
179		fzfid 12183	. . . . 5 |- ( ph -> ( 1 ... K ) e. Fin )
180		mapfi 7876	. . . . 5 |- ( ( { 0 , 1 } e. Fin /\ ( 1 ... K ) e. Fin ) -> ( { 0 , 1 } ^m ( 1 ... K ) ) e. Fin )
181	178, 179, 180	sylancr 667	. . . 4 |- ( ph -> ( { 0 , 1 } ^m ( 1 ... K ) ) e. Fin )
182		hashdom 12555	. . . 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 667	. . 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 235	. 2 |- ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) )
185		hashmap 12602	. . . 4 |- ( ( { 0 , 1 } e. Fin /\ ( 1 ... K ) e. Fin ) -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
186	178, 179, 185	sylancr 667	. . 3 |- ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
187		0ne1 10677	. . . . . 6 |- 0 =/= 1
188		0cn 9634	. . . . . . 7 |- 0 e. CC
189		ax-1cn 9596	. . . . . . 7 |- 1 e. CC
190		hashprg 12569	. . . . . . 7 |- ( ( 0 e. CC /\ 1 e. CC ) -> ( 0 =/= 1 <-> ( # ` { 0 , 1 } ) = 2 ) )
191	188, 189, 190	mp2an 676	. . . . . 6 |- ( 0 =/= 1 <-> ( # ` { 0 , 1 } ) = 2 )
192	187, 191	mpbi 211	. . . . 5 |- ( # ` { 0 , 1 } ) = 2
193	192	a1i 11	. . . 4 |- ( ph -> ( # ` { 0 , 1 } ) = 2 )
194		prmrec.2	. . . . . 6 |- ( ph -> K e. NN )
195	194	nnnn0d 10925	. . . . 5 |- ( ph -> K e. NN0 )
196		hashfz1 12526	. . . . 5 |- ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
197	195, 196	syl 17	. . . 4 |- ( ph -> ( # ` ( 1 ... K ) ) = K )
198	193, 197	oveq12d 6323	. . 3 |- ( ph -> ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) = ( 2 ^ K ) )
199	186, 198	eqtrd 2470	. 2 |- ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( 2 ^ K ) )
200	184, 199	breqtrd 4450	1 |- ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( 2 ^ K ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1870   =/= wne 2625   A.wral 2782   {crab 2786   _Vcvv 3087   \ cdif 3439   u. cun 3440   i^i cin 3441   C_ wss 3442   ifcif 3915   {cpr 4004   class class class wbr 4426   |-> cmpt 4484   Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6305   ^m cmap 7480   ~<_ cdom 7575   Fincfn 7577   supcsup 7960   CCcc 9536   RRcr 9537   0cc0 9538   1c1 9539   + caddc 9541   < clt 9674   <_ cle 9675   / cdiv 10268   NNcn 10609   2c2 10659   NN0cn0 10869   ZZcz 10937   ZZ>=cuz 11159   ...cfz 11782   ^cexp 12269   #chash 12512   || cdvds 14283   Primecprime 14593   pCnt cpc 14749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615  ax-pre-sup 9616

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-2o 7191  df-oadd 7194  df-er 7371  df-map 7482  df-pm 7483  df-en 7578  df-dom 7579  df-sdom 7580  df-fin 7581  df-sup 7962  df-inf 7963  df-card 8372  df-cda 8596  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-div 10269  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-q 11265  df-rp 11303  df-fz 11783  df-fl 12025  df-mod 12094  df-seq 12211  df-exp 12270  df-hash 12513  df-cj 13141  df-re 13142  df-im 13143  df-sqrt 13277  df-abs 13278  df-dvds 14284  df-gcd 14443  df-prm 14594  df-pc 14750

This theorem is referenced by:  prmreclem3  14825