| 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 44652 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
| 5 | 4 | sselda 3983 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β π₯ β β) |
| 6 | 5 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π₯ β π) β π₯ β β) |
| 7 | | elfzelz 13501 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π β β€) |
| 8 | 7 | zcnd 12667 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β) |
| 9 | 8 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π₯ β π) β π β β) |
| 10 | 6, 9 | negsubd 11577 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π₯ β π) β (π₯ + -π) = (π₯ β π)) |
| 11 | 10 | eqcomd 2739 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π₯ β π) β (π₯ β π) = (π₯ + -π)) |
| 12 | 11 | oveq1d 7424 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π₯ β π) β ((π₯ β π)βif(π = 0, (π β 1), π)) = ((π₯ + -π)βif(π = 0, (π β 1), π))) |
| 13 | 12 | mpteq2dva 5249 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π))) = (π₯ β π β¦ ((π₯ + -π)βif(π = 0, (π β 1), π)))) |
| 14 | 13 | mpteq2dva 5249 |
. . . . . 6
β’ (π β (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ + -π)βif(π = 0, (π β 1), π))))) |
| 15 | 1, 14 | eqtrid 2785 |
. . . . 5
β’ (π β π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ + -π)βif(π = 0, (π β 1), π))))) |
| 16 | | negeq 11452 |
. . . . . . . . 9
β’ (π = π½ β -π = -π½) |
| 17 | 16 | oveq2d 7425 |
. . . . . . . 8
β’ (π = π½ β (π₯ + -π) = (π₯ + -π½)) |
| 18 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π = π½ β (π = 0 β π½ = 0)) |
| 19 | 18 | ifbid 4552 |
. . . . . . . 8
β’ (π = π½ β if(π = 0, (π β 1), π) = if(π½ = 0, (π β 1), π)) |
| 20 | 17, 19 | oveq12d 7427 |
. . . . . . 7
β’ (π = π½ β ((π₯ + -π)βif(π = 0, (π β 1), π)) = ((π₯ + -π½)βif(π½ = 0, (π β 1), π))) |
| 21 | 20 | mpteq2dv 5251 |
. . . . . 6
β’ (π = π½ β (π₯ β π β¦ ((π₯ + -π)βif(π = 0, (π β 1), π))) = (π₯ β π β¦ ((π₯ + -π½)βif(π½ = 0, (π β 1), π)))) |
| 22 | 21 | adantl 483 |
. . . . 5
β’ ((π β§ π = π½) β (π₯ β π β¦ ((π₯ + -π)βif(π = 0, (π β 1), π))) = (π₯ β π β¦ ((π₯ + -π½)βif(π½ = 0, (π β 1), π)))) |
| 23 | | etransclem17.J |
. . . . 5
β’ (π β π½ β (0...π)) |
| 24 | | mptexg 7223 |
. . . . . 6
β’ (π β
((TopOpenββfld) βΎt π) β (π₯ β π β¦ ((π₯ + -π½)βif(π½ = 0, (π β 1), π))) β V) |
| 25 | 3, 24 | syl 17 |
. . . . 5
β’ (π β (π₯ β π β¦ ((π₯ + -π½)βif(π½ = 0, (π β 1), π))) β V) |
| 26 | 15, 22, 23, 25 | fvmptd 7006 |
. . . 4
β’ (π β (π»βπ½) = (π₯ β π β¦ ((π₯ + -π½)βif(π½ = 0, (π β 1), π)))) |
| 27 | 26 | oveq2d 7425 |
. . 3
β’ (π β (π Dπ (π»βπ½)) = (π Dπ (π₯ β π β¦ ((π₯ + -π½)βif(π½ = 0, (π β 1), π))))) |
| 28 | 27 | fveq1d 6894 |
. 2
β’ (π β ((π Dπ (π»βπ½))βπ) = ((π Dπ (π₯ β π β¦ ((π₯ + -π½)βif(π½ = 0, (π β 1), π))))βπ)) |
| 29 | | etransclem17.n |
. . 3
β’ (π β π β
β0) |
| 30 | | elfzelz 13501 |
. . . . . . 7
β’ (π½ β (0...π) β π½ β β€) |
| 31 | 30 | zcnd 12667 |
. . . . . 6
β’ (π½ β (0...π) β π½ β β) |
| 32 | 23, 31 | syl 17 |
. . . . 5
β’ (π β π½ β β) |
| 33 | 32 | negcld 11558 |
. . . 4
β’ (π β -π½ β β) |
| 34 | | etransclem17.p |
. . . . . 6
β’ (π β π β β) |
| 35 | | nnm1nn0 12513 |
. . . . . 6
β’ (π β β β (π β 1) β
β0) |
| 36 | 34, 35 | syl 17 |
. . . . 5
β’ (π β (π β 1) β
β0) |
| 37 | 34 | nnnn0d 12532 |
. . . . 5
β’ (π β π β
β0) |
| 38 | 36, 37 | ifcld 4575 |
. . . 4
β’ (π β if(π½ = 0, (π β 1), π) β
β0) |
| 39 | | eqid 2733 |
. . . 4
β’ (π₯ β π β¦ ((π₯ + -π½)βif(π½ = 0, (π β 1), π))) = (π₯ β π β¦ ((π₯ + -π½)βif(π½ = 0, (π β 1), π))) |
| 40 | 2, 3, 33, 38, 39 | dvnxpaek 44658 |
. . 3
β’ ((π β§ π β β0) β ((π Dπ (π₯ β π β¦ ((π₯ + -π½)βif(π½ = 0, (π β 1), π))))βπ) = (π₯ β π β¦ if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ + -π½)β(if(π½ = 0, (π β 1), π) β π)))))) |
| 41 | 29, 40 | mpdan 686 |
. 2
β’ (π β ((π Dπ (π₯ β π β¦ ((π₯ + -π½)βif(π½ = 0, (π β 1), π))))βπ) = (π₯ β π β¦ if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ + -π½)β(if(π½ = 0, (π β 1), π) β π)))))) |
| 42 | 32 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π½ β β) |
| 43 | 5, 42 | negsubd 11577 |
. . . . . 6
β’ ((π β§ π₯ β π) β (π₯ + -π½) = (π₯ β π½)) |
| 44 | 43 | oveq1d 7424 |
. . . . 5
β’ ((π β§ π₯ β π) β ((π₯ + -π½)β(if(π½ = 0, (π β 1), π) β π)) = ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π))) |
| 45 | 44 | oveq2d 7425 |
. . . 4
β’ ((π β§ π₯ β π) β (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ + -π½)β(if(π½ = 0, (π β 1), π) β π))) = (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π)))) |
| 46 | 45 | ifeq2d 4549 |
. . 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 5249 |
. 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 2777 |
1
β’ (π β ((π Dπ (π»βπ½))βπ) = (π₯ β π β¦ if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π)))))) |
