sqff1o

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)

	Ref	Expression
Hypotheses	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	sqff1o	\|- ( N e. NN -> F : S -1-1-onto-> ~P { p e. Prime \| p \|\| N } )

Proof

Step	Hyp	Ref	Expression
1		sqff1o.1	\|- S = { x e. NN \| ( ( mmu ` x ) =/= 0 /\ x \|\| N ) }
2		sqff1o.2	\|- F = ( n e. S \|-> { p e. Prime \| p \|\| n } )
3		sqff1o.3	\|- G = ( n e. NN \|-> ( p e. Prime \|-> ( p pCnt n ) ) )
4		fveq2	\|- ( x = n -> ( mmu ` x ) = ( mmu ` n ) )
5	4	neeq1d	\|- ( x = n -> ( ( mmu ` x ) =/= 0 <-> ( mmu ` n ) =/= 0 ) )
6		breq1	\|- ( x = n -> ( x \|\| N <-> n \|\| N ) )
7	5 6	anbi12d	\|- ( x = n -> ( ( ( mmu ` x ) =/= 0 /\ x \|\| N ) <-> ( ( mmu ` n ) =/= 0 /\ n \|\| N ) ) )
8	7 1	elrab2	\|- ( n e. S <-> ( n e. NN /\ ( ( mmu ` n ) =/= 0 /\ n \|\| N ) ) )
9	8	simprbi	\|- ( n e. S -> ( ( mmu ` n ) =/= 0 /\ n \|\| N ) )
10	9	simprd	\|- ( n e. S -> n \|\| N )
11	10	ad2antlr	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> n \|\| N )
12		prmz	\|- ( p e. Prime -> p e. ZZ )
13	12	adantl	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> p e. ZZ )
14		simplr	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> n e. S )
15	14 8	sylib	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( n e. NN /\ ( ( mmu ` n ) =/= 0 /\ n \|\| N ) ) )
16	15	simpld	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> n e. NN )
17	16	nnzd	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> n e. ZZ )
18		nnz	\|- ( N e. NN -> N e. ZZ )
19	18	ad2antrr	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> N e. ZZ )
20		dvdstr	\|- ( ( p e. ZZ /\ n e. ZZ /\ N e. ZZ ) -> ( ( p \|\| n /\ n \|\| N ) -> p \|\| N ) )
21	13 17 19 20	syl3anc	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p \|\| n /\ n \|\| N ) -> p \|\| N ) )
22	11 21	mpan2d	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( p \|\| n -> p \|\| N ) )
23	22	ss2rabdv	\|- ( ( N e. NN /\ n e. S ) -> { p e. Prime \| p \|\| n } C_ { p e. Prime \| p \|\| N } )
24		prmex	\|- Prime e. _V
25	24	rabex	\|- { p e. Prime \| p \|\| n } e. _V
26	25	elpw	\|- ( { p e. Prime \| p \|\| n } e. ~P { p e. Prime \| p \|\| N } <-> { p e. Prime \| p \|\| n } C_ { p e. Prime \| p \|\| N } )
27	23 26	sylibr	\|- ( ( N e. NN /\ n e. S ) -> { p e. Prime \| p \|\| n } e. ~P { p e. Prime \| p \|\| N } )
28		cnveq	\|- ( y = ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) -> `' y = `' ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) )
29	28	imaeq1d	\|- ( y = ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) -> ( `' y " NN ) = ( `' ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) " NN ) )
30	29	eleq1d	\|- ( 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 ) )
31		1nn0	\|- 1 e. NN0
32		0nn0	\|- 0 e. NN0
33	31 32	ifcli	\|- if ( k e. z , 1 , 0 ) e. NN0
34	33	rgenw	\|- A. k e. Prime if ( k e. z , 1 , 0 ) e. NN0
35		eqid	\|- ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) = ( k e. Prime \|-> if ( k e. z , 1 , 0 ) )
36	35	fmpt	\|- ( A. k e. Prime if ( k e. z , 1 , 0 ) e. NN0 <-> ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) : Prime --> NN0 )
37	34 36	mpbi	\|- ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) : Prime --> NN0
38	37	a1i	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) : Prime --> NN0 )
39		nn0ex	\|- NN0 e. _V
40	39 24	elmap	\|- ( ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) e. ( NN0 ^m Prime ) <-> ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) : Prime --> NN0 )
41	38 40	sylibr	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) e. ( NN0 ^m Prime ) )
42		fzfi	\|- ( 1 ... N ) e. Fin
43		ffn	\|- ( ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) : Prime --> NN0 -> ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) Fn Prime )
44		elpreima	\|- ( ( 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 ) ) )
45	37 43 44	mp2b	\|- ( 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 ) )
46		elequ1	\|- ( k = x -> ( k e. z <-> x e. z ) )
47	46	ifbid	\|- ( k = x -> if ( k e. z , 1 , 0 ) = if ( x e. z , 1 , 0 ) )
48	31 32	ifcli	\|- if ( x e. z , 1 , 0 ) e. NN0
49	48	elexi	\|- if ( x e. z , 1 , 0 ) e. _V
50	47 35 49	fvmpt	\|- ( x e. Prime -> ( ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ` x ) = if ( x e. z , 1 , 0 ) )
51	50	eleq1d	\|- ( x e. Prime -> ( ( ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ` x ) e. NN <-> if ( x e. z , 1 , 0 ) e. NN ) )
52	51	biimpa	\|- ( ( x e. Prime /\ ( ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ` x ) e. NN ) -> if ( x e. z , 1 , 0 ) e. NN )
53	45 52	sylbi	\|- ( x e. ( `' ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) " NN ) -> if ( x e. z , 1 , 0 ) e. NN )
54		0nnn	\|- -. 0 e. NN
55		iffalse	\|- ( -. x e. z -> if ( x e. z , 1 , 0 ) = 0 )
56	55	eleq1d	\|- ( -. x e. z -> ( if ( x e. z , 1 , 0 ) e. NN <-> 0 e. NN ) )
57	54 56	mtbiri	\|- ( -. x e. z -> -. if ( x e. z , 1 , 0 ) e. NN )
58	57	con4i	\|- ( if ( x e. z , 1 , 0 ) e. NN -> x e. z )
59	53 58	syl	\|- ( x e. ( `' ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) " NN ) -> x e. z )
60	59	ssriv	\|- ( `' ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) " NN ) C_ z
61		elpwi	\|- ( z e. ~P { p e. Prime \| p \|\| N } -> z C_ { p e. Prime \| p \|\| N } )
62	61	adantl	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> z C_ { p e. Prime \| p \|\| N } )
63		prmssnn	\|- Prime C_ NN
64		rabss2	\|- ( Prime C_ NN -> { p e. Prime \| p \|\| N } C_ { p e. NN \| p \|\| N } )
65	63 64	ax-mp	\|- { p e. Prime \| p \|\| N } C_ { p e. NN \| p \|\| N }
66		dvdsssfz1	\|- ( N e. NN -> { p e. NN \| p \|\| N } C_ ( 1 ... N ) )
67	66	adantr	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> { p e. NN \| p \|\| N } C_ ( 1 ... N ) )
68	65 67	sstrid	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> { p e. Prime \| p \|\| N } C_ ( 1 ... N ) )
69	62 68	sstrd	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> z C_ ( 1 ... N ) )
70	60 69	sstrid	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> ( `' ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) " NN ) C_ ( 1 ... N ) )
71		ssfi	\|- ( ( ( 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 )
72	42 70 71	sylancr	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> ( `' ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) " NN ) e. Fin )
73	30 41 72	elrabd	\|- ( ( 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 } )
74		eqid	\|- { y e. ( NN0 ^m Prime ) \| ( `' y " NN ) e. Fin } = { y e. ( NN0 ^m Prime ) \| ( `' y " NN ) e. Fin }
75	3 74	1arith	\|- G : NN -1-1-onto-> { y e. ( NN0 ^m Prime ) \| ( `' y " NN ) e. Fin }
76		f1ocnv	\|- ( 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 )
77		f1of	\|- ( `' 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 )
78	75 76 77	mp2b	\|- `' G : { y e. ( NN0 ^m Prime ) \| ( `' y " NN ) e. Fin } --> NN
79	78	ffvelcdmi	\|- ( ( 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 )
80	73 79	syl	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) e. NN )
81		f1ocnvfv2	\|- ( ( 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 ) ) )
82	75 73 81	sylancr	\|- ( ( 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 ) ) )
83	3	1arithlem1	\|- ( ( `' 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 ) ) ) ) ) )
84	80 83	syl	\|- ( ( 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 ) ) ) ) ) )
85	82 84	eqtr3d	\|- ( ( 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 ) ) ) ) ) )
86	85	fveq1d	\|- ( ( 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 ) )
87		elequ1	\|- ( k = q -> ( k e. z <-> q e. z ) )
88	87	ifbid	\|- ( k = q -> if ( k e. z , 1 , 0 ) = if ( q e. z , 1 , 0 ) )
89	31 32	ifcli	\|- if ( q e. z , 1 , 0 ) e. NN0
90	89	elexi	\|- if ( q e. z , 1 , 0 ) e. _V
91	88 35 90	fvmpt	\|- ( q e. Prime -> ( ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ` q ) = if ( q e. z , 1 , 0 ) )
92	86 91	sylan9req	\|- ( ( ( 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 ) )
93		oveq1	\|- ( 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 ) ) ) ) )
94		eqid	\|- ( 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 ) ) ) ) )
95		ovex	\|- ( q pCnt ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) ) e. _V
96	93 94 95	fvmpt	\|- ( 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 ) ) ) ) )
97	96	adantl	\|- ( ( ( 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 ) ) ) ) )
98	92 97	eqtr3d	\|- ( ( ( 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 ) ) ) ) )
99		breq1	\|- ( 1 = if ( q e. z , 1 , 0 ) -> ( 1 <_ 1 <-> if ( q e. z , 1 , 0 ) <_ 1 ) )
100		breq1	\|- ( 0 = if ( q e. z , 1 , 0 ) -> ( 0 <_ 1 <-> if ( q e. z , 1 , 0 ) <_ 1 ) )
101		1le1	\|- 1 <_ 1
102		0le1	\|- 0 <_ 1
103	99 100 101 102	keephyp	\|- if ( q e. z , 1 , 0 ) <_ 1
104	98 103	eqbrtrrdi	\|- ( ( ( 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 )
105	104	ralrimiva	\|- ( ( 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 )
106		issqf	\|- ( ( `' 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 ) )
107	80 106	syl	\|- ( ( 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 ) )
108	105 107	mpbird	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> ( mmu ` ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) ) =/= 0 )
109		iftrue	\|- ( q e. z -> if ( q e. z , 1 , 0 ) = 1 )
110	109	adantl	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. z ) -> if ( q e. z , 1 , 0 ) = 1 )
111	62	sselda	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. z ) -> q e. { p e. Prime \| p \|\| N } )
112		breq1	\|- ( p = q -> ( p \|\| N <-> q \|\| N ) )
113	112	elrab	\|- ( q e. { p e. Prime \| p \|\| N } <-> ( q e. Prime /\ q \|\| N ) )
114	111 113	sylib	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. z ) -> ( q e. Prime /\ q \|\| N ) )
115	114	simprd	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. z ) -> q \|\| N )
116	114	simpld	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. z ) -> q e. Prime )
117		simpll	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. z ) -> N e. NN )
118		pcelnn	\|- ( ( q e. Prime /\ N e. NN ) -> ( ( q pCnt N ) e. NN <-> q \|\| N ) )
119	116 117 118	syl2anc	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. z ) -> ( ( q pCnt N ) e. NN <-> q \|\| N ) )
120	115 119	mpbird	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. z ) -> ( q pCnt N ) e. NN )
121	120	nnge1d	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. z ) -> 1 <_ ( q pCnt N ) )
122	110 121	eqbrtrd	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. z ) -> if ( q e. z , 1 , 0 ) <_ ( q pCnt N ) )
123	122	ex	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> ( q e. z -> if ( q e. z , 1 , 0 ) <_ ( q pCnt N ) ) )
124	123	adantr	\|- ( ( ( 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 ) ) )
125		simpr	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. Prime ) -> q e. Prime )
126	18	ad2antrr	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. Prime ) -> N e. ZZ )
127		pcge0	\|- ( ( q e. Prime /\ N e. ZZ ) -> 0 <_ ( q pCnt N ) )
128	125 126 127	syl2anc	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. Prime ) -> 0 <_ ( q pCnt N ) )
129		iffalse	\|- ( -. q e. z -> if ( q e. z , 1 , 0 ) = 0 )
130	129	breq1d	\|- ( -. q e. z -> ( if ( q e. z , 1 , 0 ) <_ ( q pCnt N ) <-> 0 <_ ( q pCnt N ) ) )
131	128 130	syl5ibrcom	\|- ( ( ( 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 ) ) )
132	124 131	pm2.61d	\|- ( ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) /\ q e. Prime ) -> if ( q e. z , 1 , 0 ) <_ ( q pCnt N ) )
133	98 132	eqbrtrrd	\|- ( ( ( 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 ) )
134	133	ralrimiva	\|- ( ( 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 ) )
135	80	nnzd	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) e. ZZ )
136	18	adantr	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> N e. ZZ )
137		pc2dvds	\|- ( ( ( `' 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 ) ) )
138	135 136 137	syl2anc	\|- ( ( 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 ) ) )
139	134 138	mpbird	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) \|\| N )
140	108 139	jca	\|- ( ( 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 ) )
141		fveq2	\|- ( x = ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) -> ( mmu ` x ) = ( mmu ` ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) ) )
142	141	neeq1d	\|- ( 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 ) )
143		breq1	\|- ( x = ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) -> ( x \|\| N <-> ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) \|\| N ) )
144	142 143	anbi12d	\|- ( 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 ) ) )
145	144 1	elrab2	\|- ( ( `' 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 ) ) )
146	80 140 145	sylanbrc	\|- ( ( N e. NN /\ z e. ~P { p e. Prime \| p \|\| N } ) -> ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) e. S )
147		eqcom	\|- ( n = ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) <-> ( `' G ` ( k e. Prime \|-> if ( k e. z , 1 , 0 ) ) ) = n )
148	8	simplbi	\|- ( n e. S -> n e. NN )
149	148	ad2antrl	\|- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime \| p \|\| N } ) ) -> n e. NN )
150	24	mptex	\|- ( p e. Prime \|-> ( p pCnt n ) ) e. _V
151	3	fvmpt2	\|- ( ( n e. NN /\ ( p e. Prime \|-> ( p pCnt n ) ) e. _V ) -> ( G ` n ) = ( p e. Prime \|-> ( p pCnt n ) ) )
152	149 150 151	sylancl	\|- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime \| p \|\| N } ) ) -> ( G ` n ) = ( p e. Prime \|-> ( p pCnt n ) ) )
153	152	eqeq1d	\|- ( ( 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 ) ) ) )
154	75	a1i	\|- ( ( 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 } )
155	73	adantrl	\|- ( ( 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 } )
156		f1ocnvfvb	\|- ( ( 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 ) )
157	154 149 155 156	syl3anc	\|- ( ( 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 ) )
158	24	a1i	\|- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime \| p \|\| N } ) ) -> Prime e. _V )
159		0cnd	\|- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime \| p \|\| N } ) ) -> 0 e. CC )
160		1cnd	\|- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime \| p \|\| N } ) ) -> 1 e. CC )
161		0ne1	\|- 0 =/= 1
162	161	a1i	\|- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime \| p \|\| N } ) ) -> 0 =/= 1 )
163	158 159 160 162	pw2f1olem	\|- ( ( 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 } ) ) ) )
164		ssrab2	\|- { p e. Prime \| p \|\| N } C_ Prime
165	164	sspwi	\|- ~P { p e. Prime \| p \|\| N } C_ ~P Prime
166		simprr	\|- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime \| p \|\| N } ) ) -> z e. ~P { p e. Prime \| p \|\| N } )
167	165 166	sselid	\|- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime \| p \|\| N } ) ) -> z e. ~P Prime )
168	167	biantrurd	\|- ( ( 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 ) ) ) ) )
169		id	\|- ( p e. Prime -> p e. Prime )
170	148	adantl	\|- ( ( N e. NN /\ n e. S ) -> n e. NN )
171		pccl	\|- ( ( p e. Prime /\ n e. NN ) -> ( p pCnt n ) e. NN0 )
172	169 170 171	syl2anr	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( p pCnt n ) e. NN0 )
173		elnn0	\|- ( ( p pCnt n ) e. NN0 <-> ( ( p pCnt n ) e. NN \/ ( p pCnt n ) = 0 ) )
174	172 173	sylib	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) e. NN \/ ( p pCnt n ) = 0 ) )
175	174	orcomd	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) = 0 \/ ( p pCnt n ) e. NN ) )
176	9	simpld	\|- ( n e. S -> ( mmu ` n ) =/= 0 )
177	176	adantl	\|- ( ( N e. NN /\ n e. S ) -> ( mmu ` n ) =/= 0 )
178		issqf	\|- ( n e. NN -> ( ( mmu ` n ) =/= 0 <-> A. p e. Prime ( p pCnt n ) <_ 1 ) )
179	170 178	syl	\|- ( ( N e. NN /\ n e. S ) -> ( ( mmu ` n ) =/= 0 <-> A. p e. Prime ( p pCnt n ) <_ 1 ) )
180	177 179	mpbid	\|- ( ( N e. NN /\ n e. S ) -> A. p e. Prime ( p pCnt n ) <_ 1 )
181	180	r19.21bi	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( p pCnt n ) <_ 1 )
182		nnle1eq1	\|- ( ( p pCnt n ) e. NN -> ( ( p pCnt n ) <_ 1 <-> ( p pCnt n ) = 1 ) )
183	181 182	syl5ibcom	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) e. NN -> ( p pCnt n ) = 1 ) )
184	183	orim2d	\|- ( ( ( 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 ) ) )
185	175 184	mpd	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) = 0 \/ ( p pCnt n ) = 1 ) )
186		ovex	\|- ( p pCnt n ) e. _V
187	186	elpr	\|- ( ( p pCnt n ) e. { 0 , 1 } <-> ( ( p pCnt n ) = 0 \/ ( p pCnt n ) = 1 ) )
188	185 187	sylibr	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( p pCnt n ) e. { 0 , 1 } )
189	188	fmpttd	\|- ( ( N e. NN /\ n e. S ) -> ( p e. Prime \|-> ( p pCnt n ) ) : Prime --> { 0 , 1 } )
190	189	adantrr	\|- ( ( N e. NN /\ ( n e. S /\ z e. ~P { p e. Prime \| p \|\| N } ) ) -> ( p e. Prime \|-> ( p pCnt n ) ) : Prime --> { 0 , 1 } )
191		prex	\|- { 0 , 1 } e. _V
192	191 24	elmap	\|- ( ( p e. Prime \|-> ( p pCnt n ) ) e. ( { 0 , 1 } ^m Prime ) <-> ( p e. Prime \|-> ( p pCnt n ) ) : Prime --> { 0 , 1 } )
193	190 192	sylibr	\|- ( ( 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 ) )
194	193	biantrurd	\|- ( ( 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 } ) ) ) )
195	163 168 194	3bitr4d	\|- ( ( 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 } ) ) )
196		eqid	\|- ( p e. Prime \|-> ( p pCnt n ) ) = ( p e. Prime \|-> ( p pCnt n ) )
197	196	mptiniseg	\|- ( 1 e. NN0 -> ( `' ( p e. Prime \|-> ( p pCnt n ) ) " { 1 } ) = { p e. Prime \| ( p pCnt n ) = 1 } )
198	31 197	ax-mp	\|- ( `' ( p e. Prime \|-> ( p pCnt n ) ) " { 1 } ) = { p e. Prime \| ( p pCnt n ) = 1 }
199		id	\|- ( ( p pCnt n ) = 1 -> ( p pCnt n ) = 1 )
200		1nn	\|- 1 e. NN
201	199 200	eqeltrdi	\|- ( ( p pCnt n ) = 1 -> ( p pCnt n ) e. NN )
202	201 183	impbid2	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) = 1 <-> ( p pCnt n ) e. NN ) )
203		simpr	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> p e. Prime )
204		pcelnn	\|- ( ( p e. Prime /\ n e. NN ) -> ( ( p pCnt n ) e. NN <-> p \|\| n ) )
205	203 16 204	syl2anc	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) e. NN <-> p \|\| n ) )
206	202 205	bitrd	\|- ( ( ( N e. NN /\ n e. S ) /\ p e. Prime ) -> ( ( p pCnt n ) = 1 <-> p \|\| n ) )
207	206	rabbidva	\|- ( ( N e. NN /\ n e. S ) -> { p e. Prime \| ( p pCnt n ) = 1 } = { p e. Prime \| p \|\| n } )
208	207	adantrr	\|- ( ( 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 } )
209	198 208	eqtrid	\|- ( ( 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 } )
210	209	eqeq2d	\|- ( ( 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 } ) )
211	195 210	bitrd	\|- ( ( 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 } ) )
212	153 157 211	3bitr3d	\|- ( ( 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 } ) )
213	147 212	bitrid	\|- ( ( 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 } ) )
214	2 27 146 213	f1o2d	\|- ( N e. NN -> F : S -1-1-onto-> ~P { p e. Prime \| p \|\| N } )

Metamath Proof Explorer

Theorem sqff1o

Proof