Proof of Theorem etransclem21
Step | Hyp | Ref
| Expression |
1 | | etransclem21.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
2 | | etransclem21.x |
. . 3
⊢ (𝜑 → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
3 | | etransclem21.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℕ) |
4 | | etransclem21.h |
. . 3
⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
5 | | etransclem21.j |
. . 3
⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) |
6 | | etransclem21.n |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
7 | 1, 2, 3, 4, 5, 6 | etransclem17 43334 |
. 2
⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) = (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))))) |
8 | | oveq1 7177 |
. . . . . 6
⊢ (𝑥 = 𝑌 → (𝑥 − 𝐽) = (𝑌 − 𝐽)) |
9 | 8 | oveq1d 7185 |
. . . . 5
⊢ (𝑥 = 𝑌 → ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) = ((𝑌 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) |
10 | 9 | oveq2d 7186 |
. . . 4
⊢ (𝑥 = 𝑌 → (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) = (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑌 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) |
11 | 10 | ifeq2d 4434 |
. . 3
⊢ (𝑥 = 𝑌 → if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) = if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑌 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))) |
12 | 11 | adantl 485 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝑌) → if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) = if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑌 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))) |
13 | | etransclem21.y |
. 2
⊢ (𝜑 → 𝑌 ∈ 𝑋) |
14 | | 0cnd 10712 |
. . 3
⊢ ((𝜑 ∧ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → 0 ∈ ℂ) |
15 | | nnm1nn0 12017 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
16 | 3, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
17 | 3 | nnnn0d 12036 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
18 | 16, 17 | ifcld 4460 |
. . . . . . . 8
⊢ (𝜑 → if(𝐽 = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
19 | 18 | faccld 13736 |
. . . . . . 7
⊢ (𝜑 → (!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) ∈ ℕ) |
20 | 19 | nncnd 11732 |
. . . . . 6
⊢ (𝜑 → (!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ) |
21 | 20 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ) |
22 | 18 | nn0zd 12166 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝐽 = 0, (𝑃 − 1), 𝑃) ∈ ℤ) |
23 | 6 | nn0zd 12166 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
24 | 22, 23 | zsubcld 12173 |
. . . . . . . . 9
⊢ (𝜑 → (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ∈ ℤ) |
25 | 24 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ∈ ℤ) |
26 | 6 | nn0red 12037 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) |
27 | 26 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → 𝑁 ∈ ℝ) |
28 | 18 | nn0red 12037 |
. . . . . . . . . . 11
⊢ (𝜑 → if(𝐽 = 0, (𝑃 − 1), 𝑃) ∈ ℝ) |
29 | 28 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → if(𝐽 = 0, (𝑃 − 1), 𝑃) ∈ ℝ) |
30 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) |
31 | 27, 29, 30 | nltled 10868 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → 𝑁 ≤ if(𝐽 = 0, (𝑃 − 1), 𝑃)) |
32 | 29, 27 | subge0d 11308 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (0 ≤ (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ↔ 𝑁 ≤ if(𝐽 = 0, (𝑃 − 1), 𝑃))) |
33 | 31, 32 | mpbird 260 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → 0 ≤ (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) |
34 | | elnn0z 12075 |
. . . . . . . 8
⊢
((if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ∈ ℕ0 ↔
((if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ∈ ℤ ∧ 0 ≤ (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) |
35 | 25, 33, 34 | sylanbrc 586 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁) ∈
ℕ0) |
36 | 35 | faccld 13736 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) ∈ ℕ) |
37 | 36 | nncnd 11732 |
. . . . 5
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) ∈ ℂ) |
38 | 36 | nnne0d 11766 |
. . . . 5
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) ≠ 0) |
39 | 21, 37, 38 | divcld 11494 |
. . . 4
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → ((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) ∈ ℂ) |
40 | 1, 2 | dvdmsscn 43019 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
41 | 40, 13 | sseldd 3878 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℂ) |
42 | 5 | elfzelzd 12999 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ ℤ) |
43 | 42 | zcnd 12169 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ℂ) |
44 | 41, 43 | subcld 11075 |
. . . . . 6
⊢ (𝜑 → (𝑌 − 𝐽) ∈ ℂ) |
45 | 44 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (𝑌 − 𝐽) ∈ ℂ) |
46 | 45, 35 | expcld 13602 |
. . . 4
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → ((𝑌 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) ∈ ℂ) |
47 | 39, 46 | mulcld 10739 |
. . 3
⊢ ((𝜑 ∧ ¬ if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁) → (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑌 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) ∈ ℂ) |
48 | 14, 47 | ifclda 4449 |
. 2
⊢ (𝜑 → if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑌 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) ∈ ℂ) |
49 | 7, 12, 13, 48 | fvmptd 6782 |
1
⊢ (𝜑 → (((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁)‘𝑌) = if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑌 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))))) |