Step | Hyp | Ref
| Expression |
1 | | zre 12510 |
. . 3
β’ (π β β€ β π β
β) |
2 | | chtval 26475 |
. . 3
β’ (π β β β
(ΞΈβπ) =
Ξ£π β ((0[,]π) β© β)(logβπ)) |
3 | 1, 2 | syl 17 |
. 2
β’ (π β β€ β
(ΞΈβπ) =
Ξ£π β ((0[,]π) β© β)(logβπ)) |
4 | | nnz 12527 |
. . . . . . 7
β’ (π β β β π β
β€) |
5 | | ppisval 26469 |
. . . . . . . . 9
β’ (π β β β
((0[,]π) β© β) =
((2...(ββπ))
β© β)) |
6 | 1, 5 | syl 17 |
. . . . . . . 8
β’ (π β β€ β
((0[,]π) β© β) =
((2...(ββπ))
β© β)) |
7 | | flid 13720 |
. . . . . . . . . 10
β’ (π β β€ β
(ββπ) = π) |
8 | 7 | oveq2d 7378 |
. . . . . . . . 9
β’ (π β β€ β
(2...(ββπ)) =
(2...π)) |
9 | 8 | ineq1d 4176 |
. . . . . . . 8
β’ (π β β€ β
((2...(ββπ))
β© β) = ((2...π)
β© β)) |
10 | 6, 9 | eqtrd 2777 |
. . . . . . 7
β’ (π β β€ β
((0[,]π) β© β) =
((2...π) β©
β)) |
11 | 4, 10 | syl 17 |
. . . . . 6
β’ (π β β β
((0[,]π) β© β) =
((2...π) β©
β)) |
12 | | 2nn 12233 |
. . . . . . . . . . . . 13
β’ 2 β
β |
13 | | nnuz 12813 |
. . . . . . . . . . . . 13
β’ β =
(β€β₯β1) |
14 | 12, 13 | eleqtri 2836 |
. . . . . . . . . . . 12
β’ 2 β
(β€β₯β1) |
15 | | fzss1 13487 |
. . . . . . . . . . . 12
β’ (2 β
(β€β₯β1) β (2...π) β (1...π)) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . 11
β’
(2...π) β
(1...π) |
17 | | ssdif0 4328 |
. . . . . . . . . . 11
β’
((2...π) β
(1...π) β ((2...π) β (1...π)) = β
) |
18 | 16, 17 | mpbi 229 |
. . . . . . . . . 10
β’
((2...π) β
(1...π)) =
β
|
19 | 18 | ineq1i 4173 |
. . . . . . . . 9
β’
(((2...π) β
(1...π)) β© β) =
(β
β© β) |
20 | | 0in 4358 |
. . . . . . . . 9
β’ (β
β© β) = β
|
21 | 19, 20 | eqtri 2765 |
. . . . . . . 8
β’
(((2...π) β
(1...π)) β© β) =
β
|
22 | 21 | a1i 11 |
. . . . . . 7
β’ (π β β β
(((2...π) β
(1...π)) β© β) =
β
) |
23 | 13 | eleq2i 2830 |
. . . . . . . . . . . . 13
β’ (π β β β π β
(β€β₯β1)) |
24 | | fzpred 13496 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β1) β (1...π) = ({1} βͺ ((1 + 1)...π))) |
25 | 23, 24 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π β β β
(1...π) = ({1} βͺ ((1 +
1)...π))) |
26 | 25 | eqcomd 2743 |
. . . . . . . . . . 11
β’ (π β β β ({1}
βͺ ((1 + 1)...π)) =
(1...π)) |
27 | | 1p1e2 12285 |
. . . . . . . . . . . . 13
β’ (1 + 1) =
2 |
28 | 27 | oveq1i 7372 |
. . . . . . . . . . . 12
β’ ((1 +
1)...π) = (2...π) |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β ((1 +
1)...π) = (2...π)) |
30 | 26, 29 | difeq12d 4088 |
. . . . . . . . . 10
β’ (π β β β (({1}
βͺ ((1 + 1)...π))
β ((1 + 1)...π)) =
((1...π) β (2...π))) |
31 | | difun2 4445 |
. . . . . . . . . . 11
β’ (({1}
βͺ ((1 + 1)...π))
β ((1 + 1)...π)) =
({1} β ((1 + 1)...π)) |
32 | | fzpreddisj 13497 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β1) β ({1} β© ((1 + 1)...π)) = β
) |
33 | 23, 32 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π β β β ({1}
β© ((1 + 1)...π)) =
β
) |
34 | | disjdif2 4444 |
. . . . . . . . . . . 12
β’ (({1}
β© ((1 + 1)...π)) =
β
β ({1} β ((1 + 1)...π)) = {1}) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . 11
β’ (π β β β ({1}
β ((1 + 1)...π)) =
{1}) |
36 | 31, 35 | eqtrid 2789 |
. . . . . . . . . 10
β’ (π β β β (({1}
βͺ ((1 + 1)...π))
β ((1 + 1)...π)) =
{1}) |
37 | 30, 36 | eqtr3d 2779 |
. . . . . . . . 9
β’ (π β β β
((1...π) β (2...π)) = {1}) |
38 | 37 | ineq1d 4176 |
. . . . . . . 8
β’ (π β β β
(((1...π) β
(2...π)) β© β) =
({1} β© β)) |
39 | | incom 4166 |
. . . . . . . . 9
β’ (β
β© {1}) = ({1} β© β) |
40 | | 1nprm 16562 |
. . . . . . . . . 10
β’ Β¬ 1
β β |
41 | | disjsn 4677 |
. . . . . . . . . 10
β’ ((β
β© {1}) = β
β Β¬ 1 β β) |
42 | 40, 41 | mpbir 230 |
. . . . . . . . 9
β’ (β
β© {1}) = β
|
43 | 39, 42 | eqtr3i 2767 |
. . . . . . . 8
β’ ({1}
β© β) = β
|
44 | 38, 43 | eqtrdi 2793 |
. . . . . . 7
β’ (π β β β
(((1...π) β
(2...π)) β© β) =
β
) |
45 | | difininv 31486 |
. . . . . . 7
β’
(((((2...π) β
(1...π)) β© β) =
β
β§ (((1...π)
β (2...π)) β©
β) = β
) β ((2...π) β© β) = ((1...π) β© β)) |
46 | 22, 44, 45 | syl2anc 585 |
. . . . . 6
β’ (π β β β
((2...π) β© β) =
((1...π) β©
β)) |
47 | 11, 46 | eqtrd 2777 |
. . . . 5
β’ (π β β β
((0[,]π) β© β) =
((1...π) β©
β)) |
48 | 47 | adantl 483 |
. . . 4
β’ ((π β β€ β§ π β β) β
((0[,]π) β© β) =
((1...π) β©
β)) |
49 | | znnnlt1 12537 |
. . . . . 6
β’ (π β β€ β (Β¬
π β β β
π < 1)) |
50 | 49 | biimpa 478 |
. . . . 5
β’ ((π β β€ β§ Β¬
π β β) β
π < 1) |
51 | | incom 4166 |
. . . . . . 7
β’
((0[,]π) β©
β) = (β β© (0[,]π)) |
52 | | isprm3 16566 |
. . . . . . . . . . 11
β’ (π β β β (π β
(β€β₯β2) β§ βπ β (2...(π β 1)) Β¬ π β₯ π)) |
53 | 52 | simplbi 499 |
. . . . . . . . . 10
β’ (π β β β π β
(β€β₯β2)) |
54 | 53 | ssriv 3953 |
. . . . . . . . 9
β’ β
β (β€β₯β2) |
55 | 12 | nnzi 12534 |
. . . . . . . . . 10
β’ 2 β
β€ |
56 | | uzssico 31729 |
. . . . . . . . . 10
β’ (2 β
β€ β (β€β₯β2) β
(2[,)+β)) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . 9
β’
(β€β₯β2) β (2[,)+β) |
58 | 54, 57 | sstri 3958 |
. . . . . . . 8
β’ β
β (2[,)+β) |
59 | | incom 4166 |
. . . . . . . . 9
β’
((0[,]π) β©
(2[,)+β)) = ((2[,)+β) β© (0[,]π)) |
60 | | 0xr 11209 |
. . . . . . . . . . . 12
β’ 0 β
β* |
61 | 60 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π < 1) β 0 β
β*) |
62 | 12 | nnrei 12169 |
. . . . . . . . . . . . 13
β’ 2 β
β |
63 | 62 | rexri 11220 |
. . . . . . . . . . . 12
β’ 2 β
β* |
64 | 63 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π < 1) β 2 β
β*) |
65 | | 0le0 12261 |
. . . . . . . . . . . 12
β’ 0 β€
0 |
66 | 65 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π < 1) β 0 β€
0) |
67 | 1 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π < 1) β π β
β) |
68 | | 1red 11163 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π < 1) β 1 β
β) |
69 | 62 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π < 1) β 2 β
β) |
70 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π < 1) β π < 1) |
71 | | 1lt2 12331 |
. . . . . . . . . . . . 13
β’ 1 <
2 |
72 | 71 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π < 1) β 1 <
2) |
73 | 67, 68, 69, 70, 72 | lttrd 11323 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π < 1) β π < 2) |
74 | | iccssico 13343 |
. . . . . . . . . . 11
β’ (((0
β β* β§ 2 β β*) β§ (0 β€ 0
β§ π < 2)) β
(0[,]π) β
(0[,)2)) |
75 | 61, 64, 66, 73, 74 | syl22anc 838 |
. . . . . . . . . 10
β’ ((π β β€ β§ π < 1) β (0[,]π) β
(0[,)2)) |
76 | | pnfxr 11216 |
. . . . . . . . . . 11
β’ +β
β β* |
77 | | icodisj 13400 |
. . . . . . . . . . 11
β’ ((0
β β* β§ 2 β β* β§ +β
β β*) β ((0[,)2) β© (2[,)+β)) =
β
) |
78 | 60, 63, 76, 77 | mp3an 1462 |
. . . . . . . . . 10
β’ ((0[,)2)
β© (2[,)+β)) = β
|
79 | | ssdisj 4424 |
. . . . . . . . . 10
β’
(((0[,]π) β
(0[,)2) β§ ((0[,)2) β© (2[,)+β)) = β
) β ((0[,]π) β© (2[,)+β)) =
β
) |
80 | 75, 78, 79 | sylancl 587 |
. . . . . . . . 9
β’ ((π β β€ β§ π < 1) β ((0[,]π) β© (2[,)+β)) =
β
) |
81 | 59, 80 | eqtr3id 2791 |
. . . . . . . 8
β’ ((π β β€ β§ π < 1) β ((2[,)+β)
β© (0[,]π)) =
β
) |
82 | | ssdisj 4424 |
. . . . . . . 8
β’ ((β
β (2[,)+β) β§ ((2[,)+β) β© (0[,]π)) = β
) β (β β©
(0[,]π)) =
β
) |
83 | 58, 81, 82 | sylancr 588 |
. . . . . . 7
β’ ((π β β€ β§ π < 1) β (β β©
(0[,]π)) =
β
) |
84 | 51, 83 | eqtrid 2789 |
. . . . . 6
β’ ((π β β€ β§ π < 1) β ((0[,]π) β© β) =
β
) |
85 | | 1zzd 12541 |
. . . . . . . . 9
β’ ((π β β€ β§ π < 1) β 1 β
β€) |
86 | | simpl 484 |
. . . . . . . . 9
β’ ((π β β€ β§ π < 1) β π β
β€) |
87 | | fzn 13464 |
. . . . . . . . . 10
β’ ((1
β β€ β§ π
β β€) β (π
< 1 β (1...π) =
β
)) |
88 | 87 | biimpa 478 |
. . . . . . . . 9
β’ (((1
β β€ β§ π
β β€) β§ π
< 1) β (1...π) =
β
) |
89 | 85, 86, 70, 88 | syl21anc 837 |
. . . . . . . 8
β’ ((π β β€ β§ π < 1) β (1...π) = β
) |
90 | 89 | ineq1d 4176 |
. . . . . . 7
β’ ((π β β€ β§ π < 1) β ((1...π) β© β) = (β
β© β)) |
91 | 90, 20 | eqtrdi 2793 |
. . . . . 6
β’ ((π β β€ β§ π < 1) β ((1...π) β© β) =
β
) |
92 | 84, 91 | eqtr4d 2780 |
. . . . 5
β’ ((π β β€ β§ π < 1) β ((0[,]π) β© β) = ((1...π) β©
β)) |
93 | 50, 92 | syldan 592 |
. . . 4
β’ ((π β β€ β§ Β¬
π β β) β
((0[,]π) β© β) =
((1...π) β©
β)) |
94 | | exmidd 895 |
. . . 4
β’ (π β β€ β (π β β β¨ Β¬ π β
β)) |
95 | 48, 93, 94 | mpjaodan 958 |
. . 3
β’ (π β β€ β
((0[,]π) β© β) =
((1...π) β©
β)) |
96 | 95 | sumeq1d 15593 |
. 2
β’ (π β β€ β
Ξ£π β ((0[,]π) β© β)(logβπ) = Ξ£π β ((1...π) β© β)(logβπ)) |
97 | 3, 96 | eqtrd 2777 |
1
β’ (π β β€ β
(ΞΈβπ) =
Ξ£π β ((1...π) β© β)(logβπ)) |