Metamath Proof Explorer


Theorem etransclem35

Description: P does not divide the P-1 -th derivative of F applied to 0 . This is case 2 of the proof in Juillerat p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem35.p ( 𝜑𝑃 ∈ ℕ )
etransclem35.m ( 𝜑𝑀 ∈ ℕ0 )
etransclem35.f 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑗 ) ↑ 𝑃 ) ) )
etransclem35.c 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } )
etransclem35.d 𝐷 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) )
Assertion etransclem35 ( 𝜑 → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 etransclem35.p ( 𝜑𝑃 ∈ ℕ )
2 etransclem35.m ( 𝜑𝑀 ∈ ℕ0 )
3 etransclem35.f 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥𝑗 ) ↑ 𝑃 ) ) )
4 etransclem35.c 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = 𝑛 } )
5 etransclem35.d 𝐷 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) )
6 reelprrecn ℝ ∈ { ℝ , ℂ }
7 6 a1i ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
8 reopn ℝ ∈ ( topGen ‘ ran (,) )
9 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
10 9 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
11 8 10 eleqtri ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
12 11 a1i ( 𝜑 → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
13 nnm1nn0 ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
14 1 13 syl ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
15 etransclem5 ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ ℝ ↦ ( ( 𝑦𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ ℝ ↦ ( ( 𝑥𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
16 0red ( 𝜑 → 0 ∈ ℝ )
17 7 12 1 2 3 14 15 4 16 etransclem31 ( 𝜑 → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) = Σ 𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) )
18 nfv 𝑐 𝜑
19 nfcv 𝑐 ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) ) )
20 4 14 etransclem16 ( 𝜑 → ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∈ Fin )
21 simpr ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → 𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) )
22 4 14 etransclem12 ( 𝜑 → ( 𝐶 ‘ ( 𝑃 − 1 ) ) = { 𝑐 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) } )
23 22 adantr ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( 𝐶 ‘ ( 𝑃 − 1 ) ) = { 𝑐 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) } )
24 21 23 eleqtrd ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) } )
25 rabid ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) } ↔ ( 𝑐 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) ) )
26 24 25 sylib ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( 𝑐 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) ) )
27 26 simprd ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) )
28 27 eqcomd ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( 𝑃 − 1 ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) )
29 28 fveq2d ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( ! ‘ ( 𝑃 − 1 ) ) = ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) ) )
30 29 oveq1d ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) = ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) )
31 nfcv 𝑗 𝑐
32 fzfid ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( 0 ... 𝑀 ) ∈ Fin )
33 nn0ex 0 ∈ V
34 fzssnn0 ( 0 ... ( 𝑃 − 1 ) ) ⊆ ℕ0
35 mapss ( ( ℕ0 ∈ V ∧ ( 0 ... ( 𝑃 − 1 ) ) ⊆ ℕ0 ) → ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0m ( 0 ... 𝑀 ) ) )
36 33 34 35 mp2an ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0m ( 0 ... 𝑀 ) )
37 26 simpld ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → 𝑐 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) )
38 36 37 sseldi ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → 𝑐 ∈ ( ℕ0m ( 0 ... 𝑀 ) ) )
39 31 32 38 mccl ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) ∈ ℕ )
40 30 39 eqeltrd ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) ∈ ℕ )
41 40 nnzd ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) ∈ ℤ )
42 1 adantr ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℕ )
43 2 adantr ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → 𝑀 ∈ ℕ0 )
44 elmapi ( 𝑐 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... ( 𝑃 − 1 ) ) )
45 37 44 syl ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... ( 𝑃 − 1 ) ) )
46 0zd ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → 0 ∈ ℤ )
47 42 43 45 46 etransclem10 ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) ∈ ℤ )
48 fzfid ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( 1 ... 𝑀 ) ∈ Fin )
49 1 ad2antrr ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
50 45 adantr ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... ( 𝑃 − 1 ) ) )
51 fz1ssfz0 ( 1 ... 𝑀 ) ⊆ ( 0 ... 𝑀 )
52 51 sseli ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
53 52 adantl ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
54 0zd ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 0 ∈ ℤ )
55 49 50 53 54 etransclem3 ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ∈ ℤ )
56 48 55 fprodzcl ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ∈ ℤ )
57 47 56 zmulcld ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ∈ ℤ )
58 41 57 zmulcld ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) ∈ ℤ )
59 58 zcnd ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) ∈ ℂ )
60 nn0uz 0 = ( ℤ ‘ 0 )
61 14 60 eleqtrdi ( 𝜑 → ( 𝑃 − 1 ) ∈ ( ℤ ‘ 0 ) )
62 eluzfz2 ( ( 𝑃 − 1 ) ∈ ( ℤ ‘ 0 ) → ( 𝑃 − 1 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
63 61 62 syl ( 𝜑 → ( 𝑃 − 1 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
64 eluzfz1 ( ( 𝑃 − 1 ) ∈ ( ℤ ‘ 0 ) → 0 ∈ ( 0 ... ( 𝑃 − 1 ) ) )
65 61 64 syl ( 𝜑 → 0 ∈ ( 0 ... ( 𝑃 − 1 ) ) )
66 63 65 ifcld ( 𝜑 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
67 66 adantr ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
68 67 5 fmptd ( 𝜑𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... ( 𝑃 − 1 ) ) )
69 ovex ( 0 ... ( 𝑃 − 1 ) ) ∈ V
70 ovex ( 0 ... 𝑀 ) ∈ V
71 69 70 elmap ( 𝐷 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ↔ 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... ( 𝑃 − 1 ) ) )
72 68 71 sylibr ( 𝜑𝐷 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) )
73 2 60 eleqtrdi ( 𝜑𝑀 ∈ ( ℤ ‘ 0 ) )
74 fzsscn ( 0 ... ( 𝑃 − 1 ) ) ⊆ ℂ
75 68 ffvelrnda ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐷𝑗 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
76 74 75 sseldi ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐷𝑗 ) ∈ ℂ )
77 fveq2 ( 𝑗 = 0 → ( 𝐷𝑗 ) = ( 𝐷 ‘ 0 ) )
78 73 76 77 fsum1p ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷𝑗 ) = ( ( 𝐷 ‘ 0 ) + Σ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝐷𝑗 ) ) )
79 5 a1i ( 𝜑𝐷 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) ) )
80 simpr ( ( 𝜑𝑗 = 0 ) → 𝑗 = 0 )
81 80 iftrued ( ( 𝜑𝑗 = 0 ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) = ( 𝑃 − 1 ) )
82 eluzfz1 ( 𝑀 ∈ ( ℤ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
83 73 82 syl ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
84 79 81 83 14 fvmptd ( 𝜑 → ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) )
85 0p1e1 ( 0 + 1 ) = 1
86 85 oveq1i ( ( 0 + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 )
87 86 sumeq1i Σ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝐷𝑗 ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐷𝑗 )
88 87 a1i ( 𝜑 → Σ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝐷𝑗 ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐷𝑗 ) )
89 5 fvmpt2 ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) ) → ( 𝐷𝑗 ) = if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) )
90 52 66 89 syl2anr ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷𝑗 ) = if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) )
91 0red ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 ∈ ℝ )
92 1red ( 𝑗 ∈ ( 1 ... 𝑀 ) → 1 ∈ ℝ )
93 elfzelz ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℤ )
94 93 zred ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℝ )
95 0lt1 0 < 1
96 95 a1i ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 < 1 )
97 elfzle1 ( 𝑗 ∈ ( 1 ... 𝑀 ) → 1 ≤ 𝑗 )
98 91 92 94 96 97 ltletrd ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 < 𝑗 )
99 91 98 gtned ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ≠ 0 )
100 99 neneqd ( 𝑗 ∈ ( 1 ... 𝑀 ) → ¬ 𝑗 = 0 )
101 100 iffalsed ( 𝑗 ∈ ( 1 ... 𝑀 ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) = 0 )
102 101 adantl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) = 0 )
103 90 102 eqtrd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷𝑗 ) = 0 )
104 103 sumeq2dv ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( 𝐷𝑗 ) = Σ 𝑗 ∈ ( 1 ... 𝑀 ) 0 )
105 fzfi ( 1 ... 𝑀 ) ∈ Fin
106 105 olci ( ( 1 ... 𝑀 ) ⊆ ( ℤ𝐴 ) ∨ ( 1 ... 𝑀 ) ∈ Fin )
107 sumz ( ( ( 1 ... 𝑀 ) ⊆ ( ℤ𝐴 ) ∨ ( 1 ... 𝑀 ) ∈ Fin ) → Σ 𝑗 ∈ ( 1 ... 𝑀 ) 0 = 0 )
108 106 107 mp1i ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) 0 = 0 )
109 88 104 108 3eqtrd ( 𝜑 → Σ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝐷𝑗 ) = 0 )
110 84 109 oveq12d ( 𝜑 → ( ( 𝐷 ‘ 0 ) + Σ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝐷𝑗 ) ) = ( ( 𝑃 − 1 ) + 0 ) )
111 1 nncnd ( 𝜑𝑃 ∈ ℂ )
112 1cnd ( 𝜑 → 1 ∈ ℂ )
113 111 112 subcld ( 𝜑 → ( 𝑃 − 1 ) ∈ ℂ )
114 113 addid1d ( 𝜑 → ( ( 𝑃 − 1 ) + 0 ) = ( 𝑃 − 1 ) )
115 78 110 114 3eqtrd ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷𝑗 ) = ( 𝑃 − 1 ) )
116 fveq1 ( 𝑐 = 𝐷 → ( 𝑐𝑗 ) = ( 𝐷𝑗 ) )
117 116 sumeq2sdv ( 𝑐 = 𝐷 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷𝑗 ) )
118 117 eqeq1d ( 𝑐 = 𝐷 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) ↔ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷𝑗 ) = ( 𝑃 − 1 ) ) )
119 118 elrab ( 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) } ↔ ( 𝐷 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷𝑗 ) = ( 𝑃 − 1 ) ) )
120 72 115 119 sylanbrc ( 𝜑𝐷 ∈ { 𝑐 ∈ ( ( 0 ... ( 𝑃 − 1 ) ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) } )
121 120 22 eleqtrrd ( 𝜑𝐷 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) )
122 116 fveq2d ( 𝑐 = 𝐷 → ( ! ‘ ( 𝑐𝑗 ) ) = ( ! ‘ ( 𝐷𝑗 ) ) )
123 122 prodeq2ad ( 𝑐 = 𝐷 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) = ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) )
124 123 oveq2d ( 𝑐 = 𝐷 → ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) )
125 fveq1 ( 𝑐 = 𝐷 → ( 𝑐 ‘ 0 ) = ( 𝐷 ‘ 0 ) )
126 125 breq2d ( 𝑐 = 𝐷 → ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) ↔ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) )
127 125 oveq2d ( 𝑐 = 𝐷 → ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) = ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) )
128 127 fveq2d ( 𝑐 = 𝐷 → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) = ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) )
129 128 oveq2d ( 𝑐 = 𝐷 → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) )
130 127 oveq2d ( 𝑐 = 𝐷 → ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) = ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) )
131 129 130 oveq12d ( 𝑐 = 𝐷 → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) )
132 126 131 ifbieq2d ( 𝑐 = 𝐷 → if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) = if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) )
133 116 breq2d ( 𝑐 = 𝐷 → ( 𝑃 < ( 𝑐𝑗 ) ↔ 𝑃 < ( 𝐷𝑗 ) ) )
134 116 oveq2d ( 𝑐 = 𝐷 → ( 𝑃 − ( 𝑐𝑗 ) ) = ( 𝑃 − ( 𝐷𝑗 ) ) )
135 134 fveq2d ( 𝑐 = 𝐷 → ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) = ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) )
136 135 oveq2d ( 𝑐 = 𝐷 → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) = ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) )
137 134 oveq2d ( 𝑐 = 𝐷 → ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) = ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) )
138 136 137 oveq12d ( 𝑐 = 𝐷 → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) )
139 133 138 ifbieq2d ( 𝑐 = 𝐷 → if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) = if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) )
140 139 prodeq2ad ( 𝑐 = 𝐷 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) )
141 132 140 oveq12d ( 𝑐 = 𝐷 → ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) = ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) ) )
142 124 141 oveq12d ( 𝑐 = 𝐷 → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) ) ) )
143 18 19 20 59 121 142 fsumsplit1 ( 𝜑 → Σ 𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) = ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) ) ) + Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) ) )
144 34 75 sseldi ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐷𝑗 ) ∈ ℕ0 )
145 144 faccld ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝐷𝑗 ) ) ∈ ℕ )
146 145 nncnd ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝐷𝑗 ) ) ∈ ℂ )
147 77 fveq2d ( 𝑗 = 0 → ( ! ‘ ( 𝐷𝑗 ) ) = ( ! ‘ ( 𝐷 ‘ 0 ) ) )
148 73 146 147 fprod1p ( 𝜑 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) = ( ( ! ‘ ( 𝐷 ‘ 0 ) ) · ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) )
149 84 fveq2d ( 𝜑 → ( ! ‘ ( 𝐷 ‘ 0 ) ) = ( ! ‘ ( 𝑃 − 1 ) ) )
150 86 prodeq1i 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) )
151 150 a1i ( 𝜑 → ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) )
152 103 fveq2d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ! ‘ ( 𝐷𝑗 ) ) = ( ! ‘ 0 ) )
153 fac0 ( ! ‘ 0 ) = 1
154 152 153 syl6eq ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ! ‘ ( 𝐷𝑗 ) ) = 1 )
155 154 prodeq2dv ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) 1 )
156 prod1 ( ( ( 1 ... 𝑀 ) ⊆ ( ℤ𝐴 ) ∨ ( 1 ... 𝑀 ) ∈ Fin ) → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) 1 = 1 )
157 106 156 mp1i ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) 1 = 1 )
158 151 155 157 3eqtrd ( 𝜑 → ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) = 1 )
159 149 158 oveq12d ( 𝜑 → ( ( ! ‘ ( 𝐷 ‘ 0 ) ) · ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · 1 ) )
160 14 faccld ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
161 160 nncnd ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
162 161 mulid1d ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · 1 ) = ( ! ‘ ( 𝑃 − 1 ) ) )
163 148 159 162 3eqtrd ( 𝜑 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) = ( ! ‘ ( 𝑃 − 1 ) ) )
164 163 oveq2d ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
165 160 nnne0d ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
166 161 165 dividd ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = 1 )
167 164 166 eqtrd ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) = 1 )
168 14 nn0red ( 𝜑 → ( 𝑃 − 1 ) ∈ ℝ )
169 84 168 eqeltrd ( 𝜑 → ( 𝐷 ‘ 0 ) ∈ ℝ )
170 169 168 lttri3d ( 𝜑 → ( ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) ↔ ( ¬ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) ) )
171 84 170 mpbid ( 𝜑 → ( ¬ ( 𝐷 ‘ 0 ) < ( 𝑃 − 1 ) ∧ ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) ) )
172 171 simprd ( 𝜑 → ¬ ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) )
173 172 iffalsed ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) )
174 84 eqcomd ( 𝜑 → ( 𝑃 − 1 ) = ( 𝐷 ‘ 0 ) )
175 113 174 subeq0bd ( 𝜑 → ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) = 0 )
176 175 fveq2d ( 𝜑 → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = ( ! ‘ 0 ) )
177 176 153 syl6eq ( 𝜑 → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = 1 )
178 177 oveq2d ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) / 1 ) )
179 161 div1d ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) / 1 ) = ( ! ‘ ( 𝑃 − 1 ) ) )
180 178 179 eqtrd ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) = ( ! ‘ ( 𝑃 − 1 ) ) )
181 175 oveq2d ( 𝜑 → ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = ( 0 ↑ 0 ) )
182 0cnd ( 𝜑 → 0 ∈ ℂ )
183 182 exp0d ( 𝜑 → ( 0 ↑ 0 ) = 1 )
184 181 183 eqtrd ( 𝜑 → ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) = 1 )
185 180 184 oveq12d ( 𝜑 → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · 1 ) )
186 173 185 162 3eqtrd ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) = ( ! ‘ ( 𝑃 − 1 ) ) )
187 fzssre ( 0 ... ( 𝑃 − 1 ) ) ⊆ ℝ
188 68 adantr ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... ( 𝑃 − 1 ) ) )
189 52 adantl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
190 188 189 ffvelrnd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷𝑗 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
191 187 190 sseldi ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷𝑗 ) ∈ ℝ )
192 1 nnred ( 𝜑𝑃 ∈ ℝ )
193 192 adantr ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℝ )
194 1 nngt0d ( 𝜑 → 0 < 𝑃 )
195 16 192 194 ltled ( 𝜑 → 0 ≤ 𝑃 )
196 195 adantr ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ 𝑃 )
197 103 196 eqbrtrd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷𝑗 ) ≤ 𝑃 )
198 191 193 197 lensymd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ¬ 𝑃 < ( 𝐷𝑗 ) )
199 198 iffalsed ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) )
200 103 oveq2d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 − ( 𝐷𝑗 ) ) = ( 𝑃 − 0 ) )
201 111 adantr ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℂ )
202 201 subid1d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 − 0 ) = 𝑃 )
203 200 202 eqtrd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 − ( 𝐷𝑗 ) ) = 𝑃 )
204 203 fveq2d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) = ( ! ‘ 𝑃 ) )
205 204 oveq2d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) = ( ( ! ‘ 𝑃 ) / ( ! ‘ 𝑃 ) ) )
206 1 nnnn0d ( 𝜑𝑃 ∈ ℕ0 )
207 206 faccld ( 𝜑 → ( ! ‘ 𝑃 ) ∈ ℕ )
208 207 nncnd ( 𝜑 → ( ! ‘ 𝑃 ) ∈ ℂ )
209 207 nnne0d ( 𝜑 → ( ! ‘ 𝑃 ) ≠ 0 )
210 208 209 dividd ( 𝜑 → ( ( ! ‘ 𝑃 ) / ( ! ‘ 𝑃 ) ) = 1 )
211 210 adantr ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ 𝑃 ) ) = 1 )
212 205 211 eqtrd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) = 1 )
213 df-neg - 𝑗 = ( 0 − 𝑗 )
214 213 eqcomi ( 0 − 𝑗 ) = - 𝑗
215 214 a1i ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 0 − 𝑗 ) = - 𝑗 )
216 215 203 oveq12d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) = ( - 𝑗𝑃 ) )
217 212 216 oveq12d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) = ( 1 · ( - 𝑗𝑃 ) ) )
218 93 znegcld ( 𝑗 ∈ ( 1 ... 𝑀 ) → - 𝑗 ∈ ℤ )
219 218 zcnd ( 𝑗 ∈ ( 1 ... 𝑀 ) → - 𝑗 ∈ ℂ )
220 219 adantl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → - 𝑗 ∈ ℂ )
221 206 adantr ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℕ0 )
222 220 221 expcld ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( - 𝑗𝑃 ) ∈ ℂ )
223 222 mulid2d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 1 · ( - 𝑗𝑃 ) ) = ( - 𝑗𝑃 ) )
224 199 217 223 3eqtrd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) = ( - 𝑗𝑃 ) )
225 224 prodeq2dv ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) )
226 186 225 oveq12d ( 𝜑 → ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ) )
227 167 226 oveq12d ( 𝜑 → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) ) ) = ( 1 · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ) ) )
228 fzfid ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
229 zexpcl ( ( - 𝑗 ∈ ℤ ∧ 𝑃 ∈ ℕ0 ) → ( - 𝑗𝑃 ) ∈ ℤ )
230 218 206 229 syl2anr ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( - 𝑗𝑃 ) ∈ ℤ )
231 228 230 fprodzcl ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ∈ ℤ )
232 231 zcnd ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ∈ ℂ )
233 161 232 mulcld ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ) ∈ ℂ )
234 233 mulid2d ( 𝜑 → ( 1 · ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ) )
235 227 234 eqtrd ( 𝜑 → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ) )
236 eldifi ( 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) → 𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) )
237 83 adantr ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → 0 ∈ ( 0 ... 𝑀 ) )
238 45 237 ffvelrnd ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( 𝑐 ‘ 0 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
239 236 238 sylan2 ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( 𝑐 ‘ 0 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
240 187 239 sseldi ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( 𝑐 ‘ 0 ) ∈ ℝ )
241 168 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( 𝑃 − 1 ) ∈ ℝ )
242 elfzle2 ( ( 𝑐 ‘ 0 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) → ( 𝑐 ‘ 0 ) ≤ ( 𝑃 − 1 ) )
243 239 242 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( 𝑐 ‘ 0 ) ≤ ( 𝑃 − 1 ) )
244 240 241 243 lensymd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ¬ ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) )
245 244 iffalsed ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) )
246 14 nn0zd ( 𝜑 → ( 𝑃 − 1 ) ∈ ℤ )
247 246 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( 𝑃 − 1 ) ∈ ℤ )
248 239 elfzelzd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( 𝑐 ‘ 0 ) ∈ ℤ )
249 247 248 zsubcld ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ∈ ℤ )
250 45 ffnd ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → 𝑐 Fn ( 0 ... 𝑀 ) )
251 250 adantr ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) → 𝑐 Fn ( 0 ... 𝑀 ) )
252 68 ffnd ( 𝜑𝐷 Fn ( 0 ... 𝑀 ) )
253 252 ad2antrr ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) → 𝐷 Fn ( 0 ... 𝑀 ) )
254 fveq2 ( 𝑗 = 0 → ( 𝑐𝑗 ) = ( 𝑐 ‘ 0 ) )
255 254 adantl ( ( ( 𝜑 ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 = 0 ) → ( 𝑐𝑗 ) = ( 𝑐 ‘ 0 ) )
256 id ( ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) → ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) )
257 256 eqcomd ( ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) → ( 𝑐 ‘ 0 ) = ( 𝑃 − 1 ) )
258 257 ad2antlr ( ( ( 𝜑 ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 = 0 ) → ( 𝑐 ‘ 0 ) = ( 𝑃 − 1 ) )
259 77 adantl ( ( 𝜑𝑗 = 0 ) → ( 𝐷𝑗 ) = ( 𝐷 ‘ 0 ) )
260 84 adantr ( ( 𝜑𝑗 = 0 ) → ( 𝐷 ‘ 0 ) = ( 𝑃 − 1 ) )
261 259 260 eqtr2d ( ( 𝜑𝑗 = 0 ) → ( 𝑃 − 1 ) = ( 𝐷𝑗 ) )
262 261 adantlr ( ( ( 𝜑 ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 = 0 ) → ( 𝑃 − 1 ) = ( 𝐷𝑗 ) )
263 255 258 262 3eqtrd ( ( ( 𝜑 ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 = 0 ) → ( 𝑐𝑗 ) = ( 𝐷𝑗 ) )
264 263 adantllr ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 = 0 ) → ( 𝑐𝑗 ) = ( 𝐷𝑗 ) )
265 264 adantlr ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 = 0 ) → ( 𝑐𝑗 ) = ( 𝐷𝑗 ) )
266 27 ad4antr ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) )
267 168 ad5antr ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( 𝑃 − 1 ) ∈ ℝ )
268 168 ad4antr ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( 𝑃 − 1 ) ∈ ℝ )
269 45 adantr ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... ( 𝑃 − 1 ) ) )
270 51 sseli ( 𝑘 ∈ ( 1 ... 𝑀 ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
271 270 adantl ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
272 269 271 ffvelrnd ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑐𝑘 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
273 34 272 sseldi ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑐𝑘 ) ∈ ℕ0 )
274 48 273 fsumnn0cl ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) ∈ ℕ0 )
275 274 nn0red ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) ∈ ℝ )
276 275 ad3antrrr ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) ∈ ℝ )
277 0red ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → 0 ∈ ℝ )
278 45 ffvelrnda ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐𝑗 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
279 187 278 sseldi ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐𝑗 ) ∈ ℝ )
280 279 ad2antrr ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( 𝑐𝑗 ) ∈ ℝ )
281 nfv 𝑘 ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 )
282 nfcv 𝑘 ( 𝑐𝑗 )
283 fzfid ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( 1 ... 𝑀 ) ∈ Fin )
284 simp-4l ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) )
285 74 272 sseldi ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑐𝑘 ) ∈ ℂ )
286 284 285 sylancom ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑐𝑘 ) ∈ ℂ )
287 1zzd ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) → 1 ∈ ℤ )
288 elfzel2 ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℤ )
289 288 adantr ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) → 𝑀 ∈ ℤ )
290 elfzelz ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
291 290 adantr ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) → 𝑗 ∈ ℤ )
292 287 289 291 3jca ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) → ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ) )
293 elfznn0 ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℕ0 )
294 293 adantr ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) → 𝑗 ∈ ℕ0 )
295 neqne ( ¬ 𝑗 = 0 → 𝑗 ≠ 0 )
296 295 adantl ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) → 𝑗 ≠ 0 )
297 elnnne0 ( 𝑗 ∈ ℕ ↔ ( 𝑗 ∈ ℕ0𝑗 ≠ 0 ) )
298 294 296 297 sylanbrc ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) → 𝑗 ∈ ℕ )
299 298 nnge1d ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) → 1 ≤ 𝑗 )
300 elfzle2 ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗𝑀 )
301 300 adantr ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) → 𝑗𝑀 )
302 292 299 301 jca32 ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) → ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ∧ ( 1 ≤ 𝑗𝑗𝑀 ) ) )
303 elfz2 ( 𝑗 ∈ ( 1 ... 𝑀 ) ↔ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ∧ ( 1 ≤ 𝑗𝑗𝑀 ) ) )
304 302 303 sylibr ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
305 304 adantr ( ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
306 305 adantlll ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
307 fveq2 ( 𝑘 = 𝑗 → ( 𝑐𝑘 ) = ( 𝑐𝑗 ) )
308 281 282 283 286 306 307 fsumsplit1 ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) = ( ( 𝑐𝑗 ) + Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) ) )
309 308 eqcomd ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( ( 𝑐𝑗 ) + Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) )
310 309 276 eqeltrd ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( ( 𝑐𝑗 ) + Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) ) ∈ ℝ )
311 elfzle1 ( ( 𝑐𝑗 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) → 0 ≤ ( 𝑐𝑗 ) )
312 278 311 syl ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 0 ≤ ( 𝑐𝑗 ) )
313 312 ad2antrr ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → 0 ≤ ( 𝑐𝑗 ) )
314 neqne ( ¬ ( 𝑐𝑗 ) = 0 → ( 𝑐𝑗 ) ≠ 0 )
315 314 adantl ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( 𝑐𝑗 ) ≠ 0 )
316 277 280 313 315 leneltd ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → 0 < ( 𝑐𝑗 ) )
317 diffi ( ( 1 ... 𝑀 ) ∈ Fin → ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∈ Fin )
318 105 317 mp1i ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∈ Fin )
319 eldifi ( 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) → 𝑘 ∈ ( 1 ... 𝑀 ) )
320 319 adantl ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ) → 𝑘 ∈ ( 1 ... 𝑀 ) )
321 51 320 sseldi ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
322 45 ffvelrnda ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐𝑘 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
323 187 322 sseldi ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐𝑘 ) ∈ ℝ )
324 321 323 syldan ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ) → ( 𝑐𝑘 ) ∈ ℝ )
325 elfzle1 ( ( 𝑐𝑘 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) → 0 ≤ ( 𝑐𝑘 ) )
326 322 325 syl ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 0 ≤ ( 𝑐𝑘 ) )
327 321 326 syldan ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ) → 0 ≤ ( 𝑐𝑘 ) )
328 318 324 327 fsumge0 ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → 0 ≤ Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) )
329 328 adantr ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 0 ≤ Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) )
330 318 324 fsumrecl ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) → Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) ∈ ℝ )
331 330 adantr ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) ∈ ℝ )
332 279 331 addge01d ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 0 ≤ Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) ↔ ( 𝑐𝑗 ) ≤ ( ( 𝑐𝑗 ) + Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) ) ) )
333 329 332 mpbid ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐𝑗 ) ≤ ( ( 𝑐𝑗 ) + Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) ) )
334 333 ad2antrr ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( 𝑐𝑗 ) ≤ ( ( 𝑐𝑗 ) + Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) ) )
335 277 280 310 316 334 ltletrd ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → 0 < ( ( 𝑐𝑗 ) + Σ 𝑘 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( 𝑐𝑘 ) ) )
336 335 309 breqtrd ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → 0 < Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) )
337 276 336 elrpd ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) ∈ ℝ+ )
338 268 337 ltaddrpd ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( 𝑃 − 1 ) < ( ( 𝑃 − 1 ) + Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) ) )
339 338 adantl3r ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( 𝑃 − 1 ) < ( ( 𝑃 − 1 ) + Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) ) )
340 fveq2 ( 𝑗 = 𝑘 → ( 𝑐𝑗 ) = ( 𝑐𝑘 ) )
341 340 cbvsumv Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑘 )
342 341 a1i ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑘 ) )
343 73 ad5antr ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → 𝑀 ∈ ( ℤ ‘ 0 ) )
344 simp-5l ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) )
345 74 322 sseldi ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐𝑘 ) ∈ ℂ )
346 344 345 sylancom ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐𝑘 ) ∈ ℂ )
347 fveq2 ( 𝑘 = 0 → ( 𝑐𝑘 ) = ( 𝑐 ‘ 0 ) )
348 343 346 347 fsum1p ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑘 ) = ( ( 𝑐 ‘ 0 ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝑐𝑘 ) ) )
349 257 ad4antlr ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( 𝑐 ‘ 0 ) = ( 𝑃 − 1 ) )
350 86 sumeq1i Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝑐𝑘 ) = Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 )
351 350 a1i ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝑐𝑘 ) = Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) )
352 349 351 oveq12d ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( ( 𝑐 ‘ 0 ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑀 ) ( 𝑐𝑘 ) ) = ( ( 𝑃 − 1 ) + Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) ) )
353 342 348 352 3eqtrrd ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( ( 𝑃 − 1 ) + Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑐𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) )
354 339 353 breqtrd ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ( 𝑃 − 1 ) < Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) )
355 267 354 gtned ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) ≠ ( 𝑃 − 1 ) )
356 355 neneqd ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) ∧ ¬ ( 𝑐𝑗 ) = 0 ) → ¬ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐𝑗 ) = ( 𝑃 − 1 ) )
357 266 356 condan ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) → ( 𝑐𝑗 ) = 0 )
358 simpr ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
359 34 67 sseldi ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) ∈ ℕ0 )
360 5 fvmpt2 ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) ∈ ℕ0 ) → ( 𝐷𝑗 ) = if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) )
361 358 359 360 syl2anc ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐷𝑗 ) = if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) )
362 361 adantr ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) → ( 𝐷𝑗 ) = if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) )
363 simpr ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) → ¬ 𝑗 = 0 )
364 363 iffalsed ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) = 0 )
365 362 364 eqtr2d ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) → 0 = ( 𝐷𝑗 ) )
366 365 adantllr ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) → 0 = ( 𝐷𝑗 ) )
367 366 adantllr ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) → 0 = ( 𝐷𝑗 ) )
368 357 367 eqtrd ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ 𝑗 = 0 ) → ( 𝑐𝑗 ) = ( 𝐷𝑗 ) )
369 265 368 pm2.61dan ( ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐𝑗 ) = ( 𝐷𝑗 ) )
370 251 253 369 eqfnfvd ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) → 𝑐 = 𝐷 )
371 236 370 sylanl2 ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) → 𝑐 = 𝐷 )
372 eldifsni ( 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) → 𝑐𝐷 )
373 372 neneqd ( 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) → ¬ 𝑐 = 𝐷 )
374 373 ad2antlr ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) ∧ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) ) → ¬ 𝑐 = 𝐷 )
375 371 374 pm2.65da ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ¬ ( 𝑃 − 1 ) = ( 𝑐 ‘ 0 ) )
376 375 neqned ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( 𝑃 − 1 ) ≠ ( 𝑐 ‘ 0 ) )
377 240 241 243 376 leneltd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( 𝑐 ‘ 0 ) < ( 𝑃 − 1 ) )
378 240 241 posdifd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ( 𝑐 ‘ 0 ) < ( 𝑃 − 1 ) ↔ 0 < ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) )
379 377 378 mpbid ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → 0 < ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) )
380 elnnz ( ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ∈ ℕ ↔ ( ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ∈ ℤ ∧ 0 < ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) )
381 249 379 380 sylanbrc ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ∈ ℕ )
382 381 0expd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) = 0 )
383 382 oveq2d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · 0 ) )
384 161 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
385 381 nnnn0d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ∈ ℕ0 )
386 385 faccld ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ∈ ℕ )
387 386 nncnd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ∈ ℂ )
388 386 nnne0d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ≠ 0 )
389 384 387 388 divcld ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ∈ ℂ )
390 389 mul01d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · 0 ) = 0 )
391 245 383 390 3eqtrd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) = 0 )
392 391 oveq1d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) = ( 0 · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) )
393 236 56 sylan2 ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ∈ ℤ )
394 393 zcnd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ∈ ℂ )
395 394 mul02d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( 0 · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) = 0 )
396 392 395 eqtrd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) = 0 )
397 396 oveq2d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · 0 ) )
398 fzfid ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( 0 ... 𝑀 ) ∈ Fin )
399 34 278 sseldi ( ( ( 𝜑𝑐 ∈ ( 𝐶 ‘ ( 𝑃 − 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐𝑗 ) ∈ ℕ0 )
400 236 399 sylanl2 ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐𝑗 ) ∈ ℕ0 )
401 400 faccld ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝑐𝑗 ) ) ∈ ℕ )
402 398 401 fprodnncl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ∈ ℕ )
403 402 nncnd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ∈ ℂ )
404 402 nnne0d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ≠ 0 )
405 384 403 404 divcld ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) ∈ ℂ )
406 405 mul01d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · 0 ) = 0 )
407 397 406 eqtrd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) = 0 )
408 407 sumeq2dv ( 𝜑 → Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) = Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) 0 )
409 diffi ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∈ Fin → ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ∈ Fin )
410 20 409 syl ( 𝜑 → ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ∈ Fin )
411 410 olcd ( 𝜑 → ( ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ⊆ ( ℤ ‘ 0 ) ∨ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ∈ Fin ) )
412 sumz ( ( ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ⊆ ( ℤ ‘ 0 ) ∨ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ∈ Fin ) → Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) 0 = 0 )
413 411 412 syl ( 𝜑 → Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) 0 = 0 )
414 408 413 eqtrd ( 𝜑 → Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) = 0 )
415 235 414 oveq12d ( 𝜑 → ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) ) ) + Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ) + 0 ) )
416 233 addid1d ( 𝜑 → ( ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ) + 0 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ) )
417 nfv 𝑗 𝜑
418 417 206 228 220 fprodexp ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) = ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗𝑃 ) )
419 418 oveq2d ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( - 𝑗𝑃 ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗𝑃 ) ) )
420 415 416 419 3eqtrd ( 𝜑 → ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷𝑗 ) ) ) ) ) ) ) + Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑃 − 1 ) ) ∖ { 𝐷 } ) ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 0 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) · ( ( 0 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐𝑗 ) ) ) ) ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗𝑃 ) ) )
421 17 143 420 3eqtrd ( 𝜑 → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗𝑃 ) ) )