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 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
108 106 107 eleqtri ⊢ ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
109 108 a1i ⊢ ( 𝜑 → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
110 etransclem5 ⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
111 fzssre ⊢ ( 0 ... 𝑀 ) ⊆ ℝ
112 111 5 sselid ⊢ ( 𝜑 → 𝐽 ∈ ℝ )
113 105 109 1 2 3 4 110 7 112 etransclem31 ⊢ ( 𝜑 → ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝐼 ) ‘ 𝐽 ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝐼 ) ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) )
114 113 oveq1d ⊢ ( 𝜑 → ( ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝐼 ) ‘ 𝐽 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( Σ 𝑐 ∈ ( 𝐶 ‘ 𝐼 ) ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
115 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 ) ) ) )
116 114 115 eqtrd ⊢ ( 𝜑 → ( ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝐼 ) ‘ 𝐽 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝐼 ) ( ( ( ( ! ‘ 𝐼 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
117 103 116 breqtrrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝐼 ) ‘ 𝐽 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )