Step | Hyp | Ref
| Expression |
1 | | etransclem41.mp |
. . . . . . 7
⊢ (𝜑 → (!‘𝑀) < 𝑃) |
2 | | etransclem41.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
3 | 2 | faccld 13729 |
. . . . . . . . 9
⊢ (𝜑 → (!‘𝑀) ∈ ℕ) |
4 | 3 | nnred 11724 |
. . . . . . . 8
⊢ (𝜑 → (!‘𝑀) ∈ ℝ) |
5 | | etransclem41.p |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℙ) |
6 | | prmnn 16108 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) |
8 | 7 | nnred 11724 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℝ) |
9 | 4, 8 | ltnled 10858 |
. . . . . . 7
⊢ (𝜑 → ((!‘𝑀) < 𝑃 ↔ ¬ 𝑃 ≤ (!‘𝑀))) |
10 | 1, 9 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑃 ≤ (!‘𝑀)) |
11 | 7 | nnzd 12160 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℤ) |
12 | 11, 3 | jca 515 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 ∈ ℤ ∧ (!‘𝑀) ∈
ℕ)) |
13 | 12 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ (!‘𝑀)) → (𝑃 ∈ ℤ ∧ (!‘𝑀) ∈
ℕ)) |
14 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ (!‘𝑀)) → 𝑃 ∥ (!‘𝑀)) |
15 | | dvdsle 15748 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
(!‘𝑀) ∈ ℕ)
→ (𝑃 ∥
(!‘𝑀) → 𝑃 ≤ (!‘𝑀))) |
16 | 13, 14, 15 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ (!‘𝑀)) → 𝑃 ≤ (!‘𝑀)) |
17 | 10, 16 | mtand 816 |
. . . . 5
⊢ (𝜑 → ¬ 𝑃 ∥ (!‘𝑀)) |
18 | | fzfid 13425 |
. . . . . . . . . 10
⊢ (⊤
→ (1...𝑀) ∈
Fin) |
19 | | elfzelz 12991 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℤ) |
20 | 19 | znegcld 12163 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℤ) |
21 | 20 | zcnd 12162 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℂ) |
22 | 21 | adantl 485 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑗
∈ (1...𝑀)) →
-𝑗 ∈
ℂ) |
23 | 18, 22 | fprodabs2 42662 |
. . . . . . . . 9
⊢ (⊤
→ (abs‘∏𝑗
∈ (1...𝑀)-𝑗) = ∏𝑗 ∈ (1...𝑀)(abs‘-𝑗)) |
24 | 23 | mptru 1549 |
. . . . . . . 8
⊢
(abs‘∏𝑗
∈ (1...𝑀)-𝑗) = ∏𝑗 ∈ (1...𝑀)(abs‘-𝑗) |
25 | 19 | zcnd 12162 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℂ) |
26 | 25 | absnegd 14892 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...𝑀) → (abs‘-𝑗) = (abs‘𝑗)) |
27 | 19 | zred 12161 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℝ) |
28 | | 0red 10715 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑀) → 0 ∈ ℝ) |
29 | | 1red 10713 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 1 ∈ ℝ) |
30 | | 0lt1 11233 |
. . . . . . . . . . . . . 14
⊢ 0 <
1 |
31 | 30 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 0 < 1) |
32 | | elfzle1 12994 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 1 ≤ 𝑗) |
33 | 28, 29, 27, 31, 32 | ltletrd 10871 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑀) → 0 < 𝑗) |
34 | 28, 27, 33 | ltled 10859 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑀) → 0 ≤ 𝑗) |
35 | 27, 34 | absidd 14865 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...𝑀) → (abs‘𝑗) = 𝑗) |
36 | 26, 35 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑀) → (abs‘-𝑗) = 𝑗) |
37 | 36 | prodeq2i 15358 |
. . . . . . . 8
⊢
∏𝑗 ∈
(1...𝑀)(abs‘-𝑗) = ∏𝑗 ∈ (1...𝑀)𝑗 |
38 | 24, 37 | eqtri 2761 |
. . . . . . 7
⊢
(abs‘∏𝑗
∈ (1...𝑀)-𝑗) = ∏𝑗 ∈ (1...𝑀)𝑗 |
39 | | fprodfac 15412 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (!‘𝑀) =
∏𝑗 ∈ (1...𝑀)𝑗) |
40 | 2, 39 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (!‘𝑀) = ∏𝑗 ∈ (1...𝑀)𝑗) |
41 | 38, 40 | eqtr4id 2792 |
. . . . . 6
⊢ (𝜑 → (abs‘∏𝑗 ∈ (1...𝑀)-𝑗) = (!‘𝑀)) |
42 | 41 | breq2d 5039 |
. . . . 5
⊢ (𝜑 → (𝑃 ∥ (abs‘∏𝑗 ∈ (1...𝑀)-𝑗) ↔ 𝑃 ∥ (!‘𝑀))) |
43 | 17, 42 | mtbird 328 |
. . . 4
⊢ (𝜑 → ¬ 𝑃 ∥ (abs‘∏𝑗 ∈ (1...𝑀)-𝑗)) |
44 | | fzfid 13425 |
. . . . . 6
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
45 | 20 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → -𝑗 ∈ ℤ) |
46 | 44, 45 | fprodzcl 15393 |
. . . . 5
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)-𝑗 ∈ ℤ) |
47 | | dvdsabsb 15714 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
∏𝑗 ∈ (1...𝑀)-𝑗 ∈ ℤ) → (𝑃 ∥ ∏𝑗 ∈ (1...𝑀)-𝑗 ↔ 𝑃 ∥ (abs‘∏𝑗 ∈ (1...𝑀)-𝑗))) |
48 | 11, 46, 47 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝑃 ∥ ∏𝑗 ∈ (1...𝑀)-𝑗 ↔ 𝑃 ∥ (abs‘∏𝑗 ∈ (1...𝑀)-𝑗))) |
49 | 43, 48 | mtbird 328 |
. . 3
⊢ (𝜑 → ¬ 𝑃 ∥ ∏𝑗 ∈ (1...𝑀)-𝑗) |
50 | | prmdvdsexp 16149 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧
∏𝑗 ∈ (1...𝑀)-𝑗 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑃 ∥ (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃) ↔ 𝑃 ∥ ∏𝑗 ∈ (1...𝑀)-𝑗)) |
51 | 5, 46, 7, 50 | syl3anc 1372 |
. . 3
⊢ (𝜑 → (𝑃 ∥ (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃) ↔ 𝑃 ∥ ∏𝑗 ∈ (1...𝑀)-𝑗)) |
52 | 49, 51 | mtbird 328 |
. 2
⊢ (𝜑 → ¬ 𝑃 ∥ (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)) |
53 | | etransclem41.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
54 | | etransclem11 43312 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚) ↑m
(0...𝑀)) ∣
Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) |
55 | | eqeq1 2742 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝑘 = 0 ↔ 𝑗 = 0)) |
56 | 55 | ifbid 4434 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → if(𝑘 = 0, (𝑃 − 1), 0) = if(𝑗 = 0, (𝑃 − 1), 0)) |
57 | 56 | cbvmptv 5130 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑀) ↦ if(𝑘 = 0, (𝑃 − 1), 0)) = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0)) |
58 | 7, 2, 53, 54, 57 | etransclem35 43336 |
. . . . 5
⊢ (𝜑 → (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) = ((!‘(𝑃 − 1)) ·
(∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃))) |
59 | 58 | oveq1d 7179 |
. . . 4
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) =
(((!‘(𝑃 − 1))
· (∏𝑗 ∈
(1...𝑀)-𝑗↑𝑃)) / (!‘(𝑃 − 1)))) |
60 | 21 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → -𝑗 ∈ ℂ) |
61 | 44, 60 | fprodcl 15391 |
. . . . . 6
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)-𝑗 ∈ ℂ) |
62 | 7 | nnnn0d 12029 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
63 | 61, 62 | expcld 13595 |
. . . . 5
⊢ (𝜑 → (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃) ∈ ℂ) |
64 | | nnm1nn0 12010 |
. . . . . . . 8
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
65 | 7, 64 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
66 | 65 | faccld 13729 |
. . . . . 6
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℕ) |
67 | 66 | nncnd 11725 |
. . . . 5
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℂ) |
68 | 66 | nnne0d 11759 |
. . . . 5
⊢ (𝜑 → (!‘(𝑃 − 1)) ≠
0) |
69 | 63, 67, 68 | divcan3d 11492 |
. . . 4
⊢ (𝜑 → (((!‘(𝑃 − 1)) ·
(∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)) / (!‘(𝑃 − 1))) = (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)) |
70 | 59, 69 | eqtrd 2773 |
. . 3
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) = (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)) |
71 | 70 | breq2d 5039 |
. 2
⊢ (𝜑 → (𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ↔ 𝑃 ∥ (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃))) |
72 | 52, 71 | mtbird 328 |
1
⊢ (𝜑 → ¬ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) |