| Step | Hyp | Ref
| Expression |
| 1 | | etransclem38.c |
. . . 4
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) |
| 2 | | etransclem38.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈
ℕ0) |
| 3 | 1, 2 | etransclem16 46265 |
. . 3
⊢ (𝜑 → (𝐶‘𝐼) ∈ Fin) |
| 4 | | etransclem38.p |
. . . 4
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 5 | 4 | nnzd 12640 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℤ) |
| 6 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → 𝑃 ∈ ℕ) |
| 7 | | etransclem38.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 8 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → 𝑀 ∈
ℕ0) |
| 9 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → 𝐼 ∈
ℕ0) |
| 10 | | etransclem11 46260 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ {𝑐 ∈
((0...𝑛) ↑m
(0...𝑀)) ∣
Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑒 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑒‘𝑘) = 𝑚}) |
| 11 | | etransclem11 46260 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
↦ {𝑒 ∈
((0...𝑚) ↑m
(0...𝑀)) ∣
Σ𝑘 ∈ (0...𝑀)(𝑒‘𝑘) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑑‘𝑗) = 𝑛}) |
| 12 | 1, 10, 11 | 3eqtri 2769 |
. . . . 5
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑑‘𝑗) = 𝑛}) |
| 13 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → 𝑐 ∈ (𝐶‘𝐼)) |
| 14 | | etransclem38.j |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) |
| 15 | 14 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → 𝐽 ∈ (0...𝑀)) |
| 16 | | eqid 2737 |
. . . . 5
⊢
(((!‘𝐼) /
∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) = (((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) |
| 17 | 6, 8, 9, 12, 13, 15, 16 | etransclem28 46277 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → (!‘(𝑃 − 1)) ∥ (((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))) |
| 18 | | nnm1nn0 12567 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
| 19 | 4, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
| 20 | 19 | faccld 14323 |
. . . . . . 7
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℕ) |
| 21 | 20 | nnzd 12640 |
. . . . . 6
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℤ) |
| 22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → (!‘(𝑃 − 1)) ∈
ℤ) |
| 23 | 20 | nnne0d 12316 |
. . . . . 6
⊢ (𝜑 → (!‘(𝑃 − 1)) ≠
0) |
| 24 | 23 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → (!‘(𝑃 − 1)) ≠ 0) |
| 25 | 14 | elfzelzd 13565 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ℤ) |
| 26 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → 𝐽 ∈ ℤ) |
| 27 | 6, 8, 9, 26, 12, 13 | etransclem26 46275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → (((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ∈ ℤ) |
| 28 | | dvdsval2 16293 |
. . . . 5
⊢
(((!‘(𝑃
− 1)) ∈ ℤ ∧ (!‘(𝑃 − 1)) ≠ 0 ∧ (((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ∈ ℤ) →
((!‘(𝑃 − 1))
∥ (((!‘𝐼) /
∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ↔ ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))) ∈
ℤ)) |
| 29 | 22, 24, 27, 28 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → ((!‘(𝑃 − 1)) ∥ (((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ↔ ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))) ∈
ℤ)) |
| 30 | 17, 29 | mpbid 232 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))) ∈
ℤ) |
| 31 | | pm3.22 459 |
. . . . . . . 8
⊢ ((𝐽 = 0 ∧ 𝐼 = (𝑃 − 1)) → (𝐼 = (𝑃 − 1) ∧ 𝐽 = 0)) |
| 32 | 31 | adantll 714 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) ∧ 𝐼 = (𝑃 − 1)) → (𝐼 = (𝑃 − 1) ∧ 𝐽 = 0)) |
| 33 | | etransclem38.ij |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝐼 = (𝑃 − 1) ∧ 𝐽 = 0)) |
| 34 | 33 | ad3antrrr 730 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) ∧ 𝐼 = (𝑃 − 1)) → ¬ (𝐼 = (𝑃 − 1) ∧ 𝐽 = 0)) |
| 35 | 32, 34 | pm2.65da 817 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) → ¬ 𝐼 = (𝑃 − 1)) |
| 36 | 35 | neqned 2947 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) → 𝐼 ≠ (𝑃 − 1)) |
| 37 | 4 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) ∧ 𝐼 ≠ (𝑃 − 1)) → 𝑃 ∈ ℕ) |
| 38 | 7 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) ∧ 𝐼 ≠ (𝑃 − 1)) → 𝑀 ∈
ℕ0) |
| 39 | 2 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) ∧ 𝐼 ≠ (𝑃 − 1)) → 𝐼 ∈
ℕ0) |
| 40 | | simpr 484 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) ∧ 𝐼 ≠ (𝑃 − 1)) → 𝐼 ≠ (𝑃 − 1)) |
| 41 | | simplr 769 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) ∧ 𝐼 ≠ (𝑃 − 1)) → 𝐽 = 0) |
| 42 | 13 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) ∧ 𝐼 ≠ (𝑃 − 1)) → 𝑐 ∈ (𝐶‘𝐼)) |
| 43 | 37, 38, 39, 40, 41, 12, 42 | etransclem24 46273 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) ∧ 𝐼 ≠ (𝑃 − 1)) → 𝑃 ∥ ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1)))) |
| 44 | 36, 43 | mpdan 687 |
. . . 4
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ 𝐽 = 0) → 𝑃 ∥ ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1)))) |
| 45 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → 𝑃 ∈ ℕ) |
| 46 | 7 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → 𝑀 ∈
ℕ0) |
| 47 | 2 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → 𝐼 ∈
ℕ0) |
| 48 | 1, 2 | etransclem12 46261 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶‘𝐼) = {𝑐 ∈ ((0...𝐼) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝐼}) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → (𝐶‘𝐼) = {𝑐 ∈ ((0...𝐼) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝐼}) |
| 50 | 13, 49 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐼) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝐼}) |
| 51 | | rabid 3458 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ {𝑐 ∈ ((0...𝐼) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝐼} ↔ (𝑐 ∈ ((0...𝐼) ↑m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝐼)) |
| 52 | 50, 51 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → (𝑐 ∈ ((0...𝐼) ↑m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝐼)) |
| 53 | 52 | simpld 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → 𝑐 ∈ ((0...𝐼) ↑m (0...𝑀))) |
| 54 | | elmapi 8889 |
. . . . . . . . 9
⊢ (𝑐 ∈ ((0...𝐼) ↑m (0...𝑀)) → 𝑐:(0...𝑀)⟶(0...𝐼)) |
| 55 | 53, 54 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → 𝑐:(0...𝑀)⟶(0...𝐼)) |
| 56 | 55 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → 𝑐:(0...𝑀)⟶(0...𝐼)) |
| 57 | 52 | simprd 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝐼) |
| 58 | 57 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝐼) |
| 59 | | 1zzd 12648 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐽 = 0) → 1 ∈
ℤ) |
| 60 | 7 | nn0zd 12639 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 61 | 60 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐽 = 0) → 𝑀 ∈ ℤ) |
| 62 | 25 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐽 = 0) → 𝐽 ∈ ℤ) |
| 63 | | elfznn0 13660 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ (0...𝑀) → 𝐽 ∈
ℕ0) |
| 64 | 14, 63 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈
ℕ0) |
| 65 | | neqne 2948 |
. . . . . . . . . . . 12
⊢ (¬
𝐽 = 0 → 𝐽 ≠ 0) |
| 66 | 64, 65 | anim12i 613 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐽 = 0) → (𝐽 ∈ ℕ0 ∧ 𝐽 ≠ 0)) |
| 67 | | elnnne0 12540 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ ℕ ↔ (𝐽 ∈ ℕ0
∧ 𝐽 ≠
0)) |
| 68 | 66, 67 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐽 = 0) → 𝐽 ∈ ℕ) |
| 69 | 68 | nnge1d 12314 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐽 = 0) → 1 ≤ 𝐽) |
| 70 | | elfzle2 13568 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0...𝑀) → 𝐽 ≤ 𝑀) |
| 71 | 14, 70 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ≤ 𝑀) |
| 72 | 71 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐽 = 0) → 𝐽 ≤ 𝑀) |
| 73 | 59, 61, 62, 69, 72 | elfzd 13555 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐽 = 0) → 𝐽 ∈ (1...𝑀)) |
| 74 | 73 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → 𝐽 ∈ (1...𝑀)) |
| 75 | 45, 46, 47, 56, 58, 16, 74 | etransclem25 46274 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → (!‘𝑃) ∥ (((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))) |
| 76 | 4 | nncnd 12282 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℂ) |
| 77 | | 1cnd 11256 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℂ) |
| 78 | 76, 77 | npcand 11624 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃 − 1) + 1) = 𝑃) |
| 79 | 78 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 = ((𝑃 − 1) + 1)) |
| 80 | 79 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝜑 → (!‘𝑃) = (!‘((𝑃 − 1) + 1))) |
| 81 | | facp1 14317 |
. . . . . . . . 9
⊢ ((𝑃 − 1) ∈
ℕ0 → (!‘((𝑃 − 1) + 1)) = ((!‘(𝑃 − 1)) · ((𝑃 − 1) +
1))) |
| 82 | 19, 81 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (!‘((𝑃 − 1) + 1)) =
((!‘(𝑃 − 1))
· ((𝑃 − 1) +
1))) |
| 83 | 78 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → ((!‘(𝑃 − 1)) · ((𝑃 − 1) + 1)) =
((!‘(𝑃 − 1))
· 𝑃)) |
| 84 | 20 | nncnd 12282 |
. . . . . . . . . 10
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℂ) |
| 85 | 84, 76 | mulcomd 11282 |
. . . . . . . . 9
⊢ (𝜑 → ((!‘(𝑃 − 1)) · 𝑃) = (𝑃 · (!‘(𝑃 − 1)))) |
| 86 | 83, 85 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((!‘(𝑃 − 1)) · ((𝑃 − 1) + 1)) = (𝑃 · (!‘(𝑃 − 1)))) |
| 87 | 80, 82, 86 | 3eqtrrd 2782 |
. . . . . . 7
⊢ (𝜑 → (𝑃 · (!‘(𝑃 − 1))) = (!‘𝑃)) |
| 88 | 87 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → (𝑃 · (!‘(𝑃 − 1))) = (!‘𝑃)) |
| 89 | 27 | zcnd 12723 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → (((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) ∈ ℂ) |
| 90 | 84 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → (!‘(𝑃 − 1)) ∈
ℂ) |
| 91 | 89, 90, 24 | divcan1d 12044 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → (((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))) · (!‘(𝑃 − 1))) = (((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))) |
| 92 | 91 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → (((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))) · (!‘(𝑃 − 1))) = (((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))) |
| 93 | 75, 88, 92 | 3brtr4d 5175 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → (𝑃 · (!‘(𝑃 − 1))) ∥ (((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))) · (!‘(𝑃 − 1)))) |
| 94 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → 𝑃 ∈ ℤ) |
| 95 | 30 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))) ∈
ℤ) |
| 96 | 21 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → (!‘(𝑃 − 1)) ∈
ℤ) |
| 97 | 23 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → (!‘(𝑃 − 1)) ≠ 0) |
| 98 | | dvdsmulcr 16323 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧
((((!‘𝐼) /
∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))) ∈ ℤ ∧
((!‘(𝑃 − 1))
∈ ℤ ∧ (!‘(𝑃 − 1)) ≠ 0)) → ((𝑃 · (!‘(𝑃 − 1))) ∥
(((((!‘𝐼) /
∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))) · (!‘(𝑃 − 1))) ↔ 𝑃 ∥ ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))))) |
| 99 | 94, 95, 96, 97, 98 | syl112anc 1376 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → ((𝑃 · (!‘(𝑃 − 1))) ∥ (((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))) · (!‘(𝑃 − 1))) ↔ 𝑃 ∥ ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))))) |
| 100 | 93, 99 | mpbid 232 |
. . . 4
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) ∧ ¬ 𝐽 = 0) → 𝑃 ∥ ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1)))) |
| 101 | 44, 100 | pm2.61dan 813 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐶‘𝐼)) → 𝑃 ∥ ((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1)))) |
| 102 | 3, 5, 30, 101 | fsumdvds 16345 |
. 2
⊢ (𝜑 → 𝑃 ∥ Σ𝑐 ∈ (𝐶‘𝐼)((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1)))) |
| 103 | | reelprrecn 11247 |
. . . . . 6
⊢ ℝ
∈ {ℝ, ℂ} |
| 104 | 103 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
| 105 | | reopn 45301 |
. . . . . . 7
⊢ ℝ
∈ (topGen‘ran (,)) |
| 106 | | tgioo4 24826 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 107 | 105, 106 | eleqtri 2839 |
. . . . . 6
⊢ ℝ
∈ ((TopOpen‘ℂfld) ↾t
ℝ) |
| 108 | 107 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
| 109 | | etransclem38.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
| 110 | | etransclem5 46254 |
. . . . 5
⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
| 111 | | fzssre 45326 |
. . . . . 6
⊢
(0...𝑀) ⊆
ℝ |
| 112 | 111, 14 | sselid 3981 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ ℝ) |
| 113 | 104, 108,
4, 7, 109, 2, 110, 1, 112 | etransclem31 46280 |
. . . 4
⊢ (𝜑 → (((ℝ
D𝑛 𝐹)‘𝐼)‘𝐽) = Σ𝑐 ∈ (𝐶‘𝐼)(((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗)))))))) |
| 114 | 113 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘𝐼)‘𝐽) / (!‘(𝑃 − 1))) = (Σ𝑐 ∈ (𝐶‘𝐼)(((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1)))) |
| 115 | 3, 84, 89, 23 | fsumdivc 15822 |
. . 3
⊢ (𝜑 → (Σ𝑐 ∈ (𝐶‘𝐼)(((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1))) = Σ𝑐 ∈ (𝐶‘𝐼)((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1)))) |
| 116 | 114, 115 | eqtrd 2777 |
. 2
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘𝐼)‘𝐽) / (!‘(𝑃 − 1))) = Σ𝑐 ∈ (𝐶‘𝐼)((((!‘𝐼) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · (if((𝑃 − 1) < (𝑐‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝑐‘0)))) · (𝐽↑((𝑃 − 1) − (𝑐‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝑐‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝑐‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝑐‘𝑗))))))) / (!‘(𝑃 − 1)))) |
| 117 | 102, 116 | breqtrrd 5171 |
1
⊢ (𝜑 → 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘𝐼)‘𝐽) / (!‘(𝑃 − 1)))) |