Proof of Theorem etransclem25
| Step | Hyp | Ref
| Expression |
| 1 | | etransclem25.p |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 2 | 1 | nnnn0d 12587 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
| 3 | 2 | faccld 14323 |
. . . . 5
⊢ (𝜑 → (!‘𝑃) ∈ ℕ) |
| 4 | 3 | nnzd 12640 |
. . . 4
⊢ (𝜑 → (!‘𝑃) ∈ ℤ) |
| 5 | | etransclem25.sumc |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗) = 𝑁) |
| 6 | 5 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 = Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗)) |
| 7 | 6 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝜑 → (!‘𝑁) = (!‘Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗))) |
| 8 | 7 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → ((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) = ((!‘Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗)))) |
| 9 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑗𝐶 |
| 10 | | fzfid 14014 |
. . . . . . . 8
⊢ (𝜑 → (0...𝑀) ∈ Fin) |
| 11 | | etransclem25.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) |
| 12 | | nn0ex 12532 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
| 13 | | fzssnn0 45329 |
. . . . . . . . . . 11
⊢
(0...𝑁) ⊆
ℕ0 |
| 14 | | mapss 8929 |
. . . . . . . . . . 11
⊢
((ℕ0 ∈ V ∧ (0...𝑁) ⊆ ℕ0) →
((0...𝑁) ↑m
(0...𝑀)) ⊆
(ℕ0 ↑m (0...𝑀))) |
| 15 | 12, 13, 14 | mp2an 692 |
. . . . . . . . . 10
⊢
((0...𝑁)
↑m (0...𝑀))
⊆ (ℕ0 ↑m (0...𝑀)) |
| 16 | | ovex 7464 |
. . . . . . . . . . . 12
⊢
(0...𝑁) ∈
V |
| 17 | | ovexd 7466 |
. . . . . . . . . . . 12
⊢ (𝐶:(0...𝑀)⟶(0...𝑁) → (0...𝑀) ∈ V) |
| 18 | | elmapg 8879 |
. . . . . . . . . . . 12
⊢
(((0...𝑁) ∈ V
∧ (0...𝑀) ∈ V)
→ (𝐶 ∈
((0...𝑁) ↑m
(0...𝑀)) ↔ 𝐶:(0...𝑀)⟶(0...𝑁))) |
| 19 | 16, 17, 18 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝐶:(0...𝑀)⟶(0...𝑁) → (𝐶 ∈ ((0...𝑁) ↑m (0...𝑀)) ↔ 𝐶:(0...𝑀)⟶(0...𝑁))) |
| 20 | 19 | ibir 268 |
. . . . . . . . . 10
⊢ (𝐶:(0...𝑀)⟶(0...𝑁) → 𝐶 ∈ ((0...𝑁) ↑m (0...𝑀))) |
| 21 | 15, 20 | sselid 3981 |
. . . . . . . . 9
⊢ (𝐶:(0...𝑀)⟶(0...𝑁) → 𝐶 ∈ (ℕ0
↑m (0...𝑀))) |
| 22 | 11, 21 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (ℕ0
↑m (0...𝑀))) |
| 23 | 9, 10, 22 | mccl 45613 |
. . . . . . 7
⊢ (𝜑 → ((!‘Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) ∈ ℕ) |
| 24 | 8, 23 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → ((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) ∈ ℕ) |
| 25 | 24 | nnzd 12640 |
. . . . 5
⊢ (𝜑 → ((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) ∈ ℤ) |
| 26 | | etransclem25.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 27 | | etransclem25.j |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (1...𝑀)) |
| 28 | 27 | elfzelzd 13565 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℤ) |
| 29 | 1, 26, 11, 28 | etransclem10 46259 |
. . . . 5
⊢ (𝜑 → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) ∈
ℤ) |
| 30 | 25, 29 | zmulcld 12728 |
. . . 4
⊢ (𝜑 → (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))))) ∈
ℤ) |
| 31 | | fzfid 14014 |
. . . . 5
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
| 32 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ) |
| 33 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐶:(0...𝑀)⟶(0...𝑁)) |
| 34 | | 0z 12624 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
| 35 | | fzp1ss 13615 |
. . . . . . . . 9
⊢ (0 ∈
ℤ → ((0 + 1)...𝑀) ⊆ (0...𝑀)) |
| 36 | 34, 35 | ax-mp 5 |
. . . . . . . 8
⊢ ((0 +
1)...𝑀) ⊆ (0...𝑀) |
| 37 | | id 22 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (1...𝑀)) |
| 38 | | 1e0p1 12775 |
. . . . . . . . . 10
⊢ 1 = (0 +
1) |
| 39 | 38 | oveq1i 7441 |
. . . . . . . . 9
⊢
(1...𝑀) = ((0 +
1)...𝑀) |
| 40 | 37, 39 | eleqtrdi 2851 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ((0 + 1)...𝑀)) |
| 41 | 36, 40 | sselid 3981 |
. . . . . . 7
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (0...𝑀)) |
| 42 | 41 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀)) |
| 43 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐽 ∈ ℤ) |
| 44 | 32, 33, 42, 43 | etransclem3 46252 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) |
| 45 | 31, 44 | fprodzcl 15990 |
. . . 4
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) |
| 46 | 4, 30, 45 | 3jca 1129 |
. . 3
⊢ (𝜑 → ((!‘𝑃) ∈ ℤ ∧
(((!‘𝑁) /
∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))))) ∈ ℤ ∧
∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ)) |
| 47 | 28 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ ℂ) |
| 48 | 47 | subidd 11608 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 − 𝐽) = 0) |
| 49 | 48 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → 0 = (𝐽 − 𝐽)) |
| 50 | 49 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → (0↑(𝑃 − (𝐶‘𝐽))) = ((𝐽 − 𝐽)↑(𝑃 − (𝐶‘𝐽)))) |
| 51 | 50 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐽 − 𝐽)↑(𝑃 − (𝐶‘𝐽))))) |
| 52 | 51 | ifeq2d 4546 |
. . . . . 6
⊢ (𝜑 → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐽 − 𝐽)↑(𝑃 − (𝐶‘𝐽)))))) |
| 53 | | id 22 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (1...𝑀) → 𝐽 ∈ (1...𝑀)) |
| 54 | 53, 39 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ (𝐽 ∈ (1...𝑀) → 𝐽 ∈ ((0 + 1)...𝑀)) |
| 55 | 36, 54 | sselid 3981 |
. . . . . . . 8
⊢ (𝐽 ∈ (1...𝑀) → 𝐽 ∈ (0...𝑀)) |
| 56 | 27, 55 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) |
| 57 | 1, 11, 56, 28 | etransclem3 46252 |
. . . . . 6
⊢ (𝜑 → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐽 − 𝐽)↑(𝑃 − (𝐶‘𝐽))))) ∈ ℤ) |
| 58 | 52, 57 | eqeltrd 2841 |
. . . . 5
⊢ (𝜑 → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) ∈ ℤ) |
| 59 | | fzfi 14013 |
. . . . . . 7
⊢
(1...𝑀) ∈
Fin |
| 60 | | diffi 9215 |
. . . . . . 7
⊢
((1...𝑀) ∈ Fin
→ ((1...𝑀) ∖
{𝐽}) ∈
Fin) |
| 61 | 59, 60 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → ((1...𝑀) ∖ {𝐽}) ∈ Fin) |
| 62 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...𝑀) ∖ {𝐽})) → 𝑃 ∈ ℕ) |
| 63 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...𝑀) ∖ {𝐽})) → 𝐶:(0...𝑀)⟶(0...𝑁)) |
| 64 | | eldifi 4131 |
. . . . . . . . 9
⊢ (𝑗 ∈ ((1...𝑀) ∖ {𝐽}) → 𝑗 ∈ (1...𝑀)) |
| 65 | 64, 41 | syl 17 |
. . . . . . . 8
⊢ (𝑗 ∈ ((1...𝑀) ∖ {𝐽}) → 𝑗 ∈ (0...𝑀)) |
| 66 | 65 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...𝑀) ∖ {𝐽})) → 𝑗 ∈ (0...𝑀)) |
| 67 | 28 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...𝑀) ∖ {𝐽})) → 𝐽 ∈ ℤ) |
| 68 | 62, 63, 66, 67 | etransclem3 46252 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...𝑀) ∖ {𝐽})) → if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) |
| 69 | 61, 68 | fprodzcl 15990 |
. . . . 5
⊢ (𝜑 → ∏𝑗 ∈ ((1...𝑀) ∖ {𝐽})if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) |
| 70 | | dvds0 16309 |
. . . . . . . . 9
⊢
((!‘𝑃) ∈
ℤ → (!‘𝑃)
∥ 0) |
| 71 | 4, 70 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (!‘𝑃) ∥ 0) |
| 72 | 71 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 < (𝐶‘𝐽)) → (!‘𝑃) ∥ 0) |
| 73 | | iftrue 4531 |
. . . . . . . . 9
⊢ (𝑃 < (𝐶‘𝐽) → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) = 0) |
| 74 | 73 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑃 < (𝐶‘𝐽) → 0 = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
| 75 | 74 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 < (𝐶‘𝐽)) → 0 = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
| 76 | 72, 75 | breqtrd 5169 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑃 < (𝐶‘𝐽)) → (!‘𝑃) ∥ if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
| 77 | | iddvds 16307 |
. . . . . . . . . 10
⊢
((!‘𝑃) ∈
ℤ → (!‘𝑃)
∥ (!‘𝑃)) |
| 78 | 4, 77 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (!‘𝑃) ∥ (!‘𝑃)) |
| 79 | 78 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ 𝑃 = (𝐶‘𝐽)) → (!‘𝑃) ∥ (!‘𝑃)) |
| 80 | | iffalse 4534 |
. . . . . . . . . 10
⊢ (¬
𝑃 < (𝐶‘𝐽) → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) |
| 81 | 80 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ 𝑃 = (𝐶‘𝐽)) → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) |
| 82 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 = (𝐶‘𝐽) → (𝑃 − (𝐶‘𝐽)) = ((𝐶‘𝐽) − (𝐶‘𝐽))) |
| 83 | 82 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (𝑃 − (𝐶‘𝐽)) = ((𝐶‘𝐽) − (𝐶‘𝐽))) |
| 84 | 11, 56 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐶‘𝐽) ∈ (0...𝑁)) |
| 85 | 84 | elfzelzd 13565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐶‘𝐽) ∈ ℤ) |
| 86 | 85 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐶‘𝐽) ∈ ℂ) |
| 87 | 86 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (𝐶‘𝐽) ∈ ℂ) |
| 88 | 87 | subidd 11608 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → ((𝐶‘𝐽) − (𝐶‘𝐽)) = 0) |
| 89 | 83, 88 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (𝑃 − (𝐶‘𝐽)) = 0) |
| 90 | 89 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (!‘(𝑃 − (𝐶‘𝐽))) = (!‘0)) |
| 91 | | fac0 14315 |
. . . . . . . . . . . . . . 15
⊢
(!‘0) = 1 |
| 92 | 90, 91 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (!‘(𝑃 − (𝐶‘𝐽))) = 1) |
| 93 | 92 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) = ((!‘𝑃) / 1)) |
| 94 | 3 | nncnd 12282 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (!‘𝑃) ∈ ℂ) |
| 95 | 94 | div1d 12035 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((!‘𝑃) / 1) = (!‘𝑃)) |
| 96 | 95 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → ((!‘𝑃) / 1) = (!‘𝑃)) |
| 97 | 93, 96 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) = (!‘𝑃)) |
| 98 | 89 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (0↑(𝑃 − (𝐶‘𝐽))) = (0↑0)) |
| 99 | | 0cnd 11254 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → 0 ∈ ℂ) |
| 100 | 99 | exp0d 14180 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (0↑0) = 1) |
| 101 | 98, 100 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (0↑(𝑃 − (𝐶‘𝐽))) = 1) |
| 102 | 97, 101 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = ((!‘𝑃) · 1)) |
| 103 | 94 | mulridd 11278 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((!‘𝑃) · 1) = (!‘𝑃)) |
| 104 | 103 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → ((!‘𝑃) · 1) = (!‘𝑃)) |
| 105 | 102, 104 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = (!‘𝑃)) |
| 106 | 105 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ 𝑃 = (𝐶‘𝐽)) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = (!‘𝑃)) |
| 107 | 81, 106 | eqtr2d 2778 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ 𝑃 = (𝐶‘𝐽)) → (!‘𝑃) = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
| 108 | 79, 107 | breqtrd 5169 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ 𝑃 = (𝐶‘𝐽)) → (!‘𝑃) ∥ if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
| 109 | 71 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (!‘𝑃) ∥ 0) |
| 110 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → ¬ 𝑃 < (𝐶‘𝐽)) |
| 111 | 110 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → ¬ 𝑃 < (𝐶‘𝐽)) |
| 112 | 111 | iffalsed 4536 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) |
| 113 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → 𝜑) |
| 114 | 85 | zred 12722 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶‘𝐽) ∈ ℝ) |
| 115 | 114 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (𝐶‘𝐽) ∈ ℝ) |
| 116 | 1 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℝ) |
| 117 | 116 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → 𝑃 ∈ ℝ) |
| 118 | 114 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (𝐶‘𝐽) ∈ ℝ) |
| 119 | 116 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → 𝑃 ∈ ℝ) |
| 120 | 118, 119,
110 | nltled 11411 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (𝐶‘𝐽) ≤ 𝑃) |
| 121 | 120 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (𝐶‘𝐽) ≤ 𝑃) |
| 122 | | neqne 2948 |
. . . . . . . . . . . 12
⊢ (¬
𝑃 = (𝐶‘𝐽) → 𝑃 ≠ (𝐶‘𝐽)) |
| 123 | 122 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → 𝑃 ≠ (𝐶‘𝐽)) |
| 124 | 115, 117,
121, 123 | leneltd 11415 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (𝐶‘𝐽) < 𝑃) |
| 125 | 1 | nnzd 12640 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℤ) |
| 126 | 125 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → 𝑃 ∈ ℤ) |
| 127 | 85 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝐶‘𝐽) ∈ ℤ) |
| 128 | 126, 127 | zsubcld 12727 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝑃 − (𝐶‘𝐽)) ∈ ℤ) |
| 129 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝐶‘𝐽) < 𝑃) |
| 130 | 114 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝐶‘𝐽) ∈ ℝ) |
| 131 | 116 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → 𝑃 ∈ ℝ) |
| 132 | 130, 131 | posdifd 11850 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → ((𝐶‘𝐽) < 𝑃 ↔ 0 < (𝑃 − (𝐶‘𝐽)))) |
| 133 | 129, 132 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → 0 < (𝑃 − (𝐶‘𝐽))) |
| 134 | | elnnz 12623 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 − (𝐶‘𝐽)) ∈ ℕ ↔ ((𝑃 − (𝐶‘𝐽)) ∈ ℤ ∧ 0 < (𝑃 − (𝐶‘𝐽)))) |
| 135 | 128, 133,
134 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝑃 − (𝐶‘𝐽)) ∈ ℕ) |
| 136 | 135 | 0expd 14179 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (0↑(𝑃 − (𝐶‘𝐽))) = 0) |
| 137 | 136 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · 0)) |
| 138 | 94 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (!‘𝑃) ∈ ℂ) |
| 139 | 135 | nnnn0d 12587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝑃 − (𝐶‘𝐽)) ∈
ℕ0) |
| 140 | 139 | faccld 14323 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (!‘(𝑃 − (𝐶‘𝐽))) ∈ ℕ) |
| 141 | 140 | nncnd 12282 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (!‘(𝑃 − (𝐶‘𝐽))) ∈ ℂ) |
| 142 | 140 | nnne0d 12316 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (!‘(𝑃 − (𝐶‘𝐽))) ≠ 0) |
| 143 | 138, 141,
142 | divcld 12043 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) ∈ ℂ) |
| 144 | 143 | mul01d 11460 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · 0) = 0) |
| 145 | 137, 144 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = 0) |
| 146 | 113, 124,
145 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = 0) |
| 147 | 112, 146 | eqtr2d 2778 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → 0 = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
| 148 | 109, 147 | breqtrd 5169 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (!‘𝑃) ∥ if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
| 149 | 108, 148 | pm2.61dan 813 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (!‘𝑃) ∥ if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
| 150 | 76, 149 | pm2.61dan 813 |
. . . . 5
⊢ (𝜑 → (!‘𝑃) ∥ if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
| 151 | 4, 58, 69, 150 | dvdsmultr1d 16334 |
. . . 4
⊢ (𝜑 → (!‘𝑃) ∥ (if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) · ∏𝑗 ∈ ((1...𝑀) ∖ {𝐽})if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) |
| 152 | 44 | zcnd 12723 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℂ) |
| 153 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → (𝐶‘𝑗) = (𝐶‘𝐽)) |
| 154 | 153 | breq2d 5155 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → (𝑃 < (𝐶‘𝑗) ↔ 𝑃 < (𝐶‘𝐽))) |
| 155 | 154 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → (𝑃 < (𝐶‘𝑗) ↔ 𝑃 < (𝐶‘𝐽))) |
| 156 | 153 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐽 → (𝑃 − (𝐶‘𝑗)) = (𝑃 − (𝐶‘𝐽))) |
| 157 | 156 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (!‘(𝑃 − (𝐶‘𝑗))) = (!‘(𝑃 − (𝐶‘𝐽)))) |
| 158 | 157 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) = ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽))))) |
| 159 | 158 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) = ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽))))) |
| 160 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (𝐽 − 𝑗) = (𝐽 − 𝐽)) |
| 161 | 160, 48 | sylan9eqr 2799 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → (𝐽 − 𝑗) = 0) |
| 162 | 156 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → (𝑃 − (𝐶‘𝑗)) = (𝑃 − (𝐶‘𝐽))) |
| 163 | 161, 162 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))) = (0↑(𝑃 − (𝐶‘𝐽)))) |
| 164 | 159, 163 | oveq12d 7449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) |
| 165 | 155, 164 | ifbieq2d 4552 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
| 166 | 31, 152, 27, 165 | fprodsplit1 45608 |
. . . 4
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) = (if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) · ∏𝑗 ∈ ((1...𝑀) ∖ {𝐽})if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) |
| 167 | 151, 166 | breqtrrd 5171 |
. . 3
⊢ (𝜑 → (!‘𝑃) ∥ ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))) |
| 168 | | dvdsmultr2 16335 |
. . 3
⊢
(((!‘𝑃) ∈
ℤ ∧ (((!‘𝑁)
/ ∏𝑗 ∈
(0...𝑀)(!‘(𝐶‘𝑗))) · if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))))) ∈ ℤ ∧
∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) → ((!‘𝑃) ∥ ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) → (!‘𝑃) ∥ ((((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))))) |
| 169 | 46, 167, 168 | sylc 65 |
. 2
⊢ (𝜑 → (!‘𝑃) ∥ ((((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) |
| 170 | | etransclem25.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 171 | 170 | faccld 14323 |
. . . . . 6
⊢ (𝜑 → (!‘𝑁) ∈ ℕ) |
| 172 | 171 | nncnd 12282 |
. . . . 5
⊢ (𝜑 → (!‘𝑁) ∈ ℂ) |
| 173 | 11 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐶‘𝑗) ∈ (0...𝑁)) |
| 174 | 13, 173 | sselid 3981 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐶‘𝑗) ∈
ℕ0) |
| 175 | 174 | faccld 14323 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐶‘𝑗)) ∈ ℕ) |
| 176 | 175 | nncnd 12282 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐶‘𝑗)) ∈ ℂ) |
| 177 | 10, 176 | fprodcl 15988 |
. . . . 5
⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗)) ∈ ℂ) |
| 178 | 175 | nnne0d 12316 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐶‘𝑗)) ≠ 0) |
| 179 | 10, 176, 178 | fprodn0 16015 |
. . . . 5
⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗)) ≠ 0) |
| 180 | 172, 177,
179 | divcld 12043 |
. . . 4
⊢ (𝜑 → ((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) ∈ ℂ) |
| 181 | 29 | zcnd 12723 |
. . . 4
⊢ (𝜑 → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) ∈
ℂ) |
| 182 | 31, 152 | fprodcl 15988 |
. . . 4
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℂ) |
| 183 | 180, 181,
182 | mulassd 11284 |
. . 3
⊢ (𝜑 → ((((!‘𝑁) / ∏𝑗 ∈ (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, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))))) |
| 184 | | etransclem25.t |
. . 3
⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) |
| 185 | 183, 184 | eqtr4di 2795 |
. 2
⊢ (𝜑 → ((((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))) = 𝑇) |
| 186 | 169, 185 | breqtrd 5169 |
1
⊢ (𝜑 → (!‘𝑃) ∥ 𝑇) |