Definition df-phi

Description: Define the Euler phi function (also called "Euler totient function"), which counts the number of integers less than n and coprime to it, see definition in ApostolNT p. 25. (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Assertion	df-phi	$$⊢\mathrm{\varphi }=\left(n\in \mathbb{N}⟼\left|\left\{x\in \left(1\dots n\right)|x\gcd n=1\right\}\right|\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cphi	$$class\mathrm{\varphi }$$
1		vn	$$setvarn$$
2		cn	$$class\mathbb{N}$$
3		chash	$$class\left|.\right|$$
4		vx	$$setvarx$$
5		c1	$$class1$$
6		cfz	$$class\dots$$
7	1	cv	$$setvarn$$
8	5 7 6	co	$$class\left(1\dots n\right)$$
9	4	cv	$$setvarx$$
10		cgcd	$$class\gcd$$
11	9 7 10	co	$$class\left(x\gcd n\right)$$
12	11 5	wceq	$$wffx\gcd n=1$$
13	12 4 8	crab	$$class\left\{x\in \left(1\dots n\right)|x\gcd n=1\right\}$$
14	13 3	cfv	$$class\left|\left\{x\in \left(1\dots n\right)|x\gcd n=1\right\}\right|$$
15	1 2 14	cmpt	$$class\left(n\in \mathbb{N}⟼\left|\left\{x\in \left(1\dots n\right)|x\gcd n=1\right\}\right|\right)$$
16	0 15	wceq	$$wff\mathrm{\varphi }=\left(n\in \mathbb{N}⟼\left|\left\{x\in \left(1\dots n\right)|x\gcd n=1\right\}\right|\right)$$