Step | Hyp | Ref
| Expression |
1 | | simprr 770 |
. . . . . . . . . . . . 13
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β ((2...(π΄ + 1)) β©
β)) |
2 | 1 | elin2d 4194 |
. . . . . . . . . . . 12
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β
β) |
3 | | simprl 768 |
. . . . . . . . . . . 12
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
Β¬ (π΄ + 1) β
β) |
4 | | nelne2 3034 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ Β¬
(π΄ + 1) β β)
β π₯ β (π΄ + 1)) |
5 | 2, 3, 4 | syl2anc 583 |
. . . . . . . . . . 11
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β (π΄ + 1)) |
6 | | velsn 4639 |
. . . . . . . . . . . 12
β’ (π₯ β {(π΄ + 1)} β π₯ = (π΄ + 1)) |
7 | 6 | necon3bbii 2982 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β {(π΄ + 1)} β π₯ β (π΄ + 1)) |
8 | 5, 7 | sylibr 233 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
Β¬ π₯ β {(π΄ + 1)}) |
9 | 1 | elin1d 4193 |
. . . . . . . . . . . . 13
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β (2...(π΄ + 1))) |
10 | | 2z 12595 |
. . . . . . . . . . . . . 14
β’ 2 β
β€ |
11 | | zcn 12564 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β€ β π΄ β
β) |
12 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π΄ β
β) |
13 | | ax-1cn 11167 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β |
14 | | pncan 11467 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§ 1 β
β) β ((π΄ + 1)
β 1) = π΄) |
15 | 12, 13, 14 | sylancl 585 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
((π΄ + 1) β 1) = π΄) |
16 | | elfzuz2 13509 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (2...(π΄ + 1)) β (π΄ + 1) β
(β€β₯β2)) |
17 | | uz2m1nn 12908 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ + 1) β
(β€β₯β2) β ((π΄ + 1) β 1) β
β) |
18 | 9, 16, 17 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
((π΄ + 1) β 1) β
β) |
19 | 15, 18 | eqeltrrd 2828 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π΄ β
β) |
20 | | nnuz 12866 |
. . . . . . . . . . . . . . . 16
β’ β =
(β€β₯β1) |
21 | | 2m1e1 12339 |
. . . . . . . . . . . . . . . . 17
β’ (2
β 1) = 1 |
22 | 21 | fveq2i 6887 |
. . . . . . . . . . . . . . . 16
β’
(β€β₯β(2 β 1)) =
(β€β₯β1) |
23 | 20, 22 | eqtr4i 2757 |
. . . . . . . . . . . . . . 15
β’ β =
(β€β₯β(2 β 1)) |
24 | 19, 23 | eleqtrdi 2837 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π΄ β
(β€β₯β(2 β 1))) |
25 | | fzsuc2 13562 |
. . . . . . . . . . . . . 14
β’ ((2
β β€ β§ π΄
β (β€β₯β(2 β 1))) β (2...(π΄ + 1)) = ((2...π΄) βͺ {(π΄ + 1)})) |
26 | 10, 24, 25 | sylancr 586 |
. . . . . . . . . . . . 13
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
(2...(π΄ + 1)) = ((2...π΄) βͺ {(π΄ + 1)})) |
27 | 9, 26 | eleqtrd 2829 |
. . . . . . . . . . . 12
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β ((2...π΄) βͺ {(π΄ + 1)})) |
28 | | elun 4143 |
. . . . . . . . . . . 12
β’ (π₯ β ((2...π΄) βͺ {(π΄ + 1)}) β (π₯ β (2...π΄) β¨ π₯ β {(π΄ + 1)})) |
29 | 27, 28 | sylib 217 |
. . . . . . . . . . 11
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
(π₯ β (2...π΄) β¨ π₯ β {(π΄ + 1)})) |
30 | 29 | ord 861 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
(Β¬ π₯ β (2...π΄) β π₯ β {(π΄ + 1)})) |
31 | 8, 30 | mt3d 148 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β (2...π΄)) |
32 | 31, 2 | elind 4189 |
. . . . . . . 8
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β ((2...π΄) β©
β)) |
33 | 32 | expr 456 |
. . . . . . 7
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (π₯ β
((2...(π΄ + 1)) β©
β) β π₯ β
((2...π΄) β©
β))) |
34 | 33 | ssrdv 3983 |
. . . . . 6
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...(π΄ + 1)) β©
β) β ((2...π΄)
β© β)) |
35 | | uzid 12838 |
. . . . . . . 8
β’ (π΄ β β€ β π΄ β
(β€β₯βπ΄)) |
36 | 35 | adantr 480 |
. . . . . . 7
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β π΄ β
(β€β₯βπ΄)) |
37 | | peano2uz 12886 |
. . . . . . 7
β’ (π΄ β
(β€β₯βπ΄) β (π΄ + 1) β
(β€β₯βπ΄)) |
38 | | fzss2 13544 |
. . . . . . 7
β’ ((π΄ + 1) β
(β€β₯βπ΄) β (2...π΄) β (2...(π΄ + 1))) |
39 | | ssrin 4228 |
. . . . . . 7
β’
((2...π΄) β
(2...(π΄ + 1)) β
((2...π΄) β© β)
β ((2...(π΄ + 1))
β© β)) |
40 | 36, 37, 38, 39 | 4syl 19 |
. . . . . 6
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...π΄) β©
β) β ((2...(π΄ +
1)) β© β)) |
41 | 34, 40 | eqssd 3994 |
. . . . 5
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...(π΄ + 1)) β©
β) = ((2...π΄) β©
β)) |
42 | | peano2z 12604 |
. . . . . . . . 9
β’ (π΄ β β€ β (π΄ + 1) β
β€) |
43 | 42 | adantr 480 |
. . . . . . . 8
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (π΄ + 1) β
β€) |
44 | | flid 13776 |
. . . . . . . 8
β’ ((π΄ + 1) β β€ β
(ββ(π΄ + 1)) =
(π΄ + 1)) |
45 | 43, 44 | syl 17 |
. . . . . . 7
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (ββ(π΄ +
1)) = (π΄ +
1)) |
46 | 45 | oveq2d 7420 |
. . . . . 6
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (2...(ββ(π΄ + 1))) = (2...(π΄ + 1))) |
47 | 46 | ineq1d 4206 |
. . . . 5
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...(ββ(π΄ + 1))) β© β) = ((2...(π΄ + 1)) β©
β)) |
48 | | flid 13776 |
. . . . . . . 8
β’ (π΄ β β€ β
(ββπ΄) = π΄) |
49 | 48 | adantr 480 |
. . . . . . 7
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (ββπ΄) =
π΄) |
50 | 49 | oveq2d 7420 |
. . . . . 6
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (2...(ββπ΄)) = (2...π΄)) |
51 | 50 | ineq1d 4206 |
. . . . 5
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...(ββπ΄)) β© β) = ((2...π΄) β© β)) |
52 | 41, 47, 51 | 3eqtr4d 2776 |
. . . 4
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...(ββ(π΄ + 1))) β© β) =
((2...(ββπ΄))
β© β)) |
53 | | zre 12563 |
. . . . . 6
β’ (π΄ β β€ β π΄ β
β) |
54 | 53 | adantr 480 |
. . . . 5
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β π΄ β
β) |
55 | | peano2re 11388 |
. . . . 5
β’ (π΄ β β β (π΄ + 1) β
β) |
56 | | ppisval 26986 |
. . . . 5
β’ ((π΄ + 1) β β β
((0[,](π΄ + 1)) β©
β) = ((2...(ββ(π΄ + 1))) β© β)) |
57 | 54, 55, 56 | 3syl 18 |
. . . 4
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((0[,](π΄ + 1)) β©
β) = ((2...(ββ(π΄ + 1))) β© β)) |
58 | | ppisval 26986 |
. . . . 5
β’ (π΄ β β β
((0[,]π΄) β© β) =
((2...(ββπ΄))
β© β)) |
59 | 54, 58 | syl 17 |
. . . 4
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((0[,]π΄) β©
β) = ((2...(ββπ΄)) β© β)) |
60 | 52, 57, 59 | 3eqtr4d 2776 |
. . 3
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((0[,](π΄ + 1)) β©
β) = ((0[,]π΄) β©
β)) |
61 | 60 | sumeq1d 15650 |
. 2
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β Ξ£π β
((0[,](π΄ + 1)) β©
β)(logβπ) =
Ξ£π β ((0[,]π΄) β© β)(logβπ)) |
62 | | chtval 26992 |
. . 3
β’ ((π΄ + 1) β β β
(ΞΈβ(π΄ + 1)) =
Ξ£π β
((0[,](π΄ + 1)) β©
β)(logβπ)) |
63 | 54, 55, 62 | 3syl 18 |
. 2
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (ΞΈβ(π΄ +
1)) = Ξ£π β
((0[,](π΄ + 1)) β©
β)(logβπ)) |
64 | | chtval 26992 |
. . 3
β’ (π΄ β β β
(ΞΈβπ΄) =
Ξ£π β ((0[,]π΄) β© β)(logβπ)) |
65 | 54, 64 | syl 17 |
. 2
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (ΞΈβπ΄) =
Ξ£π β ((0[,]π΄) β© β)(logβπ)) |
66 | 61, 63, 65 | 3eqtr4d 2776 |
1
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (ΞΈβ(π΄ +
1)) = (ΞΈβπ΄)) |