etransclem35 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > etransclem35		Structured version Visualization version GIF version

Theorem etransclem35 46289

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

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

**Assertion**
Ref	Expression
etransclem35	⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑃 − 1))‘0) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)))

Distinct variable groups: 𝐶,𝑐,𝑗,𝑥 𝐷,𝑐,𝑗 𝑀,𝑐,𝑗,𝑛,𝑥 𝑃,𝑐,𝑗,𝑛,𝑥 𝜑,𝑐,𝑗,𝑛,𝑥 Allowed substitution hints: 𝐶(𝑛) 𝐷(𝑥,𝑛) 𝐹(𝑥,𝑗,𝑛,𝑐)

Proof of Theorem etransclem35 Dummy variables 𝐴 𝑘 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reelprrecn 11248	. . . 4 ⊢ ℝ ∈ {ℝ, ℂ}
2	1	a1i 11	. . 3 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
3		reopn 45306	. . . . 5 ⊢ ℝ ∈ (topGen‘ran (,))
4		tgioo4 24827	. . . . 5 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
5	3, 4	eleqtri 2838	. . . 4 ⊢ ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
6	5	a1i 11	. . 3 ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
7		etransclem35.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ ℕ)
8		etransclem35.m	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
9		etransclem35.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
10		nnm1nn0 12569	. . . 4 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
11	7, 10	syl 17	. . 3 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
12		etransclem5 46259	. . 3 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
13		etransclem35.c	. . 3 ⊢ 𝐶 = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})
14		0red 11265	. . 3 ⊢ (𝜑 → 0 ∈ ℝ)
15	2, 6, 7, 8, 9, 11, 12, 13, 14	etransclem31 46285	. 2 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑃 − 1))‘0) = Σ𝑐 ∈ (𝐶‘(𝑃 − 1))(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))))
16		nfv 1913	. . 3 ⊢ Ⅎ𝑐𝜑
17		nfcv 2904	. . 3 ⊢ Ⅎ𝑐(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))))
18	13, 11	etransclem16 46270	. . 3 ⊢ (𝜑 → (𝐶‘(𝑃 − 1)) ∈ Fin)
19		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ (𝐶‘(𝑃 − 1)))
20	13, 11	etransclem12 46266	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶‘(𝑃 − 1)) = {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
21	20	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝐶‘(𝑃 − 1)) = {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
22	19, 21	eleqtrd 2842	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
23		rabid 3457	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)} ↔ (𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)))
24	22, 23	sylib 218	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)))
25	24	simprd 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
26	25	eqcomd 2742	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑃 − 1) = Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
27	26	fveq2d 6909	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (!‘(𝑃 − 1)) = (!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)))
28	27	oveq1d 7447	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) = ((!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))))
29		nfcv 2904	. . . . . . . 8 ⊢ Ⅎ𝑗𝑐
30		fzfid 14015	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (0...𝑀) ∈ Fin)
31		nn0ex 12534	. . . . . . . . . 10 ⊢ ℕ₀ ∈ V
32		fzssnn0 45334	. . . . . . . . . 10 ⊢ (0...(𝑃 − 1)) ⊆ ℕ₀
33		mapss 8930	. . . . . . . . . 10 ⊢ ((ℕ₀ ∈ V ∧ (0...(𝑃 − 1)) ⊆ ℕ₀) → ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ⊆ (ℕ₀ ↑_m (0...𝑀)))
34	31, 32, 33	mp2an 692	. . . . . . . . 9 ⊢ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ⊆ (ℕ₀ ↑_m (0...𝑀))
35	24	simpld 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)))
36	34, 35	sselid 3980	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ (ℕ₀ ↑_m (0...𝑀)))
37	29, 30, 36	mccl 45618	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℕ)
38	28, 37	eqeltrd 2840	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℕ)
39	38	nnzd 12642	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℤ)
40	7	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑃 ∈ ℕ)
41	8	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑀 ∈ ℕ₀)
42		elmapi 8890	. . . . . . . 8 ⊢ (𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
43	35, 42	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
44		0zd 12627	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ∈ ℤ)
45	40, 41, 43, 44	etransclem10 46264	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) ∈ ℤ)
46		fzfid 14015	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (1...𝑀) ∈ Fin)
47	7	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ)
48	43	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
49		fz1ssfz0 13664	. . . . . . . . . 10 ⊢ (1...𝑀) ⊆ (0...𝑀)
50	49	sseli 3978	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (0...𝑀))
51	50	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀))
52		0zd 12627	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 0 ∈ ℤ)
53	47, 48, 51, 52	etransclem3 46257	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℤ)
54	46, 53	fprodzcl 15991	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℤ)
55	45, 54	zmulcld 12730	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) ∈ ℤ)
56	39, 55	zmulcld 12730	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ∈ ℤ)
57	56	zcnd 12725	. . 3 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ∈ ℂ)
58		nn0uz 12921	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
59	11, 58	eleqtrdi 2850	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃 − 1) ∈ (ℤ_≥‘0))
60		eluzfz2 13573	. . . . . . . . . 10 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘0) → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
61	59, 60	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
62		eluzfz1 13572	. . . . . . . . . 10 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘0) → 0 ∈ (0...(𝑃 − 1)))
63	59, 62	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...(𝑃 − 1)))
64	61, 63	ifcld 4571	. . . . . . . 8 ⊢ (𝜑 → if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1)))
65	64	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1)))
66		etransclem35.d	. . . . . . 7 ⊢ 𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0))
67	65, 66	fmptd 7133	. . . . . 6 ⊢ (𝜑 → 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
68		ovex 7465	. . . . . . 7 ⊢ (0...(𝑃 − 1)) ∈ V
69		ovex 7465	. . . . . . 7 ⊢ (0...𝑀) ∈ V
70	68, 69	elmap 8912	. . . . . 6 ⊢ (𝐷 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ↔ 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
71	67, 70	sylibr 234	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)))
72	8, 58	eleqtrdi 2850	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
73		fzsscn 45328	. . . . . . . 8 ⊢ (0...(𝑃 − 1)) ⊆ ℂ
74	67	ffvelcdmda 7103	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ (0...(𝑃 − 1)))
75	73, 74	sselid 3980	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ ℂ)
76		fveq2 6905	. . . . . . 7 ⊢ (𝑗 = 0 → (𝐷‘𝑗) = (𝐷‘0))
77	72, 75, 76	fsum1p 15790	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = ((𝐷‘0) + Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗)))
78	66	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0)))
79		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 = 0) → 𝑗 = 0)
80	79	iftrued 4532	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 = 0) → if(𝑗 = 0, (𝑃 − 1), 0) = (𝑃 − 1))
81		eluzfz1 13572	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
82	72, 81	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
83	78, 80, 82, 11	fvmptd 7022	. . . . . . 7 ⊢ (𝜑 → (𝐷‘0) = (𝑃 − 1))
84		0p1e1 12389	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
85	84	oveq1i 7442	. . . . . . . . . 10 ⊢ ((0 + 1)...𝑀) = (1...𝑀)
86	85	sumeq1i 15734	. . . . . . . . 9 ⊢ Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗)
87	86	a1i 11	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗))
88	66	fvmpt2 7026	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ (0...𝑀) ∧ if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1))) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
89	50, 64, 88	syl2anr 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
90		0red 11265	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 0 ∈ ℝ)
91		1red 11263	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 1 ∈ ℝ)
92		elfzelz 13565	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℤ)
93	92	zred 12724	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℝ)
94		0lt1 11786	. . . . . . . . . . . . . . . 16 ⊢ 0 < 1
95	94	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 0 < 1)
96		elfzle1 13568	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 1 ≤ 𝑗)
97	90, 91, 93, 95, 96	ltletrd 11422	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 0 < 𝑗)
98	90, 97	gtned 11397	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ≠ 0)
99	98	neneqd 2944	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑀) → ¬ 𝑗 = 0)
100	99	iffalsed 4535	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑀) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
101	100	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
102	89, 101	eqtrd 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) = 0)
103	102	sumeq2dv 15739	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)0)
104		fzfi 14014	. . . . . . . . . 10 ⊢ (1...𝑀) ∈ Fin
105	104	olci 866	. . . . . . . . 9 ⊢ ((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin)
106		sumz 15759	. . . . . . . . 9 ⊢ (((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin) → Σ𝑗 ∈ (1...𝑀)0 = 0)
107	105, 106	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)0 = 0)
108	87, 103, 107	3eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = 0)
109	83, 108	oveq12d 7450	. . . . . 6 ⊢ (𝜑 → ((𝐷‘0) + Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗)) = ((𝑃 − 1) + 0))
110	7	nncnd 12283	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℂ)
111		1cnd 11257	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
112	110, 111	subcld 11621	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 1) ∈ ℂ)
113	112	addridd 11462	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 1) + 0) = (𝑃 − 1))
114	77, 109, 113	3eqtrd 2780	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = (𝑃 − 1))
115		fveq1 6904	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → (𝑐‘𝑗) = (𝐷‘𝑗))
116	115	sumeq2sdv 15740	. . . . . . 7 ⊢ (𝑐 = 𝐷 → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗))
117	116	eqeq1d 2738	. . . . . 6 ⊢ (𝑐 = 𝐷 → (Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1) ↔ Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = (𝑃 − 1)))
118	117	elrab 3691	. . . . 5 ⊢ (𝐷 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)} ↔ (𝐷 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = (𝑃 − 1)))
119	71, 114, 118	sylanbrc 583	. . . 4 ⊢ (𝜑 → 𝐷 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
120	119, 20	eleqtrrd 2843	. . 3 ⊢ (𝜑 → 𝐷 ∈ (𝐶‘(𝑃 − 1)))
121	115	fveq2d 6909	. . . . . 6 ⊢ (𝑐 = 𝐷 → (!‘(𝑐‘𝑗)) = (!‘(𝐷‘𝑗)))
122	121	prodeq2ad 45612	. . . . 5 ⊢ (𝑐 = 𝐷 → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) = ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)))
123	122	oveq2d 7448	. . . 4 ⊢ (𝑐 = 𝐷 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) = ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))))
124		fveq1 6904	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (𝑐‘0) = (𝐷‘0))
125	124	breq2d 5154	. . . . . 6 ⊢ (𝑐 = 𝐷 → ((𝑃 − 1) < (𝑐‘0) ↔ (𝑃 − 1) < (𝐷‘0)))
126	124	oveq2d 7448	. . . . . . . . 9 ⊢ (𝑐 = 𝐷 → ((𝑃 − 1) − (𝑐‘0)) = ((𝑃 − 1) − (𝐷‘0)))
127	126	fveq2d 6909	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → (!‘((𝑃 − 1) − (𝑐‘0))) = (!‘((𝑃 − 1) − (𝐷‘0))))
128	127	oveq2d 7448	. . . . . . 7 ⊢ (𝑐 = 𝐷 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) = ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))))
129	126	oveq2d 7448	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (0↑((𝑃 − 1) − (𝑐‘0))) = (0↑((𝑃 − 1) − (𝐷‘0))))
130	128, 129	oveq12d 7450	. . . . . 6 ⊢ (𝑐 = 𝐷 → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))))
131	125, 130	ifbieq2d 4551	. . . . 5 ⊢ (𝑐 = 𝐷 → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))))
132	115	breq2d 5154	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (𝑃 < (𝑐‘𝑗) ↔ 𝑃 < (𝐷‘𝑗)))
133	115	oveq2d 7448	. . . . . . . . . 10 ⊢ (𝑐 = 𝐷 → (𝑃 − (𝑐‘𝑗)) = (𝑃 − (𝐷‘𝑗)))
134	133	fveq2d 6909	. . . . . . . . 9 ⊢ (𝑐 = 𝐷 → (!‘(𝑃 − (𝑐‘𝑗))) = (!‘(𝑃 − (𝐷‘𝑗))))
135	134	oveq2d 7448	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → ((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) = ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))))
136	133	oveq2d 7448	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))) = ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))
137	135, 136	oveq12d 7450	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))) = (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))
138	132, 137	ifbieq2d 4551	. . . . . 6 ⊢ (𝑐 = 𝐷 → if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) = if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))
139	138	prodeq2ad 45612	. . . . 5 ⊢ (𝑐 = 𝐷 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) = ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))
140	131, 139	oveq12d 7450	. . . 4 ⊢ (𝑐 = 𝐷 → (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 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))))
141	123, 140	oveq12d 7450	. . 3 ⊢ (𝑐 = 𝐷 → (((!‘(𝑃 − 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 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))))
142	16, 17, 18, 57, 120, 141	fsumsplit1 15782	. 2 ⊢ (𝜑 → Σ𝑐 ∈ (𝐶‘(𝑃 − 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 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))))
143	32, 74	sselid 3980	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ ℕ₀)
144	143	faccld 14324	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐷‘𝑗)) ∈ ℕ)
145	144	nncnd 12283	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐷‘𝑗)) ∈ ℂ)
146	76	fveq2d 6909	. . . . . . . . . 10 ⊢ (𝑗 = 0 → (!‘(𝐷‘𝑗)) = (!‘(𝐷‘0)))
147	72, 145, 146	fprod1p 16005	. . . . . . . . 9 ⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)) = ((!‘(𝐷‘0)) · ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗))))
148	83	fveq2d 6909	. . . . . . . . . 10 ⊢ (𝜑 → (!‘(𝐷‘0)) = (!‘(𝑃 − 1)))
149	85	prodeq1i 15953	. . . . . . . . . . . 12 ⊢ ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗))
150	149	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗)))
151	102	fveq2d 6909	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝐷‘𝑗)) = (!‘0))
152		fac0 14316	. . . . . . . . . . . . 13 ⊢ (!‘0) = 1
153	151, 152	eqtrdi 2792	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝐷‘𝑗)) = 1)
154	153	prodeq2dv 15959	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)1)
155		prod1 15981	. . . . . . . . . . . 12 ⊢ (((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin) → ∏𝑗 ∈ (1...𝑀)1 = 1)
156	105, 155	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)1 = 1)
157	150, 154, 156	3eqtrd 2780	. . . . . . . . . 10 ⊢ (𝜑 → ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = 1)
158	148, 157	oveq12d 7450	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝐷‘0)) · ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗))) = ((!‘(𝑃 − 1)) · 1))
159	11	faccld 14324	. . . . . . . . . . 11 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
160	159	nncnd 12283	. . . . . . . . . 10 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
161	160	mulridd 11279	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · 1) = (!‘(𝑃 − 1)))
162	147, 158, 161	3eqtrd 2780	. . . . . . . 8 ⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)) = (!‘(𝑃 − 1)))
163	162	oveq2d 7448	. . . . . . 7 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) = ((!‘(𝑃 − 1)) / (!‘(𝑃 − 1))))
164	159	nnne0d 12317	. . . . . . . 8 ⊢ (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
165	160, 164	dividd 12042	. . . . . . 7 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘(𝑃 − 1))) = 1)
166	163, 165	eqtrd 2776	. . . . . 6 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) = 1)
167	11	nn0red 12590	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 − 1) ∈ ℝ)
168	83, 167	eqeltrd 2840	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘0) ∈ ℝ)
169	168, 167	lttri3d 11402	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘0) = (𝑃 − 1) ↔ (¬ (𝐷‘0) < (𝑃 − 1) ∧ ¬ (𝑃 − 1) < (𝐷‘0))))
170	83, 169	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (¬ (𝐷‘0) < (𝑃 − 1) ∧ ¬ (𝑃 − 1) < (𝐷‘0)))
171	170	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → ¬ (𝑃 − 1) < (𝐷‘0))
172	171	iffalsed 4535	. . . . . . . 8 ⊢ (𝜑 → if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))))
173	83	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 − 1) = (𝐷‘0))
174	112, 173	subeq0bd 11690	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑃 − 1) − (𝐷‘0)) = 0)
175	174	fveq2d 6909	. . . . . . . . . . . 12 ⊢ (𝜑 → (!‘((𝑃 − 1) − (𝐷‘0))) = (!‘0))
176	175, 152	eqtrdi 2792	. . . . . . . . . . 11 ⊢ (𝜑 → (!‘((𝑃 − 1) − (𝐷‘0))) = 1)
177	176	oveq2d 7448	. . . . . . . . . 10 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) = ((!‘(𝑃 − 1)) / 1))
178	160	div1d 12036	. . . . . . . . . 10 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / 1) = (!‘(𝑃 − 1)))
179	177, 178	eqtrd 2776	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) = (!‘(𝑃 − 1)))
180	174	oveq2d 7448	. . . . . . . . . 10 ⊢ (𝜑 → (0↑((𝑃 − 1) − (𝐷‘0))) = (0↑0))
181		0cnd 11255	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℂ)
182	181	exp0d 14181	. . . . . . . . . 10 ⊢ (𝜑 → (0↑0) = 1)
183	180, 182	eqtrd 2776	. . . . . . . . 9 ⊢ (𝜑 → (0↑((𝑃 − 1) − (𝐷‘0))) = 1)
184	179, 183	oveq12d 7450	. . . . . . . 8 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))) = ((!‘(𝑃 − 1)) · 1))
185	172, 184, 161	3eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) = (!‘(𝑃 − 1)))
186		fzssre 45331	. . . . . . . . . . . 12 ⊢ (0...(𝑃 − 1)) ⊆ ℝ
187	67	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
188	50	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀))
189	187, 188	ffvelcdmd 7104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ∈ (0...(𝑃 − 1)))
190	186, 189	sselid 3980	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ∈ ℝ)
191	7	nnred 12282	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℝ)
192	191	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℝ)
193	7	nngt0d 12316	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 𝑃)
194	14, 191, 193	ltled 11410	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ 𝑃)
195	194	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 0 ≤ 𝑃)
196	102, 195	eqbrtrd 5164	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ≤ 𝑃)
197	190, 192, 196	lensymd 11413	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ¬ 𝑃 < (𝐷‘𝑗))
198	197	iffalsed 4535	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))
199	102	oveq2d 7448	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐷‘𝑗)) = (𝑃 − 0))
200	110	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℂ)
201	200	subid1d 11610	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − 0) = 𝑃)
202	199, 201	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐷‘𝑗)) = 𝑃)
203	202	fveq2d 6909	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝑃 − (𝐷‘𝑗))) = (!‘𝑃))
204	203	oveq2d 7448	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) = ((!‘𝑃) / (!‘𝑃)))
205	7	nnnn0d 12589	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
206	205	faccld 14324	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (!‘𝑃) ∈ ℕ)
207	206	nncnd 12283	. . . . . . . . . . . . 13 ⊢ (𝜑 → (!‘𝑃) ∈ ℂ)
208	206	nnne0d 12317	. . . . . . . . . . . . 13 ⊢ (𝜑 → (!‘𝑃) ≠ 0)
209	207, 208	dividd 12042	. . . . . . . . . . . 12 ⊢ (𝜑 → ((!‘𝑃) / (!‘𝑃)) = 1)
210	209	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘𝑃)) = 1)
211	204, 210	eqtrd 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) = 1)
212		df-neg 11496	. . . . . . . . . . . . 13 ⊢ -𝑗 = (0 − 𝑗)
213	212	eqcomi 2745	. . . . . . . . . . . 12 ⊢ (0 − 𝑗) = -𝑗
214	213	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (0 − 𝑗) = -𝑗)
215	214, 202	oveq12d 7450	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))) = (-𝑗↑𝑃))
216	211, 215	oveq12d 7450	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))) = (1 · (-𝑗↑𝑃)))
217	92	znegcld 12726	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℤ)
218	217	zcnd 12725	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℂ)
219	218	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → -𝑗 ∈ ℂ)
220	205	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ₀)
221	219, 220	expcld 14187	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (-𝑗↑𝑃) ∈ ℂ)
222	221	mullidd 11280	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1 · (-𝑗↑𝑃)) = (-𝑗↑𝑃))
223	198, 216, 222	3eqtrd 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = (-𝑗↑𝑃))
224	223	prodeq2dv 15959	. . . . . . 7 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))
225	185, 224	oveq12d 7450	. . . . . 6 ⊢ (𝜑 → (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
226	166, 225	oveq12d 7450	. . . . 5 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) = (1 · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))))
227		fzfid 14015	. . . . . . . . 9 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
228		zexpcl 14118	. . . . . . . . . 10 ⊢ ((-𝑗 ∈ ℤ ∧ 𝑃 ∈ ℕ₀) → (-𝑗↑𝑃) ∈ ℤ)
229	217, 205, 228	syl2anr 597	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (-𝑗↑𝑃) ∈ ℤ)
230	227, 229	fprodzcl 15991	. . . . . . . 8 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) ∈ ℤ)
231	230	zcnd 12725	. . . . . . 7 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) ∈ ℂ)
232	160, 231	mulcld 11282	. . . . . 6 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) ∈ ℂ)
233	232	mullidd 11280	. . . . 5 ⊢ (𝜑 → (1 · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
234	226, 233	eqtrd 2776	. . . 4 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
235		eldifi 4130	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → 𝑐 ∈ (𝐶‘(𝑃 − 1)))
236	82	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ∈ (0...𝑀))
237	43, 236	ffvelcdmd 7104	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑐‘0) ∈ (0...(𝑃 − 1)))
238	235, 237	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ (0...(𝑃 − 1)))
239	186, 238	sselid 3980	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ ℝ)
240	167	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ∈ ℝ)
241		elfzle2 13569	. . . . . . . . . . . . . 14 ⊢ ((𝑐‘0) ∈ (0...(𝑃 − 1)) → (𝑐‘0) ≤ (𝑃 − 1))
242	238, 241	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ≤ (𝑃 − 1))
243	239, 240, 242	lensymd 11413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ¬ (𝑃 − 1) < (𝑐‘0))
244	243	iffalsed 4535	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))))
245	11	nn0zd 12641	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − 1) ∈ ℤ)
246	245	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ∈ ℤ)
247	238	elfzelzd 13566	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ ℤ)
248	246, 247	zsubcld 12729	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℤ)
249	43	ffnd 6736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 Fn (0...𝑀))
250	249	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 Fn (0...𝑀))
251	67	ffnd 6736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 Fn (0...𝑀))
252	251	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝐷 Fn (0...𝑀))
253		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 0 → (𝑐‘𝑗) = (𝑐‘0))
254	253	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝑐‘0))
255		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 − 1) = (𝑐‘0) → (𝑃 − 1) = (𝑐‘0))
256	255	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑃 − 1) = (𝑐‘0) → (𝑐‘0) = (𝑃 − 1))
257	256	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘0) = (𝑃 − 1))
258	76	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝐷‘𝑗) = (𝐷‘0))
259	83	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝐷‘0) = (𝑃 − 1))
260	258, 259	eqtr2d 2777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝑃 − 1) = (𝐷‘𝑗))
261	260	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑃 − 1) = (𝐷‘𝑗))
262	254, 257, 261	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
263	262	adantllr 719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
264	263	adantlr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
265	25	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
266	167	ad5antr 734	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) ∈ ℝ)
267	167	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) ∈ ℝ)
268	43	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
269	49	sseli 3978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ (0...𝑀))
270	269	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (0...𝑀))
271	268, 270	ffvelcdmd 7104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ (0...(𝑃 − 1)))
272	32, 271	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℕ₀)
273	46, 272	fsumnn0cl 15773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℕ₀)
274	273	nn0red 12590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ)
275	274	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ)
276		0red 11265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 ∈ ℝ)
277	43	ffvelcdmda 7103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ (0...(𝑃 − 1)))
278	186, 277	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℝ)
279	278	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ∈ ℝ)
280		nfv 1913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0)
281		nfcv 2904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘(𝑐‘𝑗)
282		fzfid 14015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (1...𝑀) ∈ Fin)
283		simp-4l 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (1...𝑀)) → (𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))))
284	73, 271	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
285	283, 284	sylancom 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
286		1zzd 12650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 1 ∈ ℤ)
287		elfzel2 13563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
288	287	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑀 ∈ ℤ)
289		elfzelz 13565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
290	289	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℤ)
291		elfznn0 13661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
292	291	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℕ₀)
293		neqne 2947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (¬ 𝑗 = 0 → 𝑗 ≠ 0)
294	293	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ≠ 0)
295		elnnne0 12542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑗 ∈ ℕ ↔ (𝑗 ∈ ℕ₀ ∧ 𝑗 ≠ 0))
296	292, 294, 295	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℕ)
297	296	nnge1d 12315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 1 ≤ 𝑗)
298		elfzle2 13569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
299	298	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ≤ 𝑀)
300	286, 288, 290, 297, 299	elfzd 13556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ (1...𝑀))
301	300	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑗 ∈ (1...𝑀))
302	301	adantlll 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑗 ∈ (1...𝑀))
303		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 = 𝑗 → (𝑐‘𝑘) = (𝑐‘𝑗))
304	280, 281, 282, 285, 302, 303	fsumsplit1 15782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) = ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
305	304	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
306	305, 275	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)) ∈ ℝ)
307		elfzle1 13568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑐‘𝑗) ∈ (0...(𝑃 − 1)) → 0 ≤ (𝑐‘𝑗))
308	277, 307	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ (𝑐‘𝑗))
309	308	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 ≤ (𝑐‘𝑗))
310		neqne 2947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ (𝑐‘𝑗) = 0 → (𝑐‘𝑗) ≠ 0)
311	310	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ≠ 0)
312	276, 279, 309, 311	leneltd 11416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < (𝑐‘𝑗))
313		diffi 9216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((1...𝑀) ∈ Fin → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
314	104, 313	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
315		eldifi 4130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑘 ∈ ((1...𝑀) ∖ {𝑗}) → 𝑘 ∈ (1...𝑀))
316	315	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑘 ∈ (1...𝑀))
317	49, 316	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑘 ∈ (0...𝑀))
318	43	ffvelcdmda 7103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ (0...(𝑃 − 1)))
319	186, 318	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℝ)
320	317, 319	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → (𝑐‘𝑘) ∈ ℝ)
321		elfzle1 13568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑐‘𝑘) ∈ (0...(𝑃 − 1)) → 0 ≤ (𝑐‘𝑘))
322	318, 321	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → 0 ≤ (𝑐‘𝑘))
323	317, 322	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 0 ≤ (𝑐‘𝑘))
324	314, 320, 323	fsumge0 15832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))
325	324	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))
326	314, 320	fsumrecl 15771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ∈ ℝ)
327	326	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ∈ ℝ)
328	278, 327	addge01d 11852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ↔ (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))))
329	325, 328	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
330	329	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
331	276, 279, 306, 312, 330	ltletrd 11422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
332	331, 305	breqtrd 5168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
333	275, 332	elrpd 13075	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ⁺)
334	267, 333	ltaddrpd 13111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
335	334	adantl3r 750	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
336		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = 𝑘 → (𝑐‘𝑗) = (𝑐‘𝑘))
337	336	cbvsumv 15733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘)
338	337	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘))
339	72	ad5antr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑀 ∈ (ℤ_≥‘0))
340		simp-5l 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (0...𝑀)) → (𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))))
341	73, 318	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
342	340, 341	sylancom 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
343		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 0 → (𝑐‘𝑘) = (𝑐‘0))
344	339, 342, 343	fsum1p 15790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘) = ((𝑐‘0) + Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘)))
345	256	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘0) = (𝑃 − 1))
346	85	sumeq1i 15734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)
347	346	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
348	345, 347	oveq12d 7450	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘0) + Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘)) = ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
349	338, 344, 348	3eqtrrd 2781	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)) = Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
350	335, 349	breqtrd 5168	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
351	266, 350	gtned 11397	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) ≠ (𝑃 − 1))
352	351	neneqd 2944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ¬ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
353	265, 352	condan 817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝑐‘𝑗) = 0)
354		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0...𝑀))
355	32, 65	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) ∈ ℕ₀)
356	66	fvmpt2 7026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ if(𝑗 = 0, (𝑃 − 1), 0) ∈ ℕ₀) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
357	354, 355, 356	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
358	357	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
359		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → ¬ 𝑗 = 0)
360	359	iffalsed 4535	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
361	358, 360	eqtr2d 2777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
362	361	adantllr 719	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
363	362	adantllr 719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
364	353, 363	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
365	264, 364	pm2.61dan 812	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) = (𝐷‘𝑗))
366	250, 252, 365	eqfnfvd 7053	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 = 𝐷)
367	235, 366	sylanl2 681	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 = 𝐷)
368		eldifsni 4789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → 𝑐 ≠ 𝐷)
369	368	neneqd 2944	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → ¬ 𝑐 = 𝐷)
370	369	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ (𝑃 − 1) = (𝑐‘0)) → ¬ 𝑐 = 𝐷)
371	367, 370	pm2.65da 816	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ¬ (𝑃 − 1) = (𝑐‘0))
372	371	neqned 2946	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ≠ (𝑐‘0))
373	239, 240, 242, 372	leneltd 11416	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) < (𝑃 − 1))
374	239, 240	posdifd 11851	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑐‘0) < (𝑃 − 1) ↔ 0 < ((𝑃 − 1) − (𝑐‘0))))
375	373, 374	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → 0 < ((𝑃 − 1) − (𝑐‘0)))
376		elnnz 12625	. . . . . . . . . . . . . 14 ⊢ (((𝑃 − 1) − (𝑐‘0)) ∈ ℕ ↔ (((𝑃 − 1) − (𝑐‘0)) ∈ ℤ ∧ 0 < ((𝑃 − 1) − (𝑐‘0))))
377	248, 375, 376	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℕ)
378	377	0expd 14180	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0↑((𝑃 − 1) − (𝑐‘0))) = 0)
379	378	oveq2d 7448	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · 0))
380	160	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘(𝑃 − 1)) ∈ ℂ)
381	377	nnnn0d 12589	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℕ₀)
382	381	faccld 14324	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ∈ ℕ)
383	382	nncnd 12283	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ∈ ℂ)
384	382	nnne0d 12317	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ≠ 0)
385	380, 383, 384	divcld 12044	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) ∈ ℂ)
386	385	mul01d 11461	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · 0) = 0)
387	244, 379, 386	3eqtrd 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = 0)
388	387	oveq1d 7447	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) = (0 · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))
389	235, 54	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℤ)
390	389	zcnd 12725	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℂ)
391	390	mul02d 11460	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0 · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) = 0)
392	388, 391	eqtrd 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) = 0)
393	392	oveq2d 7448	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · 0))
394		fzfid 14015	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0...𝑀) ∈ Fin)
395	32, 277	sselid 3980	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℕ₀)
396	235, 395	sylanl2 681	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℕ₀)
397	396	faccld 14324	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝑐‘𝑗)) ∈ ℕ)
398	394, 397	fprodnncl 15992	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ∈ ℕ)
399	398	nncnd 12283	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ∈ ℂ)
400	398	nnne0d 12317	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ≠ 0)
401	380, 399, 400	divcld 12044	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℂ)
402	401	mul01d 11461	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · 0) = 0)
403	393, 402	eqtrd 2776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = 0)
404	403	sumeq2dv 15739	. . . . 5 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0)
405		diffi 9216	. . . . . . . 8 ⊢ ((𝐶‘(𝑃 − 1)) ∈ Fin → ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin)
406	18, 405	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin)
407	406	olcd 874	. . . . . 6 ⊢ (𝜑 → (((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ⊆ (ℤ_≥‘0) ∨ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin))
408		sumz 15759	. . . . . 6 ⊢ ((((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ⊆ (ℤ_≥‘0) ∨ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin) → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0 = 0)
409	407, 408	syl 17	. . . . 5 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0 = 0)
410	404, 409	eqtrd 2776	. . . 4 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = 0)
411	234, 410	oveq12d 7450	. . 3 ⊢ (𝜑 → ((((!‘(𝑃 − 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))
412	232	addridd 11462	. . 3 ⊢ (𝜑 → (((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) + 0) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
413		nfv 1913	. . . . 5 ⊢ Ⅎ𝑗𝜑
414	413, 205, 227, 219	fprodexp 45614	. . . 4 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) = (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃))
415	414	oveq2d 7448	. . 3 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)))
416	411, 412, 415	3eqtrd 2780	. 2 ⊢ (𝜑 → ((((!‘(𝑃 − 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...𝑀)-𝑗↑𝑃)))
417	15, 142, 416	3eqtrd 2780	1 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑃 − 1))‘0) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1539 ∈ wcel 2107 ≠ wne 2939 {crab 3435 Vcvv 3479 ∖ cdif 3947 ⊆ wss 3950 ifcif 4524 {csn 4625 {cpr 4627 class class class wbr 5142 ↦ cmpt 5224 ran crn 5685 Fn wfn 6555 ⟶wf 6556 ‘cfv 6560 (class class class)co 7432 ↑_m cmap 8867 Fincfn 8986 ℂcc 11154 ℝcr 11155 0cc0 11156 1c1 11157 + caddc 11159 · cmul 11161 < clt 11296 ≤ cle 11297 − cmin 11493 -cneg 11494 / cdiv 11921 ℕcn 12267 ℕ₀cn0 12528 ℤcz 12615 ℤ_≥cuz 12879 (,)cioo 13388 ...cfz 13548 ↑cexp 14103 !cfa 14313 Σcsu 15723 ∏cprod 15940 ↾_t crest 17466 TopOpenctopn 17467 topGenctg 17483 ℂ_fldccnfld 21365 D^𝑛 cdvn 25900

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-inf2 9682 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233 ax-pre-sup 11234 ax-addf 11235

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-tp 4630 df-op 4632 df-uni 4907 df-int 4946 df-iun 4992 df-iin 4993 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-se 5637 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-isom 6569 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-of 7698 df-om 7889 df-1st 8015 df-2nd 8016 df-supp 8187 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-1o 8507 df-2o 8508 df-er 8746 df-map 8869 df-pm 8870 df-ixp 8939 df-en 8987 df-dom 8988 df-sdom 8989 df-fin 8990 df-fsupp 9403 df-fi 9452 df-sup 9483 df-inf 9484 df-oi 9551 df-card 9980 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-div 11922 df-nn 12268 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12529 df-z 12616 df-dec 12736 df-uz 12880 df-q 12992 df-rp 13036 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13392 df-ico 13394 df-icc 13395 df-fz 13549 df-fzo 13696 df-seq 14044 df-exp 14104 df-fac 14314 df-bc 14343 df-hash 14371 df-cj 15139 df-re 15140 df-im 15141 df-sqrt 15275 df-abs 15276 df-clim 15525 df-sum 15724 df-prod 15941 df-struct 17185 df-sets 17202 df-slot 17220 df-ndx 17232 df-base 17249 df-ress 17276 df-plusg 17311 df-mulr 17312 df-starv 17313 df-sca 17314 df-vsca 17315 df-ip 17316 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-hom 17322 df-cco 17323 df-rest 17468 df-topn 17469 df-0g 17487 df-gsum 17488 df-topgen 17489 df-pt 17490 df-prds 17493 df-xrs 17548 df-qtop 17553 df-imas 17554 df-xps 17556 df-mre 17630 df-mrc 17631 df-acs 17633 df-mgm 18654 df-sgrp 18733 df-mnd 18749 df-submnd 18798 df-mulg 19087 df-cntz 19336 df-cmn 19801 df-psmet 21357 df-xmet 21358 df-met 21359 df-bl 21360 df-mopn 21361 df-fbas 21362 df-fg 21363 df-cnfld 21366 df-top 22901 df-topon 22918 df-topsp 22940 df-bases 22954 df-cld 23028 df-ntr 23029 df-cls 23030 df-nei 23107 df-lp 23145 df-perf 23146 df-cn 23236 df-cnp 23237 df-haus 23324 df-tx 23571 df-hmeo 23764 df-fil 23855 df-fm 23947 df-flim 23948 df-flf 23949 df-xms 24331 df-ms 24332 df-tms 24333 df-cncf 24905 df-limc 25902 df-dv 25903 df-dvn 25904

This theorem is referenced by: etransclem41 46295

W3C validator