Theorem etransclem1

Description: H is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem1.x	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
	etransclem1.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem1.h	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
	etransclem1.j	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
Assertion	etransclem1	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐽 ) : 𝑋 ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		etransclem1.x	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
2		etransclem1.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
3		etransclem1.h	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
4		etransclem1.j	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
5	1	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ℂ )
6	4	elfzelzd	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
7	6	zcnd	⊢ ( 𝜑 → 𝐽 ∈ ℂ )
8	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐽 ∈ ℂ )
9	5 8	subcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 − 𝐽 ) ∈ ℂ )
10		nnm1nn0	⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
11	2 10	syl	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
12	2	nnnn0d	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
13	11 12	ifcld	⊢ ( 𝜑 → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
15	9 14	expcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 − 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℂ )
16		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
17	15 16	fmptd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) : 𝑋 ⟶ ℂ )
18		oveq2	⊢ ( 𝑗 = 𝑛 → ( 𝑥 − 𝑗 ) = ( 𝑥 − 𝑛 ) )
19		eqeq1	⊢ ( 𝑗 = 𝑛 → ( 𝑗 = 0 ↔ 𝑛 = 0 ) )
20	19	ifbid	⊢ ( 𝑗 = 𝑛 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) = if ( 𝑛 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
21	18 20	oveq12d	⊢ ( 𝑗 = 𝑛 → ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑥 − 𝑛 ) ↑ if ( 𝑛 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
22	21	mpteq2dv	⊢ ( 𝑗 = 𝑛 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑛 ) ↑ if ( 𝑛 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
23	22	cbvmptv	⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑛 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑛 ) ↑ if ( 𝑛 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
24	3 23	eqtri	⊢ 𝐻 = ( 𝑛 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑛 ) ↑ if ( 𝑛 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
25		oveq2	⊢ ( 𝑛 = 𝐽 → ( 𝑥 − 𝑛 ) = ( 𝑥 − 𝐽 ) )
26		eqeq1	⊢ ( 𝑛 = 𝐽 → ( 𝑛 = 0 ↔ 𝐽 = 0 ) )
27	26	ifbid	⊢ ( 𝑛 = 𝐽 → if ( 𝑛 = 0 , ( 𝑃 − 1 ) , 𝑃 ) = if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
28	25 27	oveq12d	⊢ ( 𝑛 = 𝐽 → ( ( 𝑥 − 𝑛 ) ↑ if ( 𝑛 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑥 − 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
29	28	mpteq2dv	⊢ ( 𝑛 = 𝐽 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑛 ) ↑ if ( 𝑛 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
30		cnex	⊢ ℂ ∈ V
31	30	ssex	⊢ ( 𝑋 ⊆ ℂ → 𝑋 ∈ V )
32		mptexg	⊢ ( 𝑋 ∈ V → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V )
33	1 31 32	3syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V )
34	24 29 4 33	fvmptd3	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐽 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
35	34	feq1d	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐽 ) : 𝑋 ⟶ ℂ ↔ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝐽 ) ↑ if ( 𝐽 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) : 𝑋 ⟶ ℂ ) )
36	17 35	mpbird	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐽 ) : 𝑋 ⟶ ℂ )