Theorem sqff1o 24908

Description: There is a bijection from the squarefree divisors of a number N to the powerset of the prime divisors of N. Among other things, this implies that a number has 2 ^ k squarefree divisors where k is the number of prime divisors, and a squarefree number has 2 ^ k divisors (because all divisors of a squarefree number are squarefree). The inverse function to F takes the product of all the primes in some subset of prime divisors of N. (Contributed by Mario Carneiro, 1-Jul-2015.)

Hypotheses

Ref	Expression
sqff1o.1	|- S = { x e. NN | ( ( mmu ` x ) =/= 0 /\ x || N ) }
sqff1o.2	|- F = ( n e. S |-> { p e. Prime | p || n } )
sqff1o.3	|- G = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )

Assertion

Ref	Expression
sqff1o	|- ( N e. NN -> F : S -1-1-onto-> ~P { p e. Prime | p || N } )

Distinct variable groups:   n, p, x, G   n, N, p, x   S, n, p

Allowed substitution hints:   S( x)   F( x, n, p)

Proof of Theorem sqff1o

Dummy variables k q y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sqff1o.2	. 2 |- F = ( n e. S |-> { p e. Prime | p || n } )
2		fveq2 6191	. . . . . . . . . . 11 |- ( x = n -> ( mmu ` x ) = ( mmu ` n ) )
3	2	neeq1d 2853	. . . . . . . . . 10 |- ( x = n -> ( ( mmu ` x ) =/= 0 <-> ( mmu ` n ) =/= 0 ) )
4		breq1 4656	. . . . . . . . . 10 |- ( x = n -> ( x || N <-> n || N ) )
5	3, 4	anbi12d 747	. . . . . . . . 9 |- ( x = n -> ( ( ( mmu ` x ) =/= 0 /\ x || N ) <-> ( ( mmu ` n ) =/= 0 /\ n || N ) ) )
6		sqff1o.1	. . . . . . . . 9 |- S = { x e. NN | ( ( mmu ` x ) =/= 0 /\ x || N ) }
7	5, 6	elrab2 3366	. . . . . . . 8 |- ( n e. S <-> ( n e. NN /\ ( ( mmu ` n ) =/= 0 /\ n || N ) ) )
8	7	simprbi 480	. . . . . . 7 |- ( n e. S -> ( ( mmu ` n ) =/= 0 /\ n || N ) )
9	8	simprd 479	. . . . . 6 |- ( n e. S -> n || N )
10	9	ad2antlr 763	. . . . 5 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> n || N )
11		prmz 15389	. . . . . . 7 |- ( p e. Prime -> p e. ZZ )
12	11	adantl 482	. . . . . 6 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> p e. ZZ )
13		simplr 792	. . . . . . . . 9 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> n e. S )
14	13, 7	sylib 208	. . . . . . . 8 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( n e. NN /\ ( ( mmu ` n ) =/= 0 /\ n || N ) ) )
15	14	simpld 475	. . . . . . 7 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> n e. NN )
16	15	nnzd 11481	. . . . . 6 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> n e. ZZ )
17		nnz 11399	. . . . . . 7 |- ( N e. NN -> N e. ZZ )
18	17	ad2antrr 762	. . . . . 6 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> N e. ZZ )
19		dvdstr 15018	. . . . . 6 |- ( ( p e. ZZ /\ n e. ZZ /\ N e. ZZ ) -> ( ( p || n /\ n || N ) -> p || N ) )
20	12, 16, 18, 19	syl3anc 1326	. . . . 5 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p || n /\ n || N ) -> p || N ) )
21	10, 20	mpan2d 710	. . . 4 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( p || n -> p || N ) )
22	21	ss2rabdv 3683	. . 3 |- ( ( N e. NN /\ n e. S ) -> { p e. Prime | p || n } C_ { p e. Prime | p || N } )
23		nnex 11026	. . . . . 6 |- NN e. _V
24		prmnn 15388	. . . . . . 7 |- ( p e. Prime -> p e. NN )
25	24	ssriv 3607	. . . . . 6 |- Prime C_ NN
26	23, 25	ssexi 4803	. . . . 5 |- Prime e. _V
27	26	rabex 4813	. . . 4 |- { p e. Prime | p || n } e. _V
28	27	elpw 4164	. . 3 |- ( { p e. Prime | p || n } e. ~P { p e. Prime | p || N } <-> { p e. Prime | p || n } C_ { p e. Prime | p || N } )
29	22, 28	sylibr 224	. 2 |- ( ( N e. NN /\ n e. S ) -> { p e. Prime | p || n } e. ~P { p e. Prime | p || N } )
30		1nn0 11308	. . . . . . . . . 10 |- 1 e. NN0
31		0nn0 11307	. . . . . . . . . 10 |- 0 e. NN0
32	30, 31	keepel 4155	. . . . . . . . 9 |- if ( k e. z , 1 , 0 ) e. NN0
33	32	rgenw 2924	. . . . . . . 8 |- A. k e. Prime if ( k e. z , 1 , 0 ) e. NN0
34		eqid 2622	. . . . . . . . 9 |- ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) )
35	34	fmpt 6381	. . . . . . . 8 |- ( A. k e. Prime if ( k e. z , 1 , 0 ) e. NN0 <-> ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) : Prime --> NN0 )
36	33, 35	mpbi 220	. . . . . . 7 |- ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) : Prime --> NN0
37	36	a1i 11	. . . . . 6 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) : Prime --> NN0 )
38		nn0ex 11298	. . . . . . 7 |- NN0 e. _V
39	38, 26	elmap 7886	. . . . . 6 |- ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) e. ( NN0 ^m Prime ) <-> ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) : Prime --> NN0 )
40	37, 39	sylibr 224	. . . . 5 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) e. ( NN0 ^m Prime ) )
41		fzfi 12771	. . . . . 6 |- ( 1 ... N ) e. Fin
42		ffn 6045	. . . . . . . . . . 11 |- ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) : Prime --> NN0 -> ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) Fn Prime )
43		elpreima 6337	. . . . . . . . . . 11 |- ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) Fn Prime -> ( x e. ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) <-> ( x e. Prime /\ ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ` x ) e. NN ) ) )
44	36, 42, 43	mp2b 10	. . . . . . . . . 10 |- ( x e. ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) <-> ( x e. Prime /\ ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ` x ) e. NN ) )
45		elequ1 1997	. . . . . . . . . . . . . 14 |- ( k = x -> ( k e. z <-> x e. z ) )
46	45	ifbid 4108	. . . . . . . . . . . . 13 |- ( k = x -> if ( k e. z , 1 , 0 ) = if ( x e. z , 1 , 0 ) )
47	30, 31	keepel 4155	. . . . . . . . . . . . . 14 |- if ( x e. z , 1 , 0 ) e. NN0
48	47	elexi 3213	. . . . . . . . . . . . 13 |- if ( x e. z , 1 , 0 ) e. _V
49	46, 34, 48	fvmpt 6282	. . . . . . . . . . . 12 |- ( x e. Prime -> ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ` x ) = if ( x e. z , 1 , 0 ) )
50	49	eleq1d 2686	. . . . . . . . . . 11 |- ( x e. Prime -> ( ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ` x ) e. NN <-> if ( x e. z , 1 , 0 ) e. NN ) )
51	50	biimpa 501	. . . . . . . . . 10 |- ( ( x e. Prime /\ ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ` x ) e. NN ) -> if ( x e. z , 1 , 0 ) e. NN )
52	44, 51	sylbi 207	. . . . . . . . 9 |- ( x e. ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) -> if ( x e. z , 1 , 0 ) e. NN )
53		0nnn 11052	. . . . . . . . . . 11 |- -. 0 e. NN
54		iffalse 4095	. . . . . . . . . . . 12 |- ( -. x e. z -> if ( x e. z , 1 , 0 ) = 0 )
55	54	eleq1d 2686	. . . . . . . . . . 11 |- ( -. x e. z -> ( if ( x e. z , 1 , 0 ) e. NN <-> 0 e. NN ) )
56	53, 55	mtbiri 317	. . . . . . . . . 10 |- ( -. x e. z -> -. if ( x e. z , 1 , 0 ) e. NN )
57	56	con4i 113	. . . . . . . . 9 |- ( if ( x e. z , 1 , 0 ) e. NN -> x e. z )
58	52, 57	syl 17	. . . . . . . 8 |- ( x e. ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) -> x e. z )
59	58	ssriv 3607	. . . . . . 7 |- ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) C_ z
60		elpwi 4168	. . . . . . . . 9 |- ( z e. ~P { p e. Prime | p || N } -> z C_ { p e. Prime | p || N } )
61	60	adantl 482	. . . . . . . 8 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> z C_ { p e. Prime | p || N } )
62		rabss2 3685	. . . . . . . . . 10 |- ( Prime C_ NN -> { p e. Prime | p || N } C_ { p e. NN | p || N } )
63	25, 62	ax-mp 5	. . . . . . . . 9 |- { p e. Prime | p || N } C_ { p e. NN | p || N }
64		dvdsssfz1 15040	. . . . . . . . . 10 |- ( N e. NN -> { p e. NN | p || N } C_ ( 1 ... N ) )
65	64	adantr 481	. . . . . . . . 9 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> { p e. NN | p || N } C_ ( 1 ... N ) )
66	63, 65	syl5ss 3614	. . . . . . . 8 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> { p e. Prime | p || N } C_ ( 1 ... N ) )
67	61, 66	sstrd 3613	. . . . . . 7 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> z C_ ( 1 ... N ) )
68	59, 67	syl5ss 3614	. . . . . 6 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) C_ ( 1 ... N ) )
69		ssfi 8180	. . . . . 6 |- ( ( ( 1 ... N ) e. Fin /\ ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) C_ ( 1 ... N ) ) -> ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) e. Fin )
70	41, 68, 69	sylancr 695	. . . . 5 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) e. Fin )
71		cnveq 5296	. . . . . . . 8 |- ( y = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) -> `' y = `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) )
72	71	imaeq1d 5465	. . . . . . 7 |- ( y = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) -> ( `' y " NN ) = ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) )
73	72	eleq1d 2686	. . . . . 6 |- ( y = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) -> ( ( `' y " NN ) e. Fin <-> ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) e. Fin ) )
74	73	elrab 3363	. . . . 5 |- ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) e. { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } <-> ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) e. ( NN0 ^m Prime ) /\ ( `' ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) " NN ) e. Fin ) )
75	40, 70, 74	sylanbrc 698	. . . 4 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) e. { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } )
76		sqff1o.3	. . . . . . 7 |- G = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )
77		eqid 2622	. . . . . . 7 |- { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } = { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin }
78	76, 77	1arith 15631	. . . . . 6 |- G : NN -1-1-onto-> { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin }
79		f1ocnv 6149	. . . . . 6 |- ( G : NN -1-1-onto-> { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } -> `' G : { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } -1-1-onto-> NN )
80		f1of 6137	. . . . . 6 |- ( `' G : { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } -1-1-onto-> NN -> `' G : { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } --> NN )
81	78, 79, 80	mp2b 10	. . . . 5 |- `' G : { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } --> NN
82	81	ffvelrni 6358	. . . 4 |- ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) e. { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } -> ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) e. NN )
83	75, 82	syl 17	. . 3 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) e. NN )
84		f1ocnvfv2 6533	. . . . . . . . . . . 12 |- ( ( G : NN -1-1-onto-> { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } /\ ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) e. { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } ) -> ( G ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) )
85	78, 75, 84	sylancr 695	. . . . . . . . . . 11 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( G ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) )
86	76	1arithlem1 15627	. . . . . . . . . . . 12 |- ( ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) e. NN -> ( G ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) = ( p e. Prime |-> ( p pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) ) )
87	83, 86	syl 17	. . . . . . . . . . 11 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( G ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) = ( p e. Prime |-> ( p pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) ) )
88	85, 87	eqtr3d 2658	. . . . . . . . . 10 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) = ( p e. Prime |-> ( p pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) ) )
89	88	fveq1d 6193	. . . . . . . . 9 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ` q ) = ( ( p e. Prime |-> ( p pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) ) ` q ) )
90		elequ1 1997	. . . . . . . . . . 11 |- ( k = q -> ( k e. z <-> q e. z ) )
91	90	ifbid 4108	. . . . . . . . . 10 |- ( k = q -> if ( k e. z , 1 , 0 ) = if ( q e. z , 1 , 0 ) )
92	30, 31	keepel 4155	. . . . . . . . . . 11 |- if ( q e. z , 1 , 0 ) e. NN0
93	92	elexi 3213	. . . . . . . . . 10 |- if ( q e. z , 1 , 0 ) e. _V
94	91, 34, 93	fvmpt 6282	. . . . . . . . 9 |- ( q e. Prime -> ( ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ` q ) = if ( q e. z , 1 , 0 ) )
95	89, 94	sylan9req 2677	. . . . . . . 8 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. Prime ) -> ( ( p e. Prime |-> ( p pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) ) ` q ) = if ( q e. z , 1 , 0 ) )
96		oveq1 6657	. . . . . . . . . 10 |- ( p = q -> ( p pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) = ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) )
97		eqid 2622	. . . . . . . . . 10 |- ( p e. Prime |-> ( p pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) ) = ( p e. Prime |-> ( p pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) )
98		ovex 6678	. . . . . . . . . 10 |- ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) e. _V
99	96, 97, 98	fvmpt 6282	. . . . . . . . 9 |- ( q e. Prime -> ( ( p e. Prime |-> ( p pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) ) ` q ) = ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) )
100	99	adantl 482	. . . . . . . 8 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. Prime ) -> ( ( p e. Prime |-> ( p pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) ) ` q ) = ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) )
101	95, 100	eqtr3d 2658	. . . . . . 7 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. Prime ) -> if ( q e. z , 1 , 0 ) = ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) )
102		breq1 4656	. . . . . . . 8 |- ( 1 = if ( q e. z , 1 , 0 ) -> ( 1 <_ 1 <-> if ( q e. z , 1 , 0 ) <_ 1 ) )
103		breq1 4656	. . . . . . . 8 |- ( 0 = if ( q e. z , 1 , 0 ) -> ( 0 <_ 1 <-> if ( q e. z , 1 , 0 ) <_ 1 ) )
104		1le1 10655	. . . . . . . 8 |- 1 <_ 1
105		0le1 10551	. . . . . . . 8 |- 0 <_ 1
106	102, 103, 104, 105	keephyp 4152	. . . . . . 7 |- if ( q e. z , 1 , 0 ) <_ 1
107	101, 106	syl6eqbrr 4693	. . . . . 6 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. Prime ) -> ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) <_ 1 )
108	107	ralrimiva 2966	. . . . 5 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> A. q e. Prime ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) <_ 1 )
109		issqf 24862	. . . . . 6 |- ( ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) e. NN -> ( ( mmu ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) =/= 0 <-> A. q e. Prime ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) <_ 1 ) )
110	83, 109	syl 17	. . . . 5 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( ( mmu ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) =/= 0 <-> A. q e. Prime ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) <_ 1 ) )
111	108, 110	mpbird 247	. . . 4 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( mmu ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) =/= 0 )
112		iftrue 4092	. . . . . . . . . . . 12 |- ( q e. z -> if ( q e. z , 1 , 0 ) = 1 )
113	112	adantl 482	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. z ) -> if ( q e. z , 1 , 0 ) = 1 )
114	61	sselda 3603	. . . . . . . . . . . . . . 15 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. z ) -> q e. { p e. Prime | p || N } )
115		breq1 4656	. . . . . . . . . . . . . . . 16 |- ( p = q -> ( p || N <-> q || N ) )
116	115	elrab 3363	. . . . . . . . . . . . . . 15 |- ( q e. { p e. Prime | p || N } <-> ( q e. Prime /\ q || N ) )
117	114, 116	sylib 208	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. z ) -> ( q e. Prime /\ q || N ) )
118	117	simprd 479	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. z ) -> q || N )
119	117	simpld 475	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. z ) -> q e. Prime )
120		simpll 790	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. z ) -> N e. NN )
121		pcelnn 15574	. . . . . . . . . . . . . 14 |- ( ( q e. Prime /\ N e. NN ) -> ( ( q pCnt N ) e. NN <-> q || N ) )
122	119, 120, 121	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. z ) -> ( ( q pCnt N ) e. NN <-> q || N ) )
123	118, 122	mpbird 247	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. z ) -> ( q pCnt N ) e. NN )
124	123	nnge1d 11063	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. z ) -> 1 <_ ( q pCnt N ) )
125	113, 124	eqbrtrd 4675	. . . . . . . . . 10 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. z ) -> if ( q e. z , 1 , 0 ) <_ ( q pCnt N ) )
126	125	ex 450	. . . . . . . . 9 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( q e. z -> if ( q e. z , 1 , 0 ) <_ ( q pCnt N ) ) )
127	126	adantr 481	. . . . . . . 8 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. Prime ) -> ( q e. z -> if ( q e. z , 1 , 0 ) <_ ( q pCnt N ) ) )
128		simpr 477	. . . . . . . . . 10 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. Prime ) -> q e. Prime )
129	17	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. Prime ) -> N e. ZZ )
130		pcge0 15566	. . . . . . . . . 10 |- ( ( q e. Prime /\ N e. ZZ ) -> 0 <_ ( q pCnt N ) )
131	128, 129, 130	syl2anc 693	. . . . . . . . 9 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. Prime ) -> 0 <_ ( q pCnt N ) )
132		iffalse 4095	. . . . . . . . . 10 |- ( -. q e. z -> if ( q e. z , 1 , 0 ) = 0 )
133	132	breq1d 4663	. . . . . . . . 9 |- ( -. q e. z -> ( if ( q e. z , 1 , 0 ) <_ ( q pCnt N ) <-> 0 <_ ( q pCnt N ) ) )
134	131, 133	syl5ibrcom 237	. . . . . . . 8 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. Prime ) -> ( -. q e. z -> if ( q e. z , 1 , 0 ) <_ ( q pCnt N ) ) )
135	127, 134	pm2.61d 170	. . . . . . 7 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. Prime ) -> if ( q e. z , 1 , 0 ) <_ ( q pCnt N ) )
136	101, 135	eqbrtrrd 4677	. . . . . 6 |- ( ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) /\ q e. Prime ) -> ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) <_ ( q pCnt N ) )
137	136	ralrimiva 2966	. . . . 5 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> A. q e. Prime ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) <_ ( q pCnt N ) )
138	83	nnzd 11481	. . . . . 6 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) e. ZZ )
139	17	adantr 481	. . . . . 6 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> N e. ZZ )
140		pc2dvds 15583	. . . . . 6 |- ( ( ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) e. ZZ /\ N e. ZZ ) -> ( ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) || N <-> A. q e. Prime ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) <_ ( q pCnt N ) ) )
141	138, 139, 140	syl2anc 693	. . . . 5 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) || N <-> A. q e. Prime ( q pCnt ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) <_ ( q pCnt N ) ) )
142	137, 141	mpbird 247	. . . 4 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) || N )
143	111, 142	jca 554	. . 3 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( ( mmu ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) =/= 0 /\ ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) || N ) )
144		fveq2 6191	. . . . . 6 |- ( x = ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) -> ( mmu ` x ) = ( mmu ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) )
145	144	neeq1d 2853	. . . . 5 |- ( x = ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) -> ( ( mmu ` x ) =/= 0 <-> ( mmu ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) =/= 0 ) )
146		breq1 4656	. . . . 5 |- ( x = ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) -> ( x || N <-> ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) || N ) )
147	145, 146	anbi12d 747	. . . 4 |- ( x = ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) -> ( ( ( mmu ` x ) =/= 0 /\ x || N ) <-> ( ( mmu ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) =/= 0 /\ ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) || N ) ) )
148	147, 6	elrab2 3366	. . 3 |- ( ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) e. S <-> ( ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) e. NN /\ ( ( mmu ` ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) =/= 0 /\ ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) || N ) ) )
149	83, 143, 148	sylanbrc 698	. 2 |- ( ( N e. NN /\ z e. ~P { p e. Prime | p || N } ) -> ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) e. S )
150		eqcom 2629	. . 3 |- ( n = ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) <-> ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) = n )
151	7	simplbi 476	. . . . . . 7 |- ( n e. S -> n e. NN )
152	151	ad2antrl 764	. . . . . 6 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> n e. NN )
153	26	mptex 6486	. . . . . 6 |- ( p e. Prime |-> ( p pCnt n ) ) e. _V
154	76	fvmpt2 6291	. . . . . 6 |- ( ( n e. NN /\ ( p e. Prime |-> ( p pCnt n ) ) e. _V ) -> ( G ` n ) = ( p e. Prime |-> ( p pCnt n ) ) )
155	152, 153, 154	sylancl 694	. . . . 5 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( G ` n ) = ( p e. Prime |-> ( p pCnt n ) ) )
156	155	eqeq1d 2624	. . . 4 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( ( G ` n ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) <-> ( p e. Prime |-> ( p pCnt n ) ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) )
157	78	a1i 11	. . . . 5 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> G : NN -1-1-onto-> { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } )
158	75	adantrl 752	. . . . 5 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) e. { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } )
159		f1ocnvfvb 6535	. . . . 5 |- ( ( G : NN -1-1-onto-> { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } /\ n e. NN /\ ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) e. { y e. ( NN0 ^m Prime ) | ( `' y " NN ) e. Fin } ) -> ( ( G ` n ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) <-> ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) = n ) )
160	157, 152, 158, 159	syl3anc 1326	. . . 4 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( ( G ` n ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) <-> ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) = n ) )
161	26	a1i 11	. . . . . . 7 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> Prime e. _V )
162		0cnd 10033	. . . . . . 7 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> 0 e. CC )
163		1cnd 10056	. . . . . . 7 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> 1 e. CC )
164		0ne1 11088	. . . . . . . 8 |- 0 =/= 1
165	164	a1i 11	. . . . . . 7 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> 0 =/= 1 )
166	161, 162, 163, 165	pw2f1olem 8064	. . . . . 6 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( ( z e. ~P Prime /\ ( p e. Prime |-> ( p pCnt n ) ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) <-> ( ( p e. Prime |-> ( p pCnt n ) ) e. ( { 0 , 1 } ^m Prime ) /\ z = ( `' ( p e. Prime |-> ( p pCnt n ) ) " { 1 } ) ) ) )
167		ssrab2 3687	. . . . . . . . 9 |- { p e. Prime | p || N } C_ Prime
168		sspwb 4917	. . . . . . . . 9 |- ( { p e. Prime | p || N } C_ Prime <-> ~P { p e. Prime | p || N } C_ ~P Prime )
169	167, 168	mpbi 220	. . . . . . . 8 |- ~P { p e. Prime | p || N } C_ ~P Prime
170		simprr 796	. . . . . . . 8 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> z e. ~P { p e. Prime | p || N } )
171	169, 170	sseldi 3601	. . . . . . 7 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> z e. ~P Prime )
172	171	biantrurd 529	. . . . . 6 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( ( p e. Prime |-> ( p pCnt n ) ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) <-> ( z e. ~P Prime /\ ( p e. Prime |-> ( p pCnt n ) ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) ) )
173		id 22	. . . . . . . . . . . . . . 15 |- ( p e. Prime -> p e. Prime )
174	151	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( N e. NN /\ n e. S ) -> n e. NN )
175		pccl 15554	. . . . . . . . . . . . . . 15 |- ( ( p e. Prime /\ n e. NN ) -> ( p pCnt n ) e. NN0 )
176	173, 174, 175	syl2anr 495	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( p pCnt n ) e. NN0 )
177		elnn0 11294	. . . . . . . . . . . . . 14 |- ( ( p pCnt n ) e. NN0 <-> ( ( p pCnt n ) e. NN \/ ( p pCnt n ) = 0 ) )
178	176, 177	sylib 208	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) e. NN \/ ( p pCnt n ) = 0 ) )
179	178	orcomd 403	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) = 0 \/ ( p pCnt n ) e. NN ) )
180	8	simpld 475	. . . . . . . . . . . . . . . . 17 |- ( n e. S -> ( mmu ` n ) =/= 0 )
181	180	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( N e. NN /\ n e. S ) -> ( mmu ` n ) =/= 0 )
182		issqf 24862	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> ( ( mmu ` n ) =/= 0 <-> A. p e. Prime ( p pCnt n ) <_ 1 ) )
183	174, 182	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( N e. NN /\ n e. S ) -> ( ( mmu ` n ) =/= 0 <-> A. p e. Prime ( p pCnt n ) <_ 1 ) )
184	181, 183	mpbid 222	. . . . . . . . . . . . . . 15 |- ( ( N e. NN /\ n e. S ) -> A. p e. Prime ( p pCnt n ) <_ 1 )
185	184	r19.21bi 2932	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( p pCnt n ) <_ 1 )
186		nnle1eq1 11048	. . . . . . . . . . . . . 14 |- ( ( p pCnt n ) e. NN -> ( ( p pCnt n ) <_ 1 <-> ( p pCnt n ) = 1 ) )
187	185, 186	syl5ibcom 235	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) e. NN -> ( p pCnt n ) = 1 ) )
188	187	orim2d 885	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( ( p pCnt n ) = 0 \/ ( p pCnt n ) e. NN ) -> ( ( p pCnt n ) = 0 \/ ( p pCnt n ) = 1 ) ) )
189	179, 188	mpd 15	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) = 0 \/ ( p pCnt n ) = 1 ) )
190		ovex 6678	. . . . . . . . . . . 12 |- ( p pCnt n ) e. _V
191	190	elpr 4198	. . . . . . . . . . 11 |- ( ( p pCnt n ) e. { 0 , 1 } <-> ( ( p pCnt n ) = 0 \/ ( p pCnt n ) = 1 ) )
192	189, 191	sylibr 224	. . . . . . . . . 10 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( p pCnt n ) e. { 0 , 1 } )
193		eqid 2622	. . . . . . . . . 10 |- ( p e. Prime |-> ( p pCnt n ) ) = ( p e. Prime |-> ( p pCnt n ) )
194	192, 193	fmptd 6385	. . . . . . . . 9 |- ( ( N e. NN /\ n e. S ) -> ( p e. Prime |-> ( p pCnt n ) ) : Prime --> { 0 , 1 } )
195	194	adantrr 753	. . . . . . . 8 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( p e. Prime |-> ( p pCnt n ) ) : Prime --> { 0 , 1 } )
196		prex 4909	. . . . . . . . 9 |- { 0 , 1 } e. _V
197	196, 26	elmap 7886	. . . . . . . 8 |- ( ( p e. Prime |-> ( p pCnt n ) ) e. ( { 0 , 1 } ^m Prime ) <-> ( p e. Prime |-> ( p pCnt n ) ) : Prime --> { 0 , 1 } )
198	195, 197	sylibr 224	. . . . . . 7 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( p e. Prime |-> ( p pCnt n ) ) e. ( { 0 , 1 } ^m Prime ) )
199	198	biantrurd 529	. . . . . 6 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( z = ( `' ( p e. Prime |-> ( p pCnt n ) ) " { 1 } ) <-> ( ( p e. Prime |-> ( p pCnt n ) ) e. ( { 0 , 1 } ^m Prime ) /\ z = ( `' ( p e. Prime |-> ( p pCnt n ) ) " { 1 } ) ) ) )
200	166, 172, 199	3bitr4d 300	. . . . 5 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( ( p e. Prime |-> ( p pCnt n ) ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) <-> z = ( `' ( p e. Prime |-> ( p pCnt n ) ) " { 1 } ) ) )
201	193	mptiniseg 5629	. . . . . . . 8 |- ( 1 e. NN0 -> ( `' ( p e. Prime |-> ( p pCnt n ) ) " { 1 } ) = { p e. Prime | ( p pCnt n ) = 1 } )
202	30, 201	ax-mp 5	. . . . . . 7 |- ( `' ( p e. Prime |-> ( p pCnt n ) ) " { 1 } ) = { p e. Prime | ( p pCnt n ) = 1 }
203		id 22	. . . . . . . . . . . 12 |- ( ( p pCnt n ) = 1 -> ( p pCnt n ) = 1 )
204		1nn 11031	. . . . . . . . . . . 12 |- 1 e. NN
205	203, 204	syl6eqel 2709	. . . . . . . . . . 11 |- ( ( p pCnt n ) = 1 -> ( p pCnt n ) e. NN )
206	205, 187	impbid2 216	. . . . . . . . . 10 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) = 1 <-> ( p pCnt n ) e. NN ) )
207		simpr 477	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> p e. Prime )
208		pcelnn 15574	. . . . . . . . . . 11 |- ( ( p e. Prime /\ n e. NN ) -> ( ( p pCnt n ) e. NN <-> p || n ) )
209	207, 15, 208	syl2anc 693	. . . . . . . . . 10 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) e. NN <-> p || n ) )
210	206, 209	bitrd 268	. . . . . . . . 9 |- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) = 1 <-> p || n ) )
211	210	rabbidva 3188	. . . . . . . 8 |- ( ( N e. NN /\ n e. S ) -> { p e. Prime | ( p pCnt n ) = 1 } = { p e. Prime | p || n } )
212	211	adantrr 753	. . . . . . 7 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> { p e. Prime | ( p pCnt n ) = 1 } = { p e. Prime | p || n } )
213	202, 212	syl5eq 2668	. . . . . 6 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( `' ( p e. Prime |-> ( p pCnt n ) ) " { 1 } ) = { p e. Prime | p || n } )
214	213	eqeq2d 2632	. . . . 5 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( z = ( `' ( p e. Prime |-> ( p pCnt n ) ) " { 1 } ) <-> z = { p e. Prime | p || n } ) )
215	200, 214	bitrd 268	. . . 4 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( ( p e. Prime |-> ( p pCnt n ) ) = ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) <-> z = { p e. Prime | p || n } ) )
216	156, 160, 215	3bitr3d 298	. . 3 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) = n <-> z = { p e. Prime | p || n } ) )
217	150, 216	syl5bb 272	. 2 |- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime | p || N } ) ) -> ( n = ( `' G ` ( k e. Prime |-> if ( k e. z , 1 , 0 ) ) ) <-> z = { p e. Prime | p || n } ) )
218	1, 29, 149, 217	f1o2d 6887	1 |- ( N e. NN -> F : S -1-1-onto-> ~P { p e. Prime | p || N } )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   {crab 2916   _Vcvv 3200   C_ wss 3574   ifcif 4086   ~Pcpw 4158   {csn 4177   {cpr 4179   class class class wbr 4653   |-> cmpt 4729   `'ccnv 5113   "cima 5117   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   Fincfn 7955   CCcc 9934   0cc0 9936   1c1 9937   <_ cle 10075   NNcn 11020   NN0cn0 11292   ZZcz 11377   ...cfz 12326   || cdvds 14983   Primecprime 15385   pCnt cpc 15541   mmucmu 24821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-q 11789  df-rp 11833  df-fz 12327  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-dvds 14984  df-gcd 15217  df-prm 15386  df-pc 15542  df-mu 24827

This theorem is referenced by:  musum  24917