Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐹 = 𝐸 )