Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . . 4
β’
(β€β₯βπ) = (β€β₯βπ) |
2 | | simp1 997 |
. . . 4
β’ ((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β π β β€) |
3 | | simp2 998 |
. . . 4
β’ ((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β π΄ β (β€β₯βπ)) |
4 | | c0ex 7950 |
. . . . . . 7
β’ 0 β
V |
5 | 4 | fvconst2 5732 |
. . . . . 6
β’ (π β
(β€β₯βπ) β
(((β€β₯βπ) Γ {0})βπ) = 0) |
6 | 5 | adantl 277 |
. . . . 5
β’ (((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β§ π β (β€β₯βπ)) β
(((β€β₯βπ) Γ {0})βπ) = 0) |
7 | | eleq1w 2238 |
. . . . . . . 8
β’ (π = π β (π β π΄ β π β π΄)) |
8 | 7 | dcbid 838 |
. . . . . . 7
β’ (π = π β (DECID π β π΄ β DECID π β π΄)) |
9 | | simpl3 1002 |
. . . . . . 7
β’ (((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β§ π β (β€β₯βπ)) β βπ β
(β€β₯βπ)DECID π β π΄) |
10 | | simpr 110 |
. . . . . . 7
β’ (((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
11 | 8, 9, 10 | rspcdva 2846 |
. . . . . 6
β’ (((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β§ π β (β€β₯βπ)) β DECID
π β π΄) |
12 | | ifiddc 3568 |
. . . . . 6
β’
(DECID π β π΄ β if(π β π΄, 0, 0) = 0) |
13 | 11, 12 | syl 14 |
. . . . 5
β’ (((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β§ π β (β€β₯βπ)) β if(π β π΄, 0, 0) = 0) |
14 | 6, 13 | eqtr4d 2213 |
. . . 4
β’ (((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β§ π β (β€β₯βπ)) β
(((β€β₯βπ) Γ {0})βπ) = if(π β π΄, 0, 0)) |
15 | | simp3 999 |
. . . . 5
β’ ((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β βπ β (β€β₯βπ)DECID π β π΄) |
16 | | eleq1w 2238 |
. . . . . . 7
β’ (π = π β (π β π΄ β π β π΄)) |
17 | 16 | dcbid 838 |
. . . . . 6
β’ (π = π β (DECID π β π΄ β DECID π β π΄)) |
18 | 17 | cbvralv 2703 |
. . . . 5
β’
(βπ β
(β€β₯βπ)DECID π β π΄ β βπ β (β€β₯βπ)DECID π β π΄) |
19 | 15, 18 | sylib 122 |
. . . 4
β’ ((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β βπ β (β€β₯βπ)DECID π β π΄) |
20 | | 0cnd 7949 |
. . . 4
β’ (((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β§ π β π΄) β 0 β β) |
21 | 1, 2, 3, 14, 19, 20 | zsumdc 11391 |
. . 3
β’ ((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β Ξ£π β π΄ 0 = ( β βseqπ( + , ((β€β₯βπ) Γ
{0})))) |
22 | | fclim 11301 |
. . . . 5
β’ β
:dom β βΆβ |
23 | | ffun 5368 |
. . . . 5
β’ ( β
:dom β βΆβ β Fun β ) |
24 | 22, 23 | ax-mp 5 |
. . . 4
β’ Fun
β |
25 | | serclim0 11312 |
. . . . 5
β’ (π β β€ β seqπ( + ,
((β€β₯βπ) Γ {0})) β 0) |
26 | 2, 25 | syl 14 |
. . . 4
β’ ((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β seqπ( + , ((β€β₯βπ) Γ {0})) β
0) |
27 | | funbrfv 5554 |
. . . 4
β’ (Fun
β β (seqπ( + ,
((β€β₯βπ) Γ {0})) β 0 β ( β
βseqπ( + ,
((β€β₯βπ) Γ {0}))) = 0)) |
28 | 24, 26, 27 | mpsyl 65 |
. . 3
β’ ((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β ( β βseqπ( + ,
((β€β₯βπ) Γ {0}))) = 0) |
29 | 21, 28 | eqtrd 2210 |
. 2
β’ ((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β Ξ£π β π΄ 0 = 0) |
30 | | fz1f1o 11382 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
31 | | sumeq1 11362 |
. . . . 5
β’ (π΄ = β
β Ξ£π β π΄ 0 = Ξ£π β β
0) |
32 | | sum0 11395 |
. . . . 5
β’
Ξ£π β
β
0 = 0 |
33 | 31, 32 | eqtrdi 2226 |
. . . 4
β’ (π΄ = β
β Ξ£π β π΄ 0 = 0) |
34 | | eqidd 2178 |
. . . . . . . . 9
β’ (π = (πβπ) β 0 = 0) |
35 | | simpl 109 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β (β―βπ΄) β
β) |
36 | | simpr 110 |
. . . . . . . . 9
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
37 | | 0cnd 7949 |
. . . . . . . . 9
β’
((((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β§ π β π΄) β 0 β β) |
38 | | elfznn 10053 |
. . . . . . . . . . 11
β’ (π β
(1...(β―βπ΄))
β π β
β) |
39 | 4 | fvconst2 5732 |
. . . . . . . . . . 11
β’ (π β β β ((β
Γ {0})βπ) =
0) |
40 | 38, 39 | syl 14 |
. . . . . . . . . 10
β’ (π β
(1...(β―βπ΄))
β ((β Γ {0})βπ) = 0) |
41 | 40 | adantl 277 |
. . . . . . . . 9
β’
((((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β§ π β (1...(β―βπ΄))) β ((β Γ
{0})βπ) =
0) |
42 | 34, 35, 36, 37, 41 | fsum3 11394 |
. . . . . . . 8
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β Ξ£π β π΄ 0 = (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), ((β Γ {0})βπ),
0)))β(β―βπ΄))) |
43 | | nnuz 9562 |
. . . . . . . . . . . . 13
β’ β =
(β€β₯β1) |
44 | 43 | fser0const 10515 |
. . . . . . . . . . . 12
β’
((β―βπ΄)
β β β (π
β β β¦ if(π
β€ (β―βπ΄),
((β Γ {0})βπ), 0)) = (β Γ
{0})) |
45 | 44 | seqeq3d 10452 |
. . . . . . . . . . 11
β’
((β―βπ΄)
β β β seq1( + , (π β β β¦ if(π β€ (β―βπ΄), ((β Γ {0})βπ), 0))) = seq1( + , (β
Γ {0}))) |
46 | 45 | fveq1d 5517 |
. . . . . . . . . 10
β’
((β―βπ΄)
β β β (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), ((β Γ {0})βπ),
0)))β(β―βπ΄)) = (seq1( + , (β Γ
{0}))β(β―βπ΄))) |
47 | 43 | ser0 10513 |
. . . . . . . . . 10
β’
((β―βπ΄)
β β β (seq1( + , (β Γ
{0}))β(β―βπ΄)) = 0) |
48 | 46, 47 | eqtrd 2210 |
. . . . . . . . 9
β’
((β―βπ΄)
β β β (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), ((β Γ {0})βπ),
0)))β(β―βπ΄)) = 0) |
49 | 35, 48 | syl 14 |
. . . . . . . 8
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), ((β Γ
{0})βπ),
0)))β(β―βπ΄)) = 0) |
50 | 42, 49 | eqtrd 2210 |
. . . . . . 7
β’
(((β―βπ΄)
β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β Ξ£π β π΄ 0 = 0) |
51 | 50 | ex 115 |
. . . . . 6
β’
((β―βπ΄)
β β β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β Ξ£π β π΄ 0 = 0)) |
52 | 51 | exlimdv 1819 |
. . . . 5
β’
((β―βπ΄)
β β β (βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β Ξ£π β π΄ 0 = 0)) |
53 | 52 | imp 124 |
. . . 4
β’
(((β―βπ΄)
β β β§ βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β Ξ£π β π΄ 0 = 0) |
54 | 33, 53 | jaoi 716 |
. . 3
β’ ((π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ 0 = 0) |
55 | 30, 54 | syl 14 |
. 2
β’ (π΄ β Fin β Ξ£π β π΄ 0 = 0) |
56 | 29, 55 | jaoi 716 |
1
β’ (((π β β€ β§ π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄) β¨ π΄ β Fin) β Ξ£π β π΄ 0 = 0) |