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 ... 𝑀 ) ) ⊆ ( ℕ0m ( 0 ... 𝑀 ) ) )
32 29 30 31 sylancl ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } → ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0m ( 0 ... 𝑀 ) ) )
33 20 simpld ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } → 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) )
34 32 33 sseldd ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑁 } → 𝑐 ∈ ( ℕ0m ( 0 ... 𝑀 ) ) )
35 18 34 syl ( ( 𝜑𝑐 ∈ ( 𝐶𝑁 ) ) → 𝑐 ∈ ( ℕ0m ( 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𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝐽 ) )