Theorem fuzxrpmcn

Description: A function mapping from an upper set of integers to the extended reals is a partial map on the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	fuzxrpmcn.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	fuzxrpmcn.2	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion	fuzxrpmcn	⊢ ( 𝜑 → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		fuzxrpmcn.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		fuzxrpmcn.2	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
3		cnex	⊢ ℂ ∈ V
4	3	a1i	⊢ ( 𝜑 → ℂ ∈ V )
5		xrex	⊢ ℝ* ∈ V
6	5	a1i	⊢ ( 𝜑 → ℝ* ∈ V )
7	1	uzsscn2	⊢ 𝑍 ⊆ ℂ
8	7	a1i	⊢ ( 𝜑 → 𝑍 ⊆ ℂ )
9	4 6 8 2	fpmd	⊢ ( 𝜑 → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )