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