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 44500

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 11143	. . . 4 ⊢ ℝ ∈ {ℝ, ℂ}
2	1	a1i 11	. . 3 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
3		reopn 43513	. . . . 5 ⊢ ℝ ∈ (topGen‘ran (,))
4		eqid 2736	. . . . . 6 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
5	4	tgioo2 24166	. . . . 5 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
6	3, 5	eleqtri 2836	. . . 4 ⊢ ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
7	6	a1i 11	. . 3 ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
8		etransclem35.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ ℕ)
9		etransclem35.m	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
10		etransclem35.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
11		nnm1nn0 12454	. . . 4 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
12	8, 11	syl 17	. . 3 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
13		etransclem5 44470	. . 3 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
14		etransclem35.c	. . 3 ⊢ 𝐶 = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})
15		0red 11158	. . 3 ⊢ (𝜑 → 0 ∈ ℝ)
16	2, 7, 8, 9, 10, 12, 13, 14, 15	etransclem31 44496	. 2 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑃 − 1))‘0) = Σ𝑐 ∈ (𝐶‘(𝑃 − 1))(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))))
17		nfv 1917	. . 3 ⊢ Ⅎ𝑐𝜑
18		nfcv 2907	. . 3 ⊢ Ⅎ𝑐(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))))
19	14, 12	etransclem16 44481	. . 3 ⊢ (𝜑 → (𝐶‘(𝑃 − 1)) ∈ Fin)
20		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ (𝐶‘(𝑃 − 1)))
21	14, 12	etransclem12 44477	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶‘(𝑃 − 1)) = {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
22	21	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝐶‘(𝑃 − 1)) = {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
23	20, 22	eleqtrd 2840	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
24		rabid 3427	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)} ↔ (𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)))
25	23, 24	sylib 217	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)))
26	25	simprd 496	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
27	26	eqcomd 2742	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑃 − 1) = Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
28	27	fveq2d 6846	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (!‘(𝑃 − 1)) = (!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)))
29	28	oveq1d 7372	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) = ((!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))))
30		nfcv 2907	. . . . . . . 8 ⊢ Ⅎ𝑗𝑐
31		fzfid 13878	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (0...𝑀) ∈ Fin)
32		nn0ex 12419	. . . . . . . . . 10 ⊢ ℕ₀ ∈ V
33		fzssnn0 43541	. . . . . . . . . 10 ⊢ (0...(𝑃 − 1)) ⊆ ℕ₀
34		mapss 8827	. . . . . . . . . 10 ⊢ ((ℕ₀ ∈ V ∧ (0...(𝑃 − 1)) ⊆ ℕ₀) → ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ⊆ (ℕ₀ ↑_m (0...𝑀)))
35	32, 33, 34	mp2an 690	. . . . . . . . 9 ⊢ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ⊆ (ℕ₀ ↑_m (0...𝑀))
36	25	simpld 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)))
37	35, 36	sselid 3942	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ (ℕ₀ ↑_m (0...𝑀)))
38	30, 31, 37	mccl 43829	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℕ)
39	29, 38	eqeltrd 2838	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℕ)
40	39	nnzd 12526	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℤ)
41	8	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑃 ∈ ℕ)
42	9	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑀 ∈ ℕ₀)
43		elmapi 8787	. . . . . . . 8 ⊢ (𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
44	36, 43	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
45		0zd 12511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ∈ ℤ)
46	41, 42, 44, 45	etransclem10 44475	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) ∈ ℤ)
47		fzfid 13878	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (1...𝑀) ∈ Fin)
48	8	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ)
49	44	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
50		fz1ssfz0 13537	. . . . . . . . . 10 ⊢ (1...𝑀) ⊆ (0...𝑀)
51	50	sseli 3940	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (0...𝑀))
52	51	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀))
53		0zd 12511	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 0 ∈ ℤ)
54	48, 49, 52, 53	etransclem3 44468	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℤ)
55	47, 54	fprodzcl 15837	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℤ)
56	46, 55	zmulcld 12613	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) ∈ ℤ)
57	40, 56	zmulcld 12613	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ∈ ℤ)
58	57	zcnd 12608	. . 3 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ∈ ℂ)
59		nn0uz 12805	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
60	12, 59	eleqtrdi 2848	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃 − 1) ∈ (ℤ_≥‘0))
61		eluzfz2 13449	. . . . . . . . . 10 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘0) → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
62	60, 61	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
63		eluzfz1 13448	. . . . . . . . . 10 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘0) → 0 ∈ (0...(𝑃 − 1)))
64	60, 63	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...(𝑃 − 1)))
65	62, 64	ifcld 4532	. . . . . . . 8 ⊢ (𝜑 → if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1)))
66	65	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1)))
67		etransclem35.d	. . . . . . 7 ⊢ 𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0))
68	66, 67	fmptd 7062	. . . . . 6 ⊢ (𝜑 → 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
69		ovex 7390	. . . . . . 7 ⊢ (0...(𝑃 − 1)) ∈ V
70		ovex 7390	. . . . . . 7 ⊢ (0...𝑀) ∈ V
71	69, 70	elmap 8809	. . . . . 6 ⊢ (𝐷 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ↔ 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
72	68, 71	sylibr 233	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)))
73	9, 59	eleqtrdi 2848	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
74		fzsscn 43535	. . . . . . . 8 ⊢ (0...(𝑃 − 1)) ⊆ ℂ
75	68	ffvelcdmda 7035	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ (0...(𝑃 − 1)))
76	74, 75	sselid 3942	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ ℂ)
77		fveq2 6842	. . . . . . 7 ⊢ (𝑗 = 0 → (𝐷‘𝑗) = (𝐷‘0))
78	73, 76, 77	fsum1p 15638	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = ((𝐷‘0) + Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗)))
79	67	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0)))
80		simpr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 = 0) → 𝑗 = 0)
81	80	iftrued 4494	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 = 0) → if(𝑗 = 0, (𝑃 − 1), 0) = (𝑃 − 1))
82		eluzfz1 13448	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
83	73, 82	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
84	79, 81, 83, 12	fvmptd 6955	. . . . . . 7 ⊢ (𝜑 → (𝐷‘0) = (𝑃 − 1))
85		0p1e1 12275	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
86	85	oveq1i 7367	. . . . . . . . . 10 ⊢ ((0 + 1)...𝑀) = (1...𝑀)
87	86	sumeq1i 15583	. . . . . . . . 9 ⊢ Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗)
88	87	a1i 11	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗))
89	67	fvmpt2 6959	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ (0...𝑀) ∧ if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1))) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
90	51, 65, 89	syl2anr 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
91		0red 11158	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 0 ∈ ℝ)
92		1red 11156	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 1 ∈ ℝ)
93		elfzelz 13441	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℤ)
94	93	zred 12607	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℝ)
95		0lt1 11677	. . . . . . . . . . . . . . . 16 ⊢ 0 < 1
96	95	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 0 < 1)
97		elfzle1 13444	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 1 ≤ 𝑗)
98	91, 92, 94, 96, 97	ltletrd 11315	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 0 < 𝑗)
99	91, 98	gtned 11290	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ≠ 0)
100	99	neneqd 2948	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑀) → ¬ 𝑗 = 0)
101	100	iffalsed 4497	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑀) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
102	101	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
103	90, 102	eqtrd 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) = 0)
104	103	sumeq2dv 15588	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)0)
105		fzfi 13877	. . . . . . . . . 10 ⊢ (1...𝑀) ∈ Fin
106	105	olci 864	. . . . . . . . 9 ⊢ ((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin)
107		sumz 15607	. . . . . . . . 9 ⊢ (((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin) → Σ𝑗 ∈ (1...𝑀)0 = 0)
108	106, 107	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)0 = 0)
109	88, 104, 108	3eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = 0)
110	84, 109	oveq12d 7375	. . . . . 6 ⊢ (𝜑 → ((𝐷‘0) + Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗)) = ((𝑃 − 1) + 0))
111	8	nncnd 12169	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℂ)
112		1cnd 11150	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
113	111, 112	subcld 11512	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 1) ∈ ℂ)
114	113	addid1d 11355	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 1) + 0) = (𝑃 − 1))
115	78, 110, 114	3eqtrd 2780	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = (𝑃 − 1))
116		fveq1 6841	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → (𝑐‘𝑗) = (𝐷‘𝑗))
117	116	sumeq2sdv 15589	. . . . . . 7 ⊢ (𝑐 = 𝐷 → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗))
118	117	eqeq1d 2738	. . . . . 6 ⊢ (𝑐 = 𝐷 → (Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1) ↔ Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = (𝑃 − 1)))
119	118	elrab 3645	. . . . 5 ⊢ (𝐷 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)} ↔ (𝐷 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = (𝑃 − 1)))
120	72, 115, 119	sylanbrc 583	. . . 4 ⊢ (𝜑 → 𝐷 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
121	120, 21	eleqtrrd 2841	. . 3 ⊢ (𝜑 → 𝐷 ∈ (𝐶‘(𝑃 − 1)))
122	116	fveq2d 6846	. . . . . 6 ⊢ (𝑐 = 𝐷 → (!‘(𝑐‘𝑗)) = (!‘(𝐷‘𝑗)))
123	122	prodeq2ad 43823	. . . . 5 ⊢ (𝑐 = 𝐷 → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) = ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)))
124	123	oveq2d 7373	. . . 4 ⊢ (𝑐 = 𝐷 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) = ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))))
125		fveq1 6841	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (𝑐‘0) = (𝐷‘0))
126	125	breq2d 5117	. . . . . 6 ⊢ (𝑐 = 𝐷 → ((𝑃 − 1) < (𝑐‘0) ↔ (𝑃 − 1) < (𝐷‘0)))
127	125	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑐 = 𝐷 → ((𝑃 − 1) − (𝑐‘0)) = ((𝑃 − 1) − (𝐷‘0)))
128	127	fveq2d 6846	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → (!‘((𝑃 − 1) − (𝑐‘0))) = (!‘((𝑃 − 1) − (𝐷‘0))))
129	128	oveq2d 7373	. . . . . . 7 ⊢ (𝑐 = 𝐷 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) = ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))))
130	127	oveq2d 7373	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (0↑((𝑃 − 1) − (𝑐‘0))) = (0↑((𝑃 − 1) − (𝐷‘0))))
131	129, 130	oveq12d 7375	. . . . . 6 ⊢ (𝑐 = 𝐷 → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))))
132	126, 131	ifbieq2d 4512	. . . . 5 ⊢ (𝑐 = 𝐷 → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))))
133	116	breq2d 5117	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (𝑃 < (𝑐‘𝑗) ↔ 𝑃 < (𝐷‘𝑗)))
134	116	oveq2d 7373	. . . . . . . . . 10 ⊢ (𝑐 = 𝐷 → (𝑃 − (𝑐‘𝑗)) = (𝑃 − (𝐷‘𝑗)))
135	134	fveq2d 6846	. . . . . . . . 9 ⊢ (𝑐 = 𝐷 → (!‘(𝑃 − (𝑐‘𝑗))) = (!‘(𝑃 − (𝐷‘𝑗))))
136	135	oveq2d 7373	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → ((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) = ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))))
137	134	oveq2d 7373	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))) = ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))
138	136, 137	oveq12d 7375	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))) = (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))
139	133, 138	ifbieq2d 4512	. . . . . 6 ⊢ (𝑐 = 𝐷 → if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) = if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))
140	139	prodeq2ad 43823	. . . . 5 ⊢ (𝑐 = 𝐷 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) = ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))
141	132, 140	oveq12d 7375	. . . 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 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))))
142	124, 141	oveq12d 7375	. . 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 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))))
143	17, 18, 19, 58, 121, 142	fsumsplit1 15630	. 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 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))))
144	33, 75	sselid 3942	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ ℕ₀)
145	144	faccld 14184	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐷‘𝑗)) ∈ ℕ)
146	145	nncnd 12169	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐷‘𝑗)) ∈ ℂ)
147	77	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝑗 = 0 → (!‘(𝐷‘𝑗)) = (!‘(𝐷‘0)))
148	73, 146, 147	fprod1p 15851	. . . . . . . . 9 ⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)) = ((!‘(𝐷‘0)) · ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗))))
149	84	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝜑 → (!‘(𝐷‘0)) = (!‘(𝑃 − 1)))
150	86	prodeq1i 15801	. . . . . . . . . . . 12 ⊢ ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗))
151	150	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗)))
152	103	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝐷‘𝑗)) = (!‘0))
153		fac0 14176	. . . . . . . . . . . . 13 ⊢ (!‘0) = 1
154	152, 153	eqtrdi 2792	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝐷‘𝑗)) = 1)
155	154	prodeq2dv 15806	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)1)
156		prod1 15827	. . . . . . . . . . . 12 ⊢ (((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin) → ∏𝑗 ∈ (1...𝑀)1 = 1)
157	106, 156	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)1 = 1)
158	151, 155, 157	3eqtrd 2780	. . . . . . . . . 10 ⊢ (𝜑 → ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = 1)
159	149, 158	oveq12d 7375	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝐷‘0)) · ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗))) = ((!‘(𝑃 − 1)) · 1))
160	12	faccld 14184	. . . . . . . . . . 11 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
161	160	nncnd 12169	. . . . . . . . . 10 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
162	161	mulid1d 11172	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · 1) = (!‘(𝑃 − 1)))
163	148, 159, 162	3eqtrd 2780	. . . . . . . 8 ⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)) = (!‘(𝑃 − 1)))
164	163	oveq2d 7373	. . . . . . 7 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) = ((!‘(𝑃 − 1)) / (!‘(𝑃 − 1))))
165	160	nnne0d 12203	. . . . . . . 8 ⊢ (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
166	161, 165	dividd 11929	. . . . . . 7 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘(𝑃 − 1))) = 1)
167	164, 166	eqtrd 2776	. . . . . 6 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) = 1)
168	12	nn0red 12474	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 − 1) ∈ ℝ)
169	84, 168	eqeltrd 2838	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘0) ∈ ℝ)
170	169, 168	lttri3d 11295	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘0) = (𝑃 − 1) ↔ (¬ (𝐷‘0) < (𝑃 − 1) ∧ ¬ (𝑃 − 1) < (𝐷‘0))))
171	84, 170	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → (¬ (𝐷‘0) < (𝑃 − 1) ∧ ¬ (𝑃 − 1) < (𝐷‘0)))
172	171	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → ¬ (𝑃 − 1) < (𝐷‘0))
173	172	iffalsed 4497	. . . . . . . 8 ⊢ (𝜑 → if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))))
174	84	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 − 1) = (𝐷‘0))
175	113, 174	subeq0bd 11581	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑃 − 1) − (𝐷‘0)) = 0)
176	175	fveq2d 6846	. . . . . . . . . . . 12 ⊢ (𝜑 → (!‘((𝑃 − 1) − (𝐷‘0))) = (!‘0))
177	176, 153	eqtrdi 2792	. . . . . . . . . . 11 ⊢ (𝜑 → (!‘((𝑃 − 1) − (𝐷‘0))) = 1)
178	177	oveq2d 7373	. . . . . . . . . 10 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) = ((!‘(𝑃 − 1)) / 1))
179	161	div1d 11923	. . . . . . . . . 10 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / 1) = (!‘(𝑃 − 1)))
180	178, 179	eqtrd 2776	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) = (!‘(𝑃 − 1)))
181	175	oveq2d 7373	. . . . . . . . . 10 ⊢ (𝜑 → (0↑((𝑃 − 1) − (𝐷‘0))) = (0↑0))
182		0cnd 11148	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℂ)
183	182	exp0d 14045	. . . . . . . . . 10 ⊢ (𝜑 → (0↑0) = 1)
184	181, 183	eqtrd 2776	. . . . . . . . 9 ⊢ (𝜑 → (0↑((𝑃 − 1) − (𝐷‘0))) = 1)
185	180, 184	oveq12d 7375	. . . . . . . 8 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))) = ((!‘(𝑃 − 1)) · 1))
186	173, 185, 162	3eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) = (!‘(𝑃 − 1)))
187		fzssre 43538	. . . . . . . . . . . 12 ⊢ (0...(𝑃 − 1)) ⊆ ℝ
188	68	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
189	51	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀))
190	188, 189	ffvelcdmd 7036	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ∈ (0...(𝑃 − 1)))
191	187, 190	sselid 3942	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ∈ ℝ)
192	8	nnred 12168	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℝ)
193	192	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℝ)
194	8	nngt0d 12202	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 𝑃)
195	15, 192, 194	ltled 11303	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ 𝑃)
196	195	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 0 ≤ 𝑃)
197	103, 196	eqbrtrd 5127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ≤ 𝑃)
198	191, 193, 197	lensymd 11306	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ¬ 𝑃 < (𝐷‘𝑗))
199	198	iffalsed 4497	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))
200	103	oveq2d 7373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐷‘𝑗)) = (𝑃 − 0))
201	111	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℂ)
202	201	subid1d 11501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − 0) = 𝑃)
203	200, 202	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐷‘𝑗)) = 𝑃)
204	203	fveq2d 6846	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝑃 − (𝐷‘𝑗))) = (!‘𝑃))
205	204	oveq2d 7373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) = ((!‘𝑃) / (!‘𝑃)))
206	8	nnnn0d 12473	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
207	206	faccld 14184	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (!‘𝑃) ∈ ℕ)
208	207	nncnd 12169	. . . . . . . . . . . . 13 ⊢ (𝜑 → (!‘𝑃) ∈ ℂ)
209	207	nnne0d 12203	. . . . . . . . . . . . 13 ⊢ (𝜑 → (!‘𝑃) ≠ 0)
210	208, 209	dividd 11929	. . . . . . . . . . . 12 ⊢ (𝜑 → ((!‘𝑃) / (!‘𝑃)) = 1)
211	210	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘𝑃)) = 1)
212	205, 211	eqtrd 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) = 1)
213		df-neg 11388	. . . . . . . . . . . . 13 ⊢ -𝑗 = (0 − 𝑗)
214	213	eqcomi 2745	. . . . . . . . . . . 12 ⊢ (0 − 𝑗) = -𝑗
215	214	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (0 − 𝑗) = -𝑗)
216	215, 203	oveq12d 7375	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))) = (-𝑗↑𝑃))
217	212, 216	oveq12d 7375	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))) = (1 · (-𝑗↑𝑃)))
218	93	znegcld 12609	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℤ)
219	218	zcnd 12608	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℂ)
220	219	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → -𝑗 ∈ ℂ)
221	206	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ₀)
222	220, 221	expcld 14051	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (-𝑗↑𝑃) ∈ ℂ)
223	222	mulid2d 11173	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1 · (-𝑗↑𝑃)) = (-𝑗↑𝑃))
224	199, 217, 223	3eqtrd 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = (-𝑗↑𝑃))
225	224	prodeq2dv 15806	. . . . . . 7 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))
226	186, 225	oveq12d 7375	. . . . . 6 ⊢ (𝜑 → (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
227	167, 226	oveq12d 7375	. . . . 5 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) = (1 · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))))
228		fzfid 13878	. . . . . . . . 9 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
229		zexpcl 13982	. . . . . . . . . 10 ⊢ ((-𝑗 ∈ ℤ ∧ 𝑃 ∈ ℕ₀) → (-𝑗↑𝑃) ∈ ℤ)
230	218, 206, 229	syl2anr 597	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (-𝑗↑𝑃) ∈ ℤ)
231	228, 230	fprodzcl 15837	. . . . . . . 8 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) ∈ ℤ)
232	231	zcnd 12608	. . . . . . 7 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) ∈ ℂ)
233	161, 232	mulcld 11175	. . . . . 6 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) ∈ ℂ)
234	233	mulid2d 11173	. . . . 5 ⊢ (𝜑 → (1 · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
235	227, 234	eqtrd 2776	. . . 4 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
236		eldifi 4086	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → 𝑐 ∈ (𝐶‘(𝑃 − 1)))
237	83	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ∈ (0...𝑀))
238	44, 237	ffvelcdmd 7036	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑐‘0) ∈ (0...(𝑃 − 1)))
239	236, 238	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ (0...(𝑃 − 1)))
240	187, 239	sselid 3942	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ ℝ)
241	168	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ∈ ℝ)
242		elfzle2 13445	. . . . . . . . . . . . . 14 ⊢ ((𝑐‘0) ∈ (0...(𝑃 − 1)) → (𝑐‘0) ≤ (𝑃 − 1))
243	239, 242	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ≤ (𝑃 − 1))
244	240, 241, 243	lensymd 11306	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ¬ (𝑃 − 1) < (𝑐‘0))
245	244	iffalsed 4497	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))))
246	12	nn0zd 12525	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − 1) ∈ ℤ)
247	246	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ∈ ℤ)
248	239	elfzelzd 13442	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ ℤ)
249	247, 248	zsubcld 12612	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℤ)
250	44	ffnd 6669	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 Fn (0...𝑀))
251	250	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 Fn (0...𝑀))
252	68	ffnd 6669	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 Fn (0...𝑀))
253	252	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝐷 Fn (0...𝑀))
254		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 0 → (𝑐‘𝑗) = (𝑐‘0))
255	254	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝑐‘0))
256		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 − 1) = (𝑐‘0) → (𝑃 − 1) = (𝑐‘0))
257	256	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑃 − 1) = (𝑐‘0) → (𝑐‘0) = (𝑃 − 1))
258	257	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘0) = (𝑃 − 1))
259	77	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝐷‘𝑗) = (𝐷‘0))
260	84	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝐷‘0) = (𝑃 − 1))
261	259, 260	eqtr2d 2777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝑃 − 1) = (𝐷‘𝑗))
262	261	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑃 − 1) = (𝐷‘𝑗))
263	255, 258, 262	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
264	263	adantllr 717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
265	264	adantlr 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
266	26	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
267	168	ad5antr 732	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) ∈ ℝ)
268	168	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) ∈ ℝ)
269	44	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
270	50	sseli 3940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ (0...𝑀))
271	270	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (0...𝑀))
272	269, 271	ffvelcdmd 7036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ (0...(𝑃 − 1)))
273	33, 272	sselid 3942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℕ₀)
274	47, 273	fsumnn0cl 15621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℕ₀)
275	274	nn0red 12474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ)
276	275	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ)
277		0red 11158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 ∈ ℝ)
278	44	ffvelcdmda 7035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ (0...(𝑃 − 1)))
279	187, 278	sselid 3942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℝ)
280	279	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ∈ ℝ)
281		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0)
282		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘(𝑐‘𝑗)
283		fzfid 13878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (1...𝑀) ∈ Fin)
284		simp-4l 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (1...𝑀)) → (𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))))
285	74, 272	sselid 3942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
286	284, 285	sylancom 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
287		1zzd 12534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 1 ∈ ℤ)
288		elfzel2 13439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
289	288	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑀 ∈ ℤ)
290		elfzelz 13441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
291	290	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℤ)
292		elfznn0 13534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
293	292	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℕ₀)
294		neqne 2951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (¬ 𝑗 = 0 → 𝑗 ≠ 0)
295	294	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ≠ 0)
296		elnnne0 12427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑗 ∈ ℕ ↔ (𝑗 ∈ ℕ₀ ∧ 𝑗 ≠ 0))
297	293, 295, 296	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℕ)
298	297	nnge1d 12201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 1 ≤ 𝑗)
299		elfzle2 13445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
300	299	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ≤ 𝑀)
301	287, 289, 291, 298, 300	elfzd 13432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ (1...𝑀))
302	301	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑗 ∈ (1...𝑀))
303	302	adantlll 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑗 ∈ (1...𝑀))
304		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 = 𝑗 → (𝑐‘𝑘) = (𝑐‘𝑗))
305	281, 282, 283, 286, 303, 304	fsumsplit1 15630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) = ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
306	305	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
307	306, 276	eqeltrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)) ∈ ℝ)
308		elfzle1 13444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑐‘𝑗) ∈ (0...(𝑃 − 1)) → 0 ≤ (𝑐‘𝑗))
309	278, 308	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ (𝑐‘𝑗))
310	309	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 ≤ (𝑐‘𝑗))
311		neqne 2951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ (𝑐‘𝑗) = 0 → (𝑐‘𝑗) ≠ 0)
312	311	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ≠ 0)
313	277, 280, 310, 312	leneltd 11309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < (𝑐‘𝑗))
314		diffi 9123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((1...𝑀) ∈ Fin → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
315	105, 314	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
316		eldifi 4086	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑘 ∈ ((1...𝑀) ∖ {𝑗}) → 𝑘 ∈ (1...𝑀))
317	316	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑘 ∈ (1...𝑀))
318	50, 317	sselid 3942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑘 ∈ (0...𝑀))
319	44	ffvelcdmda 7035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ (0...(𝑃 − 1)))
320	187, 319	sselid 3942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℝ)
321	318, 320	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → (𝑐‘𝑘) ∈ ℝ)
322		elfzle1 13444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑐‘𝑘) ∈ (0...(𝑃 − 1)) → 0 ≤ (𝑐‘𝑘))
323	319, 322	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → 0 ≤ (𝑐‘𝑘))
324	318, 323	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 0 ≤ (𝑐‘𝑘))
325	315, 321, 324	fsumge0 15680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))
326	325	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))
327	315, 321	fsumrecl 15619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ∈ ℝ)
328	327	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ∈ ℝ)
329	279, 328	addge01d 11743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ↔ (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))))
330	326, 329	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
331	330	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
332	277, 280, 307, 313, 331	ltletrd 11315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
333	332, 306	breqtrd 5131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
334	276, 333	elrpd 12954	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ⁺)
335	268, 334	ltaddrpd 12990	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
336	335	adantl3r 748	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
337		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = 𝑘 → (𝑐‘𝑗) = (𝑐‘𝑘))
338	337	cbvsumv 15581	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘)
339	338	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘))
340	73	ad5antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑀 ∈ (ℤ_≥‘0))
341		simp-5l 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (0...𝑀)) → (𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))))
342	74, 319	sselid 3942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
343	341, 342	sylancom 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
344		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 0 → (𝑐‘𝑘) = (𝑐‘0))
345	340, 343, 344	fsum1p 15638	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘) = ((𝑐‘0) + Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘)))
346	257	ad4antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘0) = (𝑃 − 1))
347	86	sumeq1i 15583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)
348	347	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
349	346, 348	oveq12d 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘0) + Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘)) = ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
350	339, 345, 349	3eqtrrd 2781	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)) = Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
351	336, 350	breqtrd 5131	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
352	267, 351	gtned 11290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) ≠ (𝑃 − 1))
353	352	neneqd 2948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ¬ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
354	266, 353	condan 816	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝑐‘𝑗) = 0)
355		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0...𝑀))
356	33, 66	sselid 3942	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) ∈ ℕ₀)
357	67	fvmpt2 6959	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ if(𝑗 = 0, (𝑃 − 1), 0) ∈ ℕ₀) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
358	355, 356, 357	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
359	358	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
360		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → ¬ 𝑗 = 0)
361	360	iffalsed 4497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
362	359, 361	eqtr2d 2777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
363	362	adantllr 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
364	363	adantllr 717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
365	354, 364	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
366	265, 365	pm2.61dan 811	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) = (𝐷‘𝑗))
367	251, 253, 366	eqfnfvd 6985	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 = 𝐷)
368	236, 367	sylanl2 679	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 = 𝐷)
369		eldifsni 4750	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → 𝑐 ≠ 𝐷)
370	369	neneqd 2948	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → ¬ 𝑐 = 𝐷)
371	370	ad2antlr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ (𝑃 − 1) = (𝑐‘0)) → ¬ 𝑐 = 𝐷)
372	368, 371	pm2.65da 815	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ¬ (𝑃 − 1) = (𝑐‘0))
373	372	neqned 2950	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ≠ (𝑐‘0))
374	240, 241, 243, 373	leneltd 11309	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) < (𝑃 − 1))
375	240, 241	posdifd 11742	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑐‘0) < (𝑃 − 1) ↔ 0 < ((𝑃 − 1) − (𝑐‘0))))
376	374, 375	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → 0 < ((𝑃 − 1) − (𝑐‘0)))
377		elnnz 12509	. . . . . . . . . . . . . 14 ⊢ (((𝑃 − 1) − (𝑐‘0)) ∈ ℕ ↔ (((𝑃 − 1) − (𝑐‘0)) ∈ ℤ ∧ 0 < ((𝑃 − 1) − (𝑐‘0))))
378	249, 376, 377	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℕ)
379	378	0expd 14044	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0↑((𝑃 − 1) − (𝑐‘0))) = 0)
380	379	oveq2d 7373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · 0))
381	161	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘(𝑃 − 1)) ∈ ℂ)
382	378	nnnn0d 12473	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℕ₀)
383	382	faccld 14184	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ∈ ℕ)
384	383	nncnd 12169	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ∈ ℂ)
385	383	nnne0d 12203	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ≠ 0)
386	381, 384, 385	divcld 11931	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) ∈ ℂ)
387	386	mul01d 11354	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · 0) = 0)
388	245, 380, 387	3eqtrd 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = 0)
389	388	oveq1d 7372	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) = (0 · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))
390	236, 55	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℤ)
391	390	zcnd 12608	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℂ)
392	391	mul02d 11353	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0 · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) = 0)
393	389, 392	eqtrd 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) = 0)
394	393	oveq2d 7373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · 0))
395		fzfid 13878	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0...𝑀) ∈ Fin)
396	33, 278	sselid 3942	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℕ₀)
397	236, 396	sylanl2 679	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℕ₀)
398	397	faccld 14184	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝑐‘𝑗)) ∈ ℕ)
399	395, 398	fprodnncl 15838	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ∈ ℕ)
400	399	nncnd 12169	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ∈ ℂ)
401	399	nnne0d 12203	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ≠ 0)
402	381, 400, 401	divcld 11931	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℂ)
403	402	mul01d 11354	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · 0) = 0)
404	394, 403	eqtrd 2776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = 0)
405	404	sumeq2dv 15588	. . . . 5 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0)
406		diffi 9123	. . . . . . . 8 ⊢ ((𝐶‘(𝑃 − 1)) ∈ Fin → ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin)
407	19, 406	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin)
408	407	olcd 872	. . . . . 6 ⊢ (𝜑 → (((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ⊆ (ℤ_≥‘0) ∨ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin))
409		sumz 15607	. . . . . 6 ⊢ ((((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ⊆ (ℤ_≥‘0) ∨ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin) → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0 = 0)
410	408, 409	syl 17	. . . . 5 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0 = 0)
411	405, 410	eqtrd 2776	. . . 4 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = 0)
412	235, 411	oveq12d 7375	. . 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))
413	233	addid1d 11355	. . 3 ⊢ (𝜑 → (((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) + 0) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
414		nfv 1917	. . . . 5 ⊢ Ⅎ𝑗𝜑
415	414, 206, 228, 220	fprodexp 43825	. . . 4 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) = (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃))
416	415	oveq2d 7373	. . 3 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)))
417	412, 413, 416	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...𝑀)-𝑗↑𝑃)))
418	16, 143, 417	3eqtrd 2780	1 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑃 − 1))‘0) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 {crab 3407 Vcvv 3445 ∖ cdif 3907 ⊆ wss 3910 ifcif 4486 {csn 4586 {cpr 4588 class class class wbr 5105 ↦ cmpt 5188 ran crn 5634 Fn wfn 6491 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 ↑_m cmap 8765 Fincfn 8883 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 · cmul 11056 < clt 11189 ≤ cle 11190 − cmin 11385 -cneg 11386 / cdiv 11812 ℕcn 12153 ℕ₀cn0 12413 ℤcz 12499 ℤ_≥cuz 12763 (,)cioo 13264 ...cfz 13424 ↑cexp 13967 !cfa 14173 Σcsu 15570 ∏cprod 15788 ↾_t crest 17302 TopOpenctopn 17303 topGenctg 17319 ℂ_fldccnfld 20796 D^𝑛 cdvn 25228

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129 ax-addf 11130 ax-mulf 11131

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-tp 4591 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-supp 8093 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-2o 8413 df-er 8648 df-map 8767 df-pm 8768 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9306 df-fi 9347 df-sup 9378 df-inf 9379 df-oi 9446 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-4 12218 df-5 12219 df-6 12220 df-7 12221 df-8 12222 df-9 12223 df-n0 12414 df-z 12500 df-dec 12619 df-uz 12764 df-q 12874 df-rp 12916 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ioo 13268 df-ico 13270 df-icc 13271 df-fz 13425 df-fzo 13568 df-seq 13907 df-exp 13968 df-fac 14174 df-bc 14203 df-hash 14231 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-clim 15370 df-sum 15571 df-prod 15789 df-struct 17019 df-sets 17036 df-slot 17054 df-ndx 17066 df-base 17084 df-ress 17113 df-plusg 17146 df-mulr 17147 df-starv 17148 df-sca 17149 df-vsca 17150 df-ip 17151 df-tset 17152 df-ple 17153 df-ds 17155 df-unif 17156 df-hom 17157 df-cco 17158 df-rest 17304 df-topn 17305 df-0g 17323 df-gsum 17324 df-topgen 17325 df-pt 17326 df-prds 17329 df-xrs 17384 df-qtop 17389 df-imas 17390 df-xps 17392 df-mre 17466 df-mrc 17467 df-acs 17469 df-mgm 18497 df-sgrp 18546 df-mnd 18557 df-submnd 18602 df-mulg 18873 df-cntz 19097 df-cmn 19564 df-psmet 20788 df-xmet 20789 df-met 20790 df-bl 20791 df-mopn 20792 df-fbas 20793 df-fg 20794 df-cnfld 20797 df-top 22243 df-topon 22260 df-topsp 22282 df-bases 22296 df-cld 22370 df-ntr 22371 df-cls 22372 df-nei 22449 df-lp 22487 df-perf 22488 df-cn 22578 df-cnp 22579 df-haus 22666 df-tx 22913 df-hmeo 23106 df-fil 23197 df-fm 23289 df-flim 23290 df-flf 23291 df-xms 23673 df-ms 23674 df-tms 23675 df-cncf 24241 df-limc 25230 df-dv 25231 df-dvn 25232

This theorem is referenced by: etransclem41 44506

W3C validator