Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
β’ ((π β§ π) β π) |
2 | | rpnnen2.6 |
. . . 4
β’ (π β Ξ£π β β ((πΉβπ΄)βπ) = Ξ£π β β ((πΉβπ΅)βπ)) |
3 | 1, 2 | sylib 217 |
. . 3
β’ ((π β§ π) β Ξ£π β β ((πΉβπ΄)βπ) = Ξ£π β β ((πΉβπ΅)βπ)) |
4 | | rpnnen2.2 |
. . . . . 6
β’ (π β π΄ β β) |
5 | | rpnnen2.4 |
. . . . . . 7
β’ (π β π β (π΄ β π΅)) |
6 | | eldifi 4091 |
. . . . . . . 8
β’ (π β (π΄ β π΅) β π β π΄) |
7 | | ssel2 3944 |
. . . . . . . 8
β’ ((π΄ β β β§ π β π΄) β π β β) |
8 | 6, 7 | sylan2 594 |
. . . . . . 7
β’ ((π΄ β β β§ π β (π΄ β π΅)) β π β β) |
9 | 4, 5, 8 | syl2anc 585 |
. . . . . 6
β’ (π β π β β) |
10 | | rpnnen2.1 |
. . . . . . 7
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) |
11 | 10 | rpnnen2lem8 16110 |
. . . . . 6
β’ ((π΄ β β β§ π β β) β
Ξ£π β β
((πΉβπ΄)βπ) = (Ξ£π β (1...(π β 1))((πΉβπ΄)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ))) |
12 | 4, 9, 11 | syl2anc 585 |
. . . . 5
β’ (π β Ξ£π β β ((πΉβπ΄)βπ) = (Ξ£π β (1...(π β 1))((πΉβπ΄)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ))) |
13 | | 1z 12540 |
. . . . . . . . . . . . . 14
β’ 1 β
β€ |
14 | | nnz 12527 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β€) |
15 | | elfzm11 13519 |
. . . . . . . . . . . . . 14
β’ ((1
β β€ β§ π
β β€) β (π
β (1...(π β 1))
β (π β β€
β§ 1 β€ π β§ π < π))) |
16 | 13, 14, 15 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (π β β β (π β (1...(π β 1)) β (π β β€ β§ 1 β€ π β§ π < π))) |
17 | 16 | biimpa 478 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β (1...(π β 1))) β (π β β€ β§ 1 β€ π β§ π < π)) |
18 | 9, 17 | sylan 581 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...(π β 1))) β (π β β€ β§ 1 β€ π β§ π < π)) |
19 | 18 | simp3d 1145 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(π β 1))) β π < π) |
20 | | rpnnen2.5 |
. . . . . . . . . . 11
β’ (π β βπ β β (π < π β (π β π΄ β π β π΅))) |
21 | | elfznn 13477 |
. . . . . . . . . . 11
β’ (π β (1...(π β 1)) β π β β) |
22 | | breq1 5113 |
. . . . . . . . . . . . 13
β’ (π = π β (π < π β π < π)) |
23 | | eleq1w 2821 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π΄ β π β π΄)) |
24 | | eleq1w 2821 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π΅ β π β π΅)) |
25 | 23, 24 | bibi12d 346 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β π΄ β π β π΅) β (π β π΄ β π β π΅))) |
26 | 22, 25 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = π β ((π < π β (π β π΄ β π β π΅)) β (π < π β (π β π΄ β π β π΅)))) |
27 | 26 | rspccva 3583 |
. . . . . . . . . . 11
β’
((βπ β
β (π < π β (π β π΄ β π β π΅)) β§ π β β) β (π < π β (π β π΄ β π β π΅))) |
28 | 20, 21, 27 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(π β 1))) β (π < π β (π β π΄ β π β π΅))) |
29 | 19, 28 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ π β (1...(π β 1))) β (π β π΄ β π β π΅)) |
30 | 29 | ifbid 4514 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β if(π β π΄, ((1 / 3)βπ), 0) = if(π β π΅, ((1 / 3)βπ), 0)) |
31 | 10 | rpnnen2lem1 16103 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β) β ((πΉβπ΄)βπ) = if(π β π΄, ((1 / 3)βπ), 0)) |
32 | 4, 21, 31 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β ((πΉβπ΄)βπ) = if(π β π΄, ((1 / 3)βπ), 0)) |
33 | | rpnnen2.3 |
. . . . . . . . 9
β’ (π β π΅ β β) |
34 | 10 | rpnnen2lem1 16103 |
. . . . . . . . 9
β’ ((π΅ β β β§ π β β) β ((πΉβπ΅)βπ) = if(π β π΅, ((1 / 3)βπ), 0)) |
35 | 33, 21, 34 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β ((πΉβπ΅)βπ) = if(π β π΅, ((1 / 3)βπ), 0)) |
36 | 30, 32, 35 | 3eqtr4d 2787 |
. . . . . . 7
β’ ((π β§ π β (1...(π β 1))) β ((πΉβπ΄)βπ) = ((πΉβπ΅)βπ)) |
37 | 36 | sumeq2dv 15595 |
. . . . . 6
β’ (π β Ξ£π β (1...(π β 1))((πΉβπ΄)βπ) = Ξ£π β (1...(π β 1))((πΉβπ΅)βπ)) |
38 | 37 | oveq1d 7377 |
. . . . 5
β’ (π β (Ξ£π β (1...(π β 1))((πΉβπ΄)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ)) = (Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ))) |
39 | 12, 38 | eqtrd 2777 |
. . . 4
β’ (π β Ξ£π β β ((πΉβπ΄)βπ) = (Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ))) |
40 | 39 | adantr 482 |
. . 3
β’ ((π β§ π) β Ξ£π β β ((πΉβπ΄)βπ) = (Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ))) |
41 | 10 | rpnnen2lem8 16110 |
. . . . 5
β’ ((π΅ β β β§ π β β) β
Ξ£π β β
((πΉβπ΅)βπ) = (Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ))) |
42 | 33, 9, 41 | syl2anc 585 |
. . . 4
β’ (π β Ξ£π β β ((πΉβπ΅)βπ) = (Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ))) |
43 | 42 | adantr 482 |
. . 3
β’ ((π β§ π) β Ξ£π β β ((πΉβπ΅)βπ) = (Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ))) |
44 | 3, 40, 43 | 3eqtr3d 2785 |
. 2
β’ ((π β§ π) β (Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ)) = (Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ))) |
45 | 10 | rpnnen2lem6 16108 |
. . . . 5
β’ ((π΄ β β β§ π β β) β
Ξ£π β
(β€β₯βπ)((πΉβπ΄)βπ) β β) |
46 | 4, 9, 45 | syl2anc 585 |
. . . 4
β’ (π β Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ) β β) |
47 | 10 | rpnnen2lem6 16108 |
. . . . 5
β’ ((π΅ β β β§ π β β) β
Ξ£π β
(β€β₯βπ)((πΉβπ΅)βπ) β β) |
48 | 33, 9, 47 | syl2anc 585 |
. . . 4
β’ (π β Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ) β β) |
49 | | fzfid 13885 |
. . . . 5
β’ (π β (1...(π β 1)) β Fin) |
50 | 10 | rpnnen2lem2 16104 |
. . . . . . 7
β’ (π΅ β β β (πΉβπ΅):ββΆβ) |
51 | 33, 50 | syl 17 |
. . . . . 6
β’ (π β (πΉβπ΅):ββΆβ) |
52 | | ffvelcdm 7037 |
. . . . . 6
β’ (((πΉβπ΅):ββΆβ β§ π β β) β ((πΉβπ΅)βπ) β β) |
53 | 51, 21, 52 | syl2an 597 |
. . . . 5
β’ ((π β§ π β (1...(π β 1))) β ((πΉβπ΅)βπ) β β) |
54 | 49, 53 | fsumrecl 15626 |
. . . 4
β’ (π β Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) β β) |
55 | | readdcan 11336 |
. . . 4
β’
((Ξ£π β
(β€β₯βπ)((πΉβπ΄)βπ) β β β§ Ξ£π β
(β€β₯βπ)((πΉβπ΅)βπ) β β β§ Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) β β) β ((Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ)) = (Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ)) β Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ) = Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ))) |
56 | 46, 48, 54, 55 | syl3anc 1372 |
. . 3
β’ (π β ((Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ)) = (Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ)) β Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ) = Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ))) |
57 | 56 | adantr 482 |
. 2
β’ ((π β§ π) β ((Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ)) = (Ξ£π β (1...(π β 1))((πΉβπ΅)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ)) β Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ) = Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ))) |
58 | 44, 57 | mpbid 231 |
1
β’ ((π β§ π) β Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ) = Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ)) |