Definition df-mu

Description: Define the Möbius function, which is zero for non-squarefree numbers and is -u 1 or 1 for squarefree numbers according as to the number of prime divisors of the number is even or odd, see definition in ApostolNT p. 24. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	df-mu	|- mmu = ( x e. NN |-> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmu	|- mmu
1		vx	|- x
2		cn	|- NN
3		vp	|- p
4		cprime	|- Prime
5	3	cv	|- p
6		cexp	|- ^
7		c2	|- 2
8	5 7 6	co	|- ( p ^ 2 )
9		cdvds	|- ||
10	1	cv	|- x
11	8 10 9	wbr	|- ( p ^ 2 ) || x
12	11 3 4	wrex	|- E. p e. Prime ( p ^ 2 ) || x
13		cc0	|- 0
14		c1	|- 1
15	14	cneg	|- -u 1
16		chash	|- #
17	5 10 9	wbr	|- p || x
18	17 3 4	crab	|- { p e. Prime | p || x }
19	18 16	cfv	|- ( # ` { p e. Prime | p || x } )
20	15 19 6	co	|- ( -u 1 ^ ( # ` { p e. Prime | p || x } ) )
21	12 13 20	cif	|- if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) )
22	1 2 21	cmpt	|- ( x e. NN |-> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) )
23	0 22	wceq	|- mmu = ( x e. NN |-> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) )