Step | Hyp | Ref
| Expression |
1 | | df-sumdc 11361 |
. 2
β’
Ξ£π β
π΄ π΅ = (β©π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
2 | | nnuz 9562 |
. . . . 5
β’ β =
(β€β₯β1) |
3 | | 1zzd 9279 |
. . . . 5
β’ (π β 1 β
β€) |
4 | | elnnuz 9563 |
. . . . . 6
β’ (π₯ β β β π₯ β
(β€β₯β1)) |
5 | 2 | eqimss2i 3212 |
. . . . . . . . . 10
β’
(β€β₯β1) β β |
6 | 5 | sseli 3151 |
. . . . . . . . 9
β’ (π₯ β
(β€β₯β1) β π₯ β β) |
7 | 6 | adantl 277 |
. . . . . . . 8
β’ ((π β§ π₯ β (β€β₯β1))
β π₯ β
β) |
8 | | fveq2 5515 |
. . . . . . . . . . 11
β’ (π = π₯ β (πΊβπ) = (πΊβπ₯)) |
9 | 8 | eleq1d 2246 |
. . . . . . . . . 10
β’ (π = π₯ β ((πΊβπ) β β β (πΊβπ₯) β β)) |
10 | | fsum.1 |
. . . . . . . . . . . 12
β’ (π = (πΉβπ) β π΅ = πΆ) |
11 | | fsum.2 |
. . . . . . . . . . . 12
β’ (π β π β β) |
12 | | fsum.3 |
. . . . . . . . . . . 12
β’ (π β πΉ:(1...π)β1-1-ontoβπ΄) |
13 | | fsum.4 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π΅ β β) |
14 | | fsum.5 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (πΊβπ) = πΆ) |
15 | 10, 11, 12, 13, 14 | fsumgcl 11393 |
. . . . . . . . . . 11
β’ (π β βπ β (1...π)(πΊβπ) β β) |
16 | 15 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β βπ β (1...π)(πΊβπ) β β) |
17 | | 1zzd 9279 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β 1 β
β€) |
18 | 11 | nnzd 9373 |
. . . . . . . . . . . . 13
β’ (π β π β β€) |
19 | 18 | ad2antrr 488 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β π β β€) |
20 | | eluzelz 9536 |
. . . . . . . . . . . . 13
β’ (π₯ β
(β€β₯β1) β π₯ β β€) |
21 | 20 | ad2antlr 489 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β π₯ β β€) |
22 | 17, 19, 21 | 3jca 1177 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β (1 β β€ β§
π β β€ β§
π₯ β
β€)) |
23 | | eluzle 9539 |
. . . . . . . . . . . . 13
β’ (π₯ β
(β€β₯β1) β 1 β€ π₯) |
24 | 23 | ad2antlr 489 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β 1 β€ π₯) |
25 | | simpr 110 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β π₯ β€ π) |
26 | 24, 25 | jca 306 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β (1 β€ π₯ β§ π₯ β€ π)) |
27 | | elfz2 10014 |
. . . . . . . . . . 11
β’ (π₯ β (1...π) β ((1 β β€ β§ π β β€ β§ π₯ β β€) β§ (1 β€
π₯ β§ π₯ β€ π))) |
28 | 22, 26, 27 | sylanbrc 417 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β π₯ β (1...π)) |
29 | 9, 16, 28 | rspcdva 2846 |
. . . . . . . . 9
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β (πΊβπ₯) β β) |
30 | | 0cnd 7949 |
. . . . . . . . 9
β’ (((π β§ π₯ β (β€β₯β1))
β§ Β¬ π₯ β€ π) β 0 β
β) |
31 | 7 | nnzd 9373 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (β€β₯β1))
β π₯ β
β€) |
32 | 18 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (β€β₯β1))
β π β
β€) |
33 | | zdcle 9328 |
. . . . . . . . . 10
β’ ((π₯ β β€ β§ π β β€) β
DECID π₯ β€
π) |
34 | 31, 32, 33 | syl2anc 411 |
. . . . . . . . 9
β’ ((π β§ π₯ β (β€β₯β1))
β DECID π₯ β€ π) |
35 | 29, 30, 34 | ifcldadc 3563 |
. . . . . . . 8
β’ ((π β§ π₯ β (β€β₯β1))
β if(π₯ β€ π, (πΊβπ₯), 0) β β) |
36 | | breq1 4006 |
. . . . . . . . . 10
β’ (π = π₯ β (π β€ π β π₯ β€ π)) |
37 | 36, 8 | ifbieq1d 3556 |
. . . . . . . . 9
β’ (π = π₯ β if(π β€ π, (πΊβπ), 0) = if(π₯ β€ π, (πΊβπ₯), 0)) |
38 | | eqid 2177 |
. . . . . . . . 9
β’ (π β β β¦ if(π β€ π, (πΊβπ), 0)) = (π β β β¦ if(π β€ π, (πΊβπ), 0)) |
39 | 37, 38 | fvmptg 5592 |
. . . . . . . 8
β’ ((π₯ β β β§ if(π₯ β€ π, (πΊβπ₯), 0) β β) β ((π β β β¦ if(π β€ π, (πΊβπ), 0))βπ₯) = if(π₯ β€ π, (πΊβπ₯), 0)) |
40 | 7, 35, 39 | syl2anc 411 |
. . . . . . 7
β’ ((π β§ π₯ β (β€β₯β1))
β ((π β β
β¦ if(π β€ π, (πΊβπ), 0))βπ₯) = if(π₯ β€ π, (πΊβπ₯), 0)) |
41 | 40, 35 | eqeltrd 2254 |
. . . . . 6
β’ ((π β§ π₯ β (β€β₯β1))
β ((π β β
β¦ if(π β€ π, (πΊβπ), 0))βπ₯) β β) |
42 | 4, 41 | sylan2b 287 |
. . . . 5
β’ ((π β§ π₯ β β) β ((π β β β¦ if(π β€ π, (πΊβπ), 0))βπ₯) β β) |
43 | 2, 3, 42 | serf 10473 |
. . . 4
β’ (π β seq1( + , (π β β β¦ if(π β€ π, (πΊβπ),
0))):ββΆβ) |
44 | 43, 11 | ffvelcdmd 5652 |
. . 3
β’ (π β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β β) |
45 | 44 | adantr 276 |
. . . . . . . 8
β’ ((π β§ (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β β) |
46 | | eleq1w 2238 |
. . . . . . . . . . . . 13
β’ (π = π β (π β π΄ β π β π΄)) |
47 | | csbeq1 3060 |
. . . . . . . . . . . . 13
β’ (π = π β β¦π / πβ¦π΅ = β¦π / πβ¦π΅) |
48 | 46, 47 | ifbieq1d 3556 |
. . . . . . . . . . . 12
β’ (π = π β if(π β π΄, β¦π / πβ¦π΅, 0) = if(π β π΄, β¦π / πβ¦π΅, 0)) |
49 | 48 | cbvmptv 4099 |
. . . . . . . . . . 11
β’ (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0)) = (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0)) |
50 | 13 | ralrimiva 2550 |
. . . . . . . . . . . 12
β’ (π β βπ β π΄ π΅ β β) |
51 | | nfcsb1v 3090 |
. . . . . . . . . . . . . 14
β’
β²πβ¦π / πβ¦π΅ |
52 | 51 | nfel1 2330 |
. . . . . . . . . . . . 13
β’
β²πβ¦π / πβ¦π΅ β β |
53 | | csbeq1a 3066 |
. . . . . . . . . . . . . 14
β’ (π = π β π΅ = β¦π / πβ¦π΅) |
54 | 53 | eleq1d 2246 |
. . . . . . . . . . . . 13
β’ (π = π β (π΅ β β β β¦π / πβ¦π΅ β β)) |
55 | 52, 54 | rspc 2835 |
. . . . . . . . . . . 12
β’ (π β π΄ β (βπ β π΄ π΅ β β β β¦π / πβ¦π΅ β β)) |
56 | 50, 55 | mpan9 281 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β β¦π / πβ¦π΅ β β) |
57 | | breq1 4006 |
. . . . . . . . . . . . 13
β’ (π = π β (π β€ (β―βπ΄) β π β€ (β―βπ΄))) |
58 | | fveq2 5515 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
59 | 58 | csbeq1d 3064 |
. . . . . . . . . . . . . 14
β’ (π = π β β¦(πβπ) / πβ¦π΅ = β¦(πβπ) / πβ¦π΅) |
60 | | csbco 3067 |
. . . . . . . . . . . . . 14
β’
β¦(πβπ) / πβ¦β¦π / πβ¦π΅ = β¦(πβπ) / πβ¦π΅ |
61 | 59, 60 | eqtr4di 2228 |
. . . . . . . . . . . . 13
β’ (π = π β β¦(πβπ) / πβ¦π΅ = β¦(πβπ) / πβ¦β¦π / πβ¦π΅) |
62 | 57, 61 | ifbieq1d 3556 |
. . . . . . . . . . . 12
β’ (π = π β if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0) = if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦β¦π / πβ¦π΅, 0)) |
63 | 62 | cbvmptv 4099 |
. . . . . . . . . . 11
β’ (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0)) = (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦β¦π / πβ¦π΅, 0)) |
64 | 49, 56, 63, 63 | summodc 11390 |
. . . . . . . . . 10
β’ (π β β*π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ βπ’ β
(β€β₯βπ)DECID π’ β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
65 | | eleq1w 2238 |
. . . . . . . . . . . . . . . 16
β’ (π’ = π β (π’ β π΄ β π β π΄)) |
66 | 65 | dcbid 838 |
. . . . . . . . . . . . . . 15
β’ (π’ = π β (DECID π’ β π΄ β DECID π β π΄)) |
67 | 66 | cbvralv 2703 |
. . . . . . . . . . . . . 14
β’
(βπ’ β
(β€β₯βπ)DECID π’ β π΄ β βπ β (β€β₯βπ)DECID π β π΄) |
68 | 67 | 3anbi2i 1191 |
. . . . . . . . . . . . 13
β’ ((π΄ β
(β€β₯βπ) β§ βπ’ β (β€β₯βπ)DECID π’ β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯)) |
69 | 68 | rexbii 2484 |
. . . . . . . . . . . 12
β’
(βπ β
β€ (π΄ β
(β€β₯βπ) β§ βπ’ β (β€β₯βπ)DECID π’ β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯)) |
70 | | 1zzd 9279 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β 1 β
β€) |
71 | | nnz 9271 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β π β
β€) |
72 | 70, 71 | fzfigd 10430 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β
(1...π) β
Fin) |
73 | | fihasheqf1oi 10766 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((1...π) β Fin
β§ π:(1...π)β1-1-ontoβπ΄) β
(β―β(1...π)) =
(β―βπ΄)) |
74 | 72, 73 | sylan 283 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ π:(1...π)β1-1-ontoβπ΄) β
(β―β(1...π)) =
(β―βπ΄)) |
75 | | nnnn0 9182 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β π β
β0) |
76 | 75 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ π:(1...π)β1-1-ontoβπ΄) β π β β0) |
77 | | hashfz1 10762 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β0
β (β―β(1...π)) = π) |
78 | 76, 77 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ π:(1...π)β1-1-ontoβπ΄) β
(β―β(1...π)) =
π) |
79 | 74, 78 | eqtr3d 2212 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π:(1...π)β1-1-ontoβπ΄) β (β―βπ΄) = π) |
80 | 79 | breq2d 4015 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π:(1...π)β1-1-ontoβπ΄) β (π β€ (β―βπ΄) β π β€ π)) |
81 | 80 | ifbid 3555 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π:(1...π)β1-1-ontoβπ΄) β if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0) = if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)) |
82 | 81 | mpteq2dv 4094 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π:(1...π)β1-1-ontoβπ΄) β (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0)) = (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0))) |
83 | 82 | seqeq3d 10452 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π:(1...π)β1-1-ontoβπ΄) β seq1( + , (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0))) = seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))) |
84 | 83 | fveq1d 5517 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π:(1...π)β1-1-ontoβπ΄) β (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)) |
85 | 84 | eqeq2d 2189 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π:(1...π)β1-1-ontoβπ΄) β (π₯ = (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0)))βπ) β π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) |
86 | 85 | pm5.32da 452 |
. . . . . . . . . . . . . 14
β’ (π β β β ((π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0)))βπ)) β (π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
87 | 86 | exbidv 1825 |
. . . . . . . . . . . . 13
β’ (π β β β
(βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0)))βπ)) β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
88 | 87 | rexbiia 2492 |
. . . . . . . . . . . 12
β’
(βπ β
β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0)))βπ)) β βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) |
89 | 69, 88 | orbi12i 764 |
. . . . . . . . . . 11
β’
((βπ β
β€ (π΄ β
(β€β₯βπ) β§ βπ’ β (β€β₯βπ)DECID π’ β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0)))βπ))) β (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
90 | 89 | mobii 2063 |
. . . . . . . . . 10
β’
(β*π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ βπ’ β
(β€β₯βπ)DECID π’ β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ (β―βπ΄), β¦(πβπ) / πβ¦π΅, 0)))βπ))) β β*π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
91 | 64, 90 | sylib 122 |
. . . . . . . . 9
β’ (π β β*π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
92 | 91 | adantr 276 |
. . . . . . . 8
β’ ((π β§ (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) β β*π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
93 | | simpr 110 |
. . . . . . . 8
β’ ((π β§ (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) β (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
94 | | f1of 5461 |
. . . . . . . . . . . . . 14
β’ (πΉ:(1...π)β1-1-ontoβπ΄ β πΉ:(1...π)βΆπ΄) |
95 | 12, 94 | syl 14 |
. . . . . . . . . . . . 13
β’ (π β πΉ:(1...π)βΆπ΄) |
96 | 3, 18 | fzfigd 10430 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β Fin) |
97 | | fex 5745 |
. . . . . . . . . . . . 13
β’ ((πΉ:(1...π)βΆπ΄ β§ (1...π) β Fin) β πΉ β V) |
98 | 95, 96, 97 | syl2anc 411 |
. . . . . . . . . . . 12
β’ (π β πΉ β V) |
99 | 11, 2 | eleqtrdi 2270 |
. . . . . . . . . . . . . 14
β’ (π β π β
(β€β₯β1)) |
100 | 14 | ralrimiva 2550 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ β (1...π)(πΊβπ) = πΆ) |
101 | | nfv 1528 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(πΊβπ) = πΆ |
102 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πβ¦π / πβ¦πΆ |
103 | 102 | nfeq2 2331 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(πΊβπ) = β¦π / πβ¦πΆ |
104 | | fveq2 5515 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πΊβπ) = (πΊβπ)) |
105 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β πΆ = β¦π / πβ¦πΆ) |
106 | 104, 105 | eqeq12d 2192 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((πΊβπ) = πΆ β (πΊβπ) = β¦π / πβ¦πΆ)) |
107 | 101, 103,
106 | cbvral 2699 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
(1...π)(πΊβπ) = πΆ β βπ β (1...π)(πΊβπ) = β¦π / πβ¦πΆ) |
108 | 100, 107 | sylib 122 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ β (1...π)(πΊβπ) = β¦π / πβ¦πΆ) |
109 | 108 | r19.21bi 2565 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β (πΊβπ) = β¦π / πβ¦πΆ) |
110 | | elfznn 10053 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β π β β) |
111 | 110 | adantl 277 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β π β β) |
112 | | elfzle2 10027 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) β π β€ π) |
113 | 112 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (1...π)) β π β€ π) |
114 | 113 | iftrued 3541 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β if(π β€ π, (πΊβπ), 0) = (πΊβπ)) |
115 | 104 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((πΊβπ) β β β (πΊβπ) β β)) |
116 | 15 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (1...π)) β βπ β (1...π)(πΊβπ) β β) |
117 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (1...π)) β π β (1...π)) |
118 | 115, 116,
117 | rspcdva 2846 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β (πΊβπ) β β) |
119 | 114, 118 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β if(π β€ π, (πΊβπ), 0) β β) |
120 | | breq1 4006 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π β€ π β π β€ π)) |
121 | 120, 104 | ifbieq1d 3556 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β if(π β€ π, (πΊβπ), 0) = if(π β€ π, (πΊβπ), 0)) |
122 | 121, 38 | fvmptg 5592 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ if(π β€ π, (πΊβπ), 0) β β) β ((π β β β¦ if(π β€ π, (πΊβπ), 0))βπ) = if(π β€ π, (πΊβπ), 0)) |
123 | 111, 119,
122 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...π)) β ((π β β β¦ if(π β€ π, (πΊβπ), 0))βπ) = if(π β€ π, (πΊβπ), 0)) |
124 | 123, 114 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β ((π β β β¦ if(π β€ π, (πΊβπ), 0))βπ) = (πΊβπ)) |
125 | 113 | iftrued 3541 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β if(π β€ π, β¦π / πβ¦πΆ, 0) = β¦π / πβ¦πΆ) |
126 | 95 | ffvelcdmda 5651 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (1...π)) β (πΉβπ) β π΄) |
127 | 10 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (1...π)) β§ π = (πΉβπ)) β π΅ = πΆ) |
128 | 126, 127 | csbied 3103 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (1...π)) β β¦(πΉβπ) / πβ¦π΅ = πΆ) |
129 | 50 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (1...π)) β βπ β π΄ π΅ β β) |
130 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²πβ¦(πΉβπ) / πβ¦π΅ |
131 | 130 | nfel1 2330 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²πβ¦(πΉβπ) / πβ¦π΅ β β |
132 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πΉβπ) β π΅ = β¦(πΉβπ) / πβ¦π΅) |
133 | 132 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (πΉβπ) β (π΅ β β β β¦(πΉβπ) / πβ¦π΅ β β)) |
134 | 131, 133 | rspc 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΉβπ) β π΄ β (βπ β π΄ π΅ β β β β¦(πΉβπ) / πβ¦π΅ β β)) |
135 | 126, 129,
134 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (1...π)) β β¦(πΉβπ) / πβ¦π΅ β β) |
136 | 128, 135 | eqeltrrd 2255 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (1...π)) β πΆ β β) |
137 | 136 | ralrimiva 2550 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β βπ β (1...π)πΆ β β) |
138 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π πΆ β β |
139 | 102 | nfel1 2330 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²πβ¦π / πβ¦πΆ β β |
140 | 105 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (πΆ β β β β¦π / πβ¦πΆ β β)) |
141 | 138, 139,
140 | cbvral 2699 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ β
(1...π)πΆ β β β βπ β (1...π)β¦π / πβ¦πΆ β β) |
142 | 137, 141 | sylib 122 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βπ β (1...π)β¦π / πβ¦πΆ β β) |
143 | 142 | r19.21bi 2565 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β β¦π / πβ¦πΆ β β) |
144 | 125, 143 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β if(π β€ π, β¦π / πβ¦πΆ, 0) β β) |
145 | | nfcv 2319 |
. . . . . . . . . . . . . . . . . 18
β’
β²ππ |
146 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π π β€ π |
147 | | nfcv 2319 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π0 |
148 | 146, 102,
147 | nfif 3562 |
. . . . . . . . . . . . . . . . . 18
β’
β²πif(π β€ π, β¦π / πβ¦πΆ, 0) |
149 | 120, 105 | ifbieq1d 3556 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β if(π β€ π, πΆ, 0) = if(π β€ π, β¦π / πβ¦πΆ, 0)) |
150 | | eqid 2177 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β¦ if(π β€ π, πΆ, 0)) = (π β β β¦ if(π β€ π, πΆ, 0)) |
151 | 145, 148,
149, 150 | fvmptf 5608 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ if(π β€ π, β¦π / πβ¦πΆ, 0) β β) β ((π β β β¦ if(π β€ π, πΆ, 0))βπ) = if(π β€ π, β¦π / πβ¦πΆ, 0)) |
152 | 111, 144,
151 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...π)) β ((π β β β¦ if(π β€ π, πΆ, 0))βπ) = if(π β€ π, β¦π / πβ¦πΆ, 0)) |
153 | 152, 125 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β ((π β β β¦ if(π β€ π, πΆ, 0))βπ) = β¦π / πβ¦πΆ) |
154 | 109, 124,
153 | 3eqtr4d 2220 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β ((π β β β¦ if(π β€ π, (πΊβπ), 0))βπ) = ((π β β β¦ if(π β€ π, πΆ, 0))βπ)) |
155 | 137 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β βπ β (1...π)πΆ β β) |
156 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²πβ¦π₯ / πβ¦πΆ |
157 | 156 | nfel1 2330 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πβ¦π₯ / πβ¦πΆ β β |
158 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π₯ β πΆ = β¦π₯ / πβ¦πΆ) |
159 | 158 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π₯ β (πΆ β β β β¦π₯ / πβ¦πΆ β β)) |
160 | 157, 159 | rspc 2835 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (1...π) β (βπ β (1...π)πΆ β β β β¦π₯ / πβ¦πΆ β β)) |
161 | 28, 155, 160 | sylc 62 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (β€β₯β1))
β§ π₯ β€ π) β β¦π₯ / πβ¦πΆ β β) |
162 | 161, 30, 34 | ifcldadc 3563 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (β€β₯β1))
β if(π₯ β€ π, β¦π₯ / πβ¦πΆ, 0) β β) |
163 | | nfcv 2319 |
. . . . . . . . . . . . . . . . 17
β’
β²ππ₯ |
164 | | nfv 1528 |
. . . . . . . . . . . . . . . . . 18
β’
β²π π₯ β€ π |
165 | 164, 156,
147 | nfif 3562 |
. . . . . . . . . . . . . . . . 17
β’
β²πif(π₯ β€ π, β¦π₯ / πβ¦πΆ, 0) |
166 | 36, 158 | ifbieq1d 3556 |
. . . . . . . . . . . . . . . . 17
β’ (π = π₯ β if(π β€ π, πΆ, 0) = if(π₯ β€ π, β¦π₯ / πβ¦πΆ, 0)) |
167 | 163, 165,
166, 150 | fvmptf 5608 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ if(π₯ β€ π, β¦π₯ / πβ¦πΆ, 0) β β) β ((π β β β¦ if(π β€ π, πΆ, 0))βπ₯) = if(π₯ β€ π, β¦π₯ / πβ¦πΆ, 0)) |
168 | 7, 162, 167 | syl2anc 411 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (β€β₯β1))
β ((π β β
β¦ if(π β€ π, πΆ, 0))βπ₯) = if(π₯ β€ π, β¦π₯ / πβ¦πΆ, 0)) |
169 | 168, 162 | eqeltrd 2254 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (β€β₯β1))
β ((π β β
β¦ if(π β€ π, πΆ, 0))βπ₯) β β) |
170 | | addcl 7935 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
171 | 170 | adantl 277 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ + π¦) β β) |
172 | 99, 154, 41, 169, 171 | seq3fveq 10470 |
. . . . . . . . . . . . 13
β’ (π β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, πΆ, 0)))βπ)) |
173 | 12, 172 | jca 306 |
. . . . . . . . . . . 12
β’ (π β (πΉ:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, πΆ, 0)))βπ))) |
174 | | f1oeq1 5449 |
. . . . . . . . . . . . . 14
β’ (π = πΉ β (π:(1...π)β1-1-ontoβπ΄ β πΉ:(1...π)β1-1-ontoβπ΄)) |
175 | | fveq1 5514 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = πΉ β (πβπ) = (πΉβπ)) |
176 | 175 | csbeq1d 3064 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = πΉ β β¦(πβπ) / πβ¦π΅ = β¦(πΉβπ) / πβ¦π΅) |
177 | | vex 2740 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π β V |
178 | | vex 2740 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π β V |
179 | 177, 178 | fvex 5535 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πβπ) β V |
180 | 175, 179 | eqeltrrdi 2269 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = πΉ β (πΉβπ) β V) |
181 | 10 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π = πΉ β§ π = (πΉβπ)) β π΅ = πΆ) |
182 | 180, 181 | csbied 3103 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = πΉ β β¦(πΉβπ) / πβ¦π΅ = πΆ) |
183 | 176, 182 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = πΉ β β¦(πβπ) / πβ¦π΅ = πΆ) |
184 | 183 | ifeq1d 3551 |
. . . . . . . . . . . . . . . . . 18
β’ (π = πΉ β if(π β€ π, β¦(πβπ) / πβ¦π΅, 0) = if(π β€ π, πΆ, 0)) |
185 | 184 | mpteq2dv 4094 |
. . . . . . . . . . . . . . . . 17
β’ (π = πΉ β (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)) = (π β β β¦ if(π β€ π, πΆ, 0))) |
186 | 185 | seqeq3d 10452 |
. . . . . . . . . . . . . . . 16
β’ (π = πΉ β seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0))) = seq1( + , (π β β β¦ if(π β€ π, πΆ, 0)))) |
187 | 186 | fveq1d 5517 |
. . . . . . . . . . . . . . 15
β’ (π = πΉ β (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, πΆ, 0)))βπ)) |
188 | 187 | eqeq2d 2189 |
. . . . . . . . . . . . . 14
β’ (π = πΉ β ((seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ) β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, πΆ, 0)))βπ))) |
189 | 174, 188 | anbi12d 473 |
. . . . . . . . . . . . 13
β’ (π = πΉ β ((π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)) β (πΉ:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, πΆ, 0)))βπ)))) |
190 | 189 | spcegv 2825 |
. . . . . . . . . . . 12
β’ (πΉ β V β ((πΉ:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, πΆ, 0)))βπ)) β βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
191 | 98, 173, 190 | sylc 62 |
. . . . . . . . . . 11
β’ (π β βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) |
192 | | oveq2 5882 |
. . . . . . . . . . . . . . 15
β’ (π = π β (1...π) = (1...π)) |
193 | | f1oeq2 5450 |
. . . . . . . . . . . . . . 15
β’
((1...π) =
(1...π) β (π:(1...π)β1-1-ontoβπ΄ β π:(1...π)β1-1-ontoβπ΄)) |
194 | 192, 193 | syl 14 |
. . . . . . . . . . . . . 14
β’ (π = π β (π:(1...π)β1-1-ontoβπ΄ β π:(1...π)β1-1-ontoβπ΄)) |
195 | | breq2 4007 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π β€ π β π β€ π)) |
196 | 195 | ifbid 3555 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β if(π β€ π, β¦(πβπ) / πβ¦π΅, 0) = if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)) |
197 | 196 | mpteq2dv 4094 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)) = (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0))) |
198 | 197 | seqeq3d 10452 |
. . . . . . . . . . . . . . . 16
β’ (π = π β seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0))) = seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))) |
199 | | id 19 |
. . . . . . . . . . . . . . . 16
β’ (π = π β π = π) |
200 | 198, 199 | fveq12d 5522 |
. . . . . . . . . . . . . . 15
β’ (π = π β (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)) |
201 | 200 | eqeq2d 2189 |
. . . . . . . . . . . . . 14
β’ (π = π β ((seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ) β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) |
202 | 194, 201 | anbi12d 473 |
. . . . . . . . . . . . 13
β’ (π = π β ((π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)) β (π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
203 | 202 | exbidv 1825 |
. . . . . . . . . . . 12
β’ (π = π β (βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)) β βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
204 | 203 | rspcev 2841 |
. . . . . . . . . . 11
β’ ((π β β β§
βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) β βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) |
205 | 11, 191, 204 | syl2anc 411 |
. . . . . . . . . 10
β’ (π β βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) |
206 | 205 | olcd 734 |
. . . . . . . . 9
β’ (π β (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ)) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
207 | 206 | adantr 276 |
. . . . . . . 8
β’ ((π β§ (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) β (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ)) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
208 | | breq2 4007 |
. . . . . . . . . . . 12
β’ (π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β (seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯ β seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ))) |
209 | 208 | 3anbi3d 1318 |
. . . . . . . . . . 11
β’ (π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β ((π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ)))) |
210 | 209 | rexbidv 2478 |
. . . . . . . . . 10
β’ (π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ)))) |
211 | | eqeq1 2184 |
. . . . . . . . . . . . 13
β’ (π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β (π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ) β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) |
212 | 211 | anbi2d 464 |
. . . . . . . . . . . 12
β’ (π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β ((π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)) β (π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
213 | 212 | exbidv 1825 |
. . . . . . . . . . 11
β’ (π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β (βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)) β βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
214 | 213 | rexbidv 2478 |
. . . . . . . . . 10
β’ (π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β (βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)) β βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) |
215 | 210, 214 | orbi12d 793 |
. . . . . . . . 9
β’ (π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β ((βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) β (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ)) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))))) |
216 | 215 | moi2 2918 |
. . . . . . . 8
β’ ((((seq1(
+ , (π β β
β¦ if(π β€ π, (πΊβπ), 0)))βπ) β β β§ β*π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) β§ ((βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) β§ (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ)) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))))) β π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ)) |
217 | 45, 92, 93, 207, 216 | syl22anc 1239 |
. . . . . . 7
β’ ((π β§ (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) β π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ)) |
218 | 217 | ex 115 |
. . . . . 6
β’ (π β ((βπ β β€ (π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) β π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ))) |
219 | 206, 215 | syl5ibrcom 157 |
. . . . . 6
β’ (π β (π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β (βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))))) |
220 | 218, 219 | impbid 129 |
. . . . 5
β’ (π β ((βπ β β€ (π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) β π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ))) |
221 | 220 | adantr 276 |
. . . 4
β’ ((π β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β β) β ((βπ β β€ (π΄ β
(β€β₯βπ) β§ βπ β (β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ))) β π₯ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ))) |
222 | 221 | iota5 5198 |
. . 3
β’ ((π β§ (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ) β β) β (β©π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ)) |
223 | 44, 222 | mpdan 421 |
. 2
β’ (π β (β©π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ βπ β
(β€β₯βπ)DECID π β π΄ β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ if(π β€ π, β¦(πβπ) / πβ¦π΅, 0)))βπ)))) = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ)) |
224 | 1, 223 | eqtrid 2222 |
1
β’ (π β Ξ£π β π΄ π΅ = (seq1( + , (π β β β¦ if(π β€ π, (πΊβπ), 0)))βπ)) |