Metamath Proof Explorer


Theorem etransclem38

Description: P divides the I -th derivative of F applied to J . if it is not the case that I = P - 1 and J = 0 . This is case 1 and the second part of case 2 proven in in Juillerat p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem38.p ( 𝜑𝑃 ∈ ℕ )
etransclem38.m ( 𝜑𝑀 ∈ ℕ0 )
etransclem38.f 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑗 ) ↑ 𝑃 ) ) )
etransclem38.i ( 𝜑𝐼 ∈ ℕ0 )
etransclem38.j ( 𝜑𝐽 ∈ ( 0 ... 𝑀 ) )
etransclem38.ij ( 𝜑 → ¬ ( 𝐼 = ( 𝑃 − 1 ) ∧ 𝐽 = 0 ) )
etransclem38.c 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } )
Assertion etransclem38 ( 𝜑𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝐼 ) ‘ 𝐽 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 etransclem38.p ( 𝜑𝑃 ∈ ℕ )
2 etransclem38.m ( 𝜑𝑀 ∈ ℕ0 )
3 etransclem38.f 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑗 ) ↑ 𝑃 ) ) )
4 etransclem38.i ( 𝜑𝐼 ∈ ℕ0 )
5 etransclem38.j ( 𝜑𝐽 ∈ ( 0 ... 𝑀 ) )
6 etransclem38.ij ( 𝜑 → ¬ ( 𝐼 = ( 𝑃 − 1 ) ∧ 𝐽 = 0 ) )
7 etransclem38.c 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } )
8 7 4 etransclem16 ( 𝜑 → ( 𝐶𝐼 ) ∈ Fin )
9 1 nnzd ( 𝜑𝑃 ∈ ℤ )
10 1 adantr ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → 𝑃 ∈ ℕ )
11 2 adantr ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → 𝑀 ∈ ℕ0 )
12 4 adantr ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → 𝐼 ∈ ℕ0 )
13 etransclem11 ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } ) = ( 𝑚 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑒𝑘 ) = 𝑚 } )
14 etransclem11 ( 𝑚 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑒𝑘 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑗 ) = 𝑛 } )
15 7 13 14 3eqtri 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑑𝑗 ) = 𝑛 } )
16 simpr ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → 𝑐 ∈ ( 𝐶𝐼 ) )
17 5 adantr ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → 𝐽 ∈ ( 0 ... 𝑀 ) )
18 eqid ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 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 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) )
19 10 11 12 15 16 17 18 etransclem28 ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) )
20 nnm1nn0 ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
21 1 20 syl ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
22 21 faccld ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
23 22 nnzd ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
24 23 adantr ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
25 22 nnne0d ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
26 25 adantr ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
27 5 elfzelzd ( 𝜑𝐽 ∈ ℤ )
28 27 adantr ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → 𝐽 ∈ ℤ )
29 10 11 12 28 15 16 etransclem26 ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) ∈ ℤ )
30 dvdsval2 ( ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 ∧ ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) ∈ ℤ ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 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 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ) )
31 24 26 29 30 syl3anc ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 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 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ) )
32 19 31 mpbid ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
33 pm3.22 ( ( 𝐽 = 0 ∧ 𝐼 = ( 𝑃 − 1 ) ) → ( 𝐼 = ( 𝑃 − 1 ) ∧ 𝐽 = 0 ) )
34 33 adantll ( ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) ∧ 𝐼 = ( 𝑃 − 1 ) ) → ( 𝐼 = ( 𝑃 − 1 ) ∧ 𝐽 = 0 ) )
35 6 ad3antrrr ( ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) ∧ 𝐼 = ( 𝑃 − 1 ) ) → ¬ ( 𝐼 = ( 𝑃 − 1 ) ∧ 𝐽 = 0 ) )
36 34 35 pm2.65da ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) → ¬ 𝐼 = ( 𝑃 − 1 ) )
37 36 neqned ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) → 𝐼 ≠ ( 𝑃 − 1 ) )
38 1 ad3antrrr ( ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) ∧ 𝐼 ≠ ( 𝑃 − 1 ) ) → 𝑃 ∈ ℕ )
39 2 ad3antrrr ( ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) ∧ 𝐼 ≠ ( 𝑃 − 1 ) ) → 𝑀 ∈ ℕ0 )
40 4 ad3antrrr ( ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) ∧ 𝐼 ≠ ( 𝑃 − 1 ) ) → 𝐼 ∈ ℕ0 )
41 simpr ( ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) ∧ 𝐼 ≠ ( 𝑃 − 1 ) ) → 𝐼 ≠ ( 𝑃 − 1 ) )
42 simplr ( ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) ∧ 𝐼 ≠ ( 𝑃 − 1 ) ) → 𝐽 = 0 )
43 16 ad2antrr ( ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) ∧ 𝐼 ≠ ( 𝑃 − 1 ) ) → 𝑐 ∈ ( 𝐶𝐼 ) )
44 38 39 40 41 42 15 43 etransclem24 ( ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) ∧ 𝐼 ≠ ( 𝑃 − 1 ) ) → 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
45 37 44 mpdan ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ 𝐽 = 0 ) → 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
46 1 ad2antrr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → 𝑃 ∈ ℕ )
47 2 ad2antrr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → 𝑀 ∈ ℕ0 )
48 4 ad2antrr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → 𝐼 ∈ ℕ0 )
49 7 4 etransclem12 ( 𝜑 → ( 𝐶𝐼 ) = { 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝐼 } )
50 49 adantr ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → ( 𝐶𝐼 ) = { 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝐼 } )
51 16 50 eleqtrd ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝐼 } )
52 rabid ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝐼 } ↔ ( 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝐼 ) )
53 51 52 sylib ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → ( 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝐼 ) )
54 53 simpld ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑m ( 0 ... 𝑀 ) ) )
55 elmapi ( 𝑐 ∈ ( ( 0 ... 𝐼 ) ↑m ( 0 ... 𝑀 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝐼 ) )
56 54 55 syl ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝐼 ) )
57 56 adantr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝐼 ) )
58 53 simprd ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝐼 )
59 58 adantr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝐼 )
60 1zzd ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 1 ∈ ℤ )
61 2 nn0zd ( 𝜑𝑀 ∈ ℤ )
62 61 adantr ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝑀 ∈ ℤ )
63 27 adantr ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝐽 ∈ ℤ )
64 elfznn0 ( 𝐽 ∈ ( 0 ... 𝑀 ) → 𝐽 ∈ ℕ0 )
65 5 64 syl ( 𝜑𝐽 ∈ ℕ0 )
66 neqne ( ¬ 𝐽 = 0 → 𝐽 ≠ 0 )
67 65 66 anim12i ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → ( 𝐽 ∈ ℕ0𝐽 ≠ 0 ) )
68 elnnne0 ( 𝐽 ∈ ℕ ↔ ( 𝐽 ∈ ℕ0𝐽 ≠ 0 ) )
69 67 68 sylibr ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝐽 ∈ ℕ )
70 69 nnge1d ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 1 ≤ 𝐽 )
71 elfzle2 ( 𝐽 ∈ ( 0 ... 𝑀 ) → 𝐽𝑀 )
72 5 71 syl ( 𝜑𝐽𝑀 )
73 72 adantr ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝐽𝑀 )
74 60 62 63 70 73 elfzd ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝐽 ∈ ( 1 ... 𝑀 ) )
75 74 adantlr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → 𝐽 ∈ ( 1 ... 𝑀 ) )
76 46 47 48 57 59 18 75 etransclem25 ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → ( ! ‘ 𝑃 ) ∥ ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) )
77 1 nncnd ( 𝜑𝑃 ∈ ℂ )
78 1cnd ( 𝜑 → 1 ∈ ℂ )
79 77 78 npcand ( 𝜑 → ( ( 𝑃 − 1 ) + 1 ) = 𝑃 )
80 79 eqcomd ( 𝜑𝑃 = ( ( 𝑃 − 1 ) + 1 ) )
81 80 fveq2d ( 𝜑 → ( ! ‘ 𝑃 ) = ( ! ‘ ( ( 𝑃 − 1 ) + 1 ) ) )
82 facp1 ( ( 𝑃 − 1 ) ∈ ℕ0 → ( ! ‘ ( ( 𝑃 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ( 𝑃 − 1 ) + 1 ) ) )
83 21 82 syl ( 𝜑 → ( ! ‘ ( ( 𝑃 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ( 𝑃 − 1 ) + 1 ) ) )
84 79 oveq2d ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ( 𝑃 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · 𝑃 ) )
85 22 nncnd ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
86 85 77 mulcomd ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · 𝑃 ) = ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) )
87 84 86 eqtrd ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ( 𝑃 − 1 ) + 1 ) ) = ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) )
88 81 83 87 3eqtrrd ( 𝜑 → ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ! ‘ 𝑃 ) )
89 88 ad2antrr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ! ‘ 𝑃 ) )
90 29 zcnd ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) ∈ ℂ )
91 85 adantr ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
92 90 91 26 divcan1d ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → ( ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) · ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) )
93 92 adantr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → ( ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) · ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) )
94 76 89 93 3brtr4d ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) ∥ ( ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) · ( ! ‘ ( 𝑃 − 1 ) ) ) )
95 9 ad2antrr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → 𝑃 ∈ ℤ )
96 32 adantr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
97 23 ad2antrr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
98 25 ad2antrr ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
99 dvdsmulcr ( ( 𝑃 ∈ ℤ ∧ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ∧ ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 ) ) → ( ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) ∥ ( ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) · ( ! ‘ ( 𝑃 − 1 ) ) ) ↔ 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
100 95 96 97 98 99 syl112anc ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → ( ( 𝑃 · ( ! ‘ ( 𝑃 − 1 ) ) ) ∥ ( ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) · ( ! ‘ ( 𝑃 − 1 ) ) ) ↔ 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
101 94 100 mpbid ( ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) ∧ ¬ 𝐽 = 0 ) → 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
102 45 101 pm2.61dan ( ( 𝜑𝑐 ∈ ( 𝐶𝐼 ) ) → 𝑃 ∥ ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
103 8 9 32 102 fsumdvds ( 𝜑𝑃 ∥ Σ 𝑐 ∈ ( 𝐶𝐼 ) ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
104 reelprrecn ℝ ∈ { ℝ , ℂ }
105 104 a1i ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
106 reopn ℝ ∈ ( topGen ‘ ran (,) )
107 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
108 107 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
109 106 108 eleqtri ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
110 109 a1i ( 𝜑 → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
111 etransclem5 ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ ℝ ↦ ( ( 𝑦𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ ℝ ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
112 fzssre ( 0 ... 𝑀 ) ⊆ ℝ
113 112 5 sseldi ( 𝜑𝐽 ∈ ℝ )
114 105 110 1 2 3 4 111 7 113 etransclem31 ( 𝜑 → ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝐼 ) ‘ 𝐽 ) = Σ 𝑐 ∈ ( 𝐶𝐼 ) ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) )
115 114 oveq1d ( 𝜑 → ( ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝐼 ) ‘ 𝐽 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( Σ 𝑐 ∈ ( 𝐶𝐼 ) ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
116 8 85 90 25 fsumdivc ( 𝜑 → ( Σ 𝑐 ∈ ( 𝐶𝐼 ) ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = Σ 𝑐 ∈ ( 𝐶𝐼 ) ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
117 115 116 eqtrd ( 𝜑 → ( ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝐼 ) ‘ 𝐽 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = Σ 𝑐 ∈ ( 𝐶𝐼 ) ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 𝐽𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
118 103 117 breqtrrd ( 𝜑𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝐼 ) ‘ 𝐽 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )