| Step | Hyp | Ref
| Expression |
| 1 | | etransclem45.k |
. 2
⊢ 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1))) |
| 2 | | fzfi 14013 |
. . . . . 6
⊢
(0...𝑀) ∈
Fin |
| 3 | | fzfi 14013 |
. . . . . 6
⊢
(0...𝑅) ∈
Fin |
| 4 | | xpfi 9358 |
. . . . . 6
⊢
(((0...𝑀) ∈ Fin
∧ (0...𝑅) ∈ Fin)
→ ((0...𝑀) ×
(0...𝑅)) ∈
Fin) |
| 5 | 2, 3, 4 | mp2an 692 |
. . . . 5
⊢
((0...𝑀) ×
(0...𝑅)) ∈
Fin |
| 6 | 5 | a1i 11 |
. . . 4
⊢ (𝜑 → ((0...𝑀) × (0...𝑅)) ∈ Fin) |
| 7 | | etransclem45.p |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 8 | | nnm1nn0 12567 |
. . . . . . 7
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
| 9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
| 10 | 9 | faccld 14323 |
. . . . 5
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℕ) |
| 11 | 10 | nncnd 12282 |
. . . 4
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℂ) |
| 12 | | etransclem45.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴:ℕ0⟶ℤ) |
| 13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → 𝐴:ℕ0⟶ℤ) |
| 14 | | xp1st 8046 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...𝑀) × (0...𝑅)) → (1st ‘𝑘) ∈ (0...𝑀)) |
| 15 | | elfznn0 13660 |
. . . . . . . . 9
⊢
((1st ‘𝑘) ∈ (0...𝑀) → (1st ‘𝑘) ∈
ℕ0) |
| 16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...𝑀) × (0...𝑅)) → (1st ‘𝑘) ∈
ℕ0) |
| 17 | 16 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (1st ‘𝑘) ∈
ℕ0) |
| 18 | 13, 17 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (𝐴‘(1st ‘𝑘)) ∈
ℤ) |
| 19 | 18 | zcnd 12723 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (𝐴‘(1st ‘𝑘)) ∈
ℂ) |
| 20 | | reelprrecn 11247 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
| 21 | 20 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → ℝ ∈ {ℝ,
ℂ}) |
| 22 | | reopn 45301 |
. . . . . . . . 9
⊢ ℝ
∈ (topGen‘ran (,)) |
| 23 | | tgioo4 24826 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 24 | 22, 23 | eleqtri 2839 |
. . . . . . . 8
⊢ ℝ
∈ ((TopOpen‘ℂfld) ↾t
ℝ) |
| 25 | 24 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → ℝ ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
| 26 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → 𝑃 ∈ ℕ) |
| 27 | | etransclem45.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 28 | 27 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → 𝑀 ∈
ℕ0) |
| 29 | | etransclem45.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
| 30 | | xp2nd 8047 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...𝑀) × (0...𝑅)) → (2nd ‘𝑘) ∈ (0...𝑅)) |
| 31 | | elfznn0 13660 |
. . . . . . . . 9
⊢
((2nd ‘𝑘) ∈ (0...𝑅) → (2nd ‘𝑘) ∈
ℕ0) |
| 32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0...𝑀) × (0...𝑅)) → (2nd ‘𝑘) ∈
ℕ0) |
| 33 | 32 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (2nd ‘𝑘) ∈
ℕ0) |
| 34 | 21, 25, 26, 28, 29, 33 | etransclem33 46282 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → ((ℝ D𝑛
𝐹)‘(2nd
‘𝑘)):ℝ⟶ℂ) |
| 35 | 17 | nn0red 12588 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (1st ‘𝑘) ∈
ℝ) |
| 36 | 34, 35 | ffvelcdmd 7105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (((ℝ D𝑛
𝐹)‘(2nd
‘𝑘))‘(1st ‘𝑘)) ∈
ℂ) |
| 37 | 19, 36 | mulcld 11281 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → ((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℂ) |
| 38 | 10 | nnne0d 12316 |
. . . 4
⊢ (𝜑 → (!‘(𝑃 − 1)) ≠
0) |
| 39 | 6, 11, 37, 38 | fsumdivc 15822 |
. . 3
⊢ (𝜑 → (Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1))) =
Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))(((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1)))) |
| 40 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (!‘(𝑃 − 1)) ∈
ℂ) |
| 41 | 38 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (!‘(𝑃 − 1)) ≠ 0) |
| 42 | 19, 36, 40, 41 | divassd 12078 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1))) =
((𝐴‘(1st
‘𝑘)) ·
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 −
1))))) |
| 43 | | etransclem5 46254 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
| 44 | | etransclem11 46260 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚) ↑m
(0...𝑀)) ∣
Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) |
| 45 | 14 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (1st ‘𝑘) ∈ (0...𝑀)) |
| 46 | 21, 25, 26, 28, 29, 33, 43, 44, 45, 35 | etransclem37 46286 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (!‘(𝑃 − 1)) ∥ (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) |
| 47 | 10 | nnzd 12640 |
. . . . . . . . 9
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℤ) |
| 48 | 47 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (!‘(𝑃 − 1)) ∈
ℤ) |
| 49 | 17 | nn0zd 12639 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (1st ‘𝑘) ∈
ℤ) |
| 50 | 21, 25, 26, 28, 29, 33, 35, 49 | etransclem42 46291 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (((ℝ D𝑛
𝐹)‘(2nd
‘𝑘))‘(1st ‘𝑘)) ∈
ℤ) |
| 51 | | dvdsval2 16293 |
. . . . . . . 8
⊢
(((!‘(𝑃
− 1)) ∈ ℤ ∧ (!‘(𝑃 − 1)) ≠ 0 ∧ (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ∈ ℤ)
→ ((!‘(𝑃 −
1)) ∥ (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ↔
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ)) |
| 52 | 48, 41, 50, 51 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → ((!‘(𝑃 − 1)) ∥ (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ↔
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ)) |
| 53 | 46, 52 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → ((((ℝ D𝑛
𝐹)‘(2nd
‘𝑘))‘(1st ‘𝑘)) / (!‘(𝑃 − 1))) ∈
ℤ) |
| 54 | 18, 53 | zmulcld 12728 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → ((𝐴‘(1st ‘𝑘)) · ((((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1))))
∈ ℤ) |
| 55 | 42, 54 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...𝑅))) → (((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1)))
∈ ℤ) |
| 56 | 6, 55 | fsumzcl 15771 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))(((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1)))
∈ ℤ) |
| 57 | 39, 56 | eqeltrd 2841 |
. 2
⊢ (𝜑 → (Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1)))
∈ ℤ) |
| 58 | 1, 57 | eqeltrid 2845 |
1
⊢ (𝜑 → 𝐾 ∈ ℤ) |