Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . 4
β’ (π = 0 β (πΊβπ) = (πΊβ0)) |
2 | 1 | seqeq3d 13921 |
. . 3
β’ (π = 0 β seq0( + , (πΊβπ)) = seq0( + , (πΊβ0))) |
3 | 2 | eleq1d 2823 |
. 2
β’ (π = 0 β (seq0( + , (πΊβπ)) β dom β β seq0( + , (πΊβ0)) β dom β
)) |
4 | | 0red 11165 |
. 2
β’ (π β 0 β
β) |
5 | | nn0uz 12812 |
. . 3
β’
β0 = (β€β₯β0) |
6 | | 0zd 12518 |
. . 3
β’ (π β 0 β
β€) |
7 | | snfi 8995 |
. . . 4
β’ {0}
β Fin |
8 | 7 | a1i 11 |
. . 3
β’ (π β {0} β
Fin) |
9 | | 0nn0 12435 |
. . . . 5
β’ 0 β
β0 |
10 | 9 | a1i 11 |
. . . 4
β’ (π β 0 β
β0) |
11 | 10 | snssd 4774 |
. . 3
β’ (π β {0} β
β0) |
12 | | ifid 4531 |
. . . 4
β’ if(π β {0}, ((πΊβ0)βπ), ((πΊβ0)βπ)) = ((πΊβ0)βπ) |
13 | | 0cnd 11155 |
. . . . . . . 8
β’ (π β 0 β
β) |
14 | | pser.g |
. . . . . . . . 9
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) |
15 | 14 | pserval2 25786 |
. . . . . . . 8
β’ ((0
β β β§ π
β β0) β ((πΊβ0)βπ) = ((π΄βπ) Β· (0βπ))) |
16 | 13, 15 | sylan 581 |
. . . . . . 7
β’ ((π β§ π β β0) β ((πΊβ0)βπ) = ((π΄βπ) Β· (0βπ))) |
17 | 16 | adantr 482 |
. . . . . 6
β’ (((π β§ π β β0) β§ Β¬
π β {0}) β
((πΊβ0)βπ) = ((π΄βπ) Β· (0βπ))) |
18 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β π β
β0) |
19 | | elnn0 12422 |
. . . . . . . . . . . . 13
β’ (π β β0
β (π β β
β¨ π =
0)) |
20 | 18, 19 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β (π β β β¨ π = 0)) |
21 | 20 | ord 863 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (Β¬
π β β β
π = 0)) |
22 | | velsn 4607 |
. . . . . . . . . . 11
β’ (π β {0} β π = 0) |
23 | 21, 22 | syl6ibr 252 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (Β¬
π β β β
π β
{0})) |
24 | 23 | con1d 145 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (Β¬
π β {0} β π β
β)) |
25 | 24 | imp 408 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ Β¬
π β {0}) β π β
β) |
26 | 25 | 0expd 14051 |
. . . . . . 7
β’ (((π β§ π β β0) β§ Β¬
π β {0}) β
(0βπ) =
0) |
27 | 26 | oveq2d 7378 |
. . . . . 6
β’ (((π β§ π β β0) β§ Β¬
π β {0}) β
((π΄βπ) Β· (0βπ)) = ((π΄βπ) Β· 0)) |
28 | | radcnv.a |
. . . . . . . . 9
β’ (π β π΄:β0βΆβ) |
29 | 28 | ffvelcdmda 7040 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π΄βπ) β β) |
30 | 29 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β β0) β§ Β¬
π β {0}) β (π΄βπ) β β) |
31 | 30 | mul01d 11361 |
. . . . . 6
β’ (((π β§ π β β0) β§ Β¬
π β {0}) β
((π΄βπ) Β· 0) =
0) |
32 | 17, 27, 31 | 3eqtrd 2781 |
. . . . 5
β’ (((π β§ π β β0) β§ Β¬
π β {0}) β
((πΊβ0)βπ) = 0) |
33 | 32 | ifeq2da 4523 |
. . . 4
β’ ((π β§ π β β0) β if(π β {0}, ((πΊβ0)βπ), ((πΊβ0)βπ)) = if(π β {0}, ((πΊβ0)βπ), 0)) |
34 | 12, 33 | eqtr3id 2791 |
. . 3
β’ ((π β§ π β β0) β ((πΊβ0)βπ) = if(π β {0}, ((πΊβ0)βπ), 0)) |
35 | 11 | sselda 3949 |
. . . 4
β’ ((π β§ π β {0}) β π β β0) |
36 | 14, 28, 13 | psergf 25787 |
. . . . 5
β’ (π β (πΊβ0):β0βΆβ) |
37 | 36 | ffvelcdmda 7040 |
. . . 4
β’ ((π β§ π β β0) β ((πΊβ0)βπ) β
β) |
38 | 35, 37 | syldan 592 |
. . 3
β’ ((π β§ π β {0}) β ((πΊβ0)βπ) β β) |
39 | 5, 6, 8, 11, 34, 38 | fsumcvg3 15621 |
. 2
β’ (π β seq0( + , (πΊβ0)) β dom β
) |
40 | 3, 4, 39 | elrabd 3652 |
1
β’ (π β 0 β {π β β β£ seq0( +
, (πΊβπ)) β dom β
}) |