Proof of Theorem etransclem17
| Step | Hyp | Ref
| Expression |
| 1 | | etransclem17.1 |
. . . . . 6
⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
| 2 | | etransclem17.s |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
| 3 | | etransclem17.x |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 4 | 2, 3 | dvdmsscn 45951 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
| 5 | 4 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) |
| 6 | 5 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) |
| 7 | | elfzelz 13564 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ) |
| 8 | 7 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ) |
| 9 | 8 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝑗 ∈ ℂ) |
| 10 | 6, 9 | negsubd 11626 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → (𝑥 + -𝑗) = (𝑥 − 𝑗)) |
| 11 | 10 | eqcomd 2743 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → (𝑥 − 𝑗) = (𝑥 + -𝑗)) |
| 12 | 11 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 + -𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) |
| 13 | 12 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) = (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
| 14 | 13 | mpteq2dva 5242 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))) |
| 15 | 1, 14 | eqtrid 2789 |
. . . . 5
⊢ (𝜑 → 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))) |
| 16 | | negeq 11500 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → -𝑗 = -𝐽) |
| 17 | 16 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → (𝑥 + -𝑗) = (𝑥 + -𝐽)) |
| 18 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (𝑗 = 0 ↔ 𝐽 = 0)) |
| 19 | 18 | ifbid 4549 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → if(𝑗 = 0, (𝑃 − 1), 𝑃) = if(𝐽 = 0, (𝑃 − 1), 𝑃)) |
| 20 | 17, 19 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → ((𝑥 + -𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))) |
| 21 | 20 | mpteq2dv 5244 |
. . . . . 6
⊢ (𝑗 = 𝐽 → (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) = (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃)))) |
| 22 | 21 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) = (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃)))) |
| 23 | | etransclem17.J |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) |
| 24 | | mptexg 7241 |
. . . . . 6
⊢ (𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆) → (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))) ∈ V) |
| 25 | 3, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))) ∈ V) |
| 26 | 15, 22, 23, 25 | fvmptd 7023 |
. . . 4
⊢ (𝜑 → (𝐻‘𝐽) = (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃)))) |
| 27 | 26 | oveq2d 7447 |
. . 3
⊢ (𝜑 → (𝑆 D𝑛 (𝐻‘𝐽)) = (𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))))) |
| 28 | 27 | fveq1d 6908 |
. 2
⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))))‘𝑁)) |
| 29 | | etransclem17.n |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 30 | | elfzelz 13564 |
. . . . . . 7
⊢ (𝐽 ∈ (0...𝑀) → 𝐽 ∈ ℤ) |
| 31 | 30 | zcnd 12723 |
. . . . . 6
⊢ (𝐽 ∈ (0...𝑀) → 𝐽 ∈ ℂ) |
| 32 | 23, 31 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ ℂ) |
| 33 | 32 | negcld 11607 |
. . . 4
⊢ (𝜑 → -𝐽 ∈ ℂ) |
| 34 | | etransclem17.p |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 35 | | nnm1nn0 12567 |
. . . . . 6
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
| 36 | 34, 35 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
| 37 | 34 | nnnn0d 12587 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
| 38 | 36, 37 | ifcld 4572 |
. . . 4
⊢ (𝜑 → if(𝐽 = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
| 39 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))) = (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))) |
| 40 | 2, 3, 33, 38, 39 | dvnxpaek 45957 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))))‘𝑁) = (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 + -𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))))) |
| 41 | 29, 40 | mpdan 687 |
. 2
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ ((𝑥 + -𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))))‘𝑁) = (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 + -𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))))) |
| 42 | 32 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐽 ∈ ℂ) |
| 43 | 5, 42 | negsubd 11626 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 + -𝐽) = (𝑥 − 𝐽)) |
| 44 | 43 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 + -𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)) = ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) |
| 45 | 44 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 + -𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) = (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))) |
| 46 | 45 | ifeq2d 4546 |
. . 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), 𝑃) − 𝑁))))) |
| 47 | 46 | mpteq2dva 5242 |
. 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), 𝑃) − 𝑁)))))) |
| 48 | 28, 41, 47 | 3eqtrd 2781 |
1
⊢ (𝜑 → ((𝑆 D𝑛 (𝐻‘𝐽))‘𝑁) = (𝑥 ∈ 𝑋 ↦ if(if(𝐽 = 0, (𝑃 − 1), 𝑃) < 𝑁, 0, (((!‘if(𝐽 = 0, (𝑃 − 1), 𝑃)) / (!‘(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁))) · ((𝑥 − 𝐽)↑(if(𝐽 = 0, (𝑃 − 1), 𝑃) − 𝑁)))))) |