Metamath Proof Explorer

Theorem 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 ffvelrni 
 |-  ( ( 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 sseldi 
 |-  ( ( 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 syl5eq 
 |-  ( ( 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 syl5bb 
 |-  ( ( 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 } )