| Step | Hyp | Ref
| Expression |
| 1 | | etransclem44.k |
. . . 4
⊢ 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1))) |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐾 = (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1)))) |
| 3 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
| 4 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑘((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) |
| 5 | | fzfi 14013 |
. . . . . . 7
⊢
(0...𝑀) ∈
Fin |
| 6 | | fzfi 14013 |
. . . . . . 7
⊢
(0...((𝑀 ·
𝑃) + (𝑃 − 1))) ∈ Fin |
| 7 | | xpfi 9358 |
. . . . . . 7
⊢
(((0...𝑀) ∈ Fin
∧ (0...((𝑀 ·
𝑃) + (𝑃 − 1))) ∈ Fin) → ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin) |
| 8 | 5, 6, 7 | mp2an 692 |
. . . . . 6
⊢
((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin |
| 9 | 8 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin) |
| 10 | | etransclem44.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:ℕ0⟶ℤ) |
| 11 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝐴:ℕ0⟶ℤ) |
| 12 | | fzssnn0 45329 |
. . . . . . . . . 10
⊢
(0...𝑀) ⊆
ℕ0 |
| 13 | | xp1st 8046 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (1st
‘𝑘) ∈ (0...𝑀)) |
| 14 | 12, 13 | sselid 3981 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (1st
‘𝑘) ∈
ℕ0) |
| 15 | 14 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st
‘𝑘) ∈
ℕ0) |
| 16 | 11, 15 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (𝐴‘(1st ‘𝑘)) ∈
ℤ) |
| 17 | | reelprrecn 11247 |
. . . . . . . . 9
⊢ ℝ
∈ {ℝ, ℂ} |
| 18 | 17 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ℝ ∈
{ℝ, ℂ}) |
| 19 | | reopn 45301 |
. . . . . . . . . 10
⊢ ℝ
∈ (topGen‘ran (,)) |
| 20 | | tgioo4 24826 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 21 | 19, 20 | eleqtri 2839 |
. . . . . . . . 9
⊢ ℝ
∈ ((TopOpen‘ℂfld) ↾t
ℝ) |
| 22 | 21 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ℝ ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
| 23 | | etransclem44.p |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 24 | | prmnn 16711 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 26 | 25 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝑃 ∈ ℕ) |
| 27 | | etransclem44.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 28 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝑀 ∈
ℕ0) |
| 29 | | etransclem44.f |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
| 30 | | xp2nd 8047 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (2nd
‘𝑘) ∈
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) |
| 31 | | elfznn0 13660 |
. . . . . . . . . 10
⊢
((2nd ‘𝑘) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))) → (2nd
‘𝑘) ∈
ℕ0) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (2nd
‘𝑘) ∈
ℕ0) |
| 33 | 32 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (2nd
‘𝑘) ∈
ℕ0) |
| 34 | 15 | nn0red 12588 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st
‘𝑘) ∈
ℝ) |
| 35 | 15 | nn0zd 12639 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st
‘𝑘) ∈
ℤ) |
| 36 | 18, 22, 26, 28, 29, 33, 34, 35 | etransclem42 46291 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ∈
ℤ) |
| 37 | 16, 36 | zmulcld 12728 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℤ) |
| 38 | 37 | zcnd 12723 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℂ) |
| 39 | | nn0uz 12920 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
| 40 | 27, 39 | eleqtrdi 2851 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
| 41 | | eluzfz1 13571 |
. . . . . . 7
⊢ (𝑀 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑀)) |
| 42 | 40, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
| 43 | | 0zd 12625 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
| 44 | 27 | nn0zd 12639 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 45 | 25 | nnzd 12640 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℤ) |
| 46 | 44, 45 | zmulcld 12728 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℤ) |
| 47 | | nnm1nn0 12567 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
| 48 | 25, 47 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
| 49 | 48 | nn0zd 12639 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 − 1) ∈ ℤ) |
| 50 | 46, 49 | zaddcld 12726 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈
ℤ) |
| 51 | 48 | nn0ge0d 12590 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑃 − 1)) |
| 52 | 25 | nnnn0d 12587 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
| 53 | 27, 52 | nn0mulcld 12592 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑃) ∈
ℕ0) |
| 54 | 53 | nn0ge0d 12590 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (𝑀 · 𝑃)) |
| 55 | 48 | nn0red 12588 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 1) ∈ ℝ) |
| 56 | 46 | zred 12722 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℝ) |
| 57 | 55, 56 | addge02d 11852 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (𝑀 · 𝑃) ↔ (𝑃 − 1) ≤ ((𝑀 · 𝑃) + (𝑃 − 1)))) |
| 58 | 54, 57 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → (𝑃 − 1) ≤ ((𝑀 · 𝑃) + (𝑃 − 1))) |
| 59 | 43, 50, 49, 51, 58 | elfzd 13555 |
. . . . . 6
⊢ (𝜑 → (𝑃 − 1) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))) |
| 60 | | opelxp 5721 |
. . . . . 6
⊢ (〈0,
(𝑃 − 1)〉 ∈
((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) ↔ (0 ∈ (0...𝑀) ∧ (𝑃 − 1) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))))) |
| 61 | 42, 59, 60 | sylanbrc 583 |
. . . . 5
⊢ (𝜑 → 〈0, (𝑃 − 1)〉 ∈
((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1))))) |
| 62 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (1st
‘𝑘) = (1st
‘〈0, (𝑃 −
1)〉)) |
| 63 | | 0re 11263 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
| 64 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑃 − 1) ∈
V |
| 65 | | op1stg 8026 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ (𝑃
− 1) ∈ V) → (1st ‘〈0, (𝑃 − 1)〉) = 0) |
| 66 | 63, 64, 65 | mp2an 692 |
. . . . . . . 8
⊢
(1st ‘〈0, (𝑃 − 1)〉) = 0 |
| 67 | 62, 66 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (1st
‘𝑘) =
0) |
| 68 | 67 | fveq2d 6910 |
. . . . . 6
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (𝐴‘(1st ‘𝑘)) = (𝐴‘0)) |
| 69 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (2nd
‘𝑘) = (2nd
‘〈0, (𝑃 −
1)〉)) |
| 70 | | op2ndg 8027 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (𝑃
− 1) ∈ V) → (2nd ‘〈0, (𝑃 − 1)〉) = (𝑃 − 1)) |
| 71 | 63, 64, 70 | mp2an 692 |
. . . . . . . . 9
⊢
(2nd ‘〈0, (𝑃 − 1)〉) = (𝑃 − 1) |
| 72 | 69, 71 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (2nd
‘𝑘) = (𝑃 − 1)) |
| 73 | 72 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → ((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘)) = ((ℝ
D𝑛 𝐹)‘(𝑃 − 1))) |
| 74 | 73, 67 | fveq12d 6913 |
. . . . . 6
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) = (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) |
| 75 | 68, 74 | oveq12d 7449 |
. . . . 5
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → ((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) = ((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0))) |
| 76 | 3, 4, 9, 38, 61, 75 | fsumsplit1 15781 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) = (((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) + Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))))) |
| 77 | 76 | oveq1d 7446 |
. . 3
⊢ (𝜑 → (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1))) =
((((𝐴‘0) ·
(((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) + Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)))) /
(!‘(𝑃 −
1)))) |
| 78 | 12, 42 | sselid 3981 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℕ0) |
| 79 | 10, 78 | ffvelcdmd 7105 |
. . . . . 6
⊢ (𝜑 → (𝐴‘0) ∈ ℤ) |
| 80 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
| 81 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
| 82 | 63 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
| 83 | 80, 81, 25, 27, 29, 48, 82, 43 | etransclem42 46291 |
. . . . . 6
⊢ (𝜑 → (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈
ℤ) |
| 84 | 79, 83 | zmulcld 12728 |
. . . . 5
⊢ (𝜑 → ((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) ∈
ℤ) |
| 85 | 84 | zcnd 12723 |
. . . 4
⊢ (𝜑 → ((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) ∈
ℂ) |
| 86 | | difss 4136 |
. . . . . . . 8
⊢
(((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ⊆
((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) |
| 87 | | ssfi 9213 |
. . . . . . . 8
⊢
((((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin ∧ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ⊆
((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∈
Fin) |
| 88 | 8, 86, 87 | mp2an 692 |
. . . . . . 7
⊢
(((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∈
Fin |
| 89 | 88 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∈
Fin) |
| 90 | | eldifi 4131 |
. . . . . . 7
⊢ (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) → 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) |
| 91 | 90, 37 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℤ) |
| 92 | 89, 91 | fsumzcl 15771 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℤ) |
| 93 | 92 | zcnd 12723 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℂ) |
| 94 | 48 | faccld 14323 |
. . . . 5
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℕ) |
| 95 | 94 | nncnd 12282 |
. . . 4
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℂ) |
| 96 | 94 | nnne0d 12316 |
. . . 4
⊢ (𝜑 → (!‘(𝑃 − 1)) ≠
0) |
| 97 | 85, 93, 95, 96 | divdird 12081 |
. . 3
⊢ (𝜑 → ((((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) + Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)))) /
(!‘(𝑃 − 1))) =
((((𝐴‘0) ·
(((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) + (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1))))) |
| 98 | 2, 77, 97 | 3eqtrd 2781 |
. 2
⊢ (𝜑 → 𝐾 = ((((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) + (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1))))) |
| 99 | 25 | nnne0d 12316 |
. . 3
⊢ (𝜑 → 𝑃 ≠ 0) |
| 100 | 79 | zcnd 12723 |
. . . . 5
⊢ (𝜑 → (𝐴‘0) ∈ ℂ) |
| 101 | 83 | zcnd 12723 |
. . . . 5
⊢ (𝜑 → (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈
ℂ) |
| 102 | 100, 101,
95, 96 | divassd 12078 |
. . . 4
⊢ (𝜑 → (((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) = ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))) |
| 103 | | etransclem5 46254 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
| 104 | | etransclem11 46260 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚) ↑m
(0...𝑀)) ∣
Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) |
| 105 | 80, 81, 25, 27, 29, 48, 103, 104, 42, 82 | etransclem37 46286 |
. . . . . 6
⊢ (𝜑 → (!‘(𝑃 − 1)) ∥ (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) |
| 106 | 94 | nnzd 12640 |
. . . . . . 7
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℤ) |
| 107 | | dvdsval2 16293 |
. . . . . . 7
⊢
(((!‘(𝑃
− 1)) ∈ ℤ ∧ (!‘(𝑃 − 1)) ≠ 0 ∧ (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈ ℤ) →
((!‘(𝑃 − 1))
∥ (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ↔ ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈
ℤ)) |
| 108 | 106, 96, 83, 107 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → ((!‘(𝑃 − 1)) ∥ (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) ↔ ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈
ℤ)) |
| 109 | 105, 108 | mpbid 232 |
. . . . 5
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈
ℤ) |
| 110 | 79, 109 | zmulcld 12728 |
. . . 4
⊢ (𝜑 → ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ∈
ℤ) |
| 111 | 102, 110 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → (((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) ∈
ℤ) |
| 112 | 90, 38 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℂ) |
| 113 | 89, 95, 112, 96 | fsumdivc 15822 |
. . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1))) =
Σ𝑘 ∈
(((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})(((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1)))) |
| 114 | 16 | zcnd 12723 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (𝐴‘(1st ‘𝑘)) ∈
ℂ) |
| 115 | 90, 114 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(𝐴‘(1st
‘𝑘)) ∈
ℂ) |
| 116 | 90, 36 | sylan2 593 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ∈
ℤ) |
| 117 | 116 | zcnd 12723 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ∈
ℂ) |
| 118 | 95 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(!‘(𝑃 − 1))
∈ ℂ) |
| 119 | 96 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(!‘(𝑃 − 1))
≠ 0) |
| 120 | 115, 117,
118, 119 | divassd 12078 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1))) =
((𝐴‘(1st
‘𝑘)) ·
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 −
1))))) |
| 121 | 90, 16 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(𝐴‘(1st
‘𝑘)) ∈
ℤ) |
| 122 | 17 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
ℝ ∈ {ℝ, ℂ}) |
| 123 | 21 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
ℝ ∈ ((TopOpen‘ℂfld) ↾t
ℝ)) |
| 124 | 25 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑃 ∈
ℕ) |
| 125 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑀 ∈
ℕ0) |
| 126 | 90 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) |
| 127 | 126, 32 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(2nd ‘𝑘)
∈ ℕ0) |
| 128 | 126, 13 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(1st ‘𝑘)
∈ (0...𝑀)) |
| 129 | 90, 34 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(1st ‘𝑘)
∈ ℝ) |
| 130 | 122, 123,
124, 125, 29, 127, 103, 104, 128, 129 | etransclem37 46286 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(!‘(𝑃 − 1))
∥ (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) |
| 131 | 106 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(!‘(𝑃 − 1))
∈ ℤ) |
| 132 | | dvdsval2 16293 |
. . . . . . . . 9
⊢
(((!‘(𝑃
− 1)) ∈ ℤ ∧ (!‘(𝑃 − 1)) ≠ 0 ∧ (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ∈ ℤ)
→ ((!‘(𝑃 −
1)) ∥ (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ↔
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ)) |
| 133 | 131, 119,
116, 132 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
((!‘(𝑃 − 1))
∥ (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ↔
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ)) |
| 134 | 130, 133 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ) |
| 135 | 121, 134 | zmulcld 12728 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
((𝐴‘(1st
‘𝑘)) ·
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1))))
∈ ℤ) |
| 136 | 120, 135 | eqeltrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1)))
∈ ℤ) |
| 137 | 89, 136 | fsumzcl 15771 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})(((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1)))
∈ ℤ) |
| 138 | 113, 137 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1)))
∈ ℤ) |
| 139 | | 1zzd 12648 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) |
| 140 | | zabscl 15352 |
. . . . . . . . . . 11
⊢ ((𝐴‘0) ∈ ℤ →
(abs‘(𝐴‘0))
∈ ℤ) |
| 141 | 79, 140 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝐴‘0)) ∈
ℤ) |
| 142 | | nn0abscl 15351 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘0) ∈ ℤ →
(abs‘(𝐴‘0))
∈ ℕ0) |
| 143 | 79, 142 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝐴‘0)) ∈
ℕ0) |
| 144 | | etransclem44.a0 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴‘0) ≠ 0) |
| 145 | 100, 144 | absne0d 15486 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝐴‘0)) ≠
0) |
| 146 | | elnnne0 12540 |
. . . . . . . . . . . 12
⊢
((abs‘(𝐴‘0)) ∈ ℕ ↔
((abs‘(𝐴‘0))
∈ ℕ0 ∧ (abs‘(𝐴‘0)) ≠ 0)) |
| 147 | 143, 145,
146 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘(𝐴‘0)) ∈
ℕ) |
| 148 | 147 | nnge1d 12314 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≤ (abs‘(𝐴‘0))) |
| 149 | | etransclem44.ap |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘(𝐴‘0)) < 𝑃) |
| 150 | | zltlem1 12670 |
. . . . . . . . . . . 12
⊢
(((abs‘(𝐴‘0)) ∈ ℤ ∧ 𝑃 ∈ ℤ) →
((abs‘(𝐴‘0))
< 𝑃 ↔
(abs‘(𝐴‘0))
≤ (𝑃 −
1))) |
| 151 | 141, 45, 150 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs‘(𝐴‘0)) < 𝑃 ↔ (abs‘(𝐴‘0)) ≤ (𝑃 − 1))) |
| 152 | 149, 151 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝐴‘0)) ≤ (𝑃 − 1)) |
| 153 | 139, 49, 141, 148, 152 | elfzd 13555 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝐴‘0)) ∈ (1...(𝑃 − 1))) |
| 154 | | fzm1ndvds 16359 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℕ ∧
(abs‘(𝐴‘0))
∈ (1...(𝑃 − 1)))
→ ¬ 𝑃 ∥
(abs‘(𝐴‘0))) |
| 155 | 25, 153, 154 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑃 ∥ (abs‘(𝐴‘0))) |
| 156 | | dvdsabsb 16313 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧ (𝐴‘0) ∈ ℤ) →
(𝑃 ∥ (𝐴‘0) ↔ 𝑃 ∥ (abs‘(𝐴‘0)))) |
| 157 | 45, 79, 156 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 ∥ (𝐴‘0) ↔ 𝑃 ∥ (abs‘(𝐴‘0)))) |
| 158 | 155, 157 | mtbird 325 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑃 ∥ (𝐴‘0)) |
| 159 | | etransclem44.mp |
. . . . . . . 8
⊢ (𝜑 → (!‘𝑀) < 𝑃) |
| 160 | 27, 23, 159, 29 | etransclem41 46290 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) |
| 161 | 158, 160 | jca 511 |
. . . . . 6
⊢ (𝜑 → (¬ 𝑃 ∥ (𝐴‘0) ∧ ¬ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))) |
| 162 | | pm4.56 991 |
. . . . . 6
⊢ ((¬
𝑃 ∥ (𝐴‘0) ∧ ¬ 𝑃 ∥ ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ ¬
(𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))) |
| 163 | 161, 162 | sylib 218 |
. . . . 5
⊢ (𝜑 → ¬ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))) |
| 164 | | euclemma 16750 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴‘0) ∈ ℤ ∧
((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈ ℤ)
→ (𝑃 ∥ ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 −
1)))))) |
| 165 | 23, 79, 109, 164 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑃 ∥ ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 −
1)))))) |
| 166 | 163, 165 | mtbird 325 |
. . . 4
⊢ (𝜑 → ¬ 𝑃 ∥ ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))) |
| 167 | 102 | breq2d 5155 |
. . . 4
⊢ (𝜑 → (𝑃 ∥ (((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) ↔ 𝑃 ∥ ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 −
1)))))) |
| 168 | 166, 167 | mtbird 325 |
. . 3
⊢ (𝜑 → ¬ 𝑃 ∥ (((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1)))) |
| 169 | 45 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑃 ∈
ℤ) |
| 170 | 169, 121,
134 | 3jca 1129 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(𝑃 ∈ ℤ ∧
(𝐴‘(1st
‘𝑘)) ∈ ℤ
∧ ((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ)) |
| 171 | | eldifn 4132 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) → ¬
𝑘 ∈ {〈0, (𝑃 −
1)〉}) |
| 172 | 90 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∧
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) → 𝑘 ∈
((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1))))) |
| 173 | | 1st2nd2 8053 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → 𝑘 = 〈(1st ‘𝑘), (2nd ‘𝑘)〉) |
| 174 | 172, 173 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∧
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) → 𝑘 =
〈(1st ‘𝑘), (2nd ‘𝑘)〉) |
| 175 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘𝑘) = (𝑃 − 1) ∧ (1st
‘𝑘) = 0) →
(1st ‘𝑘) =
0) |
| 176 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘𝑘) = (𝑃 − 1) ∧ (1st
‘𝑘) = 0) →
(2nd ‘𝑘) =
(𝑃 −
1)) |
| 177 | 175, 176 | opeq12d 4881 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘𝑘) = (𝑃 − 1) ∧ (1st
‘𝑘) = 0) →
〈(1st ‘𝑘), (2nd ‘𝑘)〉 = 〈0, (𝑃 − 1)〉) |
| 178 | 177 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∧
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) → 〈(1st ‘𝑘), (2nd ‘𝑘)〉 = 〈0, (𝑃 − 1)〉) |
| 179 | 174, 178 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∧
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) → 𝑘 = 〈0,
(𝑃 −
1)〉) |
| 180 | | velsn 4642 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {〈0, (𝑃 − 1)〉} ↔ 𝑘 = 〈0, (𝑃 − 1)〉) |
| 181 | 179, 180 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∧
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) → 𝑘 ∈
{〈0, (𝑃 −
1)〉}) |
| 182 | 171, 181 | mtand 816 |
. . . . . . . . 9
⊢ (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) → ¬
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) |
| 183 | 182 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
¬ ((2nd ‘𝑘) = (𝑃 − 1) ∧ (1st
‘𝑘) =
0)) |
| 184 | 124, 125,
29, 127, 128, 183, 104 | etransclem38 46287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑃 ∥ ((((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 −
1)))) |
| 185 | | dvdsmultr2 16335 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧ (𝐴‘(1st
‘𝑘)) ∈ ℤ
∧ ((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ) → (𝑃
∥ ((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
→ 𝑃 ∥ ((𝐴‘(1st
‘𝑘)) ·
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 −
1)))))) |
| 186 | 170, 184,
185 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑃 ∥ ((𝐴‘(1st
‘𝑘)) ·
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 −
1))))) |
| 187 | 186, 120 | breqtrrd 5171 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑃 ∥ (((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1)))) |
| 188 | 89, 45, 136, 187 | fsumdvds 16345 |
. . . 4
⊢ (𝜑 → 𝑃 ∥ Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})(((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1)))) |
| 189 | 188, 113 | breqtrrd 5171 |
. . 3
⊢ (𝜑 → 𝑃 ∥ (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1)))) |
| 190 | 45, 99, 111, 138, 168, 189 | etransclem9 46258 |
. 2
⊢ (𝜑 → ((((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) + (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1))))
≠ 0) |
| 191 | 98, 190 | eqnetrd 3008 |
1
⊢ (𝜑 → 𝐾 ≠ 0) |