Step | Hyp | Ref
| Expression |
1 | | 0nn0 12436 |
. . . 4
β’ 0 β
β0 |
2 | 1 | a1i 11 |
. . 3
β’ (π β 0 β
β0) |
3 | | fwddifn0.1 |
. . 3
β’ (π β π΄ β β) |
4 | | fwddifn0.2 |
. . 3
β’ (π β πΉ:π΄βΆβ) |
5 | | fwddifn0.3 |
. . . 4
β’ (π β π β π΄) |
6 | 3, 5 | sseldd 3949 |
. . 3
β’ (π β π β β) |
7 | | 0z 12518 |
. . . . . . 7
β’ 0 β
β€ |
8 | | fzsn 13492 |
. . . . . . 7
β’ (0 β
β€ β (0...0) = {0}) |
9 | 7, 8 | ax-mp 5 |
. . . . . 6
β’ (0...0) =
{0} |
10 | 9 | eleq2i 2826 |
. . . . 5
β’ (π β (0...0) β π β {0}) |
11 | | velsn 4606 |
. . . . 5
β’ (π β {0} β π = 0) |
12 | 10, 11 | bitri 275 |
. . . 4
β’ (π β (0...0) β π = 0) |
13 | | oveq2 7369 |
. . . . . 6
β’ (π = 0 β (π + π) = (π + 0)) |
14 | 13 | adantl 483 |
. . . . 5
β’ ((π β§ π = 0) β (π + π) = (π + 0)) |
15 | 6 | addridd 11363 |
. . . . . . 7
β’ (π β (π + 0) = π) |
16 | 15, 5 | eqeltrd 2834 |
. . . . . 6
β’ (π β (π + 0) β π΄) |
17 | 16 | adantr 482 |
. . . . 5
β’ ((π β§ π = 0) β (π + 0) β π΄) |
18 | 14, 17 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π = 0) β (π + π) β π΄) |
19 | 12, 18 | sylan2b 595 |
. . 3
β’ ((π β§ π β (0...0)) β (π + π) β π΄) |
20 | 2, 3, 4, 6, 19 | fwddifnval 34801 |
. 2
β’ (π β ((0
β³n πΉ)βπ) = Ξ£π β (0...0)((0Cπ) Β· ((-1β(0 β π)) Β· (πΉβ(π + π))))) |
21 | 15 | fveq2d 6850 |
. . . . . . . . 9
β’ (π β (πΉβ(π + 0)) = (πΉβπ)) |
22 | 21 | oveq2d 7377 |
. . . . . . . 8
β’ (π β (1 Β· (πΉβ(π + 0))) = (1 Β· (πΉβπ))) |
23 | 4, 5 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ (π β (πΉβπ) β β) |
24 | 23 | mullidd 11181 |
. . . . . . . 8
β’ (π β (1 Β· (πΉβπ)) = (πΉβπ)) |
25 | 22, 24 | eqtrd 2773 |
. . . . . . 7
β’ (π β (1 Β· (πΉβ(π + 0))) = (πΉβπ)) |
26 | 25 | oveq2d 7377 |
. . . . . 6
β’ (π β (1 Β· (1 Β·
(πΉβ(π + 0)))) = (1 Β· (πΉβπ))) |
27 | 26, 24 | eqtrd 2773 |
. . . . 5
β’ (π β (1 Β· (1 Β·
(πΉβ(π + 0)))) = (πΉβπ)) |
28 | 27, 23 | eqeltrd 2834 |
. . . 4
β’ (π β (1 Β· (1 Β·
(πΉβ(π + 0)))) β β) |
29 | | oveq2 7369 |
. . . . . . 7
β’ (π = 0 β (0Cπ) = (0C0)) |
30 | | bcnn 14221 |
. . . . . . . 8
β’ (0 β
β0 β (0C0) = 1) |
31 | 1, 30 | ax-mp 5 |
. . . . . . 7
β’ (0C0) =
1 |
32 | 29, 31 | eqtrdi 2789 |
. . . . . 6
β’ (π = 0 β (0Cπ) = 1) |
33 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = 0 β (0 β π) = (0 β
0)) |
34 | | 0m0e0 12281 |
. . . . . . . . . 10
β’ (0
β 0) = 0 |
35 | 33, 34 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π = 0 β (0 β π) = 0) |
36 | 35 | oveq2d 7377 |
. . . . . . . 8
β’ (π = 0 β (-1β(0 β
π)) =
(-1β0)) |
37 | | neg1cn 12275 |
. . . . . . . . 9
β’ -1 β
β |
38 | | exp0 13980 |
. . . . . . . . 9
β’ (-1
β β β (-1β0) = 1) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . 8
β’
(-1β0) = 1 |
40 | 36, 39 | eqtrdi 2789 |
. . . . . . 7
β’ (π = 0 β (-1β(0 β
π)) = 1) |
41 | 13 | fveq2d 6850 |
. . . . . . 7
β’ (π = 0 β (πΉβ(π + π)) = (πΉβ(π + 0))) |
42 | 40, 41 | oveq12d 7379 |
. . . . . 6
β’ (π = 0 β ((-1β(0 β
π)) Β· (πΉβ(π + π))) = (1 Β· (πΉβ(π + 0)))) |
43 | 32, 42 | oveq12d 7379 |
. . . . 5
β’ (π = 0 β ((0Cπ) Β· ((-1β(0 β
π)) Β· (πΉβ(π + π)))) = (1 Β· (1 Β· (πΉβ(π + 0))))) |
44 | 43 | fsum1 15640 |
. . . 4
β’ ((0
β β€ β§ (1 Β· (1 Β· (πΉβ(π + 0)))) β β) β Ξ£π β (0...0)((0Cπ) Β· ((-1β(0 β
π)) Β· (πΉβ(π + π)))) = (1 Β· (1 Β· (πΉβ(π + 0))))) |
45 | 7, 28, 44 | sylancr 588 |
. . 3
β’ (π β Ξ£π β (0...0)((0Cπ) Β· ((-1β(0 β π)) Β· (πΉβ(π + π)))) = (1 Β· (1 Β· (πΉβ(π + 0))))) |
46 | 45, 27 | eqtrd 2773 |
. 2
β’ (π β Ξ£π β (0...0)((0Cπ) Β· ((-1β(0 β π)) Β· (πΉβ(π + π)))) = (πΉβπ)) |
47 | 20, 46 | eqtrd 2773 |
1
β’ (π β ((0
β³n πΉ)βπ) = (πΉβπ)) |