Theorem cytpfn

Description: Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Assertion	cytpfn	$$⊢\mathrm{CytP}Fn\mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		ovex	$$⊢\underset{r\in {\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}}}\left({\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)\right)\in \mathrm{V}$$
2		df-cytp	$$⊢\mathrm{CytP}=\left(n\in \mathbb{N}⟼\underset{r\in {\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}}}\left({\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)\right)\right)$$
3	1 2	fnmpti	$$⊢\mathrm{CytP}Fn\mathbb{N}$$