Theorem cytpfn

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

	Ref	Expression
Assertion	cytpfn	⊢ CytP Fn ℕ

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) Σg ( 𝑟 ∈ ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } ) ↦ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) ) ) ∈ V
2		df-cytp	⊢ CytP = ( 𝑛 ∈ ℕ ↦ ( ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) Σg ( 𝑟 ∈ ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } ) ↦ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) ) ) )
3	1 2	fnmpti	⊢ CytP Fn ℕ