Step | Hyp | Ref
| Expression |
1 | | fveq2 6892 |
. . . . 5
β’ (π¦ = π΄ β (ββπ¦) = (ββπ΄)) |
2 | 1 | eleq1d 2819 |
. . . 4
β’ (π¦ = π΄ β ((ββπ¦) β β β (ββπ΄) β
β)) |
3 | 2 | ifbid 4552 |
. . 3
β’ (π¦ = π΄ β if((ββπ¦) β β, 1, 0) =
if((ββπ΄) β
β, 1, 0)) |
4 | | fveq2 6892 |
. . 3
β’ (π¦ = π΄ β (πΉβπ¦) = (πΉβπ΄)) |
5 | 3, 4 | breq12d 5162 |
. 2
β’ (π¦ = π΄ β (if((ββπ¦) β β, 1, 0) β€
(πΉβπ¦) β if((ββπ΄) β β, 1, 0) β€ (πΉβπ΄))) |
6 | | dchrisum0flb.a |
. . 3
β’ (π β π΄ β β) |
7 | | oveq2 7417 |
. . . . . 6
β’ (π = 1 β (1...π) = (1...1)) |
8 | 7 | raleqdv 3326 |
. . . . 5
β’ (π = 1 β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β βπ¦ β (1...1)if((ββπ¦) β β, 1, 0) β€
(πΉβπ¦))) |
9 | 8 | imbi2d 341 |
. . . 4
β’ (π = 1 β ((π β βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)) β (π β βπ¦ β (1...1)if((ββπ¦) β β, 1, 0) β€
(πΉβπ¦)))) |
10 | | oveq2 7417 |
. . . . . 6
β’ (π = π β (1...π) = (1...π)) |
11 | 10 | raleqdv 3326 |
. . . . 5
β’ (π = π β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) |
12 | 11 | imbi2d 341 |
. . . 4
β’ (π = π β ((π β βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)) β (π β βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)))) |
13 | | oveq2 7417 |
. . . . . 6
β’ (π = (π + 1) β (1...π) = (1...(π + 1))) |
14 | 13 | raleqdv 3326 |
. . . . 5
β’ (π = (π + 1) β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β βπ¦ β (1...(π + 1))if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) |
15 | 14 | imbi2d 341 |
. . . 4
β’ (π = (π + 1) β ((π β βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)) β (π β βπ¦ β (1...(π + 1))if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)))) |
16 | | oveq2 7417 |
. . . . . 6
β’ (π = π΄ β (1...π) = (1...π΄)) |
17 | 16 | raleqdv 3326 |
. . . . 5
β’ (π = π΄ β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β βπ¦ β (1...π΄)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) |
18 | 17 | imbi2d 341 |
. . . 4
β’ (π = π΄ β ((π β βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)) β (π β βπ¦ β (1...π΄)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)))) |
19 | | rpvmasum.z |
. . . . . 6
β’ π =
(β€/nβ€βπ) |
20 | | rpvmasum.l |
. . . . . 6
β’ πΏ = (β€RHomβπ) |
21 | | rpvmasum.a |
. . . . . 6
β’ (π β π β β) |
22 | | rpvmasum2.g |
. . . . . 6
β’ πΊ = (DChrβπ) |
23 | | rpvmasum2.d |
. . . . . 6
β’ π· = (BaseβπΊ) |
24 | | rpvmasum2.1 |
. . . . . 6
β’ 1 =
(0gβπΊ) |
25 | | dchrisum0f.f |
. . . . . 6
β’ πΉ = (π β β β¦ Ξ£π£ β {π β β β£ π β₯ π} (πβ(πΏβπ£))) |
26 | | dchrisum0f.x |
. . . . . 6
β’ (π β π β π·) |
27 | | dchrisum0flb.r |
. . . . . 6
β’ (π β π:(Baseβπ)βΆβ) |
28 | | 2prm 16629 |
. . . . . . 7
β’ 2 β
β |
29 | 28 | a1i 11 |
. . . . . 6
β’ (π β 2 β
β) |
30 | | 0nn0 12487 |
. . . . . . 7
β’ 0 β
β0 |
31 | 30 | a1i 11 |
. . . . . 6
β’ (π β 0 β
β0) |
32 | 19, 20, 21, 22, 23, 24, 25, 26, 27, 29, 31 | dchrisum0flblem1 27011 |
. . . . 5
β’ (π β
if((ββ(2β0)) β β, 1, 0) β€ (πΉβ(2β0))) |
33 | | elfz1eq 13512 |
. . . . . . . . . . . 12
β’ (π¦ β (1...1) β π¦ = 1) |
34 | | 2nn0 12489 |
. . . . . . . . . . . . 13
β’ 2 β
β0 |
35 | 34 | numexp0 17009 |
. . . . . . . . . . . 12
β’
(2β0) = 1 |
36 | 33, 35 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π¦ β (1...1) β π¦ = (2β0)) |
37 | 36 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π¦ β (1...1) β
(ββπ¦) =
(ββ(2β0))) |
38 | 37 | eleq1d 2819 |
. . . . . . . . 9
β’ (π¦ β (1...1) β
((ββπ¦) β
β β (ββ(2β0)) β β)) |
39 | 38 | ifbid 4552 |
. . . . . . . 8
β’ (π¦ β (1...1) β
if((ββπ¦) β
β, 1, 0) = if((ββ(2β0)) β β, 1,
0)) |
40 | 36 | fveq2d 6896 |
. . . . . . . 8
β’ (π¦ β (1...1) β (πΉβπ¦) = (πΉβ(2β0))) |
41 | 39, 40 | breq12d 5162 |
. . . . . . 7
β’ (π¦ β (1...1) β
(if((ββπ¦)
β β, 1, 0) β€ (πΉβπ¦) β if((ββ(2β0)) β
β, 1, 0) β€ (πΉβ(2β0)))) |
42 | 41 | biimprcd 249 |
. . . . . 6
β’
(if((ββ(2β0)) β β, 1, 0) β€ (πΉβ(2β0)) β (π¦ β (1...1) β
if((ββπ¦) β
β, 1, 0) β€ (πΉβπ¦))) |
43 | 42 | ralrimiv 3146 |
. . . . 5
β’
(if((ββ(2β0)) β β, 1, 0) β€ (πΉβ(2β0)) β
βπ¦ β
(1...1)if((ββπ¦)
β β, 1, 0) β€ (πΉβπ¦)) |
44 | 32, 43 | syl 17 |
. . . 4
β’ (π β βπ¦ β (1...1)if((ββπ¦) β β, 1, 0) β€
(πΉβπ¦)) |
45 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π β β) |
46 | | nnuz 12865 |
. . . . . . . . . . . . . . . 16
β’ β =
(β€β₯β1) |
47 | 45, 46 | eleqtrdi 2844 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
48 | 47 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β π β
(β€β₯β1)) |
49 | | eluzp1p1 12850 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β1) β (π + 1) β (β€β₯β(1
+ 1))) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β (π + 1) β (β€β₯β(1
+ 1))) |
51 | | df-2 12275 |
. . . . . . . . . . . . . 14
β’ 2 = (1 +
1) |
52 | 51 | fveq2i 6895 |
. . . . . . . . . . . . 13
β’
(β€β₯β2) = (β€β₯β(1 +
1)) |
53 | 50, 52 | eleqtrrdi 2845 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β (π + 1) β
(β€β₯β2)) |
54 | | exprmfct 16641 |
. . . . . . . . . . . 12
β’ ((π + 1) β
(β€β₯β2) β βπ β β π β₯ (π + 1)) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β βπ β β π β₯ (π + 1)) |
56 | 21 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β π β β) |
57 | 26 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β π β π·) |
58 | 27 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β π:(Baseβπ)βΆβ) |
59 | 53 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β (π + 1) β
(β€β₯β2)) |
60 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β π β β) |
61 | | simprr 772 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β π β₯ (π + 1)) |
62 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)) |
63 | | simplrl 776 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β π β β) |
64 | 63 | nnzd 12585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β π β β€) |
65 | | fzval3 13701 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β
(1...π) = (1..^(π + 1))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β (1...π) = (1..^(π + 1))) |
67 | 66 | raleqdv 3326 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β βπ¦ β (1..^(π + 1))if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) |
68 | 62, 67 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β βπ¦ β (1..^(π + 1))if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)) |
69 | 19, 20, 56, 22, 23, 24, 25, 57, 58, 59, 60, 61, 68 | dchrisum0flblem2 27012 |
. . . . . . . . . . 11
β’ (((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β§ (π β β β§ π β₯ (π + 1))) β if((ββ(π + 1)) β β, 1, 0)
β€ (πΉβ(π + 1))) |
70 | 55, 69 | rexlimddv 3162 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β if((ββ(π + 1)) β β, 1, 0)
β€ (πΉβ(π + 1))) |
71 | | ovex 7442 |
. . . . . . . . . . 11
β’ (π + 1) β V |
72 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π + 1) β (ββπ¦) = (ββ(π + 1))) |
73 | 72 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (π¦ = (π + 1) β ((ββπ¦) β β β
(ββ(π + 1))
β β)) |
74 | 73 | ifbid 4552 |
. . . . . . . . . . . 12
β’ (π¦ = (π + 1) β if((ββπ¦) β β, 1, 0) =
if((ββ(π + 1))
β β, 1, 0)) |
75 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π¦ = (π + 1) β (πΉβπ¦) = (πΉβ(π + 1))) |
76 | 74, 75 | breq12d 5162 |
. . . . . . . . . . 11
β’ (π¦ = (π + 1) β (if((ββπ¦) β β, 1, 0) β€
(πΉβπ¦) β if((ββ(π + 1)) β β, 1, 0)
β€ (πΉβ(π + 1)))) |
77 | 71, 76 | ralsn 4686 |
. . . . . . . . . 10
β’
(βπ¦ β
{(π +
1)}if((ββπ¦)
β β, 1, 0) β€ (πΉβπ¦) β if((ββ(π + 1)) β β, 1, 0)
β€ (πΉβ(π + 1))) |
78 | 70, 77 | sylibr 233 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) β βπ¦ β {(π + 1)}if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)) |
79 | 78 | expr 458 |
. . . . . . . 8
β’ ((π β§ π β β) β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β βπ¦ β {(π + 1)}if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) |
80 | 79 | ancld 552 |
. . . . . . 7
β’ ((π β§ π β β) β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β§ βπ¦ β {(π + 1)}if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)))) |
81 | | fzsuc 13548 |
. . . . . . . . . 10
β’ (π β
(β€β₯β1) β (1...(π + 1)) = ((1...π) βͺ {(π + 1)})) |
82 | 47, 81 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β (1...(π + 1)) = ((1...π) βͺ {(π + 1)})) |
83 | 82 | raleqdv 3326 |
. . . . . . . 8
β’ ((π β§ π β β) β (βπ¦ β (1...(π + 1))if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β βπ¦ β ((1...π) βͺ {(π + 1)})if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) |
84 | | ralunb 4192 |
. . . . . . . 8
β’
(βπ¦ β
((1...π) βͺ {(π + 1)})if((ββπ¦) β β, 1, 0) β€
(πΉβπ¦) β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β§ βπ¦ β {(π + 1)}if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) |
85 | 83, 84 | bitrdi 287 |
. . . . . . 7
β’ ((π β§ π β β) β (βπ¦ β (1...(π + 1))if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β§ βπ¦ β {(π + 1)}if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)))) |
86 | 80, 85 | sylibrd 259 |
. . . . . 6
β’ ((π β§ π β β) β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β βπ¦ β (1...(π + 1))if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) |
87 | 86 | expcom 415 |
. . . . 5
β’ (π β β β (π β (βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦) β βπ¦ β (1...(π + 1))if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)))) |
88 | 87 | a2d 29 |
. . . 4
β’ (π β β β ((π β βπ¦ β (1...π)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)) β (π β βπ¦ β (1...(π + 1))if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)))) |
89 | 9, 12, 15, 18, 44, 88 | nnind 12230 |
. . 3
β’ (π΄ β β β (π β βπ¦ β (1...π΄)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦))) |
90 | 6, 89 | mpcom 38 |
. 2
β’ (π β βπ¦ β (1...π΄)if((ββπ¦) β β, 1, 0) β€ (πΉβπ¦)) |
91 | 6, 46 | eleqtrdi 2844 |
. . 3
β’ (π β π΄ β
(β€β₯β1)) |
92 | | eluzfz2 13509 |
. . 3
β’ (π΄ β
(β€β₯β1) β π΄ β (1...π΄)) |
93 | 91, 92 | syl 17 |
. 2
β’ (π β π΄ β (1...π΄)) |
94 | 5, 90, 93 | rspcdva 3614 |
1
β’ (π β if((ββπ΄) β β, 1, 0) β€
(πΉβπ΄)) |