Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
β’
(β€β₯βπ) = (β€β₯βπ) |
2 | | simpr 486 |
. . . . 5
β’ ((π΄ β
(β€β₯βπ) β§ π β β€) β π β β€) |
3 | | simpl 484 |
. . . . 5
β’ ((π΄ β
(β€β₯βπ) β§ π β β€) β π΄ β (β€β₯βπ)) |
4 | | c0ex 11156 |
. . . . . . . 8
β’ 0 β
V |
5 | 4 | fvconst2 7158 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β
(((β€β₯βπ) Γ {0})βπ) = 0) |
6 | | ifid 4531 |
. . . . . . 7
β’ if(π β π΄, 0, 0) = 0 |
7 | 5, 6 | eqtr4di 2795 |
. . . . . 6
β’ (π β
(β€β₯βπ) β
(((β€β₯βπ) Γ {0})βπ) = if(π β π΄, 0, 0)) |
8 | 7 | adantl 483 |
. . . . 5
β’ (((π΄ β
(β€β₯βπ) β§ π β β€) β§ π β (β€β₯βπ)) β
(((β€β₯βπ) Γ {0})βπ) = if(π β π΄, 0, 0)) |
9 | | 0cnd 11155 |
. . . . 5
β’ (((π΄ β
(β€β₯βπ) β§ π β β€) β§ π β π΄) β 0 β β) |
10 | 1, 2, 3, 8, 9 | zsum 15610 |
. . . 4
β’ ((π΄ β
(β€β₯βπ) β§ π β β€) β Ξ£π β π΄ 0 = ( β βseqπ( + , ((β€β₯βπ) Γ
{0})))) |
11 | | fclim 15442 |
. . . . . 6
β’ β
:dom β βΆβ |
12 | | ffun 6676 |
. . . . . 6
β’ ( β
:dom β βΆβ β Fun β ) |
13 | 11, 12 | ax-mp 5 |
. . . . 5
β’ Fun
β |
14 | | serclim0 15466 |
. . . . . 6
β’ (π β β€ β seqπ( + ,
((β€β₯βπ) Γ {0})) β 0) |
15 | 14 | adantl 483 |
. . . . 5
β’ ((π΄ β
(β€β₯βπ) β§ π β β€) β seqπ( + , ((β€β₯βπ) Γ {0})) β
0) |
16 | | funbrfv 6898 |
. . . . 5
β’ (Fun
β β (seqπ( + ,
((β€β₯βπ) Γ {0})) β 0 β ( β
βseqπ( + ,
((β€β₯βπ) Γ {0}))) = 0)) |
17 | 13, 15, 16 | mpsyl 68 |
. . . 4
β’ ((π΄ β
(β€β₯βπ) β§ π β β€) β ( β
βseqπ( + ,
((β€β₯βπ) Γ {0}))) = 0) |
18 | 10, 17 | eqtrd 2777 |
. . 3
β’ ((π΄ β
(β€β₯βπ) β§ π β β€) β Ξ£π β π΄ 0 = 0) |
19 | | uzf 12773 |
. . . . . . . . 9
β’
β€β₯:β€βΆπ« β€ |
20 | 19 | fdmi 6685 |
. . . . . . . 8
β’ dom
β€β₯ = β€ |
21 | 20 | eleq2i 2830 |
. . . . . . 7
β’ (π β dom
β€β₯ β π β β€) |
22 | | ndmfv 6882 |
. . . . . . 7
β’ (Β¬
π β dom
β€β₯ β (β€β₯βπ) = β
) |
23 | 21, 22 | sylnbir 331 |
. . . . . 6
β’ (Β¬
π β β€ β
(β€β₯βπ) = β
) |
24 | 23 | sseq2d 3981 |
. . . . 5
β’ (Β¬
π β β€ β
(π΄ β
(β€β₯βπ) β π΄ β β
)) |
25 | 24 | biimpac 480 |
. . . 4
β’ ((π΄ β
(β€β₯βπ) β§ Β¬ π β β€) β π΄ β β
) |
26 | | ss0 4363 |
. . . 4
β’ (π΄ β β
β π΄ = β
) |
27 | | sumeq1 15580 |
. . . . 5
β’ (π΄ = β
β Ξ£π β π΄ 0 = Ξ£π β β
0) |
28 | | sum0 15613 |
. . . . 5
β’
Ξ£π β
β
0 = 0 |
29 | 27, 28 | eqtrdi 2793 |
. . . 4
β’ (π΄ = β
β Ξ£π β π΄ 0 = 0) |
30 | 25, 26, 29 | 3syl 18 |
. . 3
β’ ((π΄ β
(β€β₯βπ) β§ Β¬ π β β€) β Ξ£π β π΄ 0 = 0) |
31 | 18, 30 | pm2.61dan 812 |
. 2
β’ (π΄ β
(β€β₯βπ) β Ξ£π β π΄ 0 = 0) |
32 | | fz1f1o 15602 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
33 | | eqidd 2738 |
. . . . . . . . 9
β’ (π = (πβπ) β 0 = 0) |
34 | | simpl 484 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β (β―βπ΄) β
β) |
35 | | simpr 486 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
36 | | 0cnd 11155 |
. . . . . . . . 9
β’
((((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β§ π β π΄) β 0 β β) |
37 | | elfznn 13477 |
. . . . . . . . . . 11
β’ (π β
(1...(β―βπ΄))
β π β
β) |
38 | 4 | fvconst2 7158 |
. . . . . . . . . . 11
β’ (π β β β ((β
Γ {0})βπ) =
0) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
β’ (π β
(1...(β―βπ΄))
β ((β Γ {0})βπ) = 0) |
40 | 39 | adantl 483 |
. . . . . . . . 9
β’
((((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β§ π β (1...(β―βπ΄))) β ((β Γ
{0})βπ) =
0) |
41 | 33, 34, 35, 36, 40 | fsum 15612 |
. . . . . . . 8
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β Ξ£π β π΄ 0 = (seq1( + , (β Γ
{0}))β(β―βπ΄))) |
42 | | nnuz 12813 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
43 | 42 | ser0 13967 |
. . . . . . . . 9
β’
((β―βπ΄)
β β β (seq1( + , (β Γ
{0}))β(β―βπ΄)) = 0) |
44 | 43 | adantr 482 |
. . . . . . . 8
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β (seq1( + , (β
Γ {0}))β(β―βπ΄)) = 0) |
45 | 41, 44 | eqtrd 2777 |
. . . . . . 7
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β Ξ£π β π΄ 0 = 0) |
46 | 45 | ex 414 |
. . . . . 6
β’
((β―βπ΄)
β β β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β Ξ£π β π΄ 0 = 0)) |
47 | 46 | exlimdv 1937 |
. . . . 5
β’
((β―βπ΄)
β β β (βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β Ξ£π β π΄ 0 = 0)) |
48 | 47 | imp 408 |
. . . 4
β’
(((β―βπ΄)
β β β§ βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β Ξ£π β π΄ 0 = 0) |
49 | 29, 48 | jaoi 856 |
. . 3
β’ ((π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ 0 = 0) |
50 | 32, 49 | syl 17 |
. 2
β’ (π΄ β Fin β Ξ£π β π΄ 0 = 0) |
51 | 31, 50 | jaoi 856 |
1
β’ ((π΄ β
(β€β₯βπ) β¨ π΄ β Fin) β Ξ£π β π΄ 0 = 0) |