# Metamath Proof Explorer

## Theorem etransclem4

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

Ref Expression
Hypotheses etransclem4.a ${⊢}{\phi }\to {A}\subseteq ℂ$
etransclem4.p ${⊢}{\phi }\to {P}\in ℕ$
etransclem4.M ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
etransclem4.f ${⊢}{F}=\left({x}\in {A}⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)$
etransclem4.h ${⊢}{H}=\left({j}\in \left(0\dots {M}\right)⟼\left({x}\in {A}⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\right)$
etransclem4.e ${⊢}{E}=\left({x}\in {A}⟼\prod _{{j}=0}^{{M}}{H}\left({j}\right)\left({x}\right)\right)$
Assertion etransclem4 ${⊢}{\phi }\to {F}={E}$

### Proof

Step Hyp Ref Expression
1 etransclem4.a ${⊢}{\phi }\to {A}\subseteq ℂ$
2 etransclem4.p ${⊢}{\phi }\to {P}\in ℕ$
3 etransclem4.M ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
4 etransclem4.f ${⊢}{F}=\left({x}\in {A}⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)$
5 etransclem4.h ${⊢}{H}=\left({j}\in \left(0\dots {M}\right)⟼\left({x}\in {A}⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\right)$
6 etransclem4.e ${⊢}{E}=\left({x}\in {A}⟼\prod _{{j}=0}^{{M}}{H}\left({j}\right)\left({x}\right)\right)$
7 simpr ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to {j}\in \left(0\dots {M}\right)$
8 cnex ${⊢}ℂ\in \mathrm{V}$
9 8 ssex ${⊢}{A}\subseteq ℂ\to {A}\in \mathrm{V}$
10 mptexg ${⊢}{A}\in \mathrm{V}\to \left({x}\in {A}⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\in \mathrm{V}$
11 1 9 10 3syl ${⊢}{\phi }\to \left({x}\in {A}⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\in \mathrm{V}$
12 11 adantr ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({x}\in {A}⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\in \mathrm{V}$
13 5 fvmpt2 ${⊢}\left({j}\in \left(0\dots {M}\right)\wedge \left({x}\in {A}⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\in \mathrm{V}\right)\to {H}\left({j}\right)=\left({x}\in {A}⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)$
14 7 12 13 syl2anc ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to {H}\left({j}\right)=\left({x}\in {A}⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)$
15 ovexd ${⊢}\left(\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {x}\in {A}\right)\to {\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\in \mathrm{V}$
16 14 15 fvmpt2d ${⊢}\left(\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {x}\in {A}\right)\to {H}\left({j}\right)\left({x}\right)={\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
17 16 an32s ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {H}\left({j}\right)\left({x}\right)={\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
18 17 prodeq2dv ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \prod _{{j}=0}^{{M}}{H}\left({j}\right)\left({x}\right)=\prod _{{j}=0}^{{M}}{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
19 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
20 3 19 eleqtrdi ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 0}$
21 20 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {M}\in {ℤ}_{\ge 0}$
22 1 sselda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in ℂ$
23 22 adantr ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {x}\in ℂ$
24 elfzelz ${⊢}{j}\in \left(0\dots {M}\right)\to {j}\in ℤ$
25 24 zcnd ${⊢}{j}\in \left(0\dots {M}\right)\to {j}\in ℂ$
26 25 adantl ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {j}\in ℂ$
27 23 26 subcld ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {x}-{j}\in ℂ$
28 nnm1nn0 ${⊢}{P}\in ℕ\to {P}-1\in {ℕ}_{0}$
29 2 28 syl ${⊢}{\phi }\to {P}-1\in {ℕ}_{0}$
30 2 nnnn0d ${⊢}{\phi }\to {P}\in {ℕ}_{0}$
31 29 30 ifcld ${⊢}{\phi }\to if\left({j}=0,{P}-1,{P}\right)\in {ℕ}_{0}$
32 31 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to if\left({j}=0,{P}-1,{P}\right)\in {ℕ}_{0}$
33 27 32 expcld ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\in ℂ$
34 oveq2 ${⊢}{j}=0\to {x}-{j}={x}-0$
35 iftrue ${⊢}{j}=0\to if\left({j}=0,{P}-1,{P}\right)={P}-1$
36 34 35 oveq12d ${⊢}{j}=0\to {\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}={\left({x}-0\right)}^{{P}-1}$
37 21 33 36 fprod1p ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \prod _{{j}=0}^{{M}}{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}={\left({x}-0\right)}^{{P}-1}\prod _{{j}=0+1}^{{M}}{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
38 22 subid1d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}-0={x}$
39 38 oveq1d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {\left({x}-0\right)}^{{P}-1}={{x}}^{{P}-1}$
40 0p1e1 ${⊢}0+1=1$
41 40 oveq1i ${⊢}\left(0+1\dots {M}\right)=\left(1\dots {M}\right)$
42 41 a1i ${⊢}{\phi }\to \left(0+1\dots {M}\right)=\left(1\dots {M}\right)$
43 0red ${⊢}{j}\in \left(1\dots {M}\right)\to 0\in ℝ$
44 1red ${⊢}{j}\in \left(1\dots {M}\right)\to 1\in ℝ$
45 elfzelz ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\in ℤ$
46 45 zred ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\in ℝ$
47 0lt1 ${⊢}0<1$
48 47 a1i ${⊢}{j}\in \left(1\dots {M}\right)\to 0<1$
49 elfzle1 ${⊢}{j}\in \left(1\dots {M}\right)\to 1\le {j}$
50 43 44 46 48 49 ltletrd ${⊢}{j}\in \left(1\dots {M}\right)\to 0<{j}$
51 50 gt0ne0d ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\ne 0$
52 51 neneqd ${⊢}{j}\in \left(1\dots {M}\right)\to ¬{j}=0$
53 52 iffalsed ${⊢}{j}\in \left(1\dots {M}\right)\to if\left({j}=0,{P}-1,{P}\right)={P}$
54 53 oveq2d ${⊢}{j}\in \left(1\dots {M}\right)\to {\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}={\left({x}-{j}\right)}^{{P}}$
55 54 adantl ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}={\left({x}-{j}\right)}^{{P}}$
56 42 55 prodeq12rdv ${⊢}{\phi }\to \prod _{{j}=0+1}^{{M}}{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}=\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}$
57 56 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \prod _{{j}=0+1}^{{M}}{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}=\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}$
58 39 57 oveq12d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {\left({x}-0\right)}^{{P}-1}\prod _{{j}=0+1}^{{M}}{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}={{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}$
59 18 37 58 3eqtrrd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}=\prod _{{j}=0}^{{M}}{H}\left({j}\right)\left({x}\right)$
60 59 mpteq2dva ${⊢}{\phi }\to \left({x}\in {A}⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)=\left({x}\in {A}⟼\prod _{{j}=0}^{{M}}{H}\left({j}\right)\left({x}\right)\right)$
61 60 4 6 3eqtr4g ${⊢}{\phi }\to {F}={E}$