Proof of Theorem etransclem25
Step | Hyp | Ref
| Expression |
1 | | etransclem25.p |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
2 | 1 | nnnn0d 11228 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
3 | 2 | faccld 12933 |
. . . . 5
⊢ (𝜑 → (!‘𝑃) ∈ ℕ) |
4 | 3 | nnzd 11357 |
. . . 4
⊢ (𝜑 → (!‘𝑃) ∈ ℤ) |
5 | | etransclem25.sumc |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗) = 𝑁) |
6 | 5 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 = Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗)) |
7 | 6 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 → (!‘𝑁) = (!‘Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗))) |
8 | 7 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → ((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) = ((!‘Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗)))) |
9 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑗𝐶 |
10 | | fzfid 12634 |
. . . . . . . 8
⊢ (𝜑 → (0...𝑀) ∈ Fin) |
11 | | etransclem25.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) |
12 | | nn0ex 11175 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
13 | | fzssnn0 38474 |
. . . . . . . . . . 11
⊢
(0...𝑁) ⊆
ℕ0 |
14 | | mapss 7786 |
. . . . . . . . . . 11
⊢
((ℕ0 ∈ V ∧ (0...𝑁) ⊆ ℕ0) →
((0...𝑁)
↑𝑚 (0...𝑀)) ⊆ (ℕ0
↑𝑚 (0...𝑀))) |
15 | 12, 13, 14 | mp2an 704 |
. . . . . . . . . 10
⊢
((0...𝑁)
↑𝑚 (0...𝑀)) ⊆ (ℕ0
↑𝑚 (0...𝑀)) |
16 | | ovex 6577 |
. . . . . . . . . . . 12
⊢
(0...𝑁) ∈
V |
17 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
(0...𝑀) ∈
V |
18 | 17 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐶:(0...𝑀)⟶(0...𝑁) → (0...𝑀) ∈ V) |
19 | | elmapg 7757 |
. . . . . . . . . . . 12
⊢
(((0...𝑁) ∈ V
∧ (0...𝑀) ∈ V)
→ (𝐶 ∈
((0...𝑁)
↑𝑚 (0...𝑀)) ↔ 𝐶:(0...𝑀)⟶(0...𝑁))) |
20 | 16, 18, 19 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝐶:(0...𝑀)⟶(0...𝑁) → (𝐶 ∈ ((0...𝑁) ↑𝑚 (0...𝑀)) ↔ 𝐶:(0...𝑀)⟶(0...𝑁))) |
21 | 20 | ibir 256 |
. . . . . . . . . 10
⊢ (𝐶:(0...𝑀)⟶(0...𝑁) → 𝐶 ∈ ((0...𝑁) ↑𝑚 (0...𝑀))) |
22 | 15, 21 | sseldi 3566 |
. . . . . . . . 9
⊢ (𝐶:(0...𝑀)⟶(0...𝑁) → 𝐶 ∈ (ℕ0
↑𝑚 (0...𝑀))) |
23 | 11, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (ℕ0
↑𝑚 (0...𝑀))) |
24 | 9, 10, 23 | mccl 38665 |
. . . . . . 7
⊢ (𝜑 → ((!‘Σ𝑗 ∈ (0...𝑀)(𝐶‘𝑗)) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) ∈ ℕ) |
25 | 8, 24 | eqeltrd 2688 |
. . . . . 6
⊢ (𝜑 → ((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) ∈ ℕ) |
26 | 25 | nnzd 11357 |
. . . . 5
⊢ (𝜑 → ((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) ∈ ℤ) |
27 | | etransclem25.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
28 | | etransclem25.j |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (1...𝑀)) |
29 | 28 | elfzelzd 38471 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℤ) |
30 | 1, 27, 11, 29 | etransclem10 39137 |
. . . . 5
⊢ (𝜑 → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) ∈
ℤ) |
31 | 26, 30 | zmulcld 11364 |
. . . 4
⊢ (𝜑 → (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))))) ∈
ℤ) |
32 | | fzfid 12634 |
. . . . 5
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
33 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑃 ∈ ℕ) |
34 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐶:(0...𝑀)⟶(0...𝑁)) |
35 | | 0z 11265 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
36 | | fzp1ss 12262 |
. . . . . . . . 9
⊢ (0 ∈
ℤ → ((0 + 1)...𝑀) ⊆ (0...𝑀)) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . 8
⊢ ((0 +
1)...𝑀) ⊆ (0...𝑀) |
38 | | id 22 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (1...𝑀)) |
39 | | 1e0p1 11428 |
. . . . . . . . . 10
⊢ 1 = (0 +
1) |
40 | 39 | oveq1i 6559 |
. . . . . . . . 9
⊢
(1...𝑀) = ((0 +
1)...𝑀) |
41 | 38, 40 | syl6eleq 2698 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ((0 + 1)...𝑀)) |
42 | 37, 41 | sseldi 3566 |
. . . . . . 7
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ (0...𝑀)) |
43 | 42 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ (0...𝑀)) |
44 | 29 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐽 ∈ ℤ) |
45 | 33, 34, 43, 44 | etransclem3 39130 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) |
46 | 32, 45 | fprodzcl 14523 |
. . . 4
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) |
47 | 4, 31, 46 | 3jca 1235 |
. . 3
⊢ (𝜑 → ((!‘𝑃) ∈ ℤ ∧
(((!‘𝑁) /
∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))))) ∈ ℤ ∧
∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ)) |
48 | 29 | zcnd 11359 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ ℂ) |
49 | 48 | subidd 10259 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 − 𝐽) = 0) |
50 | 49 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝜑 → 0 = (𝐽 − 𝐽)) |
51 | 50 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝜑 → (0↑(𝑃 − (𝐶‘𝐽))) = ((𝐽 − 𝐽)↑(𝑃 − (𝐶‘𝐽)))) |
52 | 51 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐽 − 𝐽)↑(𝑃 − (𝐶‘𝐽))))) |
53 | 52 | ifeq2d 4055 |
. . . . . 6
⊢ (𝜑 → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐽 − 𝐽)↑(𝑃 − (𝐶‘𝐽)))))) |
54 | | id 22 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (1...𝑀) → 𝐽 ∈ (1...𝑀)) |
55 | 54, 40 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (𝐽 ∈ (1...𝑀) → 𝐽 ∈ ((0 + 1)...𝑀)) |
56 | 37, 55 | sseldi 3566 |
. . . . . . . 8
⊢ (𝐽 ∈ (1...𝑀) → 𝐽 ∈ (0...𝑀)) |
57 | 28, 56 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) |
58 | 1, 11, 57, 29 | etransclem3 39130 |
. . . . . 6
⊢ (𝜑 → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐽 − 𝐽)↑(𝑃 − (𝐶‘𝐽))))) ∈ ℤ) |
59 | 53, 58 | eqeltrd 2688 |
. . . . 5
⊢ (𝜑 → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) ∈ ℤ) |
60 | | fzfi 12633 |
. . . . . . 7
⊢
(1...𝑀) ∈
Fin |
61 | | diffi 8077 |
. . . . . . 7
⊢
((1...𝑀) ∈ Fin
→ ((1...𝑀) ∖
{𝐽}) ∈
Fin) |
62 | 60, 61 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → ((1...𝑀) ∖ {𝐽}) ∈ Fin) |
63 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...𝑀) ∖ {𝐽})) → 𝑃 ∈ ℕ) |
64 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...𝑀) ∖ {𝐽})) → 𝐶:(0...𝑀)⟶(0...𝑁)) |
65 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑗 ∈ ((1...𝑀) ∖ {𝐽}) → 𝑗 ∈ (1...𝑀)) |
66 | 65, 42 | syl 17 |
. . . . . . . 8
⊢ (𝑗 ∈ ((1...𝑀) ∖ {𝐽}) → 𝑗 ∈ (0...𝑀)) |
67 | 66 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...𝑀) ∖ {𝐽})) → 𝑗 ∈ (0...𝑀)) |
68 | 29 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...𝑀) ∖ {𝐽})) → 𝐽 ∈ ℤ) |
69 | 63, 64, 67, 68 | etransclem3 39130 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ((1...𝑀) ∖ {𝐽})) → if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) |
70 | 62, 69 | fprodzcl 14523 |
. . . . 5
⊢ (𝜑 → ∏𝑗 ∈ ((1...𝑀) ∖ {𝐽})if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) |
71 | | dvds0 14835 |
. . . . . . . . 9
⊢
((!‘𝑃) ∈
ℤ → (!‘𝑃)
∥ 0) |
72 | 4, 71 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (!‘𝑃) ∥ 0) |
73 | 72 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 < (𝐶‘𝐽)) → (!‘𝑃) ∥ 0) |
74 | | iftrue 4042 |
. . . . . . . . 9
⊢ (𝑃 < (𝐶‘𝐽) → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) = 0) |
75 | 74 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑃 < (𝐶‘𝐽) → 0 = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
76 | 75 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 < (𝐶‘𝐽)) → 0 = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
77 | 73, 76 | breqtrd 4609 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑃 < (𝐶‘𝐽)) → (!‘𝑃) ∥ if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
78 | | iddvds 14833 |
. . . . . . . . . 10
⊢
((!‘𝑃) ∈
ℤ → (!‘𝑃)
∥ (!‘𝑃)) |
79 | 4, 78 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (!‘𝑃) ∥ (!‘𝑃)) |
80 | 79 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ 𝑃 = (𝐶‘𝐽)) → (!‘𝑃) ∥ (!‘𝑃)) |
81 | | iffalse 4045 |
. . . . . . . . . 10
⊢ (¬
𝑃 < (𝐶‘𝐽) → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) |
82 | 81 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ 𝑃 = (𝐶‘𝐽)) → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) |
83 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 = (𝐶‘𝐽) → (𝑃 − (𝐶‘𝐽)) = ((𝐶‘𝐽) − (𝐶‘𝐽))) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (𝑃 − (𝐶‘𝐽)) = ((𝐶‘𝐽) − (𝐶‘𝐽))) |
85 | 11, 57 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐶‘𝐽) ∈ (0...𝑁)) |
86 | 85 | elfzelzd 38471 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐶‘𝐽) ∈ ℤ) |
87 | 86 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐶‘𝐽) ∈ ℂ) |
88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (𝐶‘𝐽) ∈ ℂ) |
89 | 88 | subidd 10259 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → ((𝐶‘𝐽) − (𝐶‘𝐽)) = 0) |
90 | 84, 89 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (𝑃 − (𝐶‘𝐽)) = 0) |
91 | 90 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (!‘(𝑃 − (𝐶‘𝐽))) = (!‘0)) |
92 | | fac0 12925 |
. . . . . . . . . . . . . . 15
⊢
(!‘0) = 1 |
93 | 91, 92 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (!‘(𝑃 − (𝐶‘𝐽))) = 1) |
94 | 93 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) = ((!‘𝑃) / 1)) |
95 | 3 | nncnd 10913 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (!‘𝑃) ∈ ℂ) |
96 | 95 | div1d 10672 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((!‘𝑃) / 1) = (!‘𝑃)) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → ((!‘𝑃) / 1) = (!‘𝑃)) |
98 | 94, 97 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) = (!‘𝑃)) |
99 | 90 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (0↑(𝑃 − (𝐶‘𝐽))) = (0↑0)) |
100 | | 0cnd 9912 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → 0 ∈ ℂ) |
101 | 100 | exp0d 12864 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (0↑0) = 1) |
102 | 99, 101 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (0↑(𝑃 − (𝐶‘𝐽))) = 1) |
103 | 98, 102 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = ((!‘𝑃) · 1)) |
104 | 95 | mulid1d 9936 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((!‘𝑃) · 1) = (!‘𝑃)) |
105 | 104 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → ((!‘𝑃) · 1) = (!‘𝑃)) |
106 | 103, 105 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 = (𝐶‘𝐽)) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = (!‘𝑃)) |
107 | 106 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ 𝑃 = (𝐶‘𝐽)) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = (!‘𝑃)) |
108 | 82, 107 | eqtr2d 2645 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ 𝑃 = (𝐶‘𝐽)) → (!‘𝑃) = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
109 | 80, 108 | breqtrd 4609 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ 𝑃 = (𝐶‘𝐽)) → (!‘𝑃) ∥ if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
110 | 72 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (!‘𝑃) ∥ 0) |
111 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → ¬ 𝑃 < (𝐶‘𝐽)) |
112 | 111 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → ¬ 𝑃 < (𝐶‘𝐽)) |
113 | 112 | iffalsed 4047 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) |
114 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → 𝜑) |
115 | 86 | zred 11358 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶‘𝐽) ∈ ℝ) |
116 | 115 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (𝐶‘𝐽) ∈ ℝ) |
117 | 1 | nnred 10912 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℝ) |
118 | 117 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → 𝑃 ∈ ℝ) |
119 | 115 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (𝐶‘𝐽) ∈ ℝ) |
120 | 117 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → 𝑃 ∈ ℝ) |
121 | 119, 120,
111 | nltled 10066 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (𝐶‘𝐽) ≤ 𝑃) |
122 | 121 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (𝐶‘𝐽) ≤ 𝑃) |
123 | | neqne 2790 |
. . . . . . . . . . . 12
⊢ (¬
𝑃 = (𝐶‘𝐽) → 𝑃 ≠ (𝐶‘𝐽)) |
124 | 123 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → 𝑃 ≠ (𝐶‘𝐽)) |
125 | 116, 118,
122, 124 | leneltd 10070 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (𝐶‘𝐽) < 𝑃) |
126 | 1 | nnzd 11357 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℤ) |
127 | 126 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → 𝑃 ∈ ℤ) |
128 | 86 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝐶‘𝐽) ∈ ℤ) |
129 | 127, 128 | zsubcld 11363 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝑃 − (𝐶‘𝐽)) ∈ ℤ) |
130 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝐶‘𝐽) < 𝑃) |
131 | 115 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝐶‘𝐽) ∈ ℝ) |
132 | 117 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → 𝑃 ∈ ℝ) |
133 | 131, 132 | posdifd 10493 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → ((𝐶‘𝐽) < 𝑃 ↔ 0 < (𝑃 − (𝐶‘𝐽)))) |
134 | 130, 133 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → 0 < (𝑃 − (𝐶‘𝐽))) |
135 | | elnnz 11264 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 − (𝐶‘𝐽)) ∈ ℕ ↔ ((𝑃 − (𝐶‘𝐽)) ∈ ℤ ∧ 0 < (𝑃 − (𝐶‘𝐽)))) |
136 | 129, 134,
135 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝑃 − (𝐶‘𝐽)) ∈ ℕ) |
137 | 136 | 0expd 12886 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (0↑(𝑃 − (𝐶‘𝐽))) = 0) |
138 | 137 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · 0)) |
139 | 95 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (!‘𝑃) ∈ ℂ) |
140 | 136 | nnnn0d 11228 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (𝑃 − (𝐶‘𝐽)) ∈
ℕ0) |
141 | 140 | faccld 12933 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (!‘(𝑃 − (𝐶‘𝐽))) ∈ ℕ) |
142 | 141 | nncnd 10913 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (!‘(𝑃 − (𝐶‘𝐽))) ∈ ℂ) |
143 | 141 | nnne0d 10942 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (!‘(𝑃 − (𝐶‘𝐽))) ≠ 0) |
144 | 139, 142,
143 | divcld 10680 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) ∈ ℂ) |
145 | 144 | mul01d 10114 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · 0) = 0) |
146 | 138, 145 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶‘𝐽) < 𝑃) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = 0) |
147 | 114, 125,
146 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))) = 0) |
148 | 113, 147 | eqtr2d 2645 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → 0 = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
149 | 110, 148 | breqtrd 4609 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) ∧ ¬ 𝑃 = (𝐶‘𝐽)) → (!‘𝑃) ∥ if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
150 | 109, 149 | pm2.61dan 828 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑃 < (𝐶‘𝐽)) → (!‘𝑃) ∥ if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
151 | 77, 150 | pm2.61dan 828 |
. . . . 5
⊢ (𝜑 → (!‘𝑃) ∥ if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
152 | 4, 59, 70, 151 | dvdsmultr1d 14858 |
. . . 4
⊢ (𝜑 → (!‘𝑃) ∥ (if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) · ∏𝑗 ∈ ((1...𝑀) ∖ {𝐽})if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) |
153 | 45 | zcnd 11359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℂ) |
154 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → (𝐶‘𝑗) = (𝐶‘𝐽)) |
155 | 154 | breq2d 4595 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → (𝑃 < (𝐶‘𝑗) ↔ 𝑃 < (𝐶‘𝐽))) |
156 | 155 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → (𝑃 < (𝐶‘𝑗) ↔ 𝑃 < (𝐶‘𝐽))) |
157 | 154 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐽 → (𝑃 − (𝐶‘𝑗)) = (𝑃 − (𝐶‘𝐽))) |
158 | 157 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (!‘(𝑃 − (𝐶‘𝑗))) = (!‘(𝑃 − (𝐶‘𝐽)))) |
159 | 158 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) = ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽))))) |
160 | 159 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) = ((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽))))) |
161 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (𝐽 − 𝑗) = (𝐽 − 𝐽)) |
162 | 161, 49 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → (𝐽 − 𝑗) = 0) |
163 | 157 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → (𝑃 − (𝐶‘𝑗)) = (𝑃 − (𝐶‘𝐽))) |
164 | 162, 163 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))) = (0↑(𝑃 − (𝐶‘𝐽)))) |
165 | 160, 164 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))) = (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) |
166 | 156, 165 | ifbieq2d 4061 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) = if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽)))))) |
167 | 32, 153, 28, 166 | fprodsplit1 38660 |
. . . 4
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) = (if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · (0↑(𝑃 − (𝐶‘𝐽))))) · ∏𝑗 ∈ ((1...𝑀) ∖ {𝐽})if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) |
168 | 152, 167 | breqtrrd 4611 |
. . 3
⊢ (𝜑 → (!‘𝑃) ∥ ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))) |
169 | | dvdsmultr2 14859 |
. . 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, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))))) |
170 | 47, 168, 169 | sylc 63 |
. 2
⊢ (𝜑 → (!‘𝑃) ∥ ((((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) |
171 | | etransclem25.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
172 | 171 | faccld 12933 |
. . . . . 6
⊢ (𝜑 → (!‘𝑁) ∈ ℕ) |
173 | 172 | nncnd 10913 |
. . . . 5
⊢ (𝜑 → (!‘𝑁) ∈ ℂ) |
174 | 11 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐶‘𝑗) ∈ (0...𝑁)) |
175 | 13, 174 | sseldi 3566 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐶‘𝑗) ∈
ℕ0) |
176 | 175 | faccld 12933 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐶‘𝑗)) ∈ ℕ) |
177 | 176 | nncnd 10913 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐶‘𝑗)) ∈ ℂ) |
178 | 10, 177 | fprodcl 14521 |
. . . . 5
⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗)) ∈ ℂ) |
179 | 176 | nnne0d 10942 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝐶‘𝑗)) ≠ 0) |
180 | 10, 177, 179 | fprodn0 14548 |
. . . . 5
⊢ (𝜑 → ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗)) ≠ 0) |
181 | 173, 178,
180 | divcld 10680 |
. . . 4
⊢ (𝜑 → ((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) ∈ ℂ) |
182 | 30 | zcnd 11359 |
. . . 4
⊢ (𝜑 → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) ∈
ℂ) |
183 | 32, 153 | fprodcl 14521 |
. . . 4
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℂ) |
184 | 181, 182,
183 | mulassd 9942 |
. . 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, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))))) |
185 | | etransclem25.t |
. . 3
⊢ 𝑇 = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · (if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))))) |
186 | 184, 185 | syl6eqr 2662 |
. 2
⊢ (𝜑 → ((((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝐶‘𝑗))) · if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0)))))) · ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗)))))) = 𝑇) |
187 | 170, 186 | breqtrd 4609 |
1
⊢ (𝜑 → (!‘𝑃) ∥ 𝑇) |