Metamath Proof Explorer

Theorem etransclem14

Description: Value of the term T , when J = 0 and ( C0 ) = P - 1 (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem14.n ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem14.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
etransclem14.c ⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
etransclem14.t ⊢ 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
etransclem14.j ⊢ ( 𝜑 → 𝐽 = 0 )
etransclem14.cpm1 ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) = ( 𝑃 − 1 ) )
Assertion etransclem14 ( 𝜑 → 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 etransclem14.n ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2 etransclem14.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3 etransclem14.c ⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
4 etransclem14.t ⊢ 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
5 etransclem14.j ⊢ ( 𝜑 → 𝐽 = 0 )
6 etransclem14.cpm1 ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) = ( 𝑃 − 1 ) )
7 fzssre ⊢ ( 0 ... 𝑁 ) ⊆ ℝ
8 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
9 2 8 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
10 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
11 9 10 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
12 3 11 ffvelrnd ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ ( 0 ... 𝑁 ) )
13 7 12 sseldi ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ ℝ )
14 6 13 eqeltrrd ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℝ )
15 13 14 lttri3d ⊢ ( 𝜑 → ( ( 𝐶 ‘ 0 ) = ( 𝑃 − 1 ) ↔ ( ¬ ( 𝐶 ‘ 0 ) < ( 𝑃 − 1 ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) ) )
16 6 15 mpbid ⊢ ( 𝜑 → ( ¬ ( 𝐶 ‘ 0 ) < ( 𝑃 − 1 ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) )
17 16 simprd ⊢ ( 𝜑 → ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) )
18 17 iffalsed ⊢ ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) )
19 14 recnd ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℂ )
20 6 eqcomd ⊢ ( 𝜑 → ( 𝑃 − 1 ) = ( 𝐶 ‘ 0 ) )
21 19 20 subeq0bd ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) = 0 )
22 21 fveq2d ⊢ ( 𝜑 → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) = ( ! ‘ 0 ) )
23 fac0 ⊢ ( ! ‘ 0 ) = 1
24 22 23 eqtrdi ⊢ ( 𝜑 → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) = 1 )
25 24 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) / 1 ) )
26 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
27 1 26 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
28 27 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
29 28 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
30 29 div1d ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) / 1 ) = ( ! ‘ ( 𝑃 − 1 ) ) )
31 25 30 eqtrd ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) = ( ! ‘ ( 𝑃 − 1 ) ) )
32 5 21 oveq12d ⊢ ( 𝜑 → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) = ( 0 ↑ 0 ) )
33 0exp0e1 ⊢ ( 0 ↑ 0 ) = 1
34 32 33 eqtrdi ⊢ ( 𝜑 → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) = 1 )
35 31 34 oveq12d ⊢ ( 𝜑 → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · 1 ) )
36 29 mulid1d ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · 1 ) = ( ! ‘ ( 𝑃 − 1 ) ) )
37 18 35 36 3eqtrd ⊢ ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) = ( ! ‘ ( 𝑃 − 1 ) ) )
38 5 oveq1d ⊢ ( 𝜑 → ( 𝐽 − 𝑗 ) = ( 0 − 𝑗 ) )
39 df-neg ⊢ - 𝑗 = ( 0 − 𝑗 )
40 38 39 eqtr4di ⊢ ( 𝜑 → ( 𝐽 − 𝑗 ) = - 𝑗 )
41 40 oveq1d ⊢ ( 𝜑 → ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) = ( - 𝑗 ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) )
42 41 oveq2d ⊢ ( 𝜑 → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) )
43 42 ifeq2d ⊢ ( 𝜑 → if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) = if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) )
44 43 prodeq2ad ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) )
45 37 44 oveq12d ⊢ ( 𝜑 → ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
46 45 oveq2d ⊢ ( 𝜑 → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) ) = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) ) )
47 4 46 syl5eq ⊢ ( 𝜑 → 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) ) )