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 1922 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
4 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑘((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) |
5 | | fzfi 13545 |
. . . . . . 7
⊢
(0...𝑀) ∈
Fin |
6 | | fzfi 13545 |
. . . . . . 7
⊢
(0...((𝑀 ·
𝑃) + (𝑃 − 1))) ∈ Fin |
7 | | xpfi 8942 |
. . . . . . 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 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝐴:ℕ0⟶ℤ) |
12 | | fzssnn0 42529 |
. . . . . . . . . 10
⊢
(0...𝑀) ⊆
ℕ0 |
13 | | xp1st 7793 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (1st
‘𝑘) ∈ (0...𝑀)) |
14 | 12, 13 | sseldi 3899 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (1st
‘𝑘) ∈
ℕ0) |
15 | 14 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st
‘𝑘) ∈
ℕ0) |
16 | 11, 15 | ffvelrnd 6905 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (𝐴‘(1st ‘𝑘)) ∈
ℤ) |
17 | | reelprrecn 10821 |
. . . . . . . . 9
⊢ ℝ
∈ {ℝ, ℂ} |
18 | 17 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ℝ ∈
{ℝ, ℂ}) |
19 | | reopn 42500 |
. . . . . . . . . 10
⊢ ℝ
∈ (topGen‘ran (,)) |
20 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
21 | 20 | tgioo2 23700 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
22 | 19, 21 | eleqtri 2836 |
. . . . . . . . 9
⊢ ℝ
∈ ((TopOpen‘ℂfld) ↾t
ℝ) |
23 | 22 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ℝ ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
24 | | etransclem44.p |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℙ) |
25 | | prmnn 16231 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) |
27 | 26 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝑃 ∈ ℕ) |
28 | | etransclem44.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
29 | 28 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝑀 ∈
ℕ0) |
30 | | etransclem44.f |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
31 | | xp2nd 7794 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (2nd
‘𝑘) ∈
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) |
32 | | elfznn0 13205 |
. . . . . . . . . 10
⊢
((2nd ‘𝑘) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))) → (2nd
‘𝑘) ∈
ℕ0) |
33 | 31, 32 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (2nd
‘𝑘) ∈
ℕ0) |
34 | 33 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (2nd
‘𝑘) ∈
ℕ0) |
35 | 15 | nn0red 12151 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st
‘𝑘) ∈
ℝ) |
36 | 15 | nn0zd 12280 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1st
‘𝑘) ∈
ℤ) |
37 | 18, 23, 27, 29, 30, 34, 35, 36 | etransclem42 43492 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ∈
ℤ) |
38 | 16, 37 | zmulcld 12288 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℤ) |
39 | 38 | zcnd 12283 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℂ) |
40 | | nn0uz 12476 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
41 | 28, 40 | eleqtrdi 2848 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
42 | | eluzfz1 13119 |
. . . . . . 7
⊢ (𝑀 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑀)) |
43 | 41, 42 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
44 | | 0zd 12188 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
45 | 28 | nn0zd 12280 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
46 | 26 | nnzd 12281 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℤ) |
47 | 45, 46 | zmulcld 12288 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℤ) |
48 | | nnm1nn0 12131 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
49 | 26, 48 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
50 | 49 | nn0zd 12280 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 − 1) ∈ ℤ) |
51 | 47, 50 | zaddcld 12286 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈
ℤ) |
52 | 49 | nn0ge0d 12153 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑃 − 1)) |
53 | 26 | nnnn0d 12150 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
54 | 28, 53 | nn0mulcld 12155 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑃) ∈
ℕ0) |
55 | 54 | nn0ge0d 12153 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (𝑀 · 𝑃)) |
56 | 49 | nn0red 12151 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 1) ∈ ℝ) |
57 | 47 | zred 12282 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℝ) |
58 | 56, 57 | addge02d 11421 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (𝑀 · 𝑃) ↔ (𝑃 − 1) ≤ ((𝑀 · 𝑃) + (𝑃 − 1)))) |
59 | 55, 58 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → (𝑃 − 1) ≤ ((𝑀 · 𝑃) + (𝑃 − 1))) |
60 | 44, 51, 50, 52, 59 | elfzd 13103 |
. . . . . 6
⊢ (𝜑 → (𝑃 − 1) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))) |
61 | | opelxp 5587 |
. . . . . 6
⊢ (〈0,
(𝑃 − 1)〉 ∈
((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) ↔ (0 ∈ (0...𝑀) ∧ (𝑃 − 1) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))))) |
62 | 43, 60, 61 | sylanbrc 586 |
. . . . 5
⊢ (𝜑 → 〈0, (𝑃 − 1)〉 ∈
((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1))))) |
63 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (1st
‘𝑘) = (1st
‘〈0, (𝑃 −
1)〉)) |
64 | | 0re 10835 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
65 | | ovex 7246 |
. . . . . . . . 9
⊢ (𝑃 − 1) ∈
V |
66 | | op1stg 7773 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ (𝑃
− 1) ∈ V) → (1st ‘〈0, (𝑃 − 1)〉) = 0) |
67 | 64, 65, 66 | mp2an 692 |
. . . . . . . 8
⊢
(1st ‘〈0, (𝑃 − 1)〉) = 0 |
68 | 63, 67 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (1st
‘𝑘) =
0) |
69 | 68 | fveq2d 6721 |
. . . . . 6
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (𝐴‘(1st ‘𝑘)) = (𝐴‘0)) |
70 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (2nd
‘𝑘) = (2nd
‘〈0, (𝑃 −
1)〉)) |
71 | | op2ndg 7774 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (𝑃
− 1) ∈ V) → (2nd ‘〈0, (𝑃 − 1)〉) = (𝑃 − 1)) |
72 | 64, 65, 71 | mp2an 692 |
. . . . . . . . 9
⊢
(2nd ‘〈0, (𝑃 − 1)〉) = (𝑃 − 1) |
73 | 70, 72 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (2nd
‘𝑘) = (𝑃 − 1)) |
74 | 73 | fveq2d 6721 |
. . . . . . 7
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → ((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘)) = ((ℝ
D𝑛 𝐹)‘(𝑃 − 1))) |
75 | 74, 68 | fveq12d 6724 |
. . . . . 6
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) = (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) |
76 | 69, 75 | oveq12d 7231 |
. . . . 5
⊢ (𝑘 = 〈0, (𝑃 − 1)〉 → ((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) = ((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0))) |
77 | 3, 4, 9, 39, 62, 76 | fsumsplit1 15309 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) = (((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) + Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))))) |
78 | 77 | oveq1d 7228 |
. . 3
⊢ (𝜑 → (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1st ‘𝑘)) · (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1))) =
((((𝐴‘0) ·
(((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0)) + Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)))) /
(!‘(𝑃 −
1)))) |
79 | 12, 43 | sseldi 3899 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℕ0) |
80 | 10, 79 | ffvelrnd 6905 |
. . . . . 6
⊢ (𝜑 → (𝐴‘0) ∈ ℤ) |
81 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
82 | 22 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
83 | 64 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
84 | 81, 82, 26, 28, 30, 49, 83, 44 | etransclem42 43492 |
. . . . . 6
⊢ (𝜑 → (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈
ℤ) |
85 | 80, 84 | zmulcld 12288 |
. . . . 5
⊢ (𝜑 → ((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) ∈
ℤ) |
86 | 85 | zcnd 12283 |
. . . 4
⊢ (𝜑 → ((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) ∈
ℂ) |
87 | | difss 4046 |
. . . . . . . 8
⊢
(((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ⊆
((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) |
88 | | ssfi 8851 |
. . . . . . . 8
⊢
((((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin ∧ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ⊆
((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∈
Fin) |
89 | 8, 87, 88 | mp2an 692 |
. . . . . . 7
⊢
(((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∈
Fin |
90 | 89 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∈
Fin) |
91 | | eldifi 4041 |
. . . . . . 7
⊢ (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) → 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) |
92 | 91, 38 | sylan2 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℤ) |
93 | 90, 92 | fsumzcl 15299 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℤ) |
94 | 93 | zcnd 12283 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℂ) |
95 | 49 | faccld 13850 |
. . . . 5
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℕ) |
96 | 95 | nncnd 11846 |
. . . 4
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℂ) |
97 | 95 | nnne0d 11880 |
. . . 4
⊢ (𝜑 → (!‘(𝑃 − 1)) ≠
0) |
98 | 86, 94, 96, 97 | divdird 11646 |
. . 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))))) |
99 | 2, 78, 98 | 3eqtrd 2781 |
. 2
⊢ (𝜑 → 𝐾 = ((((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) + (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1))))) |
100 | 26 | nnne0d 11880 |
. . 3
⊢ (𝜑 → 𝑃 ≠ 0) |
101 | 80 | zcnd 12283 |
. . . . 5
⊢ (𝜑 → (𝐴‘0) ∈ ℂ) |
102 | 84 | zcnd 12283 |
. . . . 5
⊢ (𝜑 → (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈
ℂ) |
103 | 101, 102,
96, 97 | divassd 11643 |
. . . 4
⊢ (𝜑 → (((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) = ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))) |
104 | | etransclem5 43455 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
105 | | etransclem11 43461 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚) ↑m
(0...𝑀)) ∣
Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) |
106 | 81, 82, 26, 28, 30, 49, 104, 105, 43, 83 | etransclem37 43487 |
. . . . . 6
⊢ (𝜑 → (!‘(𝑃 − 1)) ∥ (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) |
107 | 95 | nnzd 12281 |
. . . . . . 7
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℤ) |
108 | | dvdsval2 15818 |
. . . . . . 7
⊢
(((!‘(𝑃
− 1)) ∈ ℤ ∧ (!‘(𝑃 − 1)) ≠ 0 ∧ (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) ∈ ℤ) →
((!‘(𝑃 − 1))
∥ (((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) ↔ ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈
ℤ)) |
109 | 107, 97, 84, 108 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → ((!‘(𝑃 − 1)) ∥ (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) ↔ ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈
ℤ)) |
110 | 106, 109 | mpbid 235 |
. . . . 5
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈
ℤ) |
111 | 80, 110 | zmulcld 12288 |
. . . 4
⊢ (𝜑 → ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ∈
ℤ) |
112 | 103, 111 | eqeltrd 2838 |
. . 3
⊢ (𝜑 → (((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) ∈
ℤ) |
113 | 91, 39 | sylan2 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) ∈
ℂ) |
114 | 90, 96, 113, 97 | fsumdivc 15350 |
. . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1))) =
Σ𝑘 ∈
(((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})(((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1)))) |
115 | 16 | zcnd 12283 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (𝐴‘(1st ‘𝑘)) ∈
ℂ) |
116 | 91, 115 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(𝐴‘(1st
‘𝑘)) ∈
ℂ) |
117 | 91, 37 | sylan2 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ∈
ℤ) |
118 | 117 | zcnd 12283 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ∈
ℂ) |
119 | 96 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(!‘(𝑃 − 1))
∈ ℂ) |
120 | 97 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(!‘(𝑃 − 1))
≠ 0) |
121 | 116, 118,
119, 120 | divassd 11643 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1))) =
((𝐴‘(1st
‘𝑘)) ·
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 −
1))))) |
122 | 91, 16 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(𝐴‘(1st
‘𝑘)) ∈
ℤ) |
123 | 17 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
ℝ ∈ {ℝ, ℂ}) |
124 | 22 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
ℝ ∈ ((TopOpen‘ℂfld) ↾t
ℝ)) |
125 | 26 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑃 ∈
ℕ) |
126 | 28 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑀 ∈
ℕ0) |
127 | 91 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) |
128 | 127, 33 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(2nd ‘𝑘)
∈ ℕ0) |
129 | 127, 13 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(1st ‘𝑘)
∈ (0...𝑀)) |
130 | 91, 35 | sylan2 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(1st ‘𝑘)
∈ ℝ) |
131 | 123, 124,
125, 126, 30, 128, 104, 105, 129, 130 | etransclem37 43487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(!‘(𝑃 − 1))
∥ (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) |
132 | 107 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(!‘(𝑃 − 1))
∈ ℤ) |
133 | | dvdsval2 15818 |
. . . . . . . . 9
⊢
(((!‘(𝑃
− 1)) ∈ ℤ ∧ (!‘(𝑃 − 1)) ≠ 0 ∧ (((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ∈ ℤ)
→ ((!‘(𝑃 −
1)) ∥ (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ↔
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ)) |
134 | 132, 120,
117, 133 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
((!‘(𝑃 − 1))
∥ (((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) ↔
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ)) |
135 | 131, 134 | mpbid 235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ) |
136 | 122, 135 | zmulcld 12288 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
((𝐴‘(1st
‘𝑘)) ·
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1))))
∈ ℤ) |
137 | 121, 136 | eqeltrd 2838 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1)))
∈ ℤ) |
138 | 90, 137 | fsumzcl 15299 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})(((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1)))
∈ ℤ) |
139 | 114, 138 | eqeltrd 2838 |
. . 3
⊢ (𝜑 → (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1)))
∈ ℤ) |
140 | | 1zzd 12208 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) |
141 | | zabscl 14877 |
. . . . . . . . . . 11
⊢ ((𝐴‘0) ∈ ℤ →
(abs‘(𝐴‘0))
∈ ℤ) |
142 | 80, 141 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝐴‘0)) ∈
ℤ) |
143 | | nn0abscl 14876 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘0) ∈ ℤ →
(abs‘(𝐴‘0))
∈ ℕ0) |
144 | 80, 143 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝐴‘0)) ∈
ℕ0) |
145 | | etransclem44.a0 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴‘0) ≠ 0) |
146 | 101, 145 | absne0d 15011 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝐴‘0)) ≠
0) |
147 | | elnnne0 12104 |
. . . . . . . . . . . 12
⊢
((abs‘(𝐴‘0)) ∈ ℕ ↔
((abs‘(𝐴‘0))
∈ ℕ0 ∧ (abs‘(𝐴‘0)) ≠ 0)) |
148 | 144, 146,
147 | sylanbrc 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘(𝐴‘0)) ∈
ℕ) |
149 | 148 | nnge1d 11878 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≤ (abs‘(𝐴‘0))) |
150 | | etransclem44.ap |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘(𝐴‘0)) < 𝑃) |
151 | | zltlem1 12230 |
. . . . . . . . . . . 12
⊢
(((abs‘(𝐴‘0)) ∈ ℤ ∧ 𝑃 ∈ ℤ) →
((abs‘(𝐴‘0))
< 𝑃 ↔
(abs‘(𝐴‘0))
≤ (𝑃 −
1))) |
152 | 142, 46, 151 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs‘(𝐴‘0)) < 𝑃 ↔ (abs‘(𝐴‘0)) ≤ (𝑃 − 1))) |
153 | 150, 152 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝐴‘0)) ≤ (𝑃 − 1)) |
154 | 140, 50, 142, 149, 153 | elfzd 13103 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝐴‘0)) ∈ (1...(𝑃 − 1))) |
155 | | fzm1ndvds 15883 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℕ ∧
(abs‘(𝐴‘0))
∈ (1...(𝑃 − 1)))
→ ¬ 𝑃 ∥
(abs‘(𝐴‘0))) |
156 | 26, 154, 155 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑃 ∥ (abs‘(𝐴‘0))) |
157 | | dvdsabsb 15837 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧ (𝐴‘0) ∈ ℤ) →
(𝑃 ∥ (𝐴‘0) ↔ 𝑃 ∥ (abs‘(𝐴‘0)))) |
158 | 46, 80, 157 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 ∥ (𝐴‘0) ↔ 𝑃 ∥ (abs‘(𝐴‘0)))) |
159 | 156, 158 | mtbird 328 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑃 ∥ (𝐴‘0)) |
160 | | etransclem44.mp |
. . . . . . . 8
⊢ (𝜑 → (!‘𝑀) < 𝑃) |
161 | 28, 24, 160, 30 | etransclem41 43491 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) |
162 | 159, 161 | jca 515 |
. . . . . 6
⊢ (𝜑 → (¬ 𝑃 ∥ (𝐴‘0) ∧ ¬ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))) |
163 | | pm4.56 989 |
. . . . . 6
⊢ ((¬
𝑃 ∥ (𝐴‘0) ∧ ¬ 𝑃 ∥ ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ ¬
(𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))) |
164 | 162, 163 | sylib 221 |
. . . . 5
⊢ (𝜑 → ¬ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))) |
165 | | euclemma 16270 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴‘0) ∈ ℤ ∧
((((ℝ D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ∈ ℤ)
→ (𝑃 ∥ ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 −
1)))))) |
166 | 24, 80, 110, 165 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑃 ∥ ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) ↔ (𝑃 ∥ (𝐴‘0) ∨ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 −
1)))))) |
167 | 164, 166 | mtbird 328 |
. . . 4
⊢ (𝜑 → ¬ 𝑃 ∥ ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))))) |
168 | 103 | breq2d 5065 |
. . . 4
⊢ (𝜑 → (𝑃 ∥ (((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) ↔ 𝑃 ∥ ((𝐴‘0) · ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 −
1)))))) |
169 | 167, 168 | mtbird 328 |
. . 3
⊢ (𝜑 → ¬ 𝑃 ∥ (((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1)))) |
170 | 46 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑃 ∈
ℤ) |
171 | 170, 122,
135 | 3jca 1130 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
(𝑃 ∈ ℤ ∧
(𝐴‘(1st
‘𝑘)) ∈ ℤ
∧ ((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ)) |
172 | | eldifn 4042 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) → ¬
𝑘 ∈ {〈0, (𝑃 −
1)〉}) |
173 | 91 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∧
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) → 𝑘 ∈
((0...𝑀) ×
(0...((𝑀 · 𝑃) + (𝑃 − 1))))) |
174 | | 1st2nd2 7800 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → 𝑘 = 〈(1st ‘𝑘), (2nd ‘𝑘)〉) |
175 | 173, 174 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∧
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) → 𝑘 =
〈(1st ‘𝑘), (2nd ‘𝑘)〉) |
176 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘𝑘) = (𝑃 − 1) ∧ (1st
‘𝑘) = 0) →
(1st ‘𝑘) =
0) |
177 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘𝑘) = (𝑃 − 1) ∧ (1st
‘𝑘) = 0) →
(2nd ‘𝑘) =
(𝑃 −
1)) |
178 | 176, 177 | opeq12d 4792 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘𝑘) = (𝑃 − 1) ∧ (1st
‘𝑘) = 0) →
〈(1st ‘𝑘), (2nd ‘𝑘)〉 = 〈0, (𝑃 − 1)〉) |
179 | 178 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∧
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) → 〈(1st ‘𝑘), (2nd ‘𝑘)〉 = 〈0, (𝑃 − 1)〉) |
180 | 175, 179 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∧
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) → 𝑘 = 〈0,
(𝑃 −
1)〉) |
181 | | velsn 4557 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {〈0, (𝑃 − 1)〉} ↔ 𝑘 = 〈0, (𝑃 − 1)〉) |
182 | 180, 181 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) ∧
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) → 𝑘 ∈
{〈0, (𝑃 −
1)〉}) |
183 | 172, 182 | mtand 816 |
. . . . . . . . 9
⊢ (𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉}) → ¬
((2nd ‘𝑘)
= (𝑃 − 1) ∧
(1st ‘𝑘) =
0)) |
184 | 183 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
¬ ((2nd ‘𝑘) = (𝑃 − 1) ∧ (1st
‘𝑘) =
0)) |
185 | 125, 126,
30, 128, 129, 184, 105 | etransclem38 43488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑃 ∥ ((((ℝ
D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 −
1)))) |
186 | | dvdsmultr2 15859 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧ (𝐴‘(1st
‘𝑘)) ∈ ℤ
∧ ((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
∈ ℤ) → (𝑃
∥ ((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 − 1)))
→ 𝑃 ∥ ((𝐴‘(1st
‘𝑘)) ·
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 −
1)))))) |
187 | 171, 185,
186 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑃 ∥ ((𝐴‘(1st
‘𝑘)) ·
((((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘)) /
(!‘(𝑃 −
1))))) |
188 | 187, 121 | breqtrrd 5081 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})) →
𝑃 ∥ (((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1)))) |
189 | 90, 46, 137, 188 | fsumdvds 15869 |
. . . 4
⊢ (𝜑 → 𝑃 ∥ Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})(((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1)))) |
190 | 189, 114 | breqtrrd 5081 |
. . 3
⊢ (𝜑 → 𝑃 ∥ (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 −
1)))) |
191 | 46, 100, 112, 139, 169, 190 | etransclem9 43459 |
. 2
⊢ (𝜑 → ((((𝐴‘0) · (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0)) / (!‘(𝑃 − 1))) + (Σ𝑘 ∈ (((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∖ {〈0, (𝑃 − 1)〉})((𝐴‘(1st
‘𝑘)) ·
(((ℝ D𝑛 𝐹)‘(2nd ‘𝑘))‘(1st
‘𝑘))) /
(!‘(𝑃 − 1))))
≠ 0) |
192 | 99, 191 | eqnetrd 3008 |
1
⊢ (𝜑 → 𝐾 ≠ 0) |