Metamath Proof Explorer

Theorem etransclem28

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

Ref Expression
Hypotheses etransclem28.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem28.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
etransclem28.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
etransclem28.c ⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
etransclem28.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ‘ 𝑁 ) )
etransclem28.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
etransclem28.t ⊢ 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
Assertion etransclem28 ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∥ 𝑇 )

Proof

Step Hyp Ref Expression
1 etransclem28.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2 etransclem28.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3 etransclem28.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 etransclem28.c ⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
5 etransclem28.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ‘ 𝑁 ) )
6 etransclem28.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
7 etransclem28.t ⊢ 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
8 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
9 1 8 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
10 9 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
11 10 nnzd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = 0 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
13 4 3 etransclem12 ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
14 5 13 eleqtrd ⊢ ( 𝜑 → 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
15 fveq1 ⊢ ( 𝑐 = 𝐷 → ( 𝑐 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑗 ) )
16 15 sumeq2sdv ⊢ ( 𝑐 = 𝐷 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) )
17 16 eqeq1d ⊢ ( 𝑐 = 𝐷 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 ↔ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝑁 ) )
18 17 elrab ⊢ ( 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ↔ ( 𝐷 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝑁 ) )
19 18 simprbi ⊢ ( 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝑁 )
20 14 19 syl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝑁 )
21 20 eqcomd ⊢ ( 𝜑 → 𝑁 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) )
22 21 fveq2d ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) = ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ) )
23 22 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
24 nfcv ⊢ Ⅎ 𝑗 𝐷
25 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
26 nn0ex ⊢ ℕ0 ∈ V
27 fzssnn0 ⊢ ( 0 ... 𝑁 ) ⊆ ℕ0
28 27 a1i ⊢ ( 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → ( 0 ... 𝑁 ) ⊆ ℕ0 )
29 mapss ⊢ ( ( ℕ0 ∈ V ∧ ( 0 ... 𝑁 ) ⊆ ℕ0 ) → ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
30 26 28 29 sylancr ⊢ ( 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
31 elrabi ⊢ ( 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → 𝐷 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) )
32 30 31 sseldd ⊢ ( 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → 𝐷 ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
33 14 32 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
34 24 25 33 mccl ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℕ )
35 23 34 eqeltrd ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℕ )
36 35 nnzd ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℤ )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = 0 ) → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℤ )
38 df-neg ⊢ - 𝑗 = ( 0 − 𝑗 )
39 oveq1 ⊢ ( 𝐽 = 0 → ( 𝐽 − 𝑗 ) = ( 0 − 𝑗 ) )
40 38 39 eqtr4id ⊢ ( 𝐽 = 0 → - 𝑗 = ( 𝐽 − 𝑗 ) )
41 40 oveq1d ⊢ ( 𝐽 = 0 → ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) = ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) )
42 41 oveq2d ⊢ ( 𝐽 = 0 → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) )
43 42 ifeq2d ⊢ ( 𝐽 = 0 → if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) = if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
44 43 prodeq2ad ⊢ ( 𝐽 = 0 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝐽 = 0 ) → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) )
46 14 31 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) )
47 elmapi ⊢ ( 𝐷 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
48 46 47 syl ⊢ ( 𝜑 → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
49 1 48 6 etransclem7 ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = 0 ) → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
51 45 50 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐽 = 0 ) → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
52 12 51 zmulcld ⊢ ( ( 𝜑 ∧ 𝐽 = 0 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℤ )
53 12 37 52 3jca ⊢ ( ( 𝜑 ∧ 𝐽 = 0 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℤ ∧ ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℤ ) )
54 dvdsmul1 ⊢ ( ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
55 12 51 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝐽 = 0 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
56 dvdsmultr2 ⊢ ( ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℤ ∧ ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℤ ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ) )
57 53 55 56 sylc ⊢ ( ( 𝜑 ∧ 𝐽 = 0 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
58 57 adantr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
59 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → 𝑃 ∈ ℕ )
60 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → 𝑀 ∈ ℕ0 )
61 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
62 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 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) )
63 simplr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → 𝐽 = 0 )
64 simpr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) )
65 59 60 61 62 63 64 etransclem14 ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( - 𝑗 ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
66 58 65 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
67 dvds0 ⊢ ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ → ( ! ‘ ( 𝑃 − 1 ) ) ∥ 0 )
68 11 67 syl ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∥ 0 )
69 68 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ¬ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ 0 )
70 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ¬ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → 𝑃 ∈ ℕ )
71 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ¬ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → 𝑀 ∈ ℕ0 )
72 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ¬ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → 𝑁 ∈ ℕ0 )
73 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ¬ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
74 simplr ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ¬ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → 𝐽 = 0 )
75 neqne ⊢ ( ¬ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) → ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) )
76 75 adantl ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ¬ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( 𝐷 ‘ 0 ) ≠ ( 𝑃 − 1 ) )
77 70 71 72 73 62 74 76 etransclem15 ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ¬ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) = 0 )
78 69 77 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐽 = 0 ) ∧ ¬ ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
79 66 78 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝐽 = 0 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
80 1 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
81 elfznn0 ⊢ ( 𝐽 ∈ ( 0 ... 𝑀 ) → 𝐽 ∈ ℕ0 )
82 6 81 syl ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
83 82 nn0zd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
84 1 2 3 83 4 5 etransclem26 ⊢ ( 𝜑 → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ∈ ℤ )
85 11 80 84 3jca ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ∈ ℤ ) )
86 85 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ∈ ℤ ) )
87 1 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
88 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
89 87 88 npcand ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) + 1 ) = 𝑃 )
90 89 eqcomd ⊢ ( 𝜑 → 𝑃 = ( ( 𝑃 − 1 ) + 1 ) )
91 90 fveq2d ⊢ ( 𝜑 → ( ! ‘ 𝑃 ) = ( ! ‘ ( ( 𝑃 − 1 ) + 1 ) ) )
92 facp1 ⊢ ( ( 𝑃 − 1 ) ∈ ℕ0 → ( ! ‘ ( ( 𝑃 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ( 𝑃 − 1 ) + 1 ) ) )
93 9 92 syl ⊢ ( 𝜑 → ( ! ‘ ( ( 𝑃 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ( 𝑃 − 1 ) + 1 ) ) )
94 89 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ( 𝑃 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · 𝑃 ) )
95 91 93 94 3eqtrrd ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · 𝑃 ) = ( ! ‘ 𝑃 ) )
96 95 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) · 𝑃 ) = ( ! ‘ 𝑃 ) )
97 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝑃 ∈ ℕ )
98 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝑀 ∈ ℕ0 )
99 3 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝑁 ∈ ℕ0 )
100 48 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
101 20 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝑁 )
102 1zzd ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 1 ∈ ℤ )
103 2 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
104 103 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝑀 ∈ ℤ )
105 83 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝐽 ∈ ℤ )
106 102 104 105 3jca ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ) )
107 82 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝐽 ∈ ℕ0 )
108 neqne ⊢ ( ¬ 𝐽 = 0 → 𝐽 ≠ 0 )
109 108 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝐽 ≠ 0 )
110 elnnne0 ⊢ ( 𝐽 ∈ ℕ ↔ ( 𝐽 ∈ ℕ0 ∧ 𝐽 ≠ 0 ) )
111 107 109 110 sylanbrc ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝐽 ∈ ℕ )
112 111 nnge1d ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 1 ≤ 𝐽 )
113 elfzle2 ⊢ ( 𝐽 ∈ ( 0 ... 𝑀 ) → 𝐽 ≤ 𝑀 )
114 6 113 syl ⊢ ( 𝜑 → 𝐽 ≤ 𝑀 )
115 114 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝐽 ≤ 𝑀 )
116 106 112 115 jca32 ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( 1 ≤ 𝐽 ∧ 𝐽 ≤ 𝑀 ) ) )
117 elfz2 ⊢ ( 𝐽 ∈ ( 1 ... 𝑀 ) ↔ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( 1 ≤ 𝐽 ∧ 𝐽 ≤ 𝑀 ) ) )
118 116 117 sylibr ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → 𝐽 ∈ ( 1 ... 𝑀 ) )
119 97 98 99 100 101 62 118 etransclem25 ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → ( ! ‘ 𝑃 ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
120 96 119 eqbrtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) · 𝑃 ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
121 muldvds1 ⊢ ( ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 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 ) ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ) )
122 86 120 121 sylc ⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 0 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
123 79 122 pm2.61dan ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) )
124 123 7 breqtrrdi ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∥ 𝑇 )