Theorem prmreclem2 14297

Description: Lemma for prmrec 14302. 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 6310	. . . 4 |- ( { 0 , 1 } ^m ( 1 ... K ) ) e. _V
2		fveq2 5866	. . . . . . . 8 |- ( x = y -> ( Q ` x ) = ( Q ` y ) )
3	2	eqeq1d 2469	. . . . . . 7 |- ( x = y -> ( ( Q ` x ) = 1 <-> ( Q ` y ) = 1 ) )
4	3	elrab 3261	. . . . . 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 3585	. . . . . . . . . . . . . . . . . . . 20 |- { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n } C_ ( 1 ... N )
7	5, 6	eqsstri 3534	. . . . . . . . . . . . . . . . . . 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 3502	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ( 1 ... N ) )
11		elfznn 11715	. . . . . . . . . . . . . . . . . 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 14097	. . . . . . . . . . . . . . . . . 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 14296	. . . . . . . . . . . . . . . . . 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 1010	. . . . . . . . . . . . . . . . 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 6300	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = ( 1 ^ 2 ) )
23		sq1 12231	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 ^ 2 ) = 1
24	22, 23	syl6eq 2524	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( ( Q ` y ) ^ 2 ) = 1 )
25	24	oveq2d 6301	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = ( y / 1 ) )
26	12	nncnd 10553	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. CC )
27	26	div1d 10313	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / 1 ) = y )
28	25, 27	eqtrd 2508	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( y / ( ( Q ` y ) ^ 2 ) ) = y )
29	28	breq2d 4459	. . . . . . . . . . . . . . . . 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 10966	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> y e. ZZ )
31		2nn0 10813	. . . . . . . . . . . . . . . . . . 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 14254	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. Prime /\ y e. ZZ /\ 2 e. NN0 ) -> ( 2 <_ ( n pCnt y ) <-> ( n ^ 2 ) || y ) )
34	13, 30, 32, 33	syl3anc 1228	. . . . . . . . . . . . . . . . 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 14236	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. NN0 )
38	37	nn0red 10854	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. RR )
39		2re 10606	. . . . . . . . . . . . . . . 16 |- 2 e. RR
40		ltnle 9665	. . . . . . . . . . . . . . . 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 10595	. . . . . . . . . . . . . 14 |- 2 = ( 1 + 1 )
44	42, 43	syl6breq 4486	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) < ( 1 + 1 ) )
45	37	nn0zd 10965	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ZZ )
46		1z 10895	. . . . . . . . . . . . . 14 |- 1 e. ZZ
47		zleltp1 10914	. . . . . . . . . . . . . 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 11117	. . . . . . . . . . . . . 14 |- NN0 = ( ZZ>= ` 0 )
51	37, 50	syl6eleq 2565	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. ( ZZ>= ` 0 ) )
52		elfz5 11681	. . . . . . . . . . . . 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 10876	. . . . . . . . . . . . 13 |- 0 e. ZZ
56		fzpr 11736	. . . . . . . . . . . . 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 11005	. . . . . . . . . . . . 13 |- 1 = ( 0 + 1 )
59	58	oveq2i 6296	. . . . . . . . . . . 12 |- ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
60	58	preq2i 4110	. . . . . . . . . . . 12 |- { 0 , 1 } = { 0 , ( 0 + 1 ) }
61	57, 59, 60	3eqtr4i 2506	. . . . . . . . . . 11 |- ( 0 ... 1 ) = { 0 , 1 }
62	54, 61	syl6eleq 2565	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( y e. M /\ ( Q ` y ) = 1 ) ) /\ n e. ( 1 ... K ) ) /\ n e. Prime ) -> ( n pCnt y ) e. { 0 , 1 } )
63		c0ex 9591	. . . . . . . . . . . 12 |- 0 e. _V
64	63	prid1 4135	. . . . . . . . . . 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 3971	. . . . . . . . 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 2467	. . . . . . . . 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 6046	. . . . . . . 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 4689	. . . . . . . . 9 |- { 0 , 1 } e. _V
70		ovex 6310	. . . . . . . . 9 |- ( 1 ... K ) e. _V
71	69, 70	elmap 7448	. . . . . . . 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 5866	. . . . . . . . 9 |- ( x = z -> ( Q ` x ) = ( Q ` z ) )
76	75	eqeq1d 2469	. . . . . . . 8 |- ( x = z -> ( ( Q ` x ) = 1 <-> ( Q ` z ) = 1 ) )
77	76	elrab 3261	. . . . . . 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 6310	. . . . . . . . . . . 12 |- ( n pCnt y ) e. _V
80	79, 63	ifex 4008	. . . . . . . . . . 11 |- if ( n e. Prime , ( n pCnt y ) , 0 ) e. _V
81	80, 67	fnmpti 5709	. . . . . . . . . 10 |- ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt y ) , 0 ) ) Fn ( 1 ... K )
82		ovex 6310	. . . . . . . . . . . 12 |- ( n pCnt z ) e. _V
83	82, 63	ifex 4008	. . . . . . . . . . 11 |- if ( n e. Prime , ( n pCnt z ) , 0 ) e. _V
84		eqid 2467	. . . . . . . . . . 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 5709	. . . . . . . . . 10 |- ( n e. ( 1 ... K ) |-> if ( n e. Prime , ( n pCnt z ) , 0 ) ) Fn ( 1 ... K )
86		eqfnfv 5976	. . . . . . . . . 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 2539	. . . . . . . . . . . . 13 |- ( n = p -> ( n e. Prime <-> p e. Prime ) )
89		oveq1 6292	. . . . . . . . . . . . 13 |- ( n = p -> ( n pCnt y ) = ( p pCnt y ) )
90	88, 89	ifbieq1d 3962	. . . . . . . . . . . 12 |- ( n = p -> if ( n e. Prime , ( n pCnt y ) , 0 ) = if ( p e. Prime , ( p pCnt y ) , 0 ) )
91		ovex 6310	. . . . . . . . . . . . 13 |- ( p pCnt y ) e. _V
92	91, 63	ifex 4008	. . . . . . . . . . . 12 |- if ( p e. Prime , ( p pCnt y ) , 0 ) e. _V
93	90, 67, 92	fvmpt 5951	. . . . . . . . . . 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 6292	. . . . . . . . . . . . 13 |- ( n = p -> ( n pCnt z ) = ( p pCnt z ) )
95	88, 94	ifbieq1d 3962	. . . . . . . . . . . 12 |- ( n = p -> if ( n e. Prime , ( n pCnt z ) , 0 ) = if ( p e. Prime , ( p pCnt z ) , 0 ) )
96		ovex 6310	. . . . . . . . . . . . 13 |- ( p pCnt z ) e. _V
97	96, 63	ifex 4008	. . . . . . . . . . . 12 |- if ( p e. Prime , ( p pCnt z ) , 0 ) e. _V
98	95, 84, 97	fvmpt 5951	. . . . . . . . . . 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 2489	. . . . . . . . . 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 2894	. . . . . . . . 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 4451	. . . . . . . . . . . . . . . . 17 |- ( n = y -> ( p || n <-> p || y ) )
104	103	notbid 294	. . . . . . . . . . . . . . . 16 |- ( n = y -> ( -. p || n <-> -. p || y ) )
105	104	ralbidv 2903	. . . . . . . . . . . . . . 15 |- ( n = y -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
106	105, 5	elrab2 3263	. . . . . . . . . . . . . 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 4451	. . . . . . . . . . . . . . . . 17 |- ( n = z -> ( p || n <-> p || z ) )
111	110	notbid 294	. . . . . . . . . . . . . . . 16 |- ( n = z -> ( -. p || n <-> -. p || z ) )
112	111	ralbidv 2903	. . . . . . . . . . . . . . 15 |- ( n = z -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || z ) )
113	112, 5	elrab2 3263	. . . . . . . . . . . . . 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 2989	. . . . . . . . . . . . 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 3626	. . . . . . . . . . . . . . . . 17 |- ( p e. ( Prime \ ( 1 ... K ) ) -> p e. Prime )
118	11	ssriv 3508	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ... N ) C_ NN
119	7, 118	sstri 3513	. . . . . . . . . . . . . . . . . 18 |- M C_ NN
120	119, 102	sseldi 3502	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN )
121		pceq0 14256	. . . . . . . . . . . . . . . . 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 3502	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN )
124		pceq0 14256	. . . . . . . . . . . . . . . . 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 2495	. . . . . . . . . . . . . . 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 2872	. . . . . . . . . . . . 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 3691	. . . . . . . . . . . . . . 15 |- ( Prime i^i ( 1 ... K ) ) = ( ( 1 ... K ) i^i Prime )
134	133	uneq1i 3654	. . . . . . . . . . . . . 14 |- ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) )
135		inundif 3905	. . . . . . . . . . . . . 14 |- ( ( ( 1 ... K ) i^i Prime ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
136	134, 135	eqtri 2496	. . . . . . . . . . . . 13 |- ( ( Prime i^i ( 1 ... K ) ) u. ( ( 1 ... K ) \ Prime ) ) = ( 1 ... K )
137	136	raleqi 3062	. . . . . . . . . . . 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 3685	. . . . . . . . . . . 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 3627	. . . . . . . . . . . . . . 15 |- ( p e. ( ( 1 ... K ) \ Prime ) -> -. p e. Prime )
141		iffalse 3948	. . . . . . . . . . . . . . . 16 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = 0 )
142		iffalse 3948	. . . . . . . . . . . . . . . 16 |- ( -. p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = 0 )
143	141, 142	eqtr4d 2511	. . . . . . . . . . . . . . 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 2824	. . . . . . . . . . . . 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 3718	. . . . . . . . . . . . . . 15 |- ( Prime i^i ( 1 ... K ) ) C_ Prime
148	147	sseli 3500	. . . . . . . . . . . . . 14 |- ( p e. ( Prime i^i ( 1 ... K ) ) -> p e. Prime )
149		iftrue 3945	. . . . . . . . . . . . . . 15 |- ( p e. Prime -> if ( p e. Prime , ( p pCnt y ) , 0 ) = ( p pCnt y ) )
150		iftrue 3945	. . . . . . . . . . . . . . 15 |- ( p e. Prime -> if ( p e. Prime , ( p pCnt z ) , 0 ) = ( p pCnt z ) )
151	149, 150	eqeq12d 2489	. . . . . . . . . . . . . 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 2894	. . . . . . . . . . . 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 3905	. . . . . . . . . . . 12 |- ( ( Prime i^i ( 1 ... K ) ) u. ( Prime \ ( 1 ... K ) ) ) = Prime
157	156	raleqi 3062	. . . . . . . . . . 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 3685	. . . . . . . . . . 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 10853	. . . . . . . . . 10 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> y e. NN0 )
162	123	nnnn0d 10853	. . . . . . . . . 10 |- ( ( ph /\ ( ( y e. M /\ ( Q ` y ) = 1 ) /\ ( z e. M /\ ( Q ` z ) = 1 ) ) ) -> z e. NN0 )
163		pc11 14265	. . . . . . . . . 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 7557	. . . 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 12051	. . . . . . 7 |- ( 1 ... N ) e. Fin
172		ssfi 7741	. . . . . . 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 2551	. . . . 5 |- M e. Fin
175		ssrab2 3585	. . . . 5 |- { x e. M | ( Q ` x ) = 1 } C_ M
176		ssfi 7741	. . . . 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 7796	. . . . 5 |- { 0 , 1 } e. Fin
179		fzfid 12052	. . . . 5 |- ( ph -> ( 1 ... K ) e. Fin )
180		mapfi 7817	. . . . 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 12416	. . . 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 12460	. . . 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 10604	. . . . . 6 |- 0 =/= 1
188		0cn 9589	. . . . . . 7 |- 0 e. CC
189		ax-1cn 9551	. . . . . . 7 |- 1 e. CC
190		hashprg 12429	. . . . . . 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 10853	. . . . 5 |- ( ph -> K e. NN0 )
196		hashfz1 12388	. . . . 5 |- ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
197	195, 196	syl 16	. . . 4 |- ( ph -> ( # ` ( 1 ... K ) ) = K )
198	193, 197	oveq12d 6303	. . 3 |- ( ph -> ( ( # ` { 0 , 1 } ) ^ ( # ` ( 1 ... K ) ) ) = ( 2 ^ K ) )
199	186, 198	eqtrd 2508	. 2 |- ( ph -> ( # ` ( { 0 , 1 } ^m ( 1 ... K ) ) ) = ( 2 ^ K ) )
200	184, 199	breqtrd 4471	1 |- ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( 2 ^ K ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2814   {crab 2818   _Vcvv 3113   \ cdif 3473   u. cun 3474   i^i cin 3475   C_ wss 3476   ifcif 3939   {cpr 4029   class class class wbr 4447   |-> cmpt 4505   Fn wfn 5583   -->wf 5584   ` cfv 5588  (class class class)co 6285   ^m cmap 7421   ~<_ cdom 7515   Fincfn 7517   supcsup 7901   CCcc 9491   RRcr 9492   0cc0 9493   1c1 9494   + caddc 9496   < clt 9629   <_ cle 9630   / cdiv 10207   NNcn 10537   2c2 10586   NN0cn0 10796   ZZcz 10865   ZZ>=cuz 11083   ...cfz 11673   ^cexp 12135   #chash 12374   || cdivides 13850   Primecprime 14079   pCnt cpc 14222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6577  ax-cnex 9549  ax-resscn 9550  ax-1cn 9551  ax-icn 9552  ax-addcl 9553  ax-addrcl 9554  ax-mulcl 9555  ax-mulrcl 9556  ax-mulcom 9557  ax-addass 9558  ax-mulass 9559  ax-distr 9560  ax-i2m1 9561  ax-1ne0 9562  ax-1rid 9563  ax-rnegex 9564  ax-rrecex 9565  ax-cnre 9566  ax-pre-lttri 9567  ax-pre-lttrn 9568  ax-pre-ltadd 9569  ax-pre-mulgt0 9570  ax-pre-sup 9571

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6246  df-ov 6288  df-oprab 6289  df-mpt2 6290  df-om 6686  df-1st 6785  df-2nd 6786  df-recs 7043  df-rdg 7077  df-1o 7131  df-2o 7132  df-oadd 7135  df-er 7312  df-map 7423  df-pm 7424  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-sup 7902  df-card 8321  df-cda 8549  df-pnf 9631  df-mnf 9632  df-xr 9633  df-ltxr 9634  df-le 9635  df-sub 9808  df-neg 9809  df-div 10208  df-nn 10538  df-2 10595  df-3 10596  df-n0 10797  df-z 10866  df-uz 11084  df-q 11184  df-rp 11222  df-fz 11674  df-fl 11898  df-mod 11966  df-seq 12077  df-exp 12136  df-hash 12375  df-cj 12898  df-re 12899  df-im 12900  df-sqrt 13034  df-abs 13035  df-dvds 13851  df-gcd 14007  df-prm 14080  df-pc 14223

This theorem is referenced by:  prmreclem3  14298