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 46225

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 11245	. . . 4 ⊢ ℝ ∈ {ℝ, ℂ}
2	1	a1i 11	. . 3 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
3		reopn 45240	. . . . 5 ⊢ ℝ ∈ (topGen‘ran (,))
4		eqid 2735	. . . . . 6 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
5	4	tgioo2 24839	. . . . 5 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
6	3, 5	eleqtri 2837	. . . 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 12565	. . . 4 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
12	8, 11	syl 17	. . 3 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
13		etransclem5 46195	. . 3 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
14		etransclem35.c	. . 3 ⊢ 𝐶 = (𝑛 ∈ ℕ₀ ↦ {𝑐 ∈ ((0...𝑛) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛})
15		0red 11262	. . 3 ⊢ (𝜑 → 0 ∈ ℝ)
16	2, 7, 8, 9, 10, 12, 13, 14, 15	etransclem31 46221	. 2 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑃 − 1))‘0) = Σ𝑐 ∈ (𝐶‘(𝑃 − 1))(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))))
17		nfv 1912	. . 3 ⊢ Ⅎ𝑐𝜑
18		nfcv 2903	. . 3 ⊢ Ⅎ𝑐(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))))
19	14, 12	etransclem16 46206	. . 3 ⊢ (𝜑 → (𝐶‘(𝑃 − 1)) ∈ Fin)
20		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ (𝐶‘(𝑃 − 1)))
21	14, 12	etransclem12 46202	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶‘(𝑃 − 1)) = {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
22	21	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝐶‘(𝑃 − 1)) = {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
23	20, 22	eleqtrd 2841	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)})
24		rabid 3455	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)} ↔ (𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)))
25	23, 24	sylib 218	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1)))
26	25	simprd 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
27	26	eqcomd 2741	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑃 − 1) = Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
28	27	fveq2d 6911	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (!‘(𝑃 − 1)) = (!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)))
29	28	oveq1d 7446	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) = ((!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))))
30		nfcv 2903	. . . . . . . 8 ⊢ Ⅎ𝑗𝑐
31		fzfid 14011	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (0...𝑀) ∈ Fin)
32		nn0ex 12530	. . . . . . . . . 10 ⊢ ℕ₀ ∈ V
33		fzssnn0 45268	. . . . . . . . . 10 ⊢ (0...(𝑃 − 1)) ⊆ ℕ₀
34		mapss 8928	. . . . . . . . . 10 ⊢ ((ℕ₀ ∈ V ∧ (0...(𝑃 − 1)) ⊆ ℕ₀) → ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ⊆ (ℕ₀ ↑_m (0...𝑀)))
35	32, 33, 34	mp2an 692	. . . . . . . . 9 ⊢ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ⊆ (ℕ₀ ↑_m (0...𝑀))
36	25	simpld 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)))
37	35, 36	sselid 3993	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ (ℕ₀ ↑_m (0...𝑀)))
38	30, 31, 37	mccl 45554	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℕ)
39	29, 38	eqeltrd 2839	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℕ)
40	39	nnzd 12638	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℤ)
41	8	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑃 ∈ ℕ)
42	9	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑀 ∈ ℕ₀)
43		elmapi 8888	. . . . . . . 8 ⊢ (𝑐 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
44	36, 43	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
45		0zd 12623	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ∈ ℤ)
46	41, 42, 44, 45	etransclem10 46200	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) ∈ ℤ)
47		fzfid 14011	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (1...𝑀) ∈ Fin)
48	8	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ)
49	44	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
50		fz1ssfz0 13660	. . . . . . . . . 10 ⊢ (1...𝑀) ⊆ (0...𝑀)
51	50	sseli 3991	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (0...𝑀))
52	51	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀))
53		0zd 12623	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 0 ∈ ℤ)
54	48, 49, 52, 53	etransclem3 46193	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℤ)
55	47, 54	fprodzcl 15987	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℤ)
56	46, 55	zmulcld 12726	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) ∈ ℤ)
57	40, 56	zmulcld 12726	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ∈ ℤ)
58	57	zcnd 12721	. . 3 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ∈ ℂ)
59		nn0uz 12918	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
60	12, 59	eleqtrdi 2849	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃 − 1) ∈ (ℤ_≥‘0))
61		eluzfz2 13569	. . . . . . . . . 10 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘0) → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
62	60, 61	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
63		eluzfz1 13568	. . . . . . . . . 10 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘0) → 0 ∈ (0...(𝑃 − 1)))
64	60, 63	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...(𝑃 − 1)))
65	62, 64	ifcld 4577	. . . . . . . 8 ⊢ (𝜑 → if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1)))
66	65	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1)))
67		etransclem35.d	. . . . . . 7 ⊢ 𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0))
68	66, 67	fmptd 7134	. . . . . 6 ⊢ (𝜑 → 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
69		ovex 7464	. . . . . . 7 ⊢ (0...(𝑃 − 1)) ∈ V
70		ovex 7464	. . . . . . 7 ⊢ (0...𝑀) ∈ V
71	69, 70	elmap 8910	. . . . . 6 ⊢ (𝐷 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)) ↔ 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
72	68, 71	sylibr 234	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ ((0...(𝑃 − 1)) ↑_m (0...𝑀)))
73	9, 59	eleqtrdi 2849	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
74		fzsscn 45262	. . . . . . . 8 ⊢ (0...(𝑃 − 1)) ⊆ ℂ
75	68	ffvelcdmda 7104	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ (0...(𝑃 − 1)))
76	74, 75	sselid 3993	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ ℂ)
77		fveq2 6907	. . . . . . 7 ⊢ (𝑗 = 0 → (𝐷‘𝑗) = (𝐷‘0))
78	73, 76, 77	fsum1p 15786	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = ((𝐷‘0) + Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗)))
79	67	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0)))
80		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 = 0) → 𝑗 = 0)
81	80	iftrued 4539	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 = 0) → if(𝑗 = 0, (𝑃 − 1), 0) = (𝑃 − 1))
82		eluzfz1 13568	. . . . . . . . 9 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
83	73, 82	syl 17	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
84	79, 81, 83, 12	fvmptd 7023	. . . . . . 7 ⊢ (𝜑 → (𝐷‘0) = (𝑃 − 1))
85		0p1e1 12386	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
86	85	oveq1i 7441	. . . . . . . . . 10 ⊢ ((0 + 1)...𝑀) = (1...𝑀)
87	86	sumeq1i 15730	. . . . . . . . 9 ⊢ Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗)
88	87	a1i 11	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗))
89	67	fvmpt2 7027	. . . . . . . . . . 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 11262	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 0 ∈ ℝ)
92		1red 11260	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 1 ∈ ℝ)
93		elfzelz 13561	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℤ)
94	93	zred 12720	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℝ)
95		0lt1 11783	. . . . . . . . . . . . . . . 16 ⊢ 0 < 1
96	95	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 0 < 1)
97		elfzle1 13564	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 1 ≤ 𝑗)
98	91, 92, 94, 96, 97	ltletrd 11419	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 0 < 𝑗)
99	91, 98	gtned 11394	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ≠ 0)
100	99	neneqd 2943	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑀) → ¬ 𝑗 = 0)
101	100	iffalsed 4542	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑀) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
102	101	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
103	90, 102	eqtrd 2775	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) = 0)
104	103	sumeq2dv 15735	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐷‘𝑗) = Σ𝑗 ∈ (1...𝑀)0)
105		fzfi 14010	. . . . . . . . . 10 ⊢ (1...𝑀) ∈ Fin
106	105	olci 866	. . . . . . . . 9 ⊢ ((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin)
107		sumz 15755	. . . . . . . . 9 ⊢ (((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin) → Σ𝑗 ∈ (1...𝑀)0 = 0)
108	106, 107	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)0 = 0)
109	88, 104, 108	3eqtrd 2779	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗) = 0)
110	84, 109	oveq12d 7449	. . . . . 6 ⊢ (𝜑 → ((𝐷‘0) + Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷‘𝑗)) = ((𝑃 − 1) + 0))
111	8	nncnd 12280	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℂ)
112		1cnd 11254	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℂ)
113	111, 112	subcld 11618	. . . . . . 7 ⊢ (𝜑 → (𝑃 − 1) ∈ ℂ)
114	113	addridd 11459	. . . . . 6 ⊢ (𝜑 → ((𝑃 − 1) + 0) = (𝑃 − 1))
115	78, 110, 114	3eqtrd 2779	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = (𝑃 − 1))
116		fveq1 6906	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → (𝑐‘𝑗) = (𝐷‘𝑗))
117	116	sumeq2sdv 15736	. . . . . . 7 ⊢ (𝑐 = 𝐷 → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗))
118	117	eqeq1d 2737	. . . . . 6 ⊢ (𝑐 = 𝐷 → (Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1) ↔ Σ𝑗 ∈ (0...𝑀)(𝐷‘𝑗) = (𝑃 − 1)))
119	118	elrab 3695	. . . . 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 2842	. . 3 ⊢ (𝜑 → 𝐷 ∈ (𝐶‘(𝑃 − 1)))
122	116	fveq2d 6911	. . . . . 6 ⊢ (𝑐 = 𝐷 → (!‘(𝑐‘𝑗)) = (!‘(𝐷‘𝑗)))
123	122	prodeq2ad 45548	. . . . 5 ⊢ (𝑐 = 𝐷 → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) = ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)))
124	123	oveq2d 7447	. . . 4 ⊢ (𝑐 = 𝐷 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) = ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))))
125		fveq1 6906	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (𝑐‘0) = (𝐷‘0))
126	125	breq2d 5160	. . . . . 6 ⊢ (𝑐 = 𝐷 → ((𝑃 − 1) < (𝑐‘0) ↔ (𝑃 − 1) < (𝐷‘0)))
127	125	oveq2d 7447	. . . . . . . . 9 ⊢ (𝑐 = 𝐷 → ((𝑃 − 1) − (𝑐‘0)) = ((𝑃 − 1) − (𝐷‘0)))
128	127	fveq2d 6911	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → (!‘((𝑃 − 1) − (𝑐‘0))) = (!‘((𝑃 − 1) − (𝐷‘0))))
129	128	oveq2d 7447	. . . . . . 7 ⊢ (𝑐 = 𝐷 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) = ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))))
130	127	oveq2d 7447	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (0↑((𝑃 − 1) − (𝑐‘0))) = (0↑((𝑃 − 1) − (𝐷‘0))))
131	129, 130	oveq12d 7449	. . . . . 6 ⊢ (𝑐 = 𝐷 → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))))
132	126, 131	ifbieq2d 4557	. . . . 5 ⊢ (𝑐 = 𝐷 → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))))
133	116	breq2d 5160	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (𝑃 < (𝑐‘𝑗) ↔ 𝑃 < (𝐷‘𝑗)))
134	116	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝑐 = 𝐷 → (𝑃 − (𝑐‘𝑗)) = (𝑃 − (𝐷‘𝑗)))
135	134	fveq2d 6911	. . . . . . . . 9 ⊢ (𝑐 = 𝐷 → (!‘(𝑃 − (𝑐‘𝑗))) = (!‘(𝑃 − (𝐷‘𝑗))))
136	135	oveq2d 7447	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → ((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) = ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))))
137	134	oveq2d 7447	. . . . . . . 8 ⊢ (𝑐 = 𝐷 → ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))) = ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))
138	136, 137	oveq12d 7449	. . . . . . 7 ⊢ (𝑐 = 𝐷 → (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))) = (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))
139	133, 138	ifbieq2d 4557	. . . . . 6 ⊢ (𝑐 = 𝐷 → if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) = if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))
140	139	prodeq2ad 45548	. . . . 5 ⊢ (𝑐 = 𝐷 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) = ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))
141	132, 140	oveq12d 7449	. . . 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 7449	. . 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 15778	. 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 3993	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐷‘𝑗) ∈ ℕ₀)
145	144	faccld 14320	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐷‘𝑗)) ∈ ℕ)
146	145	nncnd 12280	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐷‘𝑗)) ∈ ℂ)
147	77	fveq2d 6911	. . . . . . . . . 10 ⊢ (𝑗 = 0 → (!‘(𝐷‘𝑗)) = (!‘(𝐷‘0)))
148	73, 146, 147	fprod1p 16001	. . . . . . . . 9 ⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)) = ((!‘(𝐷‘0)) · ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗))))
149	84	fveq2d 6911	. . . . . . . . . 10 ⊢ (𝜑 → (!‘(𝐷‘0)) = (!‘(𝑃 − 1)))
150	86	prodeq1i 15949	. . . . . . . . . . . 12 ⊢ ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗))
151	150	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗)))
152	103	fveq2d 6911	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝐷‘𝑗)) = (!‘0))
153		fac0 14312	. . . . . . . . . . . . 13 ⊢ (!‘0) = 1
154	152, 153	eqtrdi 2791	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝐷‘𝑗)) = 1)
155	154	prodeq2dv 15955	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(!‘(𝐷‘𝑗)) = ∏𝑗 ∈ (1...𝑀)1)
156		prod1 15977	. . . . . . . . . . . 12 ⊢ (((1...𝑀) ⊆ (ℤ_≥‘𝐴) ∨ (1...𝑀) ∈ Fin) → ∏𝑗 ∈ (1...𝑀)1 = 1)
157	106, 156	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)1 = 1)
158	151, 155, 157	3eqtrd 2779	. . . . . . . . . 10 ⊢ (𝜑 → ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗)) = 1)
159	149, 158	oveq12d 7449	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝐷‘0)) · ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷‘𝑗))) = ((!‘(𝑃 − 1)) · 1))
160	12	faccld 14320	. . . . . . . . . . 11 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
161	160	nncnd 12280	. . . . . . . . . 10 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
162	161	mulridd 11276	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · 1) = (!‘(𝑃 − 1)))
163	148, 159, 162	3eqtrd 2779	. . . . . . . 8 ⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗)) = (!‘(𝑃 − 1)))
164	163	oveq2d 7447	. . . . . . 7 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) = ((!‘(𝑃 − 1)) / (!‘(𝑃 − 1))))
165	160	nnne0d 12314	. . . . . . . 8 ⊢ (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
166	161, 165	dividd 12039	. . . . . . 7 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘(𝑃 − 1))) = 1)
167	164, 166	eqtrd 2775	. . . . . 6 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) = 1)
168	12	nn0red 12586	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 − 1) ∈ ℝ)
169	84, 168	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘0) ∈ ℝ)
170	169, 168	lttri3d 11399	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘0) = (𝑃 − 1) ↔ (¬ (𝐷‘0) < (𝑃 − 1) ∧ ¬ (𝑃 − 1) < (𝐷‘0))))
171	84, 170	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (¬ (𝐷‘0) < (𝑃 − 1) ∧ ¬ (𝑃 − 1) < (𝐷‘0)))
172	171	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → ¬ (𝑃 − 1) < (𝐷‘0))
173	172	iffalsed 4542	. . . . . . . 8 ⊢ (𝜑 → if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))))
174	84	eqcomd 2741	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 − 1) = (𝐷‘0))
175	113, 174	subeq0bd 11687	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑃 − 1) − (𝐷‘0)) = 0)
176	175	fveq2d 6911	. . . . . . . . . . . 12 ⊢ (𝜑 → (!‘((𝑃 − 1) − (𝐷‘0))) = (!‘0))
177	176, 153	eqtrdi 2791	. . . . . . . . . . 11 ⊢ (𝜑 → (!‘((𝑃 − 1) − (𝐷‘0))) = 1)
178	177	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) = ((!‘(𝑃 − 1)) / 1))
179	161	div1d 12033	. . . . . . . . . 10 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / 1) = (!‘(𝑃 − 1)))
180	178, 179	eqtrd 2775	. . . . . . . . 9 ⊢ (𝜑 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) = (!‘(𝑃 − 1)))
181	175	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝜑 → (0↑((𝑃 − 1) − (𝐷‘0))) = (0↑0))
182		0cnd 11252	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℂ)
183	182	exp0d 14177	. . . . . . . . . 10 ⊢ (𝜑 → (0↑0) = 1)
184	181, 183	eqtrd 2775	. . . . . . . . 9 ⊢ (𝜑 → (0↑((𝑃 − 1) − (𝐷‘0))) = 1)
185	180, 184	oveq12d 7449	. . . . . . . 8 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))) = ((!‘(𝑃 − 1)) · 1))
186	173, 185, 162	3eqtrd 2779	. . . . . . 7 ⊢ (𝜑 → if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) = (!‘(𝑃 − 1)))
187		fzssre 45265	. . . . . . . . . . . 12 ⊢ (0...(𝑃 − 1)) ⊆ ℝ
188	68	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
189	51	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀))
190	188, 189	ffvelcdmd 7105	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ∈ (0...(𝑃 − 1)))
191	187, 190	sselid 3993	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ∈ ℝ)
192	8	nnred 12279	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℝ)
193	192	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℝ)
194	8	nngt0d 12313	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 𝑃)
195	15, 192, 194	ltled 11407	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ 𝑃)
196	195	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 0 ≤ 𝑃)
197	103, 196	eqbrtrd 5170	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐷‘𝑗) ≤ 𝑃)
198	191, 193, 197	lensymd 11410	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ¬ 𝑃 < (𝐷‘𝑗))
199	198	iffalsed 4542	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))
200	103	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐷‘𝑗)) = (𝑃 − 0))
201	111	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℂ)
202	201	subid1d 11607	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − 0) = 𝑃)
203	200, 202	eqtrd 2775	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐷‘𝑗)) = 𝑃)
204	203	fveq2d 6911	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (!‘(𝑃 − (𝐷‘𝑗))) = (!‘𝑃))
205	204	oveq2d 7447	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) = ((!‘𝑃) / (!‘𝑃)))
206	8	nnnn0d 12585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
207	206	faccld 14320	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (!‘𝑃) ∈ ℕ)
208	207	nncnd 12280	. . . . . . . . . . . . 13 ⊢ (𝜑 → (!‘𝑃) ∈ ℂ)
209	207	nnne0d 12314	. . . . . . . . . . . . 13 ⊢ (𝜑 → (!‘𝑃) ≠ 0)
210	208, 209	dividd 12039	. . . . . . . . . . . 12 ⊢ (𝜑 → ((!‘𝑃) / (!‘𝑃)) = 1)
211	210	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘𝑃)) = 1)
212	205, 211	eqtrd 2775	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) = 1)
213		df-neg 11493	. . . . . . . . . . . . 13 ⊢ -𝑗 = (0 − 𝑗)
214	213	eqcomi 2744	. . . . . . . . . . . 12 ⊢ (0 − 𝑗) = -𝑗
215	214	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (0 − 𝑗) = -𝑗)
216	215, 203	oveq12d 7449	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))) = (-𝑗↑𝑃))
217	212, 216	oveq12d 7449	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))) = (1 · (-𝑗↑𝑃)))
218	93	znegcld 12722	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℤ)
219	218	zcnd 12721	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℂ)
220	219	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → -𝑗 ∈ ℂ)
221	206	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ₀)
222	220, 221	expcld 14183	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (-𝑗↑𝑃) ∈ ℂ)
223	222	mullidd 11277	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1 · (-𝑗↑𝑃)) = (-𝑗↑𝑃))
224	199, 217, 223	3eqtrd 2779	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = (-𝑗↑𝑃))
225	224	prodeq2dv 15955	. . . . . . 7 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))) = ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))
226	186, 225	oveq12d 7449	. . . . . 6 ⊢ (𝜑 → (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗)))))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
227	167, 226	oveq12d 7449	. . . . 5 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) = (1 · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))))
228		fzfid 14011	. . . . . . . . 9 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
229		zexpcl 14114	. . . . . . . . . 10 ⊢ ((-𝑗 ∈ ℤ ∧ 𝑃 ∈ ℕ₀) → (-𝑗↑𝑃) ∈ ℤ)
230	218, 206, 229	syl2anr 597	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (-𝑗↑𝑃) ∈ ℤ)
231	228, 230	fprodzcl 15987	. . . . . . . 8 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) ∈ ℤ)
232	231	zcnd 12721	. . . . . . 7 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) ∈ ℂ)
233	161, 232	mulcld 11279	. . . . . 6 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) ∈ ℂ)
234	233	mullidd 11277	. . . . 5 ⊢ (𝜑 → (1 · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
235	227, 234	eqtrd 2775	. . . 4 ⊢ (𝜑 → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷‘𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷‘𝑗))))))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
236		eldifi 4141	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → 𝑐 ∈ (𝐶‘(𝑃 − 1)))
237	83	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ∈ (0...𝑀))
238	44, 237	ffvelcdmd 7105	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑐‘0) ∈ (0...(𝑃 − 1)))
239	236, 238	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ (0...(𝑃 − 1)))
240	187, 239	sselid 3993	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ ℝ)
241	168	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ∈ ℝ)
242		elfzle2 13565	. . . . . . . . . . . . . 14 ⊢ ((𝑐‘0) ∈ (0...(𝑃 − 1)) → (𝑐‘0) ≤ (𝑃 − 1))
243	239, 242	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ≤ (𝑃 − 1))
244	240, 241, 243	lensymd 11410	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ¬ (𝑃 − 1) < (𝑐‘0))
245	244	iffalsed 4542	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))))
246	12	nn0zd 12637	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − 1) ∈ ℤ)
247	246	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ∈ ℤ)
248	239	elfzelzd 13562	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ ℤ)
249	247, 248	zsubcld 12725	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℤ)
250	44	ffnd 6738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 Fn (0...𝑀))
251	250	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 Fn (0...𝑀))
252	68	ffnd 6738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 Fn (0...𝑀))
253	252	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝐷 Fn (0...𝑀))
254		fveq2 6907	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 0 → (𝑐‘𝑗) = (𝑐‘0))
255	254	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝑐‘0))
256		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 − 1) = (𝑐‘0) → (𝑃 − 1) = (𝑐‘0))
257	256	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑃 − 1) = (𝑐‘0) → (𝑐‘0) = (𝑃 − 1))
258	257	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘0) = (𝑃 − 1))
259	77	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝐷‘𝑗) = (𝐷‘0))
260	84	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝐷‘0) = (𝑃 − 1))
261	259, 260	eqtr2d 2776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝑃 − 1) = (𝐷‘𝑗))
262	261	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑃 − 1) = (𝐷‘𝑗))
263	255, 258, 262	3eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
264	263	adantllr 719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
265	264	adantlr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
266	26	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
267	168	ad5antr 734	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) ∈ ℝ)
268	168	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) ∈ ℝ)
269	44	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
270	50	sseli 3991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ (0...𝑀))
271	270	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (0...𝑀))
272	269, 271	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ (0...(𝑃 − 1)))
273	33, 272	sselid 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℕ₀)
274	47, 273	fsumnn0cl 15769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℕ₀)
275	274	nn0red 12586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ)
276	275	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ)
277		0red 11262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 ∈ ℝ)
278	44	ffvelcdmda 7104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ (0...(𝑃 − 1)))
279	187, 278	sselid 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℝ)
280	279	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ∈ ℝ)
281		nfv 1912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0)
282		nfcv 2903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ Ⅎ𝑘(𝑐‘𝑗)
283		fzfid 14011	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (1...𝑀) ∈ Fin)
284		simp-4l 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (1...𝑀)) → (𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))))
285	74, 272	sselid 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
286	284, 285	sylancom 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
287		1zzd 12646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 1 ∈ ℤ)
288		elfzel2 13559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
289	288	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑀 ∈ ℤ)
290		elfzelz 13561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
291	290	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℤ)
292		elfznn0 13657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
293	292	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℕ₀)
294		neqne 2946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (¬ 𝑗 = 0 → 𝑗 ≠ 0)
295	294	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ≠ 0)
296		elnnne0 12538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑗 ∈ ℕ ↔ (𝑗 ∈ ℕ₀ ∧ 𝑗 ≠ 0))
297	293, 295, 296	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℕ)
298	297	nnge1d 12312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 1 ≤ 𝑗)
299		elfzle2 13565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
300	299	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ≤ 𝑀)
301	287, 289, 291, 298, 300	elfzd 13552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ (1...𝑀))
302	301	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑗 ∈ (1...𝑀))
303	302	adantlll 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑗 ∈ (1...𝑀))
304		fveq2 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 = 𝑗 → (𝑐‘𝑘) = (𝑐‘𝑗))
305	281, 282, 283, 286, 303, 304	fsumsplit1 15778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) = ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
306	305	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
307	306, 276	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)) ∈ ℝ)
308		elfzle1 13564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑐‘𝑗) ∈ (0...(𝑃 − 1)) → 0 ≤ (𝑐‘𝑗))
309	278, 308	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ (𝑐‘𝑗))
310	309	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 ≤ (𝑐‘𝑗))
311		neqne 2946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ (𝑐‘𝑗) = 0 → (𝑐‘𝑗) ≠ 0)
312	311	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ≠ 0)
313	277, 280, 310, 312	leneltd 11413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < (𝑐‘𝑗))
314		diffi 9214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((1...𝑀) ∈ Fin → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
315	105, 314	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
316		eldifi 4141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑘 ∈ ((1...𝑀) ∖ {𝑗}) → 𝑘 ∈ (1...𝑀))
317	316	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑘 ∈ (1...𝑀))
318	50, 317	sselid 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑘 ∈ (0...𝑀))
319	44	ffvelcdmda 7104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ (0...(𝑃 − 1)))
320	187, 319	sselid 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℝ)
321	318, 320	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → (𝑐‘𝑘) ∈ ℝ)
322		elfzle1 13564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 15828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))
326	325	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))
327	315, 321	fsumrecl 15767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ∈ ℝ)
328	327	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ∈ ℝ)
329	279, 328	addge01d 11849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘) ↔ (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘))))
330	326, 329	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
331	330	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘𝑗) ≤ ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
332	277, 280, 307, 313, 331	ltletrd 11419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < ((𝑐‘𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐‘𝑘)))
333	332, 306	breqtrd 5174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 0 < Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
334	276, 333	elrpd 13072	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘) ∈ ℝ⁺)
335	268, 334	ltaddrpd 13108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
336	335	adantl3r 750	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
337		fveq2 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = 𝑘 → (𝑐‘𝑗) = (𝑐‘𝑘))
338	337	cbvsumv 15729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘)
339	338	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘))
340	73	ad5antr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → 𝑀 ∈ (ℤ_≥‘0))
341		simp-5l 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (0...𝑀)) → (𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))))
342	74, 319	sselid 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
343	341, 342	sylancom 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℂ)
344		fveq2 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 0 → (𝑐‘𝑘) = (𝑐‘0))
345	340, 343, 344	fsum1p 15786	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘) = ((𝑐‘0) + Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘)))
346	257	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑐‘0) = (𝑃 − 1))
347	86	sumeq1i 15730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)
348	347	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘) = Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘))
349	346, 348	oveq12d 7449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑐‘0) + Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐‘𝑘)) = ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)))
350	339, 345, 349	3eqtrrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐‘𝑘)) = Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
351	336, 350	breqtrd 5174	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → (𝑃 − 1) < Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗))
352	267, 351	gtned 11394	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) ≠ (𝑃 − 1))
353	352	neneqd 2943	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐‘𝑗) = 0) → ¬ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = (𝑃 − 1))
354	266, 353	condan 818	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝑐‘𝑗) = 0)
355		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0...𝑀))
356	33, 66	sselid 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) ∈ ℕ₀)
357	67	fvmpt2 7027	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝐷‘𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
360		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → ¬ 𝑗 = 0)
361	360	iffalsed 4542	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
362	359, 361	eqtr2d 2776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
363	362	adantllr 719	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
364	363	adantllr 719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷‘𝑗))
365	354, 364	eqtrd 2775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝑐‘𝑗) = (𝐷‘𝑗))
366	265, 365	pm2.61dan 813	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) = (𝐷‘𝑗))
367	251, 253, 366	eqfnfvd 7054	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 = 𝐷)
368	236, 367	sylanl2 681	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 = 𝐷)
369		eldifsni 4795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → 𝑐 ≠ 𝐷)
370	369	neneqd 2943	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → ¬ 𝑐 = 𝐷)
371	370	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ (𝑃 − 1) = (𝑐‘0)) → ¬ 𝑐 = 𝐷)
372	368, 371	pm2.65da 817	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ¬ (𝑃 − 1) = (𝑐‘0))
373	372	neqned 2945	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ≠ (𝑐‘0))
374	240, 241, 243, 373	leneltd 11413	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) < (𝑃 − 1))
375	240, 241	posdifd 11848	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑐‘0) < (𝑃 − 1) ↔ 0 < ((𝑃 − 1) − (𝑐‘0))))
376	374, 375	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → 0 < ((𝑃 − 1) − (𝑐‘0)))
377		elnnz 12621	. . . . . . . . . . . . . 14 ⊢ (((𝑃 − 1) − (𝑐‘0)) ∈ ℕ ↔ (((𝑃 − 1) − (𝑐‘0)) ∈ ℤ ∧ 0 < ((𝑃 − 1) − (𝑐‘0))))
378	249, 376, 377	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℕ)
379	378	0expd 14176	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0↑((𝑃 − 1) − (𝑐‘0))) = 0)
380	379	oveq2d 7447	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · 0))
381	161	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘(𝑃 − 1)) ∈ ℂ)
382	378	nnnn0d 12585	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℕ₀)
383	382	faccld 14320	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ∈ ℕ)
384	383	nncnd 12280	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ∈ ℂ)
385	383	nnne0d 12314	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ≠ 0)
386	381, 384, 385	divcld 12041	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) ∈ ℂ)
387	386	mul01d 11458	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · 0) = 0)
388	245, 380, 387	3eqtrd 2779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = 0)
389	388	oveq1d 7446	. . . . . . . . 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 12721	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))) ∈ ℂ)
392	391	mul02d 11457	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0 · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) = 0)
393	389, 392	eqtrd 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))) = 0)
394	393	oveq2d 7447	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · 0))
395		fzfid 14011	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0...𝑀) ∈ Fin)
396	33, 278	sselid 3993	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℕ₀)
397	236, 396	sylanl2 681	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ ℕ₀)
398	397	faccld 14320	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝑐‘𝑗)) ∈ ℕ)
399	395, 398	fprodnncl 15988	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ∈ ℕ)
400	399	nncnd 12280	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ∈ ℂ)
401	399	nnne0d 12314	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ≠ 0)
402	381, 400, 401	divcld 12041	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℂ)
403	402	mul01d 11458	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · 0) = 0)
404	394, 403	eqtrd 2775	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = 0)
405	404	sumeq2dv 15735	. . . . 5 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0)
406		diffi 9214	. . . . . . . 8 ⊢ ((𝐶‘(𝑃 − 1)) ∈ Fin → ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin)
407	19, 406	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin)
408	407	olcd 874	. . . . . 6 ⊢ (𝜑 → (((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ⊆ (ℤ_≥‘0) ∨ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin))
409		sumz 15755	. . . . . 6 ⊢ ((((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ⊆ (ℤ_≥‘0) ∨ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin) → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0 = 0)
410	408, 409	syl 17	. . . . 5 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0 = 0)
411	405, 410	eqtrd 2775	. . . 4 ⊢ (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = 0)
412	235, 411	oveq12d 7449	. . 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	addridd 11459	. . 3 ⊢ (𝜑 → (((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) + 0) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)))
414		nfv 1912	. . . . 5 ⊢ Ⅎ𝑗𝜑
415	414, 206, 228, 220	fprodexp 45550	. . . 4 ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃) = (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃))
416	415	oveq2d 7447	. . 3 ⊢ (𝜑 → ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗↑𝑃)) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)))
417	412, 413, 416	3eqtrd 2779	. 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 2779	1 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑃 − 1))‘0) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 {crab 3433 Vcvv 3478 ∖ cdif 3960 ⊆ wss 3963 ifcif 4531 {csn 4631 {cpr 4633 class class class wbr 5148 ↦ cmpt 5231 ran crn 5690 Fn wfn 6558 ⟶wf 6559 ‘cfv 6563 (class class class)co 7431 ↑_m cmap 8865 Fincfn 8984 ℂcc 11151 ℝcr 11152 0cc0 11153 1c1 11154 + caddc 11156 · cmul 11158 < clt 11293 ≤ cle 11294 − cmin 11490 -cneg 11491 / cdiv 11918 ℕcn 12264 ℕ₀cn0 12524 ℤcz 12611 ℤ_≥cuz 12876 (,)cioo 13384 ...cfz 13544 ↑cexp 14099 !cfa 14309 Σcsu 15719 ∏cprod 15936 ↾_t crest 17467 TopOpenctopn 17468 topGenctg 17484 ℂ_fldccnfld 21382 D^𝑛 cdvn 25914

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-inf2 9679 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231 ax-addf 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-tp 4636 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-iin 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-se 5642 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-isom 6572 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8013 df-2nd 8014 df-supp 8185 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-2o 8506 df-er 8744 df-map 8867 df-pm 8868 df-ixp 8937 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-fsupp 9400 df-fi 9449 df-sup 9480 df-inf 9481 df-oi 9548 df-card 9977 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12525 df-z 12612 df-dec 12732 df-uz 12877 df-q 12989 df-rp 13033 df-xneg 13152 df-xadd 13153 df-xmul 13154 df-ioo 13388 df-ico 13390 df-icc 13391 df-fz 13545 df-fzo 13692 df-seq 14040 df-exp 14100 df-fac 14310 df-bc 14339 df-hash 14367 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272 df-clim 15521 df-sum 15720 df-prod 15937 df-struct 17181 df-sets 17198 df-slot 17216 df-ndx 17228 df-base 17246 df-ress 17275 df-plusg 17311 df-mulr 17312 df-starv 17313 df-sca 17314 df-vsca 17315 df-ip 17316 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-hom 17322 df-cco 17323 df-rest 17469 df-topn 17470 df-0g 17488 df-gsum 17489 df-topgen 17490 df-pt 17491 df-prds 17494 df-xrs 17549 df-qtop 17554 df-imas 17555 df-xps 17557 df-mre 17631 df-mrc 17632 df-acs 17634 df-mgm 18666 df-sgrp 18745 df-mnd 18761 df-submnd 18810 df-mulg 19099 df-cntz 19348 df-cmn 19815 df-psmet 21374 df-xmet 21375 df-met 21376 df-bl 21377 df-mopn 21378 df-fbas 21379 df-fg 21380 df-cnfld 21383 df-top 22916 df-topon 22933 df-topsp 22955 df-bases 22969 df-cld 23043 df-ntr 23044 df-cls 23045 df-nei 23122 df-lp 23160 df-perf 23161 df-cn 23251 df-cnp 23252 df-haus 23339 df-tx 23586 df-hmeo 23779 df-fil 23870 df-fm 23962 df-flim 23963 df-flf 23964 df-xms 24346 df-ms 24347 df-tms 24348 df-cncf 24918 df-limc 25916 df-dv 25917 df-dvn 25918

This theorem is referenced by: etransclem41 46231

W3C validator