Metamath Proof Explorer

Theorem etransclem37

Description: ( P - 1 ) factorial divides the N -th derivative of F applied to J . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem37.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
etransclem37.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
etransclem37.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem37.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
etransclem37.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
etransclem37.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
etransclem37.h ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
etransclem37.c ⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
etransclem37.9 ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
etransclem37.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑋 )
Assertion etransclem37 ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 etransclem37.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 etransclem37.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 etransclem37.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4 etransclem37.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
5 etransclem37.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
6 etransclem37.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7 etransclem37.h ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
8 etransclem37.c ⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
9 etransclem37.9 ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
10 etransclem37.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑋 )
11 8 6 etransclem16 ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ∈ Fin )
12 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
13 3 12 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
14 13 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
15 14 nnzd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
16 8 6 etransclem12 ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
17 16 eleq2d ⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ↔ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) )
18 17 biimpa ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
19 rabid ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ↔ ( 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 ) )
20 19 biimpi ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → ( 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 ) )
21 20 simprd ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 )
22 18 21 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 )
23 22 eqcomd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑁 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) )
24 23 fveq2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ! ‘ 𝑁 ) = ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) ) )
25 24 oveq1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) = ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) )
26 nfcv ⊢ Ⅎ 𝑗 𝑐
27 fzfid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 0 ... 𝑀 ) ∈ Fin )
28 nn0ex ⊢ ℕ0 ∈ V
29 28 a1i ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → ℕ0 ∈ V )
30 fzssnn0 ⊢ ( 0 ... 𝑁 ) ⊆ ℕ0
31 mapss ⊢ ( ( ℕ0 ∈ V ∧ ( 0 ... 𝑁 ) ⊆ ℕ0 ) → ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
32 29 30 31 sylancl ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
33 20 simpld ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) )
34 32 33 sseldd ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → 𝑐 ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
35 18 34 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
36 26 27 35 mccl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) ∈ ℕ )
37 25 36 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) ∈ ℕ )
38 37 nnzd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) ∈ ℤ )
39 3 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑃 ∈ ℕ )
40 4 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑀 ∈ ℕ0 )
41 elmapi ⊢ ( 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
42 18 33 41 3syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
43 9 elfzelzd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝐽 ∈ ℤ )
45 39 40 42 44 etransclem10 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) ∈ ℤ )
46 fzfid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 1 ... 𝑀 ) ∈ Fin )
47 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
48 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
49 0z ⊢ 0 ∈ ℤ
50 fzp1ss ⊢ ( 0 ∈ ℤ → ( ( 0 + 1 ) ... 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
51 49 50 ax-mp ⊢ ( ( 0 + 1 ) ... 𝑀 ) ⊆ ( 0 ... 𝑀 )
52 51 sseli ⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
53 1e0p1 ⊢ 1 = ( 0 + 1 )
54 53 oveq1i ⊢ ( 1 ... 𝑀 ) = ( ( 0 + 1 ) ... 𝑀 )
55 52 54 eleq2s ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
56 55 adantl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
57 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐽 ∈ ℤ )
58 47 48 56 57 etransclem3 ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
59 46 58 fprodzcl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
60 45 59 zmulcld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ∈ ℤ )
61 38 60 zmulcld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) ∈ ℤ )
62 6 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
63 etransclem11 ⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } ) = ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } )
64 8 63 eqtri ⊢ 𝐶 = ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } )
65 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) )
66 9 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝐽 ∈ ( 0 ... 𝑀 ) )
67 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑐 ‘ 𝑗 ) = ( 𝑐 ‘ 𝑘 ) )
68 67 fveq2d ⊢ ( 𝑗 = 𝑘 → ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) = ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) )
69 68 cbvprodv ⊢ ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) = ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑘 ) )
70 69 oveq2i ⊢ ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) = ( ( ! ‘ 𝑁 ) / ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) )
71 67 breq2d ⊢ ( 𝑗 = 𝑘 → ( 𝑃 < ( 𝑐 ‘ 𝑗 ) ↔ 𝑃 < ( 𝑐 ‘ 𝑘 ) ) )
72 67 oveq2d ⊢ ( 𝑗 = 𝑘 → ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) = ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) )
73 72 fveq2d ⊢ ( 𝑗 = 𝑘 → ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) = ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) )
74 73 oveq2d ⊢ ( 𝑗 = 𝑘 → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) = ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) ) )
75 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐽 − 𝑗 ) = ( 𝐽 − 𝑘 ) )
76 75 72 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) = ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) )
77 74 76 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) ) )
78 71 77 ifbieq2d ⊢ ( 𝑗 = 𝑘 → if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) = if ( 𝑃 < ( 𝑐 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) ) ) )
79 78 cbvprodv ⊢ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) = ∏ 𝑘 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) ) )
80 79 oveq2i ⊢ ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) = ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) ) ) )
81 70 80 oveq12i ⊢ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑘 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑘 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑘 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) ) · ( ( 𝐽 − 𝑘 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑘 ) ) ) ) ) ) )
82 39 40 62 64 65 66 81 etransclem28 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) )
83 11 15 61 82 fsumdvds ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∥ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) )
84 1 2 3 4 5 6 7 8 10 etransclem31 ⊢ ( 𝜑 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝐽 ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) )
85 83 84 breqtrrd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝐽 ) )