Theorem etransclem4

Description: F expressed as a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem4.a	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
	etransclem4.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem4.M	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	etransclem4.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
	etransclem4.h	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
	etransclem4.e	⊢ 𝐸 = ( 𝑥 ∈ 𝐴 ↦ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑥 ) )
Assertion	etransclem4	⊢ ( 𝜑 → 𝐹 = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		etransclem4.a	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
2		etransclem4.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
3		etransclem4.M	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4		etransclem4.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
5		etransclem4.h	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
6		etransclem4.e	⊢ 𝐸 = ( 𝑥 ∈ 𝐴 ↦ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑥 ) )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
8		cnex	⊢ ℂ ∈ V
9	8	ssex	⊢ ( 𝐴 ⊆ ℂ → 𝐴 ∈ V )
10		mptexg	⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V )
11	1 9 10	3syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V )
13	5	fvmpt2	⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ∈ V ) → ( 𝐻 ‘ 𝑗 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
14	7 12 13	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐻 ‘ 𝑗 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
15		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ V )
16	14 15	fvmpt2d	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑥 ) = ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
17	16	an32s	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑥 ) = ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
18	17	prodeq2dv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑥 ) = ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
19		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
20	3 19	eleqtrdi	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
22	1	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℂ )
23	22	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑥 ∈ ℂ )
24		elfzelz	⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
25	24	zcnd	⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℂ )
26	25	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ℂ )
27	23 26	subcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 − 𝑗 ) ∈ ℂ )
28		nnm1nn0	⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
29	2 28	syl	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
30	2	nnnn0d	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
31	29 30	ifcld	⊢ ( 𝜑 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
32	31	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
33	27 32	expcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℂ )
34		oveq2	⊢ ( 𝑗 = 0 → ( 𝑥 − 𝑗 ) = ( 𝑥 − 0 ) )
35		iftrue	⊢ ( 𝑗 = 0 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) = ( 𝑃 − 1 ) )
36	34 35	oveq12d	⊢ ( 𝑗 = 0 → ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑥 − 0 ) ↑ ( 𝑃 − 1 ) ) )
37	21 33 36	fprod1p	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( ( 𝑥 − 0 ) ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
38	22	subid1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 − 0 ) = 𝑥 )
39	38	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 − 0 ) ↑ ( 𝑃 − 1 ) ) = ( 𝑥 ↑ ( 𝑃 − 1 ) ) )
40		0p1e1	⊢ ( 0 + 1 ) = 1
41	40	oveq1i	⊢ ( ( 0 + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 )
42	41	a1i	⊢ ( 𝜑 → ( ( 0 + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 ) )
43		0red	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 ∈ ℝ )
44		1red	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 1 ∈ ℝ )
45		elfzelz	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℤ )
46	45	zred	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℝ )
47		0lt1	⊢ 0 < 1
48	47	a1i	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 < 1 )
49		elfzle1	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 1 ≤ 𝑗 )
50	43 44 46 48 49	ltletrd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 < 𝑗 )
51	50	gt0ne0d	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ≠ 0 )
52	51	neneqd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ¬ 𝑗 = 0 )
53	52	iffalsed	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) = 𝑃 )
54	53	oveq2d	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) )
55	54	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) )
56	42 55	prodeq12rdv	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) )
57	56	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) )
58	39 57	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 − 0 ) ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
59	18 37 58	3eqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) = ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑥 ) )
60	59	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( 𝐻 ‘ 𝑗 ) ‘ 𝑥 ) ) )
61	60 4 6	3eqtr4g	⊢ ( 𝜑 → 𝐹 = 𝐸 )