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 40486

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...𝑛) ↑_𝑚 (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 10028	. . . 4 ⊢ ℝ ∈ {ℝ, ℂ}
2	1	a1i 11	. . 3 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
3		reopn 39501	. . . . 5 ⊢ ℝ ∈ (topGen‘ran (,))
4		eqid 2622	. . . . . 6 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
5	4	tgioo2 22606	. . . . 5 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
6	3, 5	eleqtri 2699	. . . 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 11334	. . . 4 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
12	8, 11	syl 17	. . 3 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
13		etransclem5 40456	. . 3 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
14		etransclem35.c	. . 3 ⊢ 𝐶 = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})
15		0red 10041	. . 3 ⊢ (𝜑 → 0 ∈ ℝ)
16	2, 7, 8, 9, 10, 12, 13, 14, 15	etransclem31 40482	. 2 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑃 − 1))‘0) = Σ𝑐 ∈ (𝐶‘(𝑃 − 1))(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))))
17		nfv 1843	. . 3 ⊢ Ⅎ𝑐𝜑
18		nfcv 2764	. . 3 ⊢ Ⅎ𝑐(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))))
19	14, 12	etransclem16 40467	. . 3 ⊢ (𝜑 → (𝐶‘(𝑃 − 1)) ∈ Fin)
20		simpr 477	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ (𝐶‘(𝑃 − 1)))
21	14, 12	etransclem12 40463	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶‘(𝑃 − 1)) = {𝑐 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
22	21	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝐶‘(𝑃 − 1)) = {𝑐 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
23	20, 22	eleqtrd 2703	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
24		rabid 3116	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)} ↔ (𝑐 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)))
25	23, 24	sylib 208	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑐 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)))
26	25	simprd 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
27	26	eqcomd 2628	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑃 − 1) = Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
28	27	fveq2d 6195	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (!‘(𝑃 − 1)) = (!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)))
29	28	oveq1d 6665	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) = ((!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))))
30		nfcv 2764	. . . . . . . 8 ⊢ Ⅎ𝑗𝑐
31		fzfid 12772	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (0...𝑀) ∈ Fin)
32		nn0ex 11298	. . . . . . . . . 10 ⊢ ℕ₀ ∈ V
33		fzssnn0 39533	. . . . . . . . . 10 ⊢ (0...(𝑃 − 1)) ⊆ ℕ₀
34		mapss 7900	. . . . . . . . . 10 ⊢ ((ℕ₀ ∈ V ∧ (0...(𝑃 − 1)) ⊆ ℕ₀) → ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ⊆ (ℕ₀ ↑_𝑚 (0...𝑀)))
35	32, 33, 34	mp2an 708	. . . . . . . . 9 ⊢ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ⊆ (ℕ₀ ↑_𝑚 (0...𝑀))
36	25	simpld 475	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)))
37	35, 36	sseldi 3601	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ (ℕ₀ ↑_𝑚 (0...𝑀)))
38	30, 31, 37	mccl 39830	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℕ)
39	29, 38	eqeltrd 2701	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℕ)
40	39	nnzd 11481	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℤ)
41	8	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑃 ∈ ℕ)
42	9	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑀 ∈ ℕ₀)
43		elmapi 7879	. . . . . . . 8 ⊢ (𝑐 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
44	36, 43	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
45		0zd 11389	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ∈ ℤ)
46	41, 42, 44, 45	etransclem10 40461	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) ∈ ℤ)
47		fzfid 12772	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (1...𝑀) ∈ Fin)
48	8	ad2antrr 762	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ)
49	44	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
50		fz1ssfz0 39524	. . . . . . . . . 10 ⊢ (1...𝑀) ⊆ (0...𝑀)
51	50	sseli 3599	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (0...𝑀))
52	51	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀))
53		0zd 11389	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 0 ∈ ℤ)
54	48, 49, 52, 53	etransclem3 40454	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℤ)
55	47, 54	fprodzcl 14684	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℤ)
56	46, 55	zmulcld 11488	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) ∈ ℤ)
57	40, 56	zmulcld 11488	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ∈ ℤ)
58	57	zcnd 11483	. . 3 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ∈ ℂ)
59		nn0uz 11722	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
60	12, 59	syl6eleq 2711	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃 − 1) ∈ (ℤ_≥‘0))
61		eluzfz2 12349	. . . . . . . . . 10 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘0) → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
62	60, 61	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
63		eluzfz1 12348	. . . . . . . . . 10 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘0) → 0 ∈ (0...(𝑃 − 1)))
64	60, 63	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...(𝑃 − 1)))
65	62, 64	ifcld 4131	. . . . . . . 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 6385	. . . . . 6 ⊢ (𝜑 → 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
69		ovex 6678	. . . . . . 7 ⊢ (0...(𝑃 − 1)) ∈ V
70		ovex 6678	. . . . . . 7 ⊢ (0...𝑀) ∈ V
71	69, 70	elmap 7886	. . . . . 6 ⊢ (𝐷 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ↔ 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
72	68, 71	sylibr 224	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)))
73	9, 59	syl6eleq 2711	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
74		fzsscn 39526	. . . . . . . 8 ⊢ (0...(𝑃 − 1)) ⊆ ℂ
75	68	ffvelrnda 6359	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ (0...(𝑃 − 1)))
76	74, 75	sseldi 3601	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ ℂ)
77		fveq2 6191	. . . . . . 7 ⊢ (𝑗 = 0 → (𝐷‘𝑗) = (𝐷‘0))
78	73, 76, 77	fsum1p 14482	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = ((𝐷‘0) + Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗)))
79	67	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0)))
80		simpr 477	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 = 0) → 𝑗 = 0)
81	80	iftrued 4094	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 = 0) → if(𝑗 = 0, (𝑃 − 1), 0) = (𝑃 − 1))
82		eluzfz1 12348	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
83	73, 82	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
84	79, 81, 83, 12	fvmptd 6288	. . . . . . 7 ⊢ (𝜑 → (𝐷‘0) = (𝑃 − 1))
85		0p1e1 11132	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
86	85	oveq1i 6660	. . . . . . . . . 10 ⊢ ((0 + 1)...𝑀) = (1...𝑀)
87	86	sumeq1i 14428	. . . . . . . . 9 ⊢ Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗)
88	87	a1i 11	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗))
89	67	fvmpt2 6291	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ (0...𝑀) ∧ if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1))) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
90	51, 65, 89	syl2anr 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
91		0red 10041	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 0 ∈ ℝ)
92		1red 10055	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 1 ∈ ℝ)
93		elfzelz 12342	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℤ)
94	93	zred 11482	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℝ)
95		0lt1 10550	. . . . . . . . . . . . . . . 16 ⊢ 0 < 1
96	95	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 0 < 1)
97		elfzle1 12344	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 1 ≤ 𝑗)
98	91, 92, 94, 96, 97	ltletrd 10197	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 0 < 𝑗)
99	91, 98	gtned 10172	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ≠ 0)
100	99	neneqd 2799	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑀) → ¬ 𝑗 = 0)
101	100	iffalsed 4097	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑀) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
102	101	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
103	90, 102	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) = 0)
104	103	sumeq2dv 14433	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)0)
105		fzfi 12771	. . . . . . . . . 10 ⊢ (1...𝑀) ∈ Fin
106	105	olci 406	. . . . . . . . 9 ⊢ ((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin)
107		sumz 14453	. . . . . . . . 9 ⊢ (((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin) → Σ𝑗 ∈ (1...𝑀)0 = 0)
108	106, 107	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)0 = 0)
109	88, 104, 108	3eqtrd 2660	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = 0)
110	84, 109	oveq12d 6668	. . . . . 6 ⊢ (𝜑 → ((𝐷‘0) + Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗)) = ((𝑃 − 1) + 0))
111	8	nncnd 11036	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℂ)
112		1cnd 10056	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
113	111, 112	subcld 10392	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 1) ∈ ℂ)
114	113	addid1d 10236	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 1) + 0) = (𝑃 − 1))
115	78, 110, 114	3eqtrd 2660	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = (𝑃 − 1))
116		fveq1 6190	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → (𝑐‘𝑗) = (𝐷‘𝑗))
117	116	sumeq2ad 14434	. . . . . . 7 ⊢ (𝑐 = 𝐷 → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗))
118	117	eqeq1d 2624	. . . . . 6 ⊢ (𝑐 = 𝐷 → (Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1) ↔ Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = (𝑃 − 1)))
119	118	elrab 3363	. . . . 5 ⊢ (𝐷 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)} ↔ (𝐷 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = (𝑃 − 1)))
120	72, 115, 119	sylanbrc 698	. . . 4 ⊢ (𝜑 → 𝐷 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_𝑚 (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
121	120, 21	eleqtrrd 2704	. . 3 ⊢ (𝜑 → 𝐷 ∈ (𝐶‘(𝑃 − 1)))
122	116	fveq2d 6195	. . . . . 6 ⊢ (𝑐 = 𝐷 → (!‘(𝑐‘𝑗)) = (!‘(𝐷‘𝑗)))
123	122	prodeq2ad 39824	. . . . 5 ⊢ (𝑐 = 𝐷 → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) = ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)))
124	123	oveq2d 6666	. . . 4 ⊢ (𝑐 = 𝐷 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) = ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))))
125		fveq1 6190	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (𝑐‘0) = (𝐷‘0))
126	125	breq2d 4665	. . . . . 6 ⊢ (𝑐 = 𝐷 → ((𝑃 − 1) < (𝑐‘0) ↔ (𝑃 − 1) < (𝐷‘0)))
127	125	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑐 = 𝐷 → ((𝑃 − 1) − (𝑐‘0)) = ((𝑃 − 1) − (𝐷‘0)))
128	127	fveq2d 6195	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → (!‘((𝑃 − 1) − (𝑐‘0))) = (!‘((𝑃 − 1) − (𝐷‘0))))
129	128	oveq2d 6666	. . . . . . 7 ⊢ (𝑐 = 𝐷 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) = ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))))
130	127	oveq2d 6666	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (0↑((𝑃 − 1) − (𝑐‘0))) = (0↑((𝑃 − 1) − (𝐷‘0))))
131	129, 130	oveq12d 6668	. . . . . 6 ⊢ (𝑐 = 𝐷 → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))))
132	126, 131	ifbieq2d 4111	. . . . 5 ⊢ (𝑐 = 𝐷 → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))))
133	116	breq2d 4665	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (𝑃 < (𝑐‘𝑗) ↔ 𝑃 < (𝐷‘𝑗)))
134	116	oveq2d 6666	. . . . . . . . . 10 ⊢ (𝑐 = 𝐷 → (𝑃 − (𝑐‘𝑗)) = (𝑃 − (𝐷‘𝑗)))
135	134	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑐 = 𝐷 → (!‘(𝑃 − (𝑐‘𝑗))) = (!‘(𝑃 − (𝐷‘𝑗))))
136	135	oveq2d 6666	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → ((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) = ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))))
137	134	oveq2d 6666	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))) = ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))
138	136, 137	oveq12d 6668	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))) = (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))
139	133, 138	ifbieq2d 4111	. . . . . 6 ⊢ (𝑐 = 𝐷 → if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) = if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))
140	139	prodeq2ad 39824	. . . . 5 ⊢ (𝑐 = 𝐷 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) = ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))
141	132, 140	oveq12d 6668	. . . 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 6668	. . 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 39804	. 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	sseldi 3601	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ ℕ₀)
145	144	faccld 13071	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐷‘𝑗)) ∈ ℕ)
146	145	nncnd 11036	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐷‘𝑗)) ∈ ℂ)
147	77	fveq2d 6195	. . . . . . . . . 10 ⊢ (𝑗 = 0 → (!‘(𝐷‘𝑗)) = (!‘(𝐷‘0)))
148	73, 146, 147	fprod1p 14698	. . . . . . . . 9 ⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)) = ((!‘(𝐷‘0)) · ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗))))
149	84	fveq2d 6195	. . . . . . . . . 10 ⊢ (𝜑 → (!‘(𝐷‘0)) = (!‘(𝑃 − 1)))
150	86	prodeq1i 14648	. . . . . . . . . . . 12 ⊢ ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗))
151	150	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗)))
152	103	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝐷‘𝑗)) = (!‘0))
153		fac0 13063	. . . . . . . . . . . . 13 ⊢ (!‘0) = 1
154	152, 153	syl6eq 2672	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝐷‘𝑗)) = 1)
155	154	prodeq2dv 14653	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)1)
156		prod1 14674	. . . . . . . . . . . 12 ⊢ (((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin) → ∏𝑗 ∈ (1...𝑀)1 = 1)
157	106, 156	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)1 = 1)
158	151, 155, 157	3eqtrd 2660	. . . . . . . . . 10 ⊢ (𝜑 → ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = 1)
159	149, 158	oveq12d 6668	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝐷‘0)) · ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗))) = ((!‘(𝑃 − 1)) · 1))
160	12	faccld 13071	. . . . . . . . . . 11 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
161	160	nncnd 11036	. . . . . . . . . 10 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
162	161	mulid1d 10057	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · 1) = (!‘(𝑃 − 1)))
163	148, 159, 162	3eqtrd 2660	. . . . . . . 8 ⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)) = (!‘(𝑃 − 1)))
164	163	oveq2d 6666	. . . . . . 7 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) = ((!‘(𝑃 − 1)) / (!‘(𝑃 − 1))))
165	160	nnne0d 11065	. . . . . . . 8 ⊢ (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
166	161, 165	dividd 10799	. . . . . . 7 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘(𝑃 − 1))) = 1)
167	164, 166	eqtrd 2656	. . . . . 6 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) = 1)
168	12	nn0red 11352	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 − 1) ∈ ℝ)
169	84, 168	eqeltrd 2701	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘0) ∈ ℝ)
170	169, 168	lttri3d 10177	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘0) = (𝑃 − 1) ↔ (¬ (𝐷‘0) < (𝑃 − 1) ∧ ¬ (𝑃 − 1) < (𝐷‘0))))
171	84, 170	mpbid 222	. . . . . . . . . 10 ⊢ (𝜑 → (¬ (𝐷‘0) < (𝑃 − 1) ∧ ¬ (𝑃 − 1) < (𝐷‘0)))
172	171	simprd 479	. . . . . . . . 9 ⊢ (𝜑 → ¬ (𝑃 − 1) < (𝐷‘0))
173	172	iffalsed 4097	. . . . . . . 8 ⊢ (𝜑 → if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))))
174	84	eqcomd 2628	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 − 1) = (𝐷‘0))
175	113, 174	subeq0bd 10456	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑃 − 1) − (𝐷‘0)) = 0)
176	175	fveq2d 6195	. . . . . . . . . . . 12 ⊢ (𝜑 → (!‘((𝑃 − 1) − (𝐷‘0))) = (!‘0))
177	176, 153	syl6eq 2672	. . . . . . . . . . 11 ⊢ (𝜑 → (!‘((𝑃 − 1) − (𝐷‘0))) = 1)
178	177	oveq2d 6666	. . . . . . . . . 10 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) = ((!‘(𝑃 − 1)) / 1))
179	161	div1d 10793	. . . . . . . . . 10 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / 1) = (!‘(𝑃 − 1)))
180	178, 179	eqtrd 2656	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) = (!‘(𝑃 − 1)))
181	175	oveq2d 6666	. . . . . . . . . 10 ⊢ (𝜑 → (0↑((𝑃 − 1) − (𝐷‘0))) = (0↑0))
182		0cnd 10033	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℂ)
183	182	exp0d 13002	. . . . . . . . . 10 ⊢ (𝜑 → (0↑0) = 1)
184	181, 183	eqtrd 2656	. . . . . . . . 9 ⊢ (𝜑 → (0↑((𝑃 − 1) − (𝐷‘0))) = 1)
185	180, 184	oveq12d 6668	. . . . . . . 8 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))) = ((!‘(𝑃 − 1)) · 1))
186	173, 185, 162	3eqtrd 2660	. . . . . . 7 ⊢ (𝜑 → if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) = (!‘(𝑃 − 1)))
187		fzssre 39529	. . . . . . . . . . . 12 ⊢ (0...(𝑃 − 1)) ⊆ ℝ
188	68	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
189	51	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀))
190	188, 189	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ∈ (0...(𝑃 − 1)))
191	187, 190	sseldi 3601	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ∈ ℝ)
192	8	nnred 11035	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℝ)
193	192	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℝ)
194	8	nngt0d 11064	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 𝑃)
195	15, 192, 194	ltled 10185	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ 𝑃)
196	195	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 0 ≤ 𝑃)
197	103, 196	eqbrtrd 4675	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ≤ 𝑃)
198	191, 193, 197	lensymd 10188	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ¬ 𝑃 < (𝐷‘𝑗))
199	198	iffalsed 4097	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))
200	103	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐷‘𝑗)) = (𝑃 − 0))
201	111	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℂ)
202	201	subid1d 10381	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − 0) = 𝑃)
203	200, 202	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐷‘𝑗)) = 𝑃)
204	203	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝑃 − (𝐷‘𝑗))) = (!‘𝑃))
205	204	oveq2d 6666	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) = ((!‘𝑃) / (!‘𝑃)))
206	8	nnnn0d 11351	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
207	206	faccld 13071	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (!‘𝑃) ∈ ℕ)
208	207	nncnd 11036	. . . . . . . . . . . . 13 ⊢ (𝜑 → (!‘𝑃) ∈ ℂ)
209	207	nnne0d 11065	. . . . . . . . . . . . 13 ⊢ (𝜑 → (!‘𝑃) ≠ 0)
210	208, 209	dividd 10799	. . . . . . . . . . . 12 ⊢ (𝜑 → ((!‘𝑃) / (!‘𝑃)) = 1)
211	210	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘𝑃)) = 1)
212	205, 211	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) = 1)
213		df-neg 10269	. . . . . . . . . . . . 13 ⊢ -𝑗 = (0 − 𝑗)
214	213	eqcomi 2631	. . . . . . . . . . . 12 ⊢ (0 − 𝑗) = -𝑗
215	214	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (0 − 𝑗) = -𝑗)
216	215, 203	oveq12d 6668	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))) = (-𝑗↑𝑃))
217	212, 216	oveq12d 6668	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))) = (1 · (-𝑗↑𝑃)))
218	93	znegcld 11484	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℤ)
219	218	zcnd 11483	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℂ)
220	219	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → -𝑗 ∈ ℂ)
221	206	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ₀)
222	220, 221	expcld 13008	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (-𝑗↑𝑃) ∈ ℂ)
223	222	mulid2d 10058	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1 · (-𝑗↑𝑃)) = (-𝑗↑𝑃))
224	199, 217, 223	3eqtrd 2660	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = (-𝑗↑𝑃))
225	224	prodeq2dv 14653	. . . . . . 7 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))
226	186, 225	oveq12d 6668	. . . . . 6 ⊢ (𝜑 → (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
227	167, 226	oveq12d 6668	. . . . 5 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) = (1 · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))))
228		fzfid 12772	. . . . . . . . 9 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
229		zexpcl 12875	. . . . . . . . . 10 ⊢ ((-𝑗 ∈ ℤ ∧ 𝑃 ∈ ℕ₀) → (-𝑗↑𝑃) ∈ ℤ)
230	218, 206, 229	syl2anr 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (-𝑗↑𝑃) ∈ ℤ)
231	228, 230	fprodzcl 14684	. . . . . . . 8 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) ∈ ℤ)
232	231	zcnd 11483	. . . . . . 7 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) ∈ ℂ)
233	161, 232	mulcld 10060	. . . . . 6 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) ∈ ℂ)
234	233	mulid2d 10058	. . . . 5 ⊢ (𝜑 → (1 · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
235	227, 234	eqtrd 2656	. . . 4 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
236		eldifi 3732	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → 𝑐 ∈ (𝐶‘(𝑃 − 1)))
237	83	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ∈ (0...𝑀))
238	44, 237	ffvelrnd 6360	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑐‘0) ∈ (0...(𝑃 − 1)))
239	236, 238	sylan2 491	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ (0...(𝑃 − 1)))
240	187, 239	sseldi 3601	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ ℝ)
241	168	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ∈ ℝ)
242		elfzle2 12345	. . . . . . . . . . . . . 14 ⊢ ((𝑐‘0) ∈ (0...(𝑃 − 1)) → (𝑐‘0) ≤ (𝑃 − 1))
243	239, 242	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ≤ (𝑃 − 1))
244	240, 241, 243	lensymd 10188	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ¬ (𝑃 − 1) < (𝑐‘0))
245	244	iffalsed 4097	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))))
246	12	nn0zd 11480	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − 1) ∈ ℤ)
247	246	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ∈ ℤ)
248	239	elfzelzd 39530	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ ℤ)
249	247, 248	zsubcld 11487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℤ)
250		ffn 6045	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐:(0...𝑀)⟶(0...(𝑃 − 1)) → 𝑐 Fn (0...𝑀))
251	44, 250	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 Fn (0...𝑀))
252	251	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 Fn (0...𝑀))
253		ffn 6045	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷:(0...𝑀)⟶(0...(𝑃 − 1)) → 𝐷 Fn (0...𝑀))
254	68, 253	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 Fn (0...𝑀))
255	254	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝐷 Fn (0...𝑀))
256		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 0 → (𝑐‘𝑗) = (𝑐‘0))
257	256	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝑐‘0))
258		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 − 1) = (𝑐‘0) → (𝑃 − 1) = (𝑐‘0))
259	258	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑃 − 1) = (𝑐‘0) → (𝑐‘0) = (𝑃 − 1))
260	259	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘0) = (𝑃 − 1))
261	77	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝐷‘𝑗) = (𝐷‘0))
262	84	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝐷‘0) = (𝑃 − 1))
263	261, 262	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝑃 − 1) = (𝐷‘𝑗))
264	263	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑃 − 1) = (𝐷‘𝑗))
265	257, 260, 264	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
266	265	adantllr 755	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
267	266	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
268	26	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
269	168	ad5antr 770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) ∈ ℝ)
270	168	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) ∈ ℝ)
271	44	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
272	50	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ (0...𝑀))
273	272	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (0...𝑀))
274	271, 273	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ (0...(𝑃 − 1)))
275	33, 274	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℕ₀)
276	47, 275	fsumnn0cl 14467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℕ₀)
277	276	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ)
278	277	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ)
279		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 ∈ ℝ)
280	44	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ (0...(𝑃 − 1)))
281	187, 280	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℝ)
282	281	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ∈ ℝ)
283		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0)
284		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘(𝑐‘𝑗)
285		fzfid 12772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (1...𝑀) ∈ Fin)
286		simp-4l 806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (1...𝑀)) → (𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))))
287	74, 274	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
288	286, 287	sylancom 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
289		1zzd 11408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 1 ∈ ℤ)
290		elfzel2 12340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
291	290	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑀 ∈ ℤ)
292		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
293	292	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℤ)
294	289, 291, 293	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → (1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ))
295		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
296	295	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℕ₀)
297		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (¬ 𝑗 = 0 → 𝑗 ≠ 0)
298	297	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ≠ 0)
299		elnnne0 11306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑗 ∈ ℕ ↔ (𝑗 ∈ ℕ₀ ∧ 𝑗 ≠ 0))
300	296, 298, 299	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℕ)
301	300	nnge1d 11063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 1 ≤ 𝑗)
302		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
303	302	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ≤ 𝑀)
304	294, 301, 303	jca32 558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ) ∧ (1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀)))
305		elfz2 12333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑗 ∈ (1...𝑀) ↔ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ) ∧ (1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀)))
306	304, 305	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ (1...𝑀))
307	306	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑗 ∈ (1...𝑀))
308	307	adantlll 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑗 ∈ (1...𝑀))
309		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 = 𝑗 → (𝑐‘𝑘) = (𝑐‘𝑗))
310	283, 284, 285, 288, 308, 309	fsumsplit1 39804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) = ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
311	310	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
312	311, 278	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)) ∈ ℝ)
313		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑐‘𝑗) ∈ (0...(𝑃 − 1)) → 0 ≤ (𝑐‘𝑗))
314	280, 313	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ (𝑐‘𝑗))
315	314	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 ≤ (𝑐‘𝑗))
316		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ (𝑐‘𝑗) = 0 → (𝑐‘𝑗) ≠ 0)
317	316	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ≠ 0)
318	279, 282, 315, 317	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < (𝑐‘𝑗))
319		diffi 8192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((1...𝑀) ∈ Fin → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
320	105, 319	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
321		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑘 ∈ ((1...𝑀) ∖ {𝑗}) → 𝑘 ∈ (1...𝑀))
322	321	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑘 ∈ (1...𝑀))
323	50, 322	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑘 ∈ (0...𝑀))
324	44	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ (0...(𝑃 − 1)))
325	187, 324	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℝ)
326	323, 325	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → (𝑐‘𝑘) ∈ ℝ)
327		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑐‘𝑘) ∈ (0...(𝑃 − 1)) → 0 ≤ (𝑐‘𝑘))
328	324, 327	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → 0 ≤ (𝑐‘𝑘))
329	323, 328	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 0 ≤ (𝑐‘𝑘))
330	320, 326, 329	fsumge0 14527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))
331	330	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))
332	320, 326	fsumrecl 14465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ∈ ℝ)
333	332	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ∈ ℝ)
334	281, 333	addge01d 10615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ↔ (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))))
335	331, 334	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
336	335	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
337	279, 282, 312, 318, 336	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
338	337, 311	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
339	278, 338	elrpd 11869	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ⁺)
340	270, 339	ltaddrpd 11905	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
341	340	adantlllr 39199	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
342		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = 𝑘 → (𝑐‘𝑗) = (𝑐‘𝑘))
343	342	cbvsumv 14426	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘)
344	343	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘))
345	73	ad5antr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑀 ∈ (ℤ_≥‘0))
346		simp-5l 808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (0...𝑀)) → (𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))))
347	74, 324	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
348	346, 347	sylancom 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
349		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 0 → (𝑐‘𝑘) = (𝑐‘0))
350	345, 348, 349	fsum1p 14482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘) = ((𝑐‘0) + Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘)))
351	259	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘0) = (𝑃 − 1))
352	86	sumeq1i 14428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)
353	352	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
354	351, 353	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘0) + Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘)) = ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
355	344, 350, 354	3eqtrrd 2661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)) = Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
356	341, 355	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
357	269, 356	gtned 10172	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) ≠ (𝑃 − 1))
358	357	neneqd 2799	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ¬ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
359	268, 358	condan 835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝑐‘𝑗) = 0)
360		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0...𝑀))
361	33, 66	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) ∈ ℕ₀)
362	67	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ if(𝑗 = 0, (𝑃 − 1), 0) ∈ ℕ₀) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
363	360, 361, 362	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
364	363	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
365		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → ¬ 𝑗 = 0)
366	365	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
367	364, 366	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
368	367	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
369	368	adantllr 755	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
370	359, 369	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
371	267, 370	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) = (𝐷‘𝑗))
372	252, 255, 371	eqfnfvd 6314	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 = 𝐷)
373	236, 372	sylanl2 683	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 = 𝐷)
374		eldifsni 4320	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → 𝑐 ≠ 𝐷)
375	374	neneqd 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → ¬ 𝑐 = 𝐷)
376	375	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ (𝑃 − 1) = (𝑐‘0)) → ¬ 𝑐 = 𝐷)
377	373, 376	pm2.65da 600	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ¬ (𝑃 − 1) = (𝑐‘0))
378	377	neqned 2801	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ≠ (𝑐‘0))
379	240, 241, 243, 378	leneltd 10191	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) < (𝑃 − 1))
380	240, 241	posdifd 10614	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑐‘0) < (𝑃 − 1) ↔ 0 < ((𝑃 − 1) − (𝑐‘0))))
381	379, 380	mpbid 222	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → 0 < ((𝑃 − 1) − (𝑐‘0)))
382		elnnz 11387	. . . . . . . . . . . . . 14 ⊢ (((𝑃 − 1) − (𝑐‘0)) ∈ ℕ ↔ (((𝑃 − 1) − (𝑐‘0)) ∈ ℤ ∧ 0 < ((𝑃 − 1) − (𝑐‘0))))
383	249, 381, 382	sylanbrc 698	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℕ)
384	383	0expd 13024	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0↑((𝑃 − 1) − (𝑐‘0))) = 0)
385	384	oveq2d 6666	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · 0))
386	161	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘(𝑃 − 1)) ∈ ℂ)
387	383	nnnn0d 11351	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℕ₀)
388	387	faccld 13071	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ∈ ℕ)
389	388	nncnd 11036	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ∈ ℂ)
390	388	nnne0d 11065	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ≠ 0)
391	386, 389, 390	divcld 10801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) ∈ ℂ)
392	391	mul01d 10235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · 0) = 0)
393	245, 385, 392	3eqtrd 2660	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = 0)
394	393	oveq1d 6665	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) = (0 · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))
395	236, 55	sylan2 491	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℤ)
396	395	zcnd 11483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℂ)
397	396	mul02d 10234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0 · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) = 0)
398	394, 397	eqtrd 2656	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) = 0)
399	398	oveq2d 6666	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · 0))
400		fzfid 12772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0...𝑀) ∈ Fin)
401	33, 280	sseldi 3601	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℕ₀)
402	236, 401	sylanl2 683	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℕ₀)
403	402	faccld 13071	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝑐‘𝑗)) ∈ ℕ)
404	400, 403	fprodnncl 14685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ∈ ℕ)
405	404	nncnd 11036	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ∈ ℂ)
406	404	nnne0d 11065	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ≠ 0)
407	386, 405, 406	divcld 10801	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℂ)
408	407	mul01d 10235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · 0) = 0)
409	399, 408	eqtrd 2656	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = 0)
410	409	sumeq2dv 14433	. . . . 5 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0)
411		diffi 8192	. . . . . . . 8 ⊢ ((𝐶‘(𝑃 − 1)) ∈ Fin → ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin)
412	19, 411	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin)
413	412	olcd 408	. . . . . 6 ⊢ (𝜑 → (((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ⊆ (ℤ_≥‘0) ∨ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin))
414		sumz 14453	. . . . . 6 ⊢ ((((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ⊆ (ℤ_≥‘0) ∨ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin) → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0 = 0)
415	413, 414	syl 17	. . . . 5 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0 = 0)
416	410, 415	eqtrd 2656	. . . 4 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = 0)
417	235, 416	oveq12d 6668	. . 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))
418	233	addid1d 10236	. . 3 ⊢ (𝜑 → (((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) + 0) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
419		nfv 1843	. . . . 5 ⊢ Ⅎ𝑗𝜑
420	419, 206, 228, 220	fprodexp 39826	. . . 4 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) = (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃))
421	420	oveq2d 6666	. . 3 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)))
422	417, 418, 421	3eqtrd 2660	. 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...𝑀)-𝑗↑𝑃)))
423	16, 143, 422	3eqtrd 2660	1 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑃 − 1))‘0) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 {crab 2916 Vcvv 3200 ∖ cdif 3571 ⊆ wss 3574 ifcif 4086 {csn 4177 {cpr 4179 class class class wbr 4653 ↦ cmpt 4729 ran crn 5115 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ↑_𝑚 cmap 7857 Fincfn 7955 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 -cneg 10267 / cdiv 10684 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 (,)cioo 12175 ...cfz 12326 ↑cexp 12860 !cfa 13060 Σcsu 14416 ∏cprod 14635 ↾_t crest 16081 TopOpenctopn 16082 topGenctg 16098 ℂ_fldccnfld 19746 D^𝑛 cdvn 23628

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-prod 14636 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-dvn 23632

This theorem is referenced by: etransclem41 40492

W3C validator