Metamath Proof Explorer

Theorem etransclem25

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

Ref Expression
Hypotheses etransclem25.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem25.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
etransclem25.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
etransclem25.c ⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
etransclem25.sumc ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐶 ‘ 𝑗 ) = 𝑁 )
etransclem25.t ⊢ 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
etransclem25.j ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑀 ) )
Assertion etransclem25 ( 𝜑 → ( ! ‘ 𝑃 ) ∥ 𝑇 )

Proof

Step Hyp Ref Expression
1 etransclem25.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2 etransclem25.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3 etransclem25.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 etransclem25.c ⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
5 etransclem25.sumc ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐶 ‘ 𝑗 ) = 𝑁 )
6 etransclem25.t ⊢ 𝑇 = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
7 etransclem25.j ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑀 ) )
8 1 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
9 8 faccld ⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∈ ℕ )
10 9 nnzd ⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∈ ℤ )
11 5 eqcomd ⊢ ( 𝜑 → 𝑁 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐶 ‘ 𝑗 ) )
12 11 fveq2d ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) = ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐶 ‘ 𝑗 ) ) )
13 12 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐶 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) )
14 nfcv ⊢ Ⅎ 𝑗 𝐶
15 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
16 nn0ex ⊢ ℕ0 ∈ V
17 fzssnn0 ⊢ ( 0 ... 𝑁 ) ⊆ ℕ0
18 mapss ⊢ ( ( ℕ0 ∈ V ∧ ( 0 ... 𝑁 ) ⊆ ℕ0 ) → ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
19 16 17 18 mp2an ⊢ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0 ↑m ( 0 ... 𝑀 ) )
20 ovex ⊢ ( 0 ... 𝑁 ) ∈ V
21 ovexd ⊢ ( 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) → ( 0 ... 𝑀 ) ∈ V )
22 elmapg ⊢ ( ( ( 0 ... 𝑁 ) ∈ V ∧ ( 0 ... 𝑀 ) ∈ V ) → ( 𝐶 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ↔ 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) ) )
23 20 21 22 sylancr ⊢ ( 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) → ( 𝐶 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ↔ 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) ) )
24 23 ibir ⊢ ( 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) → 𝐶 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) )
25 19 24 sselid ⊢ ( 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) → 𝐶 ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
26 4 25 syl ⊢ ( 𝜑 → 𝐶 ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
27 14 15 26 mccl ⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐶 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℕ )
28 13 27 eqeltrd ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℕ )
29 28 nnzd ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℤ )
30 7 elfzelzd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
31 1 2 4 30 etransclem10 ⊢ ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ∈ ℤ )
32 29 31 zmulcld ⊢ ( 𝜑 → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) ∈ ℤ )
33 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
34 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
35 4 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
36 0z ⊢ 0 ∈ ℤ
37 fzp1ss ⊢ ( 0 ∈ ℤ → ( ( 0 + 1 ) ... 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
38 36 37 ax-mp ⊢ ( ( 0 + 1 ) ... 𝑀 ) ⊆ ( 0 ... 𝑀 )
39 id ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
40 1e0p1 ⊢ 1 = ( 0 + 1 )
41 40 oveq1i ⊢ ( 1 ... 𝑀 ) = ( ( 0 + 1 ) ... 𝑀 )
42 39 41 eleqtrdi ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) )
43 38 42 sselid ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
44 43 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
45 30 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐽 ∈ ℤ )
46 34 35 44 45 etransclem3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
47 33 46 fprodzcl ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
48 10 32 47 3jca ⊢ ( 𝜑 → ( ( ! ‘ 𝑃 ) ∈ ℤ ∧ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) ∈ ℤ ∧ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ ) )
49 30 zcnd ⊢ ( 𝜑 → 𝐽 ∈ ℂ )
50 49 subidd ⊢ ( 𝜑 → ( 𝐽 − 𝐽 ) = 0 )
51 50 eqcomd ⊢ ( 𝜑 → 0 = ( 𝐽 − 𝐽 ) )
52 51 oveq1d ⊢ ( 𝜑 → ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = ( ( 𝐽 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) )
53 52 oveq2d ⊢ ( 𝜑 → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( ( 𝐽 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
54 53 ifeq2d ⊢ ( 𝜑 → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( ( 𝐽 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
55 id ⊢ ( 𝐽 ∈ ( 1 ... 𝑀 ) → 𝐽 ∈ ( 1 ... 𝑀 ) )
56 55 41 eleqtrdi ⊢ ( 𝐽 ∈ ( 1 ... 𝑀 ) → 𝐽 ∈ ( ( 0 + 1 ) ... 𝑀 ) )
57 38 56 sselid ⊢ ( 𝐽 ∈ ( 1 ... 𝑀 ) → 𝐽 ∈ ( 0 ... 𝑀 ) )
58 7 57 syl ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑀 ) )
59 1 4 58 30 etransclem3 ⊢ ( 𝜑 → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( ( 𝐽 − 𝐽 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) ∈ ℤ )
60 54 59 eqeltrd ⊢ ( 𝜑 → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) ∈ ℤ )
61 fzfi ⊢ ( 1 ... 𝑀 ) ∈ Fin
62 diffi ⊢ ( ( 1 ... 𝑀 ) ∈ Fin → ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ∈ Fin )
63 61 62 mp1i ⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ∈ Fin )
64 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ) → 𝑃 ∈ ℕ )
65 4 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ) → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
66 eldifi ⊢ ( 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
67 66 43 syl ⊢ ( 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
68 67 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
69 30 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ) → 𝐽 ∈ ℤ )
70 64 65 68 69 etransclem3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
71 63 70 fprodzcl ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
72 dvds0 ⊢ ( ( ! ‘ 𝑃 ) ∈ ℤ → ( ! ‘ 𝑃 ) ∥ 0 )
73 10 72 syl ⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ 0 )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ 0 )
75 iftrue ⊢ ( 𝑃 < ( 𝐶 ‘ 𝐽 ) → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) = 0 )
76 75 eqcomd ⊢ ( 𝑃 < ( 𝐶 ‘ 𝐽 ) → 0 = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
77 76 adantl ⊢ ( ( 𝜑 ∧ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → 0 = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
78 74 77 breqtrd ⊢ ( ( 𝜑 ∧ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
79 iddvds ⊢ ( ( ! ‘ 𝑃 ) ∈ ℤ → ( ! ‘ 𝑃 ) ∥ ( ! ‘ 𝑃 ) )
80 10 79 syl ⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ ( ! ‘ 𝑃 ) )
81 80 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ ( ! ‘ 𝑃 ) )
82 iffalse ⊢ ( ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
83 82 ad2antlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
84 oveq1 ⊢ ( 𝑃 = ( 𝐶 ‘ 𝐽 ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) = ( ( 𝐶 ‘ 𝐽 ) − ( 𝐶 ‘ 𝐽 ) ) )
85 84 adantl ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) = ( ( 𝐶 ‘ 𝐽 ) − ( 𝐶 ‘ 𝐽 ) ) )
86 4 58 ffvelrnd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ ( 0 ... 𝑁 ) )
87 86 elfzelzd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ ℤ )
88 87 zcnd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ ℂ )
89 88 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ∈ ℂ )
90 89 subidd ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( 𝐶 ‘ 𝐽 ) − ( 𝐶 ‘ 𝐽 ) ) = 0 )
91 85 90 eqtrd ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) = 0 )
92 91 fveq2d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = ( ! ‘ 0 ) )
93 fac0 ⊢ ( ! ‘ 0 ) = 1
94 92 93 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = 1 )
95 94 oveq2d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ( ! ‘ 𝑃 ) / 1 ) )
96 9 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∈ ℂ )
97 96 div1d ⊢ ( 𝜑 → ( ( ! ‘ 𝑃 ) / 1 ) = ( ! ‘ 𝑃 ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ! ‘ 𝑃 ) / 1 ) = ( ! ‘ 𝑃 ) )
99 95 98 eqtrd ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ! ‘ 𝑃 ) )
100 91 oveq2d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = ( 0 ↑ 0 ) )
101 0cnd ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → 0 ∈ ℂ )
102 101 exp0d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 0 ↑ 0 ) = 1 )
103 100 102 eqtrd ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = 1 )
104 99 103 oveq12d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ( ! ‘ 𝑃 ) · 1 ) )
105 96 mulid1d ⊢ ( 𝜑 → ( ( ! ‘ 𝑃 ) · 1 ) = ( ! ‘ 𝑃 ) )
106 105 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ! ‘ 𝑃 ) · 1 ) = ( ! ‘ 𝑃 ) )
107 104 106 eqtrd ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ! ‘ 𝑃 ) )
108 107 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ! ‘ 𝑃 ) )
109 83 108 eqtr2d ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
110 81 109 breqtrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
111 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ 0 )
112 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) )
113 112 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) )
114 113 iffalsed ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
115 simpll ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → 𝜑 )
116 87 zred ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ ℝ )
117 116 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ∈ ℝ )
118 1 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
119 118 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → 𝑃 ∈ ℝ )
120 116 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ∈ ℝ )
121 118 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → 𝑃 ∈ ℝ )
122 120 121 112 nltled ⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ≤ 𝑃 )
123 122 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) ≤ 𝑃 )
124 neqne ⊢ ( ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) → 𝑃 ≠ ( 𝐶 ‘ 𝐽 ) )
125 124 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → 𝑃 ≠ ( 𝐶 ‘ 𝐽 ) )
126 117 119 123 125 leneltd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) < 𝑃 )
127 1 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
128 127 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → 𝑃 ∈ ℤ )
129 87 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝐶 ‘ 𝐽 ) ∈ ℤ )
130 128 129 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℤ )
131 simpr ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝐶 ‘ 𝐽 ) < 𝑃 )
132 116 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝐶 ‘ 𝐽 ) ∈ ℝ )
133 118 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → 𝑃 ∈ ℝ )
134 132 133 posdifd ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ( 𝐶 ‘ 𝐽 ) < 𝑃 ↔ 0 < ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) )
135 131 134 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → 0 < ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) )
136 elnnz ⊢ ( ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℕ ↔ ( ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℤ ∧ 0 < ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) )
137 130 135 136 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℕ )
138 137 0expd ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) = 0 )
139 138 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · 0 ) )
140 96 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ! ‘ 𝑃 ) ∈ ℂ )
141 137 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ∈ ℕ0 )
142 141 faccld ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ∈ ℕ )
143 142 nncnd ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ∈ ℂ )
144 142 nnne0d ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ≠ 0 )
145 140 143 144 divcld ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ∈ ℂ )
146 145 mul01d ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · 0 ) = 0 )
147 139 146 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐶 ‘ 𝐽 ) < 𝑃 ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = 0 )
148 115 126 147 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) = 0 )
149 114 148 eqtr2d ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → 0 = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
150 111 149 breqtrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) ∧ ¬ 𝑃 = ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
151 110 150 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) → ( ! ‘ 𝑃 ) ∥ if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
152 78 151 pm2.61dan ⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
153 10 60 71 152 dvdsmultr1d ⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ ( if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) · ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
154 46 zcnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℂ )
155 fveq2 ⊢ ( 𝑗 = 𝐽 → ( 𝐶 ‘ 𝑗 ) = ( 𝐶 ‘ 𝐽 ) )
156 155 breq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑃 < ( 𝐶 ‘ 𝑗 ) ↔ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) )
157 156 adantl ⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( 𝑃 < ( 𝐶 ‘ 𝑗 ) ↔ 𝑃 < ( 𝐶 ‘ 𝐽 ) ) )
158 155 oveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) = ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) )
159 158 fveq2d ⊢ ( 𝑗 = 𝐽 → ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) = ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) )
160 159 oveq2d ⊢ ( 𝑗 = 𝐽 → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) = ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
161 160 adantl ⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) = ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
162 oveq2 ⊢ ( 𝑗 = 𝐽 → ( 𝐽 − 𝑗 ) = ( 𝐽 − 𝐽 ) )
163 162 50 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( 𝐽 − 𝑗 ) = 0 )
164 158 adantl ⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) = ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) )
165 163 164 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) = ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) )
166 161 165 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) )
167 157 166 ifbieq2d ⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) = if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) )
168 33 154 7 167 fprodsplit1 ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) = ( if ( 𝑃 < ( 𝐶 ‘ 𝐽 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) · ( 0 ↑ ( 𝑃 − ( 𝐶 ‘ 𝐽 ) ) ) ) ) · ∏ 𝑗 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝐽 } ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
169 153 168 breqtrrd ⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) )
170 dvdsmultr2 ⊢ ( ( ( ! ‘ 𝑃 ) ∈ ℤ ∧ ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) ∈ ℤ ∧ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℤ ) → ( ( ! ‘ 𝑃 ) ∥ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) → ( ! ‘ 𝑃 ) ∥ ( ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) ) )
171 48 169 170 sylc ⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ ( ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) )
172 3 faccld ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℕ )
173 172 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℂ )
174 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ( 0 ... 𝑁 ) )
175 17 174 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℕ0 )
176 175 faccld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ∈ ℕ )
177 176 nncnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
178 15 177 fprodcl ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
179 176 nnne0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ≠ 0 )
180 15 177 179 fprodn0 ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ≠ 0 )
181 173 178 180 divcld ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) ∈ ℂ )
182 31 zcnd ⊢ ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ∈ ℂ )
183 33 154 fprodcl ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ∈ ℂ )
184 181 182 183 mulassd ⊢ ( 𝜑 → ( ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 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 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) ) )
185 184 6 eqtr4di ⊢ ( 𝜑 → ( ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐶 ‘ 𝑗 ) ) ) · if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐶 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐶 ‘ 𝑗 ) ) ) ) ) ) = 𝑇 )
186 171 185 breqtrd ⊢ ( 𝜑 → ( ! ‘ 𝑃 ) ∥ 𝑇 )