Step | Hyp | Ref
| Expression |
1 | | etransclem41.mp |
. . . . . . 7
⊢ (𝜑 → (!‘𝑀) < 𝑃) |
2 | | etransclem41.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
3 | 2 | faccld 13998 |
. . . . . . . . 9
⊢ (𝜑 → (!‘𝑀) ∈ ℕ) |
4 | 3 | nnred 11988 |
. . . . . . . 8
⊢ (𝜑 → (!‘𝑀) ∈ ℝ) |
5 | | etransclem41.p |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℙ) |
6 | | prmnn 16379 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) |
8 | 7 | nnred 11988 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℝ) |
9 | 4, 8 | ltnled 11122 |
. . . . . . 7
⊢ (𝜑 → ((!‘𝑀) < 𝑃 ↔ ¬ 𝑃 ≤ (!‘𝑀))) |
10 | 1, 9 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑃 ≤ (!‘𝑀)) |
11 | 7 | nnzd 12425 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℤ) |
12 | 11, 3 | jca 512 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 ∈ ℤ ∧ (!‘𝑀) ∈
ℕ)) |
13 | 12 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ (!‘𝑀)) → (𝑃 ∈ ℤ ∧ (!‘𝑀) ∈
ℕ)) |
14 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ (!‘𝑀)) → 𝑃 ∥ (!‘𝑀)) |
15 | | dvdsle 16019 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧
(!‘𝑀) ∈ ℕ)
→ (𝑃 ∥
(!‘𝑀) → 𝑃 ≤ (!‘𝑀))) |
16 | 13, 14, 15 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ (!‘𝑀)) → 𝑃 ≤ (!‘𝑀)) |
17 | 10, 16 | mtand 813 |
. . . . 5
⊢ (𝜑 → ¬ 𝑃 ∥ (!‘𝑀)) |
18 | | fzfid 13693 |
. . . . . . . . . 10
⊢ (⊤
→ (1...𝑀) ∈
Fin) |
19 | | elfzelz 13256 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℤ) |
20 | 19 | znegcld 12428 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℤ) |
21 | 20 | zcnd 12427 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑀) → -𝑗 ∈ ℂ) |
22 | 21 | adantl 482 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑗
∈ (1...𝑀)) →
-𝑗 ∈
ℂ) |
23 | 18, 22 | fprodabs2 43136 |
. . . . . . . . 9
⊢ (⊤
→ (abs‘∏𝑗
∈ (1...𝑀)-𝑗) = ∏𝑗 ∈ (1...𝑀)(abs‘-𝑗)) |
24 | 23 | mptru 1546 |
. . . . . . . 8
⊢
(abs‘∏𝑗
∈ (1...𝑀)-𝑗) = ∏𝑗 ∈ (1...𝑀)(abs‘-𝑗) |
25 | 19 | zcnd 12427 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℂ) |
26 | 25 | absnegd 15161 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...𝑀) → (abs‘-𝑗) = (abs‘𝑗)) |
27 | 19 | zred 12426 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℝ) |
28 | | 0red 10978 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑀) → 0 ∈ ℝ) |
29 | | 1red 10976 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 1 ∈ ℝ) |
30 | | 0lt1 11497 |
. . . . . . . . . . . . . 14
⊢ 0 <
1 |
31 | 30 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 0 < 1) |
32 | | elfzle1 13259 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 1 ≤ 𝑗) |
33 | 28, 29, 27, 31, 32 | ltletrd 11135 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑀) → 0 < 𝑗) |
34 | 28, 27, 33 | ltled 11123 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...𝑀) → 0 ≤ 𝑗) |
35 | 27, 34 | absidd 15134 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...𝑀) → (abs‘𝑗) = 𝑗) |
36 | 26, 35 | eqtrd 2778 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑀) → (abs‘-𝑗) = 𝑗) |
37 | 36 | prodeq2i 15629 |
. . . . . . . 8
⊢
∏𝑗 ∈
(1...𝑀)(abs‘-𝑗) = ∏𝑗 ∈ (1...𝑀)𝑗 |
38 | 24, 37 | eqtri 2766 |
. . . . . . 7
⊢
(abs‘∏𝑗
∈ (1...𝑀)-𝑗) = ∏𝑗 ∈ (1...𝑀)𝑗 |
39 | | fprodfac 15683 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (!‘𝑀) =
∏𝑗 ∈ (1...𝑀)𝑗) |
40 | 2, 39 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (!‘𝑀) = ∏𝑗 ∈ (1...𝑀)𝑗) |
41 | 38, 40 | eqtr4id 2797 |
. . . . . 6
⊢ (𝜑 → (abs‘∏𝑗 ∈ (1...𝑀)-𝑗) = (!‘𝑀)) |
42 | 41 | breq2d 5086 |
. . . . 5
⊢ (𝜑 → (𝑃 ∥ (abs‘∏𝑗 ∈ (1...𝑀)-𝑗) ↔ 𝑃 ∥ (!‘𝑀))) |
43 | 17, 42 | mtbird 325 |
. . . 4
⊢ (𝜑 → ¬ 𝑃 ∥ (abs‘∏𝑗 ∈ (1...𝑀)-𝑗)) |
44 | | fzfid 13693 |
. . . . . 6
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
45 | 20 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → -𝑗 ∈ ℤ) |
46 | 44, 45 | fprodzcl 15664 |
. . . . 5
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)-𝑗 ∈ ℤ) |
47 | | dvdsabsb 15985 |
. . . . 5
⊢ ((𝑃 ∈ ℤ ∧
∏𝑗 ∈ (1...𝑀)-𝑗 ∈ ℤ) → (𝑃 ∥ ∏𝑗 ∈ (1...𝑀)-𝑗 ↔ 𝑃 ∥ (abs‘∏𝑗 ∈ (1...𝑀)-𝑗))) |
48 | 11, 46, 47 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑃 ∥ ∏𝑗 ∈ (1...𝑀)-𝑗 ↔ 𝑃 ∥ (abs‘∏𝑗 ∈ (1...𝑀)-𝑗))) |
49 | 43, 48 | mtbird 325 |
. . 3
⊢ (𝜑 → ¬ 𝑃 ∥ ∏𝑗 ∈ (1...𝑀)-𝑗) |
50 | | prmdvdsexp 16420 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧
∏𝑗 ∈ (1...𝑀)-𝑗 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑃 ∥ (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃) ↔ 𝑃 ∥ ∏𝑗 ∈ (1...𝑀)-𝑗)) |
51 | 5, 46, 7, 50 | syl3anc 1370 |
. . 3
⊢ (𝜑 → (𝑃 ∥ (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃) ↔ 𝑃 ∥ ∏𝑗 ∈ (1...𝑀)-𝑗)) |
52 | 49, 51 | mtbird 325 |
. 2
⊢ (𝜑 → ¬ 𝑃 ∥ (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)) |
53 | | etransclem41.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
54 | | etransclem11 43786 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚) ↑m
(0...𝑀)) ∣
Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) |
55 | | eqeq1 2742 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝑘 = 0 ↔ 𝑗 = 0)) |
56 | 55 | ifbid 4482 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → if(𝑘 = 0, (𝑃 − 1), 0) = if(𝑗 = 0, (𝑃 − 1), 0)) |
57 | 56 | cbvmptv 5187 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑀) ↦ if(𝑘 = 0, (𝑃 − 1), 0)) = (𝑗 ∈ (0...𝑀) ↦ if(𝑗 = 0, (𝑃 − 1), 0)) |
58 | 7, 2, 53, 54, 57 | etransclem35 43810 |
. . . . 5
⊢ (𝜑 → (((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) = ((!‘(𝑃 − 1)) ·
(∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃))) |
59 | 58 | oveq1d 7290 |
. . . 4
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) =
(((!‘(𝑃 − 1))
· (∏𝑗 ∈
(1...𝑀)-𝑗↑𝑃)) / (!‘(𝑃 − 1)))) |
60 | 21 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → -𝑗 ∈ ℂ) |
61 | 44, 60 | fprodcl 15662 |
. . . . . 6
⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)-𝑗 ∈ ℂ) |
62 | 7 | nnnn0d 12293 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
63 | 61, 62 | expcld 13864 |
. . . . 5
⊢ (𝜑 → (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃) ∈ ℂ) |
64 | | nnm1nn0 12274 |
. . . . . . . 8
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
65 | 7, 64 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
66 | 65 | faccld 13998 |
. . . . . 6
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℕ) |
67 | 66 | nncnd 11989 |
. . . . 5
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℂ) |
68 | 66 | nnne0d 12023 |
. . . . 5
⊢ (𝜑 → (!‘(𝑃 − 1)) ≠
0) |
69 | 63, 67, 68 | divcan3d 11756 |
. . . 4
⊢ (𝜑 → (((!‘(𝑃 − 1)) ·
(∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)) / (!‘(𝑃 − 1))) = (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)) |
70 | 59, 69 | eqtrd 2778 |
. . 3
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) = (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃)) |
71 | 70 | breq2d 5086 |
. 2
⊢ (𝜑 → (𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1))) ↔ 𝑃 ∥ (∏𝑗 ∈ (1...𝑀)-𝑗↑𝑃))) |
72 | 52, 71 | mtbird 325 |
1
⊢ (𝜑 → ¬ 𝑃 ∥ ((((ℝ D𝑛
𝐹)‘(𝑃 − 1))‘0) / (!‘(𝑃 − 1)))) |