Theorem prmreclem2 13961

Description: Lemma for prmrec 13966. 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 6105	. . . 4 |- ( { 0 , 1 } ^m ( 1 ... K ) ) e. _V
2		fveq2 5679	. . . . . . . 8 |- ( x = y -> ( Q ` x ) = ( Q ` y ) )
3	2	eqeq1d 2441	. . . . . . 7 |- ( x = y -> ( ( Q ` x ) = 1 <-> ( Q ` y ) = 1 ) )
4	3	elrab 3106	. . . . . 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 3425	. . . . . . . . . . . . . . . . . . . 20 |- { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n } C_ ( 1 ... N )
7	5, 6	eqsstri 3374	. . . . . . . . . . . . . . . . . . 19 |- M C_ ( 1 ... N )
8		simprl 748	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) -> y e. M )
9	8	ad2antrr 718	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. M )
10	7, 9	sseldi 3342	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ( 1 ... N ) )
11		elfznn 11465	. . . . . . . . . . . . . . . . . 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 458	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> n e. Prime )
14		prmuz2 13764	. . . . . . . . . . . . . . . . . 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 13960	. . . . . . . . . . . . . . . . . 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 995	. . . . . . . . . . . . . . . . 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 749	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) -> ( Q ` y ) = 1 )
21	20	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( Q ` y ) = 1 )
22	21	oveq1d 6095	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = ( 1 ^ 2 ) )
23		sq1 11944	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 ^ 2 ) = 1
24	22, 23	syl6eq 2481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = 1 )
25	24	oveq2d 6096	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = ( y / 1 ) )
26	12	nncnd 10326	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. CC )
27	26	div1d 10087	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / 1 ) = y )
28	25, 27	eqtrd 2465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = y )
29	28	breq2d 4292	. . . . . . . . . . . . . . . . 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 10734	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ZZ )
31		2nn0 10584	. . . . . . . . . . . . . . . . . . 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 13918	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. Prime /\ y e. ZZ /\ 2 e. NN0 ) -> ( 2 <_ ( n pCnt y ) <-> ( n ^ 2 ) || y ) )
34	13, 30, 32, 33	syl3anc 1211	. . . . . . . . . . . . . . . . 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 13900	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. NN0 )
38	37	nn0red 10625	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. RR )
39		2re 10379	. . . . . . . . . . . . . . . 16 |- 2 e. RR
40		ltnle 9442	. . . . . . . . . . . . . . . 16 |- ( ( ( n pCnt y ) e. RR /\ 2 e. RR ) -> ( ( n pCnt y ) < 2 <-> -. 2 <_ ( n pCnt y ) ) )
41	38, 39, 40	sylancl 655	. . . . . . . . . . . . . . 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 10368	. . . . . . . . . . . . . 14 |- 2 = ( 1 + 1 )
44	42, 43	syl6breq 4319	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) < ( 1 + 1 ) )
45	37	nn0zd 10733	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ZZ )
46		1z 10664	. . . . . . . . . . . . . 14 |- 1 e. ZZ
47		zleltp1 10683	. . . . . . . . . . . . . 14 |- ( ( ( n pCnt y ) e. ZZ /\ 1 e. ZZ ) -> ( ( n pCnt y ) <_ 1 <-> ( n pCnt y ) < ( 1 + 1 ) ) )
48	45, 46, 47	sylancl 655	. . . . . . . . . . . . 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 10883	. . . . . . . . . . . . . 14 |- NN0 = ( ZZ>= ` 0 )
51	37, 50	syl6eleq 2523	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ( ZZ>= ` 0 ) )
52		elfz5 11432	. . . . . . . . . . . . 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 655	. . . . . . . . . . . 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 10645	. . . . . . . . . . . . 13 |- 0 e. ZZ
56		fzpr 11496	. . . . . . . . . . . . 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 10771	. . . . . . . . . . . . 13 |- 1 = ( 0 + 1 )
59	58	oveq2i 6091	. . . . . . . . . . . 12 |- ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
60	58	preq2i 3946	. . . . . . . . . . . 12 |- { 0 , 1 } = { 0 , ( 0 + 1 ) }
61	57, 59, 60	3eqtr4i 2463	. . . . . . . . . . 11 |- ( 0 ... 1 ) = { 0 , 1 }
62	54, 61	syl6eleq 2523	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. { 0 , 1 } )
63		c0ex 9368	. . . . . . . . . . . 12 |- 0 e. _V
64	63	prid1 3971	. . . . . . . . . . 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 3809	. . . . . . . . 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 2433	. . . . . . . . 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 5855	. . . . . . . 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 4522	. . . . . . . . 9 |- { 0 , 1 } e. _V
70		ovex 6105	. . . . . . . . 9 |- ( 1 ... K ) e. _V
71	69, 70	elmap 7229	. . . . . . . 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 5679	. . . . . . . . 9 |- ( x = z -> ( Q ` x ) = ( Q ` z ) )
76	75	eqeq1d 2441	. . . . . . . 8 |- ( x = z -> ( ( Q ` x ) = 1 <-> ( Q ` z ) = 1 ) )
77	76	elrab 3106	. . . . . . 7 |- ( z e. { x e. M | ( Q ` x ) = 1 } <-> ( z e. M /\ ( Q ` z ) = 1 ) )
78	4, 77	anbi12i 690	. . . . . 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 6105	. . . . . . . . . . . 12 |- ( n pCnt y ) e. _V
80	79, 63	ifex 3846	. . . . . . . . . . 11 |- if ( n e. Prime , ( n pCnt y ) , 0 ) e. _V
81	80, 67	fnmpti 5527	. . . . . . . . . 10 |- ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt y ) , 0 ) ) Fn ( 1 ... K )
82		ovex 6105	. . . . . . . . . . . 12 |- ( n pCnt z ) e. _V
83	82, 63	ifex 3846	. . . . . . . . . . 11 |- if ( n e. Prime , ( n pCnt z ) , 0 ) e. _V
84		eqid 2433	. . . . . . . . . . 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 5527	. . . . . . . . . 10 |- ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt z ) , 0 ) ) Fn ( 1 ... K )
86		eqfnfv 5785	. . . . . . . . . 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 665	. . . . . . . . 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 2493	. . . . . . . . . . . . 13 |- ( n = p -> ( n e. Prime <-> p e. Prime ) )
89		oveq1 6087	. . . . . . . . . . . . 13 |- ( n = p -> ( n pCnt y ) = ( p pCnt y ) )
90	88, 89	ifbieq1d 3800	. . . . . . . . . . . 12 |- ( n = p -> if ( n e. Prime , ( n pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt y ) , 0 ) )
91		ovex 6105	. . . . . . . . . . . . 13 |- ( p pCnt y ) e. _V
92	91, 63	ifex 3846	. . . . . . . . . . . 12 |- if ( p e. Prime , ( p pCnt y ) , 0 ) e. _V
93	90, 67, 92	fvmpt 5762	. . . . . . . . . . 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 6087	. . . . . . . . . . . . 13 |- ( n = p -> ( n pCnt z ) = ( p pCnt z ) )
95	88, 94	ifbieq1d 3800	. . . . . . . . . . . 12 |- ( n = p -> if ( n e. Prime , ( n pCnt z ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
96		ovex 6105	. . . . . . . . . . . . 13 |- ( p pCnt z ) e. _V
97	96, 63	ifex 3846	. . . . . . . . . . . 12 |- if ( p e. Prime , ( p pCnt z ) , 0 ) e. _V
98	95, 84, 97	fvmpt 5762	. . . . . . . . . . 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 2447	. . . . . . . . . 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 2737	. . . . . . . . 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 754	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. M )
103		breq2 4284	. . . . . . . . . . . . . . . . 17 |- ( n = y -> ( p || n <-> p || y ) )
104	103	notbid 294	. . . . . . . . . . . . . . . 16 |- ( n = y -> ( -. p || n <-> -. p || y ) )
105	104	ralbidv 2725	. . . . . . . . . . . . . . 15 |- ( n = y -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
106	105, 5	elrab2 3108	. . . . . . . . . . . . . 14 |- ( y e. M <-> ( y e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
107	106	simprbi 461	. . . . . . . . . . . . 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 756	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. M )
110		breq2 4284	. . . . . . . . . . . . . . . . 17 |- ( n = z -> ( p || n <-> p || z ) )
111	110	notbid 294	. . . . . . . . . . . . . . . 16 |- ( n = z -> ( -. p || n <-> -. p || z ) )
112	111	ralbidv 2725	. . . . . . . . . . . . . . 15 |- ( n = z -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
113	112, 5	elrab2 3108	. . . . . . . . . . . . . 14 |- ( z e. M <-> ( z e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
114	113	simprbi 461	. . . . . . . . . . . . 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 2839	. . . . . . . . . . . . 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 3466	. . . . . . . . . . . . . . . . 17 |- ( p e. ( Prime \ ( 1 ... K ) ) -> p e. Prime )
118	11	ssriv 3348	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ... N ) C_ NN
119	7, 118	sstri 3353	. . . . . . . . . . . . . . . . . 18 |- M C_ NN
120	119, 102	sseldi 3342	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN )
121		pceq0 13920	. . . . . . . . . . . . . . . . 17 |- ( ( p e. Prime /\ y e. NN ) -> ( ( p pCnt y ) = 0 <-> -. p || y ) )
122	117, 120, 121	syl2anr 475	. . . . . . . . . . . . . . . 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 3342	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN )
124		pceq0 13920	. . . . . . . . . . . . . . . . 17 |- ( ( p e. Prime /\ z e. NN ) -> ( ( p pCnt z ) = 0 <-> -. p || z ) )
125	117, 123, 124	syl2anr 475	. . . . . . . . . . . . . . . 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 703	. . . . . . . . . . . . . . 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 2452	. . . . . . . . . . . . . . 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 2784	. . . . . . . . . . . . 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 672	. . . . . . . . . . 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 504	. . . . . . . . . 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 3531	. . . . . . . . . . . . . . 15 |- ( Prime i^i ( 1 ... K ) ) = ( ( 1 ... K ) i^i Prime )
134	133	uneq1i 3494	. . . . . . . . . . . . . 14 |- ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) )
135		inundif 3745	. . . . . . . . . . . . . 14 |- ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
136	134, 135	eqtri 2453	. . . . . . . . . . . . 13 |- ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
137	136	raleqi 2911	. . . . . . . . . . . 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 3525	. . . . . . . . . . . 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 3467	. . . . . . . . . . . . . . 15 |- ( p e. ( ( 1 ... K ) \ Prime ) -> -. p e. Prime )
141		iffalse 3787	. . . . . . . . . . . . . . . 16 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = 0 )
142		iffalse 3787	. . . . . . . . . . . . . . . 16 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = 0 )
143	141, 142	eqtr4d 2468	. . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . 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 502	. . . . . . . . . . . 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 3558	. . . . . . . . . . . . . . 15 |- ( Prime i^i ( 1 ... K ) ) C_ Prime
148	147	sseli 3340	. . . . . . . . . . . . . 14 |- ( p e. ( Prime i^i ( 1 ... K ) ) -> p e. Prime )
149		iftrue 3785	. . . . . . . . . . . . . . 15 |- ( p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = ( p pCnt y ) )
150		iftrue 3785	. . . . . . . . . . . . . . 15 |- ( p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = ( p pCnt z ) )
151	149, 150	eqeq12d 2447	. . . . . . . . . . . . . 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 2737	. . . . . . . . . . . 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 3745	. . . . . . . . . . . 12 |- ( ( Prime i^i ( 1 ... K ) ) u. ( Prime \ ( 1 ... K ) ) ) = Prime
157	156	raleqi 2911	. . . . . . . . . . 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 3525	. . . . . . . . . . 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 10624	. . . . . . . . . 10 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN0 )
162	123	nnnn0d 10624	. . . . . . . . . 10 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN0 )
163		pc11 13929	. . . . . . . . . 10 |- ( ( y e. NN0 /\ z e. NN0 ) -> ( y = z <-> A. p e. Prime ( p pCnt y ) = ( p pCnt z ) ) )
164	161, 162, 163	syl2anc 654	. . . . . . . . 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 7338	. . . 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 11778	. . . . . . 7 |- ( 1 ... N ) e. Fin
172		ssfi 7521	. . . . . . 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 665	. . . . . 6 |- { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n } e. Fin
174	5, 173	eqeltri 2503	. . . . 5 |- M e. Fin
175		ssrab2 3425	. . . . 5 |- { x e. M | ( Q ` x ) = 1 } C_ M
176		ssfi 7521	. . . . 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 665	. . . 4 |- { x e. M | ( Q ` x ) = 1 } e. Fin
178		prfi 7574	. . . . 5 |- { 0 , 1 } e. Fin
179		fzfid 11779	. . . . 5 |- ( ph -> ( 1 ... K ) e. Fin )
180		mapfi 7595	. . . . 5 |- ( ( { 0 , 1 } e. Fin /\ ( 1 ... K ) e. Fin ) -> ( { 0 , 1 } ^m ( 1 ... K ) ) e. Fin )
181	178, 179, 180	sylancr 656	. . . 4 |- ( ph -> ( { 0 , 1 } ^m ( 1 ... K ) ) e. Fin )
182		hashdom 12126	. . . 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 656	. . 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 12181	. . . 4 |- ( ( { 0 , 1 } e. Fin /\ ( 1 ... K ) e. Fin ) -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
186	178, 179, 185	sylancr 656	. . 3 |- ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) )
187		0ne1 10377	. . . . . 6 |- 0 =/= 1
188		0cn 9366	. . . . . . 7 |- 0 e. CC
189		ax-1cn 9328	. . . . . . 7 |- 1 e. CC
190		hashprg 12139	. . . . . . 7 |- ( ( 0 e. CC /\ 1 e. CC ) -> ( 0 =/= 1 <-> ( # ` { 0 , 1 } ) = 2 ) )
191	188, 189, 190	mp2an 665	. . . . . 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 10624	. . . . 5 |- ( ph -> K e. NN0 )
196		hashfz1 12101	. . . . 5 |- ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
197	195, 196	syl 16	. . . 4 |- ( ph -> ( # ` ( 1 ... K ) ) = K )
198	193, 197	oveq12d 6098	. . 3 |- ( ph -> ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) = ( 2 ^ K ) )
199	186, 198	eqtrd 2465	. 2 |- ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( 2 ^ K ) )
200	184, 199	breqtrd 4304	1 |- ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( 2 ^ K ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1362   e. wcel 1755   =/= wne 2596   A.wral 2705   {crab 2709   _Vcvv 2962   \ cdif 3313   u. cun 3314   i^i cin 3315   C_ wss 3316   ifcif 3779   {cpr 3867   class class class wbr 4280   e. cmpt 4338   Fn wfn 5401   -->wf 5402   ` cfv 5406  (class class class)co 6080   ^m cmap 7202   ~<_ cdom 7296   Fincfn 7298   supcsup 7678   CCcc 9268   RRcr 9269   0cc0 9270   1c1 9271   + caddc 9273   < clt 9406   <_ cle 9407   / cdiv 9981   NNcn 10310   2c2 10359   NN0cn0 10567   ZZcz 10634   ZZ>=cuz 10849   ...cfz 11424   ^cexp 11849   #chash 12087   || cdivides 13518   Primecprime 13746   pCnt cpc 13886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347  ax-pre-sup 9348

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-1st 6566  df-2nd 6567  df-recs 6818  df-rdg 6852  df-1o 6908  df-2o 6909  df-oadd 6912  df-er 7089  df-map 7204  df-pm 7205  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-sup 7679  df-card 8097  df-cda 8325  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-div 9982  df-nn 10311  df-2 10368  df-3 10369  df-n0 10568  df-z 10635  df-uz 10850  df-q 10942  df-rp 10980  df-fz 11425  df-fl 11626  df-mod 11693  df-seq 11791  df-exp 11850  df-hash 12088  df-cj 12572  df-re 12573  df-im 12574  df-sqr 12708  df-abs 12709  df-dvds 13519  df-gcd 13674  df-prm 13747  df-pc 13887

This theorem is referenced by:  prmreclem3  13962