Step | Hyp | Ref
| Expression |
1 | | eluzelre 12779 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β β) |
2 | | chtval 26475 |
. . . . 5
β’ (π β β β
(ΞΈβπ) =
Ξ£π β ((0[,]π) β© β)(logβπ)) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β
(β€β₯βπ) β (ΞΈβπ) = Ξ£π β ((0[,]π) β© β)(logβπ)) |
4 | | eluzel2 12773 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β π β β€) |
5 | | 2z 12540 |
. . . . . . . . . 10
β’ 2 β
β€ |
6 | | ifcl 4532 |
. . . . . . . . . 10
β’ ((π β β€ β§ 2 β
β€) β if(π β€
2, π, 2) β
β€) |
7 | 4, 5, 6 | sylancl 587 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β if(π β€ 2, π, 2) β β€) |
8 | 5 | a1i 11 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β 2 β β€) |
9 | 4 | zred 12612 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β π β β) |
10 | | 2re 12232 |
. . . . . . . . . 10
β’ 2 β
β |
11 | | min2 13115 |
. . . . . . . . . 10
β’ ((π β β β§ 2 β
β) β if(π β€
2, π, 2) β€
2) |
12 | 9, 10, 11 | sylancl 587 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β if(π β€ 2, π, 2) β€ 2) |
13 | | eluz2 12774 |
. . . . . . . . 9
β’ (2 β
(β€β₯βif(π β€ 2, π, 2)) β (if(π β€ 2, π, 2) β β€ β§ 2 β β€
β§ if(π β€ 2, π, 2) β€ 2)) |
14 | 7, 8, 12, 13 | syl3anbrc 1344 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β 2 β
(β€β₯βif(π β€ 2, π, 2))) |
15 | | ppisval2 26470 |
. . . . . . . 8
β’ ((π β β β§ 2 β
(β€β₯βif(π β€ 2, π, 2))) β ((0[,]π) β© β) = ((if(π β€ 2, π, 2)...(ββπ)) β© β)) |
16 | 1, 14, 15 | syl2anc 585 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β ((0[,]π) β© β) = ((if(π β€ 2, π, 2)...(ββπ)) β© β)) |
17 | | eluzelz 12778 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β π β β€) |
18 | | flid 13719 |
. . . . . . . . . 10
β’ (π β β€ β
(ββπ) = π) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β (ββπ) = π) |
20 | 19 | oveq2d 7374 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β (if(π β€ 2, π, 2)...(ββπ)) = (if(π β€ 2, π, 2)...π)) |
21 | 20 | ineq1d 4172 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β ((if(π β€ 2, π, 2)...(ββπ)) β© β) = ((if(π β€ 2, π, 2)...π) β© β)) |
22 | 16, 21 | eqtrd 2773 |
. . . . . 6
β’ (π β
(β€β₯βπ) β ((0[,]π) β© β) = ((if(π β€ 2, π, 2)...π) β© β)) |
23 | 22 | sumeq1d 15591 |
. . . . 5
β’ (π β
(β€β₯βπ) β Ξ£π β ((0[,]π) β© β)(logβπ) = Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ)) |
24 | 9 | ltp1d 12090 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β π < (π + 1)) |
25 | | fzdisj 13474 |
. . . . . . . . 9
β’ (π < (π + 1) β ((if(π β€ 2, π, 2)...π) β© ((π + 1)...π)) = β
) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β ((if(π β€ 2, π, 2)...π) β© ((π + 1)...π)) = β
) |
27 | 26 | ineq1d 4172 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β (((if(π β€ 2, π, 2)...π) β© ((π + 1)...π)) β© β) = (β
β©
β)) |
28 | | inindir 4188 |
. . . . . . 7
β’
(((if(π β€ 2,
π, 2)...π) β© ((π + 1)...π)) β© β) = (((if(π β€ 2, π, 2)...π) β© β) β© (((π + 1)...π) β© β)) |
29 | | 0in 4354 |
. . . . . . 7
β’ (β
β© β) = β
|
30 | 27, 28, 29 | 3eqtr3g 2796 |
. . . . . 6
β’ (π β
(β€β₯βπ) β (((if(π β€ 2, π, 2)...π) β© β) β© (((π + 1)...π) β© β)) =
β
) |
31 | | min1 13114 |
. . . . . . . . . . . 12
β’ ((π β β β§ 2 β
β) β if(π β€
2, π, 2) β€ π) |
32 | 9, 10, 31 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β if(π β€ 2, π, 2) β€ π) |
33 | | eluz2 12774 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βif(π β€ 2, π, 2)) β (if(π β€ 2, π, 2) β β€ β§ π β β€ β§ if(π β€ 2, π, 2) β€ π)) |
34 | 7, 4, 32, 33 | syl3anbrc 1344 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β π β
(β€β₯βif(π β€ 2, π, 2))) |
35 | | id 22 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β π β (β€β₯βπ)) |
36 | | elfzuzb 13441 |
. . . . . . . . . 10
β’ (π β (if(π β€ 2, π, 2)...π) β (π β
(β€β₯βif(π β€ 2, π, 2)) β§ π β (β€β₯βπ))) |
37 | 34, 35, 36 | sylanbrc 584 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β π β (if(π β€ 2, π, 2)...π)) |
38 | | fzsplit 13473 |
. . . . . . . . 9
β’ (π β (if(π β€ 2, π, 2)...π) β (if(π β€ 2, π, 2)...π) = ((if(π β€ 2, π, 2)...π) βͺ ((π + 1)...π))) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β (if(π β€ 2, π, 2)...π) = ((if(π β€ 2, π, 2)...π) βͺ ((π + 1)...π))) |
40 | 39 | ineq1d 4172 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β ((if(π β€ 2, π, 2)...π) β© β) = (((if(π β€ 2, π, 2)...π) βͺ ((π + 1)...π)) β© β)) |
41 | | indir 4236 |
. . . . . . 7
β’
(((if(π β€ 2,
π, 2)...π) βͺ ((π + 1)...π)) β© β) = (((if(π β€ 2, π, 2)...π) β© β) βͺ (((π + 1)...π) β© β)) |
42 | 40, 41 | eqtrdi 2789 |
. . . . . 6
β’ (π β
(β€β₯βπ) β ((if(π β€ 2, π, 2)...π) β© β) = (((if(π β€ 2, π, 2)...π) β© β) βͺ (((π + 1)...π) β© β))) |
43 | | fzfid 13884 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β (if(π β€ 2, π, 2)...π) β Fin) |
44 | | inss1 4189 |
. . . . . . 7
β’
((if(π β€ 2, π, 2)...π) β© β) β (if(π β€ 2, π, 2)...π) |
45 | | ssfi 9120 |
. . . . . . 7
β’
(((if(π β€ 2,
π, 2)...π) β Fin β§ ((if(π β€ 2, π, 2)...π) β© β) β (if(π β€ 2, π, 2)...π)) β ((if(π β€ 2, π, 2)...π) β© β) β
Fin) |
46 | 43, 44, 45 | sylancl 587 |
. . . . . 6
β’ (π β
(β€β₯βπ) β ((if(π β€ 2, π, 2)...π) β© β) β
Fin) |
47 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯βπ) β§ π β ((if(π β€ 2, π, 2)...π) β© β)) β π β ((if(π β€ 2, π, 2)...π) β© β)) |
48 | 47 | elin2d 4160 |
. . . . . . . . . 10
β’ ((π β
(β€β₯βπ) β§ π β ((if(π β€ 2, π, 2)...π) β© β)) β π β β) |
49 | | prmnn 16555 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ π β ((if(π β€ 2, π, 2)...π) β© β)) β π β β) |
51 | 50 | nnrpd 12960 |
. . . . . . . 8
β’ ((π β
(β€β₯βπ) β§ π β ((if(π β€ 2, π, 2)...π) β© β)) β π β β+) |
52 | 51 | relogcld 25994 |
. . . . . . 7
β’ ((π β
(β€β₯βπ) β§ π β ((if(π β€ 2, π, 2)...π) β© β)) β (logβπ) β
β) |
53 | 52 | recnd 11188 |
. . . . . 6
β’ ((π β
(β€β₯βπ) β§ π β ((if(π β€ 2, π, 2)...π) β© β)) β (logβπ) β
β) |
54 | 30, 42, 46, 53 | fsumsplit 15631 |
. . . . 5
β’ (π β
(β€β₯βπ) β Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ) = (Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ) + Ξ£π β (((π + 1)...π) β© β)(logβπ))) |
55 | 23, 54 | eqtrd 2773 |
. . . 4
β’ (π β
(β€β₯βπ) β Ξ£π β ((0[,]π) β© β)(logβπ) = (Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ) + Ξ£π β (((π + 1)...π) β© β)(logβπ))) |
56 | 3, 55 | eqtrd 2773 |
. . 3
β’ (π β
(β€β₯βπ) β (ΞΈβπ) = (Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ) + Ξ£π β (((π + 1)...π) β© β)(logβπ))) |
57 | | chtval 26475 |
. . . . 5
β’ (π β β β
(ΞΈβπ) =
Ξ£π β ((0[,]π) β© β)(logβπ)) |
58 | 9, 57 | syl 17 |
. . . 4
β’ (π β
(β€β₯βπ) β (ΞΈβπ) = Ξ£π β ((0[,]π) β© β)(logβπ)) |
59 | | ppisval2 26470 |
. . . . . . 7
β’ ((π β β β§ 2 β
(β€β₯βif(π β€ 2, π, 2))) β ((0[,]π) β© β) = ((if(π β€ 2, π, 2)...(ββπ)) β© β)) |
60 | 9, 14, 59 | syl2anc 585 |
. . . . . 6
β’ (π β
(β€β₯βπ) β ((0[,]π) β© β) = ((if(π β€ 2, π, 2)...(ββπ)) β© β)) |
61 | | flid 13719 |
. . . . . . . . 9
β’ (π β β€ β
(ββπ) = π) |
62 | 4, 61 | syl 17 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β (ββπ) = π) |
63 | 62 | oveq2d 7374 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β (if(π β€ 2, π, 2)...(ββπ)) = (if(π β€ 2, π, 2)...π)) |
64 | 63 | ineq1d 4172 |
. . . . . 6
β’ (π β
(β€β₯βπ) β ((if(π β€ 2, π, 2)...(ββπ)) β© β) = ((if(π β€ 2, π, 2)...π) β© β)) |
65 | 60, 64 | eqtrd 2773 |
. . . . 5
β’ (π β
(β€β₯βπ) β ((0[,]π) β© β) = ((if(π β€ 2, π, 2)...π) β© β)) |
66 | 65 | sumeq1d 15591 |
. . . 4
β’ (π β
(β€β₯βπ) β Ξ£π β ((0[,]π) β© β)(logβπ) = Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ)) |
67 | 58, 66 | eqtrd 2773 |
. . 3
β’ (π β
(β€β₯βπ) β (ΞΈβπ) = Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ)) |
68 | 56, 67 | oveq12d 7376 |
. 2
β’ (π β
(β€β₯βπ) β ((ΞΈβπ) β (ΞΈβπ)) = ((Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ) + Ξ£π β (((π + 1)...π) β© β)(logβπ)) β Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ))) |
69 | | fzfi 13883 |
. . . . . 6
β’ (if(π β€ 2, π, 2)...π) β Fin |
70 | | inss1 4189 |
. . . . . 6
β’
((if(π β€ 2, π, 2)...π) β© β) β (if(π β€ 2, π, 2)...π) |
71 | | ssfi 9120 |
. . . . . 6
β’
(((if(π β€ 2,
π, 2)...π) β Fin β§ ((if(π β€ 2, π, 2)...π) β© β) β (if(π β€ 2, π, 2)...π)) β ((if(π β€ 2, π, 2)...π) β© β) β
Fin) |
72 | 69, 70, 71 | mp2an 691 |
. . . . 5
β’
((if(π β€ 2, π, 2)...π) β© β) β Fin |
73 | 72 | a1i 11 |
. . . 4
β’ (π β
(β€β₯βπ) β ((if(π β€ 2, π, 2)...π) β© β) β
Fin) |
74 | | ssun1 4133 |
. . . . . . 7
β’
((if(π β€ 2, π, 2)...π) β© β) β (((if(π β€ 2, π, 2)...π) β© β) βͺ (((π + 1)...π) β© β)) |
75 | 74, 42 | sseqtrrid 3998 |
. . . . . 6
β’ (π β
(β€β₯βπ) β ((if(π β€ 2, π, 2)...π) β© β) β ((if(π β€ 2, π, 2)...π) β© β)) |
76 | 75 | sselda 3945 |
. . . . 5
β’ ((π β
(β€β₯βπ) β§ π β ((if(π β€ 2, π, 2)...π) β© β)) β π β ((if(π β€ 2, π, 2)...π) β© β)) |
77 | 76, 53 | syldan 592 |
. . . 4
β’ ((π β
(β€β₯βπ) β§ π β ((if(π β€ 2, π, 2)...π) β© β)) β (logβπ) β
β) |
78 | 73, 77 | fsumcl 15623 |
. . 3
β’ (π β
(β€β₯βπ) β Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ) β
β) |
79 | | fzfi 13883 |
. . . . . 6
β’ ((π + 1)...π) β Fin |
80 | | inss1 4189 |
. . . . . 6
β’ (((π + 1)...π) β© β) β ((π + 1)...π) |
81 | | ssfi 9120 |
. . . . . 6
β’ ((((π + 1)...π) β Fin β§ (((π + 1)...π) β© β) β ((π + 1)...π)) β (((π + 1)...π) β© β) β
Fin) |
82 | 79, 80, 81 | mp2an 691 |
. . . . 5
β’ (((π + 1)...π) β© β) β Fin |
83 | 82 | a1i 11 |
. . . 4
β’ (π β
(β€β₯βπ) β (((π + 1)...π) β© β) β
Fin) |
84 | | ssun2 4134 |
. . . . . . 7
β’ (((π + 1)...π) β© β) β (((if(π β€ 2, π, 2)...π) β© β) βͺ (((π + 1)...π) β© β)) |
85 | 84, 42 | sseqtrrid 3998 |
. . . . . 6
β’ (π β
(β€β₯βπ) β (((π + 1)...π) β© β) β ((if(π β€ 2, π, 2)...π) β© β)) |
86 | 85 | sselda 3945 |
. . . . 5
β’ ((π β
(β€β₯βπ) β§ π β (((π + 1)...π) β© β)) β π β ((if(π β€ 2, π, 2)...π) β© β)) |
87 | 86, 53 | syldan 592 |
. . . 4
β’ ((π β
(β€β₯βπ) β§ π β (((π + 1)...π) β© β)) β (logβπ) β
β) |
88 | 83, 87 | fsumcl 15623 |
. . 3
β’ (π β
(β€β₯βπ) β Ξ£π β (((π + 1)...π) β© β)(logβπ) β
β) |
89 | 78, 88 | pncan2d 11519 |
. 2
β’ (π β
(β€β₯βπ) β ((Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ) + Ξ£π β (((π + 1)...π) β© β)(logβπ)) β Ξ£π β ((if(π β€ 2, π, 2)...π) β© β)(logβπ)) = Ξ£π β (((π + 1)...π) β© β)(logβπ)) |
90 | 68, 89 | eqtrd 2773 |
1
β’ (π β
(β€β₯βπ) β ((ΞΈβπ) β (ΞΈβπ)) = Ξ£π β (((π + 1)...π) β© β)(logβπ)) |