| 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 45698 |
. 2
β’ (π β ((π Dπ (π»βπ½))βπ) = (π₯ β π β¦ if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π)))))) |
| 8 | | oveq1 7420 |
. . . . . 6
β’ (π₯ = π β (π₯ β π½) = (π β π½)) |
| 9 | 8 | oveq1d 7428 |
. . . . 5
β’ (π₯ = π β ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π)) = ((π β π½)β(if(π½ = 0, (π β 1), π) β π))) |
| 10 | 9 | oveq2d 7429 |
. . . 4
β’ (π₯ = π β (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π))) = (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π β π½)β(if(π½ = 0, (π β 1), π) β π)))) |
| 11 | 10 | ifeq2d 4545 |
. . 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 480 |
. 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 11232 |
. . 3
β’ ((π β§ if(π½ = 0, (π β 1), π) < π) β 0 β β) |
| 15 | | nnm1nn0 12538 |
. . . . . . . . . 10
β’ (π β β β (π β 1) β
β0) |
| 16 | 3, 15 | syl 17 |
. . . . . . . . 9
β’ (π β (π β 1) β
β0) |
| 17 | 3 | nnnn0d 12557 |
. . . . . . . . 9
β’ (π β π β
β0) |
| 18 | 16, 17 | ifcld 4571 |
. . . . . . . 8
β’ (π β if(π½ = 0, (π β 1), π) β
β0) |
| 19 | 18 | faccld 14270 |
. . . . . . 7
β’ (π β (!βif(π½ = 0, (π β 1), π)) β β) |
| 20 | 19 | nncnd 12253 |
. . . . . 6
β’ (π β (!βif(π½ = 0, (π β 1), π)) β β) |
| 21 | 20 | adantr 479 |
. . . . 5
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (!βif(π½ = 0, (π β 1), π)) β β) |
| 22 | 18 | nn0zd 12609 |
. . . . . . . . . 10
β’ (π β if(π½ = 0, (π β 1), π) β β€) |
| 23 | 6 | nn0zd 12609 |
. . . . . . . . . 10
β’ (π β π β β€) |
| 24 | 22, 23 | zsubcld 12696 |
. . . . . . . . 9
β’ (π β (if(π½ = 0, (π β 1), π) β π) β β€) |
| 25 | 24 | adantr 479 |
. . . . . . . 8
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (if(π½ = 0, (π β 1), π) β π) β β€) |
| 26 | 6 | nn0red 12558 |
. . . . . . . . . . 11
β’ (π β π β β) |
| 27 | 26 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β π β β) |
| 28 | 18 | nn0red 12558 |
. . . . . . . . . . 11
β’ (π β if(π½ = 0, (π β 1), π) β β) |
| 29 | 28 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β if(π½ = 0, (π β 1), π) β β) |
| 30 | | simpr 483 |
. . . . . . . . . 10
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β Β¬ if(π½ = 0, (π β 1), π) < π) |
| 31 | 27, 29, 30 | nltled 11389 |
. . . . . . . . 9
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β π β€ if(π½ = 0, (π β 1), π)) |
| 32 | 29, 27 | subge0d 11829 |
. . . . . . . . 9
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (0 β€ (if(π½ = 0, (π β 1), π) β π) β π β€ if(π½ = 0, (π β 1), π))) |
| 33 | 31, 32 | mpbird 256 |
. . . . . . . 8
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β 0 β€ (if(π½ = 0, (π β 1), π) β π)) |
| 34 | | elnn0z 12596 |
. . . . . . . 8
β’
((if(π½ = 0, (π β 1), π) β π) β β0 β
((if(π½ = 0, (π β 1), π) β π) β β€ β§ 0 β€ (if(π½ = 0, (π β 1), π) β π))) |
| 35 | 25, 33, 34 | sylanbrc 581 |
. . . . . . 7
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (if(π½ = 0, (π β 1), π) β π) β
β0) |
| 36 | 35 | faccld 14270 |
. . . . . 6
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (!β(if(π½ = 0, (π β 1), π) β π)) β β) |
| 37 | 36 | nncnd 12253 |
. . . . 5
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (!β(if(π½ = 0, (π β 1), π) β π)) β β) |
| 38 | 36 | nnne0d 12287 |
. . . . 5
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (!β(if(π½ = 0, (π β 1), π) β π)) β 0) |
| 39 | 21, 37, 38 | divcld 12015 |
. . . 4
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β ((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) β β) |
| 40 | 1, 2 | dvdmsscn 45383 |
. . . . . . . 8
β’ (π β π β β) |
| 41 | 40, 13 | sseldd 3974 |
. . . . . . 7
β’ (π β π β β) |
| 42 | 5 | elfzelzd 13529 |
. . . . . . . 8
β’ (π β π½ β β€) |
| 43 | 42 | zcnd 12692 |
. . . . . . 7
β’ (π β π½ β β) |
| 44 | 41, 43 | subcld 11596 |
. . . . . 6
β’ (π β (π β π½) β β) |
| 45 | 44 | adantr 479 |
. . . . 5
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (π β π½) β β) |
| 46 | 45, 35 | expcld 14137 |
. . . 4
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β ((π β π½)β(if(π½ = 0, (π β 1), π) β π)) β β) |
| 47 | 39, 46 | mulcld 11259 |
. . 3
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π β π½)β(if(π½ = 0, (π β 1), π) β π))) β β) |
| 48 | 14, 47 | ifclda 4560 |
. 2
β’ (π β if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π β π½)β(if(π½ = 0, (π β 1), π) β π)))) β β) |
| 49 | 7, 12, 13, 48 | fvmptd 7005 |
1
β’ (π β (((π Dπ (π»βπ½))βπ)βπ) = if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π β π½)β(if(π½ = 0, (π β 1), π) β π))))) |
