Step | Hyp | Ref
| Expression |
1 | | etransclem1.x |
. . . . . 6
β’ (π β π β β) |
2 | 1 | sselda 3981 |
. . . . 5
β’ ((π β§ π₯ β π) β π₯ β β) |
3 | | etransclem1.j |
. . . . . . . 8
β’ (π β π½ β (0...π)) |
4 | 3 | elfzelzd 13498 |
. . . . . . 7
β’ (π β π½ β β€) |
5 | 4 | zcnd 12663 |
. . . . . 6
β’ (π β π½ β β) |
6 | 5 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π) β π½ β β) |
7 | 2, 6 | subcld 11567 |
. . . 4
β’ ((π β§ π₯ β π) β (π₯ β π½) β β) |
8 | | etransclem1.p |
. . . . . . 7
β’ (π β π β β) |
9 | | nnm1nn0 12509 |
. . . . . . 7
β’ (π β β β (π β 1) β
β0) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ (π β (π β 1) β
β0) |
11 | 8 | nnnn0d 12528 |
. . . . . 6
β’ (π β π β
β0) |
12 | 10, 11 | ifcld 4573 |
. . . . 5
β’ (π β if(π½ = 0, (π β 1), π) β
β0) |
13 | 12 | adantr 481 |
. . . 4
β’ ((π β§ π₯ β π) β if(π½ = 0, (π β 1), π) β
β0) |
14 | 7, 13 | expcld 14107 |
. . 3
β’ ((π β§ π₯ β π) β ((π₯ β π½)βif(π½ = 0, (π β 1), π)) β β) |
15 | | eqid 2732 |
. . 3
β’ (π₯ β π β¦ ((π₯ β π½)βif(π½ = 0, (π β 1), π))) = (π₯ β π β¦ ((π₯ β π½)βif(π½ = 0, (π β 1), π))) |
16 | 14, 15 | fmptd 7110 |
. 2
β’ (π β (π₯ β π β¦ ((π₯ β π½)βif(π½ = 0, (π β 1), π))):πβΆβ) |
17 | | etransclem1.h |
. . . . 5
β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) |
18 | | oveq2 7413 |
. . . . . . . 8
β’ (π = π β (π₯ β π) = (π₯ β π)) |
19 | | eqeq1 2736 |
. . . . . . . . 9
β’ (π = π β (π = 0 β π = 0)) |
20 | 19 | ifbid 4550 |
. . . . . . . 8
β’ (π = π β if(π = 0, (π β 1), π) = if(π = 0, (π β 1), π)) |
21 | 18, 20 | oveq12d 7423 |
. . . . . . 7
β’ (π = π β ((π₯ β π)βif(π = 0, (π β 1), π)) = ((π₯ β π)βif(π = 0, (π β 1), π))) |
22 | 21 | mpteq2dv 5249 |
. . . . . 6
β’ (π = π β (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π))) = (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) |
23 | 22 | cbvmptv 5260 |
. . . . 5
β’ (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) |
24 | 17, 23 | eqtri 2760 |
. . . 4
β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) |
25 | | oveq2 7413 |
. . . . . 6
β’ (π = π½ β (π₯ β π) = (π₯ β π½)) |
26 | | eqeq1 2736 |
. . . . . . 7
β’ (π = π½ β (π = 0 β π½ = 0)) |
27 | 26 | ifbid 4550 |
. . . . . 6
β’ (π = π½ β if(π = 0, (π β 1), π) = if(π½ = 0, (π β 1), π)) |
28 | 25, 27 | oveq12d 7423 |
. . . . 5
β’ (π = π½ β ((π₯ β π)βif(π = 0, (π β 1), π)) = ((π₯ β π½)βif(π½ = 0, (π β 1), π))) |
29 | 28 | mpteq2dv 5249 |
. . . 4
β’ (π = π½ β (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π))) = (π₯ β π β¦ ((π₯ β π½)βif(π½ = 0, (π β 1), π)))) |
30 | | cnex 11187 |
. . . . . 6
β’ β
β V |
31 | 30 | ssex 5320 |
. . . . 5
β’ (π β β β π β V) |
32 | | mptexg 7219 |
. . . . 5
β’ (π β V β (π₯ β π β¦ ((π₯ β π½)βif(π½ = 0, (π β 1), π))) β V) |
33 | 1, 31, 32 | 3syl 18 |
. . . 4
β’ (π β (π₯ β π β¦ ((π₯ β π½)βif(π½ = 0, (π β 1), π))) β V) |
34 | 24, 29, 3, 33 | fvmptd3 7018 |
. . 3
β’ (π β (π»βπ½) = (π₯ β π β¦ ((π₯ β π½)βif(π½ = 0, (π β 1), π)))) |
35 | 34 | feq1d 6699 |
. 2
β’ (π β ((π»βπ½):πβΆβ β (π₯ β π β¦ ((π₯ β π½)βif(π½ = 0, (π β 1), π))):πβΆβ)) |
36 | 16, 35 | mpbird 256 |
1
β’ (π β (π»βπ½):πβΆβ) |