Definition df-mu 24827

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.)

Assertion

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

Distinct variable group:   x, p

Detailed syntax breakdown of Definition df-mu

Step	Hyp	Ref	Expression
1		cmu 24821	. 2 class mmu
2		vx	. . 3 setvar x
3		cn 11020	. . 3 class NN
4		vp	. . . . . . . 8 setvar p
5	4	cv 1482	. . . . . . 7 class p
6		c2 11070	. . . . . . 7 class 2
7		cexp 12860	. . . . . . 7 class ^
8	5, 6, 7	co 6650	. . . . . 6 class ( p ^ 2 )
9	2	cv 1482	. . . . . 6 class x
10		cdvds 14983	. . . . . 6 class ||
11	8, 9, 10	wbr 4653	. . . . 5 wff ( p ^ 2 ) || x
12		cprime 15385	. . . . 5 class Prime
13	11, 4, 12	wrex 2913	. . . 4 wff E. p e. Prime ( p ^ 2 ) || x
14		cc0 9936	. . . 4 class 0
15		c1 9937	. . . . . 6 class 1
16	15	cneg 10267	. . . . 5 class -u 1
17	5, 9, 10	wbr 4653	. . . . . . 7 wff p || x
18	17, 4, 12	crab 2916	. . . . . 6 class { p e. Prime | p || x }
19		chash 13117	. . . . . 6 class #
20	18, 19	cfv 5888	. . . . 5 class ( # ` { p e. Prime | p || x } )
21	16, 20, 7	co 6650	. . . 4 class ( -u 1 ^ ( # ` { p e. Prime | p || x } ) )
22	13, 14, 21	cif 4086	. . 3 class if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) )
23	2, 3, 22	cmpt 4729	. 2 class ( x e. NN |-> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) )
24	1, 23	wceq 1483	1 wff mmu = ( x e. NN |-> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) )

This definition is referenced by:  muval  24858  muf  24866