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

Theorem etransclem35 46289
Description: 𝑃 does not divide the P-1 -th derivative of 𝐹 applied to 0. This is case 2 of the proof in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
etransclem35.p (𝜑𝑃 ∈ ℕ)
etransclem35.m (𝜑𝑀 ∈ ℕ0)
etransclem35.f 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)))
etransclem35.c 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((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.
StepHypRef Expression
1 reelprrecn 11248 . . . 4 ℝ ∈ {ℝ, ℂ}
21a1i 11 . . 3 (𝜑 → ℝ ∈ {ℝ, ℂ})
3 reopn 45306 . . . . 5 ℝ ∈ (topGen‘ran (,))
4 tgioo4 24827 . . . . 5 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
53, 4eleqtri 2838 . . . 4 ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ)
65a1i 11 . . 3 (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
7 etransclem35.p . . 3 (𝜑𝑃 ∈ ℕ)
8 etransclem35.m . . 3 (𝜑𝑀 ∈ ℕ0)
9 etransclem35.f . . 3 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)))
10 nnm1nn0 12569 . . . 4 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
117, 10syl 17 . . 3 (𝜑 → (𝑃 − 1) ∈ ℕ0)
12 etransclem5 46259 . . 3 (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
13 etransclem35.c . . 3 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = 𝑛})
14 0red 11265 . . 3 (𝜑 → 0 ∈ ℝ)
152, 6, 7, 8, 9, 11, 12, 13, 14etransclem31 46285 . 2 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) = Σ𝑐 ∈ (𝐶‘(𝑃 − 1))(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))))))
16 nfv 1913 . . 3 𝑐𝜑
17 nfcv 2904 . . 3 𝑐(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗)))))))
1813, 11etransclem16 46270 . . 3 (𝜑 → (𝐶‘(𝑃 − 1)) ∈ Fin)
19 simpr 484 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ (𝐶‘(𝑃 − 1)))
2013, 11etransclem12 46266 . . . . . . . . . . . . . 14 (𝜑 → (𝐶‘(𝑃 − 1)) = {𝑐 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1)})
2120adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝐶‘(𝑃 − 1)) = {𝑐 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1)})
2219, 21eleqtrd 2842 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1)})
23 rabid 3457 . . . . . . . . . . . 12 (𝑐 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1)} ↔ (𝑐 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1)))
2422, 23sylib 218 . . . . . . . . . . 11 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑐 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1)))
2524simprd 495 . . . . . . . . . 10 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1))
2625eqcomd 2742 . . . . . . . . 9 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑃 − 1) = Σ𝑗 ∈ (0...𝑀)(𝑐𝑗))
2726fveq2d 6909 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → (!‘(𝑃 − 1)) = (!‘Σ𝑗 ∈ (0...𝑀)(𝑐𝑗)))
2827oveq1d 7447 . . . . . . 7 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) = ((!‘Σ𝑗 ∈ (0...𝑀)(𝑐𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))))
29 nfcv 2904 . . . . . . . 8 𝑗𝑐
30 fzfid 14015 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → (0...𝑀) ∈ Fin)
31 nn0ex 12534 . . . . . . . . . 10 0 ∈ V
32 fzssnn0 45334 . . . . . . . . . 10 (0...(𝑃 − 1)) ⊆ ℕ0
33 mapss 8930 . . . . . . . . . 10 ((ℕ0 ∈ V ∧ (0...(𝑃 − 1)) ⊆ ℕ0) → ((0...(𝑃 − 1)) ↑m (0...𝑀)) ⊆ (ℕ0m (0...𝑀)))
3431, 32, 33mp2an 692 . . . . . . . . 9 ((0...(𝑃 − 1)) ↑m (0...𝑀)) ⊆ (ℕ0m (0...𝑀))
3524simpld 494 . . . . . . . . 9 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)))
3634, 35sselid 3980 . . . . . . . 8 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 ∈ (ℕ0m (0...𝑀)))
3729, 30, 36mccl 45618 . . . . . . 7 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘Σ𝑗 ∈ (0...𝑀)(𝑐𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) ∈ ℕ)
3828, 37eqeltrd 2840 . . . . . 6 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) ∈ ℕ)
3938nnzd 12642 . . . . 5 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) ∈ ℤ)
407adantr 480 . . . . . . 7 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑃 ∈ ℕ)
418adantr 480 . . . . . . 7 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑀 ∈ ℕ0)
42 elmapi 8890 . . . . . . . 8 (𝑐 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
4335, 42syl 17 . . . . . . 7 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
44 0zd 12627 . . . . . . 7 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ∈ ℤ)
4540, 41, 43, 44etransclem10 46264 . . . . . 6 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) ∈ ℤ)
46 fzfid 14015 . . . . . . 7 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → (1...𝑀) ∈ Fin)
477ad2antrr 726 . . . . . . . 8 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ)
4843adantr 480 . . . . . . . 8 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
49 fz1ssfz0 13664 . . . . . . . . . 10 (1...𝑀) ⊆ (0...𝑀)
5049sseli 3978 . . . . . . . . 9 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (0...𝑀))
5150adantl 481 . . . . . . . 8 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀))
52 0zd 12627 . . . . . . . 8 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → 0 ∈ ℤ)
5347, 48, 51, 52etransclem3 46257 . . . . . . 7 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))) ∈ ℤ)
5446, 53fprodzcl 15991 . . . . . 6 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))) ∈ ℤ)
5545, 54zmulcld 12730 . . . . 5 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗)))))) ∈ ℤ)
5639, 55zmulcld 12730 . . . 4 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))))) ∈ ℤ)
5756zcnd 12725 . . 3 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))))) ∈ ℂ)
58 nn0uz 12921 . . . . . . . . . . 11 0 = (ℤ‘0)
5911, 58eleqtrdi 2850 . . . . . . . . . 10 (𝜑 → (𝑃 − 1) ∈ (ℤ‘0))
60 eluzfz2 13573 . . . . . . . . . 10 ((𝑃 − 1) ∈ (ℤ‘0) → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
6159, 60syl 17 . . . . . . . . 9 (𝜑 → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
62 eluzfz1 13572 . . . . . . . . . 10 ((𝑃 − 1) ∈ (ℤ‘0) → 0 ∈ (0...(𝑃 − 1)))
6359, 62syl 17 . . . . . . . . 9 (𝜑 → 0 ∈ (0...(𝑃 − 1)))
6461, 63ifcld 4571 . . . . . . . 8 (𝜑 → if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1)))
6564adantr 480 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1)))
66 etransclem35.d . . . . . . 7 𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0))
6765, 66fmptd 7133 . . . . . 6 (𝜑𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
68 ovex 7465 . . . . . . 7 (0...(𝑃 − 1)) ∈ V
69 ovex 7465 . . . . . . 7 (0...𝑀) ∈ V
7068, 69elmap 8912 . . . . . 6 (𝐷 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)) ↔ 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
7167, 70sylibr 234 . . . . 5 (𝜑𝐷 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)))
728, 58eleqtrdi 2850 . . . . . . 7 (𝜑𝑀 ∈ (ℤ‘0))
73 fzsscn 45328 . . . . . . . 8 (0...(𝑃 − 1)) ⊆ ℂ
7467ffvelcdmda 7103 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐷𝑗) ∈ (0...(𝑃 − 1)))
7573, 74sselid 3980 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐷𝑗) ∈ ℂ)
76 fveq2 6905 . . . . . . 7 (𝑗 = 0 → (𝐷𝑗) = (𝐷‘0))
7772, 75, 76fsum1p 15790 . . . . . 6 (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐷𝑗) = ((𝐷‘0) + Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷𝑗)))
7866a1i 11 . . . . . . . 8 (𝜑𝐷 = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0)))
79 simpr 484 . . . . . . . . 9 ((𝜑𝑗 = 0) → 𝑗 = 0)
8079iftrued 4532 . . . . . . . 8 ((𝜑𝑗 = 0) → if(𝑗 = 0, (𝑃 − 1), 0) = (𝑃 − 1))
81 eluzfz1 13572 . . . . . . . . 9 (𝑀 ∈ (ℤ‘0) → 0 ∈ (0...𝑀))
8272, 81syl 17 . . . . . . . 8 (𝜑 → 0 ∈ (0...𝑀))
8378, 80, 82, 11fvmptd 7022 . . . . . . 7 (𝜑 → (𝐷‘0) = (𝑃 − 1))
84 0p1e1 12389 . . . . . . . . . . 11 (0 + 1) = 1
8584oveq1i 7442 . . . . . . . . . 10 ((0 + 1)...𝑀) = (1...𝑀)
8685sumeq1i 15734 . . . . . . . . 9 Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷𝑗) = Σ𝑗 ∈ (1...𝑀)(𝐷𝑗)
8786a1i 11 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷𝑗) = Σ𝑗 ∈ (1...𝑀)(𝐷𝑗))
8866fvmpt2 7026 . . . . . . . . . . 11 ((𝑗 ∈ (0...𝑀) ∧ if(𝑗 = 0, (𝑃 − 1), 0) ∈ (0...(𝑃 − 1))) → (𝐷𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
8950, 64, 88syl2anr 597 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐷𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
90 0red 11265 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑀) → 0 ∈ ℝ)
91 1red 11263 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑀) → 1 ∈ ℝ)
92 elfzelz 13565 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℤ)
9392zred 12724 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℝ)
94 0lt1 11786 . . . . . . . . . . . . . . . 16 0 < 1
9594a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑀) → 0 < 1)
96 elfzle1 13568 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑀) → 1 ≤ 𝑗)
9790, 91, 93, 95, 96ltletrd 11422 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑀) → 0 < 𝑗)
9890, 97gtned 11397 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑀) → 𝑗 ≠ 0)
9998neneqd 2944 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑀) → ¬ 𝑗 = 0)
10099iffalsed 4535 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑀) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
101100adantl 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
10289, 101eqtrd 2776 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐷𝑗) = 0)
103102sumeq2dv 15739 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐷𝑗) = Σ𝑗 ∈ (1...𝑀)0)
104 fzfi 14014 . . . . . . . . . 10 (1...𝑀) ∈ Fin
105104olci 866 . . . . . . . . 9 ((1...𝑀) ⊆ (ℤ𝐴) ∨ (1...𝑀) ∈ Fin)
106 sumz 15759 . . . . . . . . 9 (((1...𝑀) ⊆ (ℤ𝐴) ∨ (1...𝑀) ∈ Fin) → Σ𝑗 ∈ (1...𝑀)0 = 0)
107105, 106mp1i 13 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ (1...𝑀)0 = 0)
10887, 103, 1073eqtrd 2780 . . . . . . 7 (𝜑 → Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷𝑗) = 0)
10983, 108oveq12d 7450 . . . . . 6 (𝜑 → ((𝐷‘0) + Σ𝑗 ∈ ((0 + 1)...𝑀)(𝐷𝑗)) = ((𝑃 − 1) + 0))
1107nncnd 12283 . . . . . . . 8 (𝜑𝑃 ∈ ℂ)
111 1cnd 11257 . . . . . . . 8 (𝜑 → 1 ∈ ℂ)
112110, 111subcld 11621 . . . . . . 7 (𝜑 → (𝑃 − 1) ∈ ℂ)
113112addridd 11462 . . . . . 6 (𝜑 → ((𝑃 − 1) + 0) = (𝑃 − 1))
11477, 109, 1133eqtrd 2780 . . . . 5 (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐷𝑗) = (𝑃 − 1))
115 fveq1 6904 . . . . . . . 8 (𝑐 = 𝐷 → (𝑐𝑗) = (𝐷𝑗))
116115sumeq2sdv 15740 . . . . . . 7 (𝑐 = 𝐷 → Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = Σ𝑗 ∈ (0...𝑀)(𝐷𝑗))
117116eqeq1d 2738 . . . . . 6 (𝑐 = 𝐷 → (Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1) ↔ Σ𝑗 ∈ (0...𝑀)(𝐷𝑗) = (𝑃 − 1)))
118117elrab 3691 . . . . 5 (𝐷 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1)} ↔ (𝐷 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝐷𝑗) = (𝑃 − 1)))
11971, 114, 118sylanbrc 583 . . . 4 (𝜑𝐷 ∈ {𝑐 ∈ ((0...(𝑃 − 1)) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1)})
120119, 20eleqtrrd 2843 . . 3 (𝜑𝐷 ∈ (𝐶‘(𝑃 − 1)))
121115fveq2d 6909 . . . . . 6 (𝑐 = 𝐷 → (!‘(𝑐𝑗)) = (!‘(𝐷𝑗)))
122121prodeq2ad 45612 . . . . 5 (𝑐 = 𝐷 → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗)) = ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗)))
123122oveq2d 7448 . . . 4 (𝑐 = 𝐷 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) = ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗))))
124 fveq1 6904 . . . . . . 7 (𝑐 = 𝐷 → (𝑐‘0) = (𝐷‘0))
125124breq2d 5154 . . . . . 6 (𝑐 = 𝐷 → ((𝑃 − 1) < (𝑐‘0) ↔ (𝑃 − 1) < (𝐷‘0)))
126124oveq2d 7448 . . . . . . . . 9 (𝑐 = 𝐷 → ((𝑃 − 1) − (𝑐‘0)) = ((𝑃 − 1) − (𝐷‘0)))
127126fveq2d 6909 . . . . . . . 8 (𝑐 = 𝐷 → (!‘((𝑃 − 1) − (𝑐‘0))) = (!‘((𝑃 − 1) − (𝐷‘0))))
128127oveq2d 7448 . . . . . . 7 (𝑐 = 𝐷 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) = ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))))
129126oveq2d 7448 . . . . . . 7 (𝑐 = 𝐷 → (0↑((𝑃 − 1) − (𝑐‘0))) = (0↑((𝑃 − 1) − (𝐷‘0))))
130128, 129oveq12d 7450 . . . . . 6 (𝑐 = 𝐷 → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))))
131125, 130ifbieq2d 4551 . . . . 5 (𝑐 = 𝐷 → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))))
132115breq2d 5154 . . . . . . 7 (𝑐 = 𝐷 → (𝑃 < (𝑐𝑗) ↔ 𝑃 < (𝐷𝑗)))
133115oveq2d 7448 . . . . . . . . . 10 (𝑐 = 𝐷 → (𝑃 − (𝑐𝑗)) = (𝑃 − (𝐷𝑗)))
134133fveq2d 6909 . . . . . . . . 9 (𝑐 = 𝐷 → (!‘(𝑃 − (𝑐𝑗))) = (!‘(𝑃 − (𝐷𝑗))))
135134oveq2d 7448 . . . . . . . 8 (𝑐 = 𝐷 → ((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) = ((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))))
136133oveq2d 7448 . . . . . . . 8 (𝑐 = 𝐷 → ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))) = ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))
137135, 136oveq12d 7450 . . . . . . 7 (𝑐 = 𝐷 → (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗)))) = (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗)))))
138132, 137ifbieq2d 4551 . . . . . 6 (𝑐 = 𝐷 → if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))) = if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))))
139138prodeq2ad 45612 . . . . 5 (𝑐 = 𝐷 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))) = ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))))
140131, 139oveq12d 7450 . . . 4 (𝑐 = 𝐷 → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗)))))) = (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗)))))))
141123, 140oveq12d 7450 . . 3 (𝑐 = 𝐷 → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))))) = (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))))))
14216, 17, 18, 57, 120, 141fsumsplit1 15782 . 2 (𝜑 → Σ𝑐 ∈ (𝐶‘(𝑃 − 1))(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))))) = ((((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))))) + Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗)))))))))
14332, 74sselid 3980 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐷𝑗) ∈ ℕ0)
144143faccld 14324 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (!‘(𝐷𝑗)) ∈ ℕ)
145144nncnd 12283 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (!‘(𝐷𝑗)) ∈ ℂ)
14676fveq2d 6909 . . . . . . . . . 10 (𝑗 = 0 → (!‘(𝐷𝑗)) = (!‘(𝐷‘0)))
14772, 145, 146fprod1p 16005 . . . . . . . . 9 (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗)) = ((!‘(𝐷‘0)) · ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷𝑗))))
14883fveq2d 6909 . . . . . . . . . 10 (𝜑 → (!‘(𝐷‘0)) = (!‘(𝑃 − 1)))
14985prodeq1i 15953 . . . . . . . . . . . 12 𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷𝑗)) = ∏𝑗 ∈ (1...𝑀)(!‘(𝐷𝑗))
150149a1i 11 . . . . . . . . . . 11 (𝜑 → ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷𝑗)) = ∏𝑗 ∈ (1...𝑀)(!‘(𝐷𝑗)))
151102fveq2d 6909 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (!‘(𝐷𝑗)) = (!‘0))
152 fac0 14316 . . . . . . . . . . . . 13 (!‘0) = 1
153151, 152eqtrdi 2792 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (!‘(𝐷𝑗)) = 1)
154153prodeq2dv 15959 . . . . . . . . . . 11 (𝜑 → ∏𝑗 ∈ (1...𝑀)(!‘(𝐷𝑗)) = ∏𝑗 ∈ (1...𝑀)1)
155 prod1 15981 . . . . . . . . . . . 12 (((1...𝑀) ⊆ (ℤ𝐴) ∨ (1...𝑀) ∈ Fin) → ∏𝑗 ∈ (1...𝑀)1 = 1)
156105, 155mp1i 13 . . . . . . . . . . 11 (𝜑 → ∏𝑗 ∈ (1...𝑀)1 = 1)
157150, 154, 1563eqtrd 2780 . . . . . . . . . 10 (𝜑 → ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷𝑗)) = 1)
158148, 157oveq12d 7450 . . . . . . . . 9 (𝜑 → ((!‘(𝐷‘0)) · ∏𝑗 ∈ ((0 + 1)...𝑀)(!‘(𝐷𝑗))) = ((!‘(𝑃 − 1)) · 1))
15911faccld 14324 . . . . . . . . . . 11 (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
160159nncnd 12283 . . . . . . . . . 10 (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
161160mulridd 11279 . . . . . . . . 9 (𝜑 → ((!‘(𝑃 − 1)) · 1) = (!‘(𝑃 − 1)))
162147, 158, 1613eqtrd 2780 . . . . . . . 8 (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗)) = (!‘(𝑃 − 1)))
163162oveq2d 7448 . . . . . . 7 (𝜑 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗))) = ((!‘(𝑃 − 1)) / (!‘(𝑃 − 1))))
164159nnne0d 12317 . . . . . . . 8 (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
165160, 164dividd 12042 . . . . . . 7 (𝜑 → ((!‘(𝑃 − 1)) / (!‘(𝑃 − 1))) = 1)
166163, 165eqtrd 2776 . . . . . 6 (𝜑 → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗))) = 1)
16711nn0red 12590 . . . . . . . . . . . . 13 (𝜑 → (𝑃 − 1) ∈ ℝ)
16883, 167eqeltrd 2840 . . . . . . . . . . . 12 (𝜑 → (𝐷‘0) ∈ ℝ)
169168, 167lttri3d 11402 . . . . . . . . . . 11 (𝜑 → ((𝐷‘0) = (𝑃 − 1) ↔ (¬ (𝐷‘0) < (𝑃 − 1) ∧ ¬ (𝑃 − 1) < (𝐷‘0))))
17083, 169mpbid 232 . . . . . . . . . 10 (𝜑 → (¬ (𝐷‘0) < (𝑃 − 1) ∧ ¬ (𝑃 − 1) < (𝐷‘0)))
171170simprd 495 . . . . . . . . 9 (𝜑 → ¬ (𝑃 − 1) < (𝐷‘0))
172171iffalsed 4535 . . . . . . . 8 (𝜑 → if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))))
17383eqcomd 2742 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 − 1) = (𝐷‘0))
174112, 173subeq0bd 11690 . . . . . . . . . . . . 13 (𝜑 → ((𝑃 − 1) − (𝐷‘0)) = 0)
175174fveq2d 6909 . . . . . . . . . . . 12 (𝜑 → (!‘((𝑃 − 1) − (𝐷‘0))) = (!‘0))
176175, 152eqtrdi 2792 . . . . . . . . . . 11 (𝜑 → (!‘((𝑃 − 1) − (𝐷‘0))) = 1)
177176oveq2d 7448 . . . . . . . . . 10 (𝜑 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) = ((!‘(𝑃 − 1)) / 1))
178160div1d 12036 . . . . . . . . . 10 (𝜑 → ((!‘(𝑃 − 1)) / 1) = (!‘(𝑃 − 1)))
179177, 178eqtrd 2776 . . . . . . . . 9 (𝜑 → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) = (!‘(𝑃 − 1)))
180174oveq2d 7448 . . . . . . . . . 10 (𝜑 → (0↑((𝑃 − 1) − (𝐷‘0))) = (0↑0))
181 0cnd 11255 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℂ)
182181exp0d 14181 . . . . . . . . . 10 (𝜑 → (0↑0) = 1)
183180, 182eqtrd 2776 . . . . . . . . 9 (𝜑 → (0↑((𝑃 − 1) − (𝐷‘0))) = 1)
184179, 183oveq12d 7450 . . . . . . . 8 (𝜑 → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0)))) = ((!‘(𝑃 − 1)) · 1))
185172, 184, 1613eqtrd 2780 . . . . . . 7 (𝜑 → if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) = (!‘(𝑃 − 1)))
186 fzssre 45331 . . . . . . . . . . . 12 (0...(𝑃 − 1)) ⊆ ℝ
18767adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → 𝐷:(0...𝑀)⟶(0...(𝑃 − 1)))
18850adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀))
189187, 188ffvelcdmd 7104 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐷𝑗) ∈ (0...(𝑃 − 1)))
190186, 189sselid 3980 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐷𝑗) ∈ ℝ)
1917nnred 12282 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℝ)
192191adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℝ)
1937nngt0d 12316 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑃)
19414, 191, 193ltled 11410 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ 𝑃)
195194adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → 0 ≤ 𝑃)
196102, 195eqbrtrd 5164 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐷𝑗) ≤ 𝑃)
197190, 192, 196lensymd 11413 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → ¬ 𝑃 < (𝐷𝑗))
198197iffalsed 4535 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))) = (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗)))))
199102oveq2d 7448 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐷𝑗)) = (𝑃 − 0))
200110adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℂ)
201200subid1d 11610 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀)) → (𝑃 − 0) = 𝑃)
202199, 201eqtrd 2776 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (𝑃 − (𝐷𝑗)) = 𝑃)
203202fveq2d 6909 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (!‘(𝑃 − (𝐷𝑗))) = (!‘𝑃))
204203oveq2d 7448 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) = ((!‘𝑃) / (!‘𝑃)))
2057nnnn0d 12589 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ ℕ0)
206205faccld 14324 . . . . . . . . . . . . . 14 (𝜑 → (!‘𝑃) ∈ ℕ)
207206nncnd 12283 . . . . . . . . . . . . 13 (𝜑 → (!‘𝑃) ∈ ℂ)
208206nnne0d 12317 . . . . . . . . . . . . 13 (𝜑 → (!‘𝑃) ≠ 0)
209207, 208dividd 12042 . . . . . . . . . . . 12 (𝜑 → ((!‘𝑃) / (!‘𝑃)) = 1)
210209adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘𝑃)) = 1)
211204, 210eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → ((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) = 1)
212 df-neg 11496 . . . . . . . . . . . . 13 -𝑗 = (0 − 𝑗)
213212eqcomi 2745 . . . . . . . . . . . 12 (0 − 𝑗) = -𝑗
214213a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (0 − 𝑗) = -𝑗)
215214, 202oveq12d 7450 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))) = (-𝑗𝑃))
216211, 215oveq12d 7450 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗)))) = (1 · (-𝑗𝑃)))
21792znegcld 12726 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℤ)
218217zcnd 12725 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℂ)
219218adantl 481 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → -𝑗 ∈ ℂ)
220205adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ0)
221219, 220expcld 14187 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (-𝑗𝑃) ∈ ℂ)
222221mullidd 11280 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → (1 · (-𝑗𝑃)) = (-𝑗𝑃))
223198, 216, 2223eqtrd 2780 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))) = (-𝑗𝑃))
224223prodeq2dv 15959 . . . . . . 7 (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))) = ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃))
225185, 224oveq12d 7450 . . . . . 6 (𝜑 → (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗)))))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃)))
226166, 225oveq12d 7450 . . . . 5 (𝜑 → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))))) = (1 · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃))))
227 fzfid 14015 . . . . . . . . 9 (𝜑 → (1...𝑀) ∈ Fin)
228 zexpcl 14118 . . . . . . . . . 10 ((-𝑗 ∈ ℤ ∧ 𝑃 ∈ ℕ0) → (-𝑗𝑃) ∈ ℤ)
229217, 205, 228syl2anr 597 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → (-𝑗𝑃) ∈ ℤ)
230227, 229fprodzcl 15991 . . . . . . . 8 (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃) ∈ ℤ)
231230zcnd 12725 . . . . . . 7 (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃) ∈ ℂ)
232160, 231mulcld 11282 . . . . . 6 (𝜑 → ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃)) ∈ ℂ)
233232mullidd 11280 . . . . 5 (𝜑 → (1 · ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃)))
234226, 233eqtrd 2776 . . . 4 (𝜑 → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))))) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃)))
235 eldifi 4130 . . . . . . . . . . . . . . 15 (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → 𝑐 ∈ (𝐶‘(𝑃 − 1)))
23682adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ∈ (0...𝑀))
23743, 236ffvelcdmd 7104 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → (𝑐‘0) ∈ (0...(𝑃 − 1)))
238235, 237sylan2 593 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ (0...(𝑃 − 1)))
239186, 238sselid 3980 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ ℝ)
240167adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ∈ ℝ)
241 elfzle2 13569 . . . . . . . . . . . . . 14 ((𝑐‘0) ∈ (0...(𝑃 − 1)) → (𝑐‘0) ≤ (𝑃 − 1))
242238, 241syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ≤ (𝑃 − 1))
243239, 240, 242lensymd 11413 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ¬ (𝑃 − 1) < (𝑐‘0))
244243iffalsed 4535 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))))
24511nn0zd 12641 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 − 1) ∈ ℤ)
246245adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ∈ ℤ)
247238elfzelzd 13566 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) ∈ ℤ)
248246, 247zsubcld 12729 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℤ)
24943ffnd 6736 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → 𝑐 Fn (0...𝑀))
250249adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 Fn (0...𝑀))
25167ffnd 6736 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐷 Fn (0...𝑀))
252251ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝐷 Fn (0...𝑀))
253 fveq2 6905 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 0 → (𝑐𝑗) = (𝑐‘0))
254253adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐𝑗) = (𝑐‘0))
255 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 − 1) = (𝑐‘0) → (𝑃 − 1) = (𝑐‘0))
256255eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 − 1) = (𝑐‘0) → (𝑐‘0) = (𝑃 − 1))
257256ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐‘0) = (𝑃 − 1))
25876adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 = 0) → (𝐷𝑗) = (𝐷‘0))
25983adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 = 0) → (𝐷‘0) = (𝑃 − 1))
260258, 259eqtr2d 2777 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 = 0) → (𝑃 − 1) = (𝐷𝑗))
261260adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑃 − 1) = (𝐷𝑗))
262254, 257, 2613eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐𝑗) = (𝐷𝑗))
263262adantllr 719 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 = 0) → (𝑐𝑗) = (𝐷𝑗))
264263adantlr 715 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 = 0) → (𝑐𝑗) = (𝐷𝑗))
26525ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1))
266167ad5antr 734 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → (𝑃 − 1) ∈ ℝ)
267167ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → (𝑃 − 1) ∈ ℝ)
26843adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → 𝑐:(0...𝑀)⟶(0...(𝑃 − 1)))
26949sseli 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ (1...𝑀) → 𝑘 ∈ (0...𝑀))
270269adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (0...𝑀))
271268, 270ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐𝑘) ∈ (0...(𝑃 − 1)))
27232, 271sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐𝑘) ∈ ℕ0)
27346, 272fsumnn0cl 15773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ (1...𝑀)(𝑐𝑘) ∈ ℕ0)
274273nn0red 12590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ (1...𝑀)(𝑐𝑘) ∈ ℝ)
275274ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐𝑘) ∈ ℝ)
276 0red 11265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → 0 ∈ ℝ)
27743ffvelcdmda 7103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐𝑗) ∈ (0...(𝑃 − 1)))
278186, 277sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐𝑗) ∈ ℝ)
279278ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → (𝑐𝑗) ∈ ℝ)
280 nfv 1913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑘((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0)
281 nfcv 2904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑘(𝑐𝑗)
282 fzfid 14015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → (1...𝑀) ∈ Fin)
283 simp-4l 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) ∧ 𝑘 ∈ (1...𝑀)) → (𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))))
28473, 271sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐𝑘) ∈ ℂ)
285283, 284sylancom 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) ∧ 𝑘 ∈ (1...𝑀)) → (𝑐𝑘) ∈ ℂ)
286 1zzd 12650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 1 ∈ ℤ)
287 elfzel2 13563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
288287adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑀 ∈ ℤ)
289 elfzelz 13565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
290289adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℤ)
291 elfznn0 13661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
292291adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℕ0)
293 neqne 2947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 𝑗 = 0 → 𝑗 ≠ 0)
294293adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ≠ 0)
295 elnnne0 12542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ ℕ ↔ (𝑗 ∈ ℕ0𝑗 ≠ 0))
296292, 294, 295sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ ℕ)
297296nnge1d 12315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 1 ≤ 𝑗)
298 elfzle2 13569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
299298adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗𝑀)
300286, 288, 290, 297, 299elfzd 13556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) → 𝑗 ∈ (1...𝑀))
301300adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑗 ∈ (0...𝑀) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → 𝑗 ∈ (1...𝑀))
302301adantlll 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → 𝑗 ∈ (1...𝑀))
303 fveq2 6905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 = 𝑗 → (𝑐𝑘) = (𝑐𝑗))
304280, 281, 282, 285, 302, 303fsumsplit1 15782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐𝑘) = ((𝑐𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘)))
305304eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → ((𝑐𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘)) = Σ𝑘 ∈ (1...𝑀)(𝑐𝑘))
306305, 275eqeltrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → ((𝑐𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘)) ∈ ℝ)
307 elfzle1 13568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐𝑗) ∈ (0...(𝑃 − 1)) → 0 ≤ (𝑐𝑗))
308277, 307syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ (𝑐𝑗))
309308ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → 0 ≤ (𝑐𝑗))
310 neqne 2947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (¬ (𝑐𝑗) = 0 → (𝑐𝑗) ≠ 0)
311310adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → (𝑐𝑗) ≠ 0)
312276, 279, 309, 311leneltd 11416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → 0 < (𝑐𝑗))
313 diffi 9216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((1...𝑀) ∈ Fin → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
314104, 313mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
315 eldifi 4130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ ((1...𝑀) ∖ {𝑗}) → 𝑘 ∈ (1...𝑀))
316315adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑘 ∈ (1...𝑀))
31749, 316sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑘 ∈ (0...𝑀))
31843ffvelcdmda 7103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐𝑘) ∈ (0...(𝑃 − 1)))
319186, 318sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐𝑘) ∈ ℝ)
320317, 319syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → (𝑐𝑘) ∈ ℝ)
321 elfzle1 13568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑐𝑘) ∈ (0...(𝑃 − 1)) → 0 ≤ (𝑐𝑘))
322318, 321syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → 0 ≤ (𝑐𝑘))
323317, 322syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ ((1...𝑀) ∖ {𝑗})) → 0 ≤ (𝑐𝑘))
324314, 320, 323fsumge0 15832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → 0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘))
325324adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘))
326314, 320fsumrecl 15771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) → Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘) ∈ ℝ)
327326adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘) ∈ ℝ)
328278, 327addge01d 11852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (0 ≤ Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘) ↔ (𝑐𝑗) ≤ ((𝑐𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘))))
329325, 328mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐𝑗) ≤ ((𝑐𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘)))
330329ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → (𝑐𝑗) ≤ ((𝑐𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘)))
331276, 279, 306, 312, 330ltletrd 11422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → 0 < ((𝑐𝑗) + Σ𝑘 ∈ ((1...𝑀) ∖ {𝑗})(𝑐𝑘)))
332331, 305breqtrd 5168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → 0 < Σ𝑘 ∈ (1...𝑀)(𝑐𝑘))
333275, 332elrpd 13075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → Σ𝑘 ∈ (1...𝑀)(𝑐𝑘) ∈ ℝ+)
334267, 333ltaddrpd 13111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → (𝑃 − 1) < ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐𝑘)))
335334adantl3r 750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → (𝑃 − 1) < ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐𝑘)))
336 fveq2 6905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 = 𝑘 → (𝑐𝑗) = (𝑐𝑘))
337336cbvsumv 15733 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = Σ𝑘 ∈ (0...𝑀)(𝑐𝑘)
338337a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = Σ𝑘 ∈ (0...𝑀)(𝑐𝑘))
33972ad5antr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → 𝑀 ∈ (ℤ‘0))
340 simp-5l 784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) ∧ 𝑘 ∈ (0...𝑀)) → (𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))))
34173, 318sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐𝑘) ∈ ℂ)
342340, 341sylancom 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐𝑘) ∈ ℂ)
343 fveq2 6905 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 0 → (𝑐𝑘) = (𝑐‘0))
344339, 342, 343fsum1p 15790 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → Σ𝑘 ∈ (0...𝑀)(𝑐𝑘) = ((𝑐‘0) + Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐𝑘)))
345256ad4antlr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → (𝑐‘0) = (𝑃 − 1))
34685sumeq1i 15734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐𝑘) = Σ𝑘 ∈ (1...𝑀)(𝑐𝑘)
347346a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐𝑘) = Σ𝑘 ∈ (1...𝑀)(𝑐𝑘))
348345, 347oveq12d 7450 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → ((𝑐‘0) + Σ𝑘 ∈ ((0 + 1)...𝑀)(𝑐𝑘)) = ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐𝑘)))
349338, 344, 3483eqtrrd 2781 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → ((𝑃 − 1) + Σ𝑘 ∈ (1...𝑀)(𝑐𝑘)) = Σ𝑗 ∈ (0...𝑀)(𝑐𝑗))
350335, 349breqtrd 5168 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → (𝑃 − 1) < Σ𝑗 ∈ (0...𝑀)(𝑐𝑗))
351266, 350gtned 11397 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) ≠ (𝑃 − 1))
352351neneqd 2944 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) ∧ ¬ (𝑐𝑗) = 0) → ¬ Σ𝑗 ∈ (0...𝑀)(𝑐𝑗) = (𝑃 − 1))
353265, 352condan 817 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝑐𝑗) = 0)
354 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0...𝑀))
35532, 65sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑀)) → if(𝑗 = 0, (𝑃 − 1), 0) ∈ ℕ0)
35666fvmpt2 7026 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ (0...𝑀) ∧ if(𝑗 = 0, (𝑃 − 1), 0) ∈ ℕ0) → (𝐷𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
357354, 355, 356syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐷𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
358357adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝐷𝑗) = if(𝑗 = 0, (𝑃 − 1), 0))
359 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → ¬ 𝑗 = 0)
360359iffalsed 4535 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → if(𝑗 = 0, (𝑃 − 1), 0) = 0)
361358, 360eqtr2d 2777 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷𝑗))
362361adantllr 719 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷𝑗))
363362adantllr 719 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → 0 = (𝐷𝑗))
364353, 363eqtrd 2776 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑗 = 0) → (𝑐𝑗) = (𝐷𝑗))
365264, 364pm2.61dan 812 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐𝑗) = (𝐷𝑗))
366250, 252, 365eqfnfvd 7053 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 = 𝐷)
367235, 366sylanl2 681 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ (𝑃 − 1) = (𝑐‘0)) → 𝑐 = 𝐷)
368 eldifsni 4789 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → 𝑐𝐷)
369368neneqd 2944 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) → ¬ 𝑐 = 𝐷)
370369ad2antlr 727 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ (𝑃 − 1) = (𝑐‘0)) → ¬ 𝑐 = 𝐷)
371367, 370pm2.65da 816 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ¬ (𝑃 − 1) = (𝑐‘0))
372371neqned 2946 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑃 − 1) ≠ (𝑐‘0))
373239, 240, 242, 372leneltd 11416 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (𝑐‘0) < (𝑃 − 1))
374239, 240posdifd 11851 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑐‘0) < (𝑃 − 1) ↔ 0 < ((𝑃 − 1) − (𝑐‘0))))
375373, 374mpbid 232 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → 0 < ((𝑃 − 1) − (𝑐‘0)))
376 elnnz 12625 . . . . . . . . . . . . . 14 (((𝑃 − 1) − (𝑐‘0)) ∈ ℕ ↔ (((𝑃 − 1) − (𝑐‘0)) ∈ ℤ ∧ 0 < ((𝑃 − 1) − (𝑐‘0))))
377248, 375, 376sylanbrc 583 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℕ)
3783770expd 14180 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0↑((𝑃 − 1) − (𝑐‘0))) = 0)
379378oveq2d 7448 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0)))) = (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · 0))
380160adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘(𝑃 − 1)) ∈ ℂ)
381377nnnn0d 12589 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((𝑃 − 1) − (𝑐‘0)) ∈ ℕ0)
382381faccld 14324 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ∈ ℕ)
383382nncnd 12283 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ∈ ℂ)
384382nnne0d 12317 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (!‘((𝑃 − 1) − (𝑐‘0))) ≠ 0)
385380, 383, 384divcld 12044 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) ∈ ℂ)
386385mul01d 11461 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · 0) = 0)
387244, 379, 3863eqtrd 2780 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) = 0)
388387oveq1d 7447 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗)))))) = (0 · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗)))))))
389235, 54sylan2 593 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))) ∈ ℤ)
390389zcnd 12725 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))) ∈ ℂ)
391390mul02d 11460 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0 · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗)))))) = 0)
392388, 391eqtrd 2776 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗)))))) = 0)
393392oveq2d 7448 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))))) = (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · 0))
394 fzfid 14015 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (0...𝑀) ∈ Fin)
39532, 277sselid 3980 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ (𝐶‘(𝑃 − 1))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐𝑗) ∈ ℕ0)
396235, 395sylanl2 681 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐𝑗) ∈ ℕ0)
397396faccld 14324 . . . . . . . . . . 11 (((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝑐𝑗)) ∈ ℕ)
398394, 397fprodnncl 15992 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗)) ∈ ℕ)
399398nncnd 12283 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗)) ∈ ℂ)
400398nnne0d 12317 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗)) ≠ 0)
401380, 399, 400divcld 12044 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → ((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) ∈ ℂ)
402401mul01d 11461 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · 0) = 0)
403393, 402eqtrd 2776 . . . . . 6 ((𝜑𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})) → (((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))))) = 0)
404403sumeq2dv 15739 . . . . 5 (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))))) = Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0)
405 diffi 9216 . . . . . . . 8 ((𝐶‘(𝑃 − 1)) ∈ Fin → ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin)
40618, 405syl 17 . . . . . . 7 (𝜑 → ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin)
407406olcd 874 . . . . . 6 (𝜑 → (((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ⊆ (ℤ‘0) ∨ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin))
408 sumz 15759 . . . . . 6 ((((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ⊆ (ℤ‘0) ∨ ((𝐶‘(𝑃 − 1)) ∖ {𝐷}) ∈ Fin) → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0 = 0)
409407, 408syl 17 . . . . 5 (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})0 = 0)
410404, 409eqtrd 2776 . . . 4 (𝜑 → Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗))))))) = 0)
411234, 410oveq12d 7450 . . 3 (𝜑 → ((((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))))) + Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗)))))))) = (((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃)) + 0))
412232addridd 11462 . . 3 (𝜑 → (((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃)) + 0) = ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃)))
413 nfv 1913 . . . . 5 𝑗𝜑
414413, 205, 227, 219fprodexp 45614 . . . 4 (𝜑 → ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃) = (∏𝑗 ∈ (1...𝑀)-𝑗𝑃))
415414oveq2d 7448 . . 3 (𝜑 → ((!‘(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)(-𝑗𝑃)) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗𝑃)))
416411, 412, 4153eqtrd 2780 . 2 (𝜑 → ((((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐷𝑗))) · (if((𝑃 − 1) < (𝐷‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐷‘0)))) · (0↑((𝑃 − 1) − (𝐷‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐷𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐷𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝐷𝑗))))))) + Σ𝑐 ∈ ((𝐶‘(𝑃 − 1)) ∖ {𝐷})(((!‘(𝑃 − 1)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (0↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐𝑗)))) · ((0 − 𝑗)↑(𝑃 − (𝑐𝑗)))))))) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗𝑃)))
41715, 142, 4163eqtrd 2780 1 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) = ((!‘(𝑃 − 1)) · (∏𝑗 ∈ (1...𝑀)-𝑗𝑃)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 847   = wceq 1539  wcel 2107  wne 2939  {crab 3435  Vcvv 3479  cdif 3947  wss 3950  ifcif 4524  {csn 4625  {cpr 4627   class class class wbr 5142  cmpt 5224  ran crn 5685   Fn wfn 6555  wf 6556  cfv 6560  (class class class)co 7432  m cmap 8867  Fincfn 8986  cc 11154  cr 11155  0cc0 11156  1c1 11157   + caddc 11159   · cmul 11161   < clt 11296  cle 11297  cmin 11493  -cneg 11494   / cdiv 11921  cn 12267  0cn0 12528  cz 12615  cuz 12879  (,)cioo 13388  ...cfz 13548  cexp 14103  !cfa 14313  Σcsu 15723  cprod 15940  t crest 17466  TopOpenctopn 17467  topGenctg 17483  fldccnfld 21365   D𝑛 cdvn 25900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-inf2 9682  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234  ax-addf 11235
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-iin 4993  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-of 7698  df-om 7889  df-1st 8015  df-2nd 8016  df-supp 8187  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-er 8746  df-map 8869  df-pm 8870  df-ixp 8939  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-fsupp 9403  df-fi 9452  df-sup 9483  df-inf 9484  df-oi 9551  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12529  df-z 12616  df-dec 12736  df-uz 12880  df-q 12992  df-rp 13036  df-xneg 13155  df-xadd 13156  df-xmul 13157  df-ioo 13392  df-ico 13394  df-icc 13395  df-fz 13549  df-fzo 13696  df-seq 14044  df-exp 14104  df-fac 14314  df-bc 14343  df-hash 14371  df-cj 15139  df-re 15140  df-im 15141  df-sqrt 15275  df-abs 15276  df-clim 15525  df-sum 15724  df-prod 15941  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17249  df-ress 17276  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-hom 17322  df-cco 17323  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18654  df-sgrp 18733  df-mnd 18749  df-submnd 18798  df-mulg 19087  df-cntz 19336  df-cmn 19801  df-psmet 21357  df-xmet 21358  df-met 21359  df-bl 21360  df-mopn 21361  df-fbas 21362  df-fg 21363  df-cnfld 21366  df-top 22901  df-topon 22918  df-topsp 22940  df-bases 22954  df-cld 23028  df-ntr 23029  df-cls 23030  df-nei 23107  df-lp 23145  df-perf 23146  df-cn 23236  df-cnp 23237  df-haus 23324  df-tx 23571  df-hmeo 23764  df-fil 23855  df-fm 23947  df-flim 23948  df-flf 23949  df-xms 24331  df-ms 24332  df-tms 24333  df-cncf 24905  df-limc 25902  df-dv 25903  df-dvn 25904
This theorem is referenced by:  etransclem41  46295
  Copyright terms: Public domain W3C validator