Step | Hyp | Ref
| Expression |
1 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β ((2...(π΄ + 1)) β©
β)) |
2 | 1 | elin2d 4160 |
. . . . . . . . . . . 12
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β
β) |
3 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
Β¬ (π΄ + 1) β
β) |
4 | | nelne2 3039 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ Β¬
(π΄ + 1) β β)
β π₯ β (π΄ + 1)) |
5 | 2, 3, 4 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β (π΄ + 1)) |
6 | | velsn 4603 |
. . . . . . . . . . . 12
β’ (π₯ β {(π΄ + 1)} β π₯ = (π΄ + 1)) |
7 | 6 | necon3bbii 2988 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β {(π΄ + 1)} β π₯ β (π΄ + 1)) |
8 | 5, 7 | sylibr 233 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
Β¬ π₯ β {(π΄ + 1)}) |
9 | 1 | elin1d 4159 |
. . . . . . . . . . . . 13
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β (2...(π΄ + 1))) |
10 | | 2z 12540 |
. . . . . . . . . . . . . 14
β’ 2 β
β€ |
11 | | zcn 12509 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β€ β π΄ β
β) |
12 | 11 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π΄ β
β) |
13 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β |
14 | | pncan 11412 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§ 1 β
β) β ((π΄ + 1)
β 1) = π΄) |
15 | 12, 13, 14 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
((π΄ + 1) β 1) = π΄) |
16 | | elfzuz2 13452 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (2...(π΄ + 1)) β (π΄ + 1) β
(β€β₯β2)) |
17 | | uz2m1nn 12853 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ + 1) β
(β€β₯β2) β ((π΄ + 1) β 1) β
β) |
18 | 9, 16, 17 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
((π΄ + 1) β 1) β
β) |
19 | 15, 18 | eqeltrrd 2835 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π΄ β
β) |
20 | | nnuz 12811 |
. . . . . . . . . . . . . . . 16
β’ β =
(β€β₯β1) |
21 | | 2m1e1 12284 |
. . . . . . . . . . . . . . . . 17
β’ (2
β 1) = 1 |
22 | 21 | fveq2i 6846 |
. . . . . . . . . . . . . . . 16
β’
(β€β₯β(2 β 1)) =
(β€β₯β1) |
23 | 20, 22 | eqtr4i 2764 |
. . . . . . . . . . . . . . 15
β’ β =
(β€β₯β(2 β 1)) |
24 | 19, 23 | eleqtrdi 2844 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π΄ β
(β€β₯β(2 β 1))) |
25 | | fzsuc2 13505 |
. . . . . . . . . . . . . 14
β’ ((2
β β€ β§ π΄
β (β€β₯β(2 β 1))) β (2...(π΄ + 1)) = ((2...π΄) βͺ {(π΄ + 1)})) |
26 | 10, 24, 25 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
(2...(π΄ + 1)) = ((2...π΄) βͺ {(π΄ + 1)})) |
27 | 9, 26 | eleqtrd 2836 |
. . . . . . . . . . . 12
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β ((2...π΄) βͺ {(π΄ + 1)})) |
28 | | elun 4109 |
. . . . . . . . . . . 12
β’ (π₯ β ((2...π΄) βͺ {(π΄ + 1)}) β (π₯ β (2...π΄) β¨ π₯ β {(π΄ + 1)})) |
29 | 27, 28 | sylib 217 |
. . . . . . . . . . 11
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
(π₯ β (2...π΄) β¨ π₯ β {(π΄ + 1)})) |
30 | 29 | ord 863 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
(Β¬ π₯ β (2...π΄) β π₯ β {(π΄ + 1)})) |
31 | 8, 30 | mt3d 148 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β (2...π΄)) |
32 | 31, 2 | elind 4155 |
. . . . . . . 8
β’ ((π΄ β β€ β§ (Β¬
(π΄ + 1) β β
β§ π₯ β ((2...(π΄ + 1)) β© β))) β
π₯ β ((2...π΄) β©
β)) |
33 | 32 | expr 458 |
. . . . . . 7
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (π₯ β
((2...(π΄ + 1)) β©
β) β π₯ β
((2...π΄) β©
β))) |
34 | 33 | ssrdv 3951 |
. . . . . 6
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...(π΄ + 1)) β©
β) β ((2...π΄)
β© β)) |
35 | | uzid 12783 |
. . . . . . . 8
β’ (π΄ β β€ β π΄ β
(β€β₯βπ΄)) |
36 | 35 | adantr 482 |
. . . . . . 7
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β π΄ β
(β€β₯βπ΄)) |
37 | | peano2uz 12831 |
. . . . . . 7
β’ (π΄ β
(β€β₯βπ΄) β (π΄ + 1) β
(β€β₯βπ΄)) |
38 | | fzss2 13487 |
. . . . . . 7
β’ ((π΄ + 1) β
(β€β₯βπ΄) β (2...π΄) β (2...(π΄ + 1))) |
39 | | ssrin 4194 |
. . . . . . 7
β’
((2...π΄) β
(2...(π΄ + 1)) β
((2...π΄) β© β)
β ((2...(π΄ + 1))
β© β)) |
40 | 36, 37, 38, 39 | 4syl 19 |
. . . . . 6
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...π΄) β©
β) β ((2...(π΄ +
1)) β© β)) |
41 | 34, 40 | eqssd 3962 |
. . . . 5
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...(π΄ + 1)) β©
β) = ((2...π΄) β©
β)) |
42 | | peano2z 12549 |
. . . . . . . . 9
β’ (π΄ β β€ β (π΄ + 1) β
β€) |
43 | 42 | adantr 482 |
. . . . . . . 8
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (π΄ + 1) β
β€) |
44 | | flid 13719 |
. . . . . . . 8
β’ ((π΄ + 1) β β€ β
(ββ(π΄ + 1)) =
(π΄ + 1)) |
45 | 43, 44 | syl 17 |
. . . . . . 7
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (ββ(π΄ +
1)) = (π΄ +
1)) |
46 | 45 | oveq2d 7374 |
. . . . . 6
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (2...(ββ(π΄ + 1))) = (2...(π΄ + 1))) |
47 | 46 | ineq1d 4172 |
. . . . 5
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...(ββ(π΄ + 1))) β© β) = ((2...(π΄ + 1)) β©
β)) |
48 | | flid 13719 |
. . . . . . . 8
β’ (π΄ β β€ β
(ββπ΄) = π΄) |
49 | 48 | adantr 482 |
. . . . . . 7
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (ββπ΄) =
π΄) |
50 | 49 | oveq2d 7374 |
. . . . . 6
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (2...(ββπ΄)) = (2...π΄)) |
51 | 50 | ineq1d 4172 |
. . . . 5
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...(ββπ΄)) β© β) = ((2...π΄) β© β)) |
52 | 41, 47, 51 | 3eqtr4d 2783 |
. . . 4
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((2...(ββ(π΄ + 1))) β© β) =
((2...(ββπ΄))
β© β)) |
53 | | zre 12508 |
. . . . . 6
β’ (π΄ β β€ β π΄ β
β) |
54 | 53 | adantr 482 |
. . . . 5
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β π΄ β
β) |
55 | | peano2re 11333 |
. . . . 5
β’ (π΄ β β β (π΄ + 1) β
β) |
56 | | ppisval 26469 |
. . . . 5
β’ ((π΄ + 1) β β β
((0[,](π΄ + 1)) β©
β) = ((2...(ββ(π΄ + 1))) β© β)) |
57 | 54, 55, 56 | 3syl 18 |
. . . 4
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((0[,](π΄ + 1)) β©
β) = ((2...(ββ(π΄ + 1))) β© β)) |
58 | | ppisval 26469 |
. . . . 5
β’ (π΄ β β β
((0[,]π΄) β© β) =
((2...(ββπ΄))
β© β)) |
59 | 54, 58 | syl 17 |
. . . 4
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((0[,]π΄) β©
β) = ((2...(ββπ΄)) β© β)) |
60 | 52, 57, 59 | 3eqtr4d 2783 |
. . 3
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β ((0[,](π΄ + 1)) β©
β) = ((0[,]π΄) β©
β)) |
61 | 60 | sumeq1d 15591 |
. 2
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β Ξ£π β
((0[,](π΄ + 1)) β©
β)(logβπ) =
Ξ£π β ((0[,]π΄) β© β)(logβπ)) |
62 | | chtval 26475 |
. . 3
β’ ((π΄ + 1) β β β
(ΞΈβ(π΄ + 1)) =
Ξ£π β
((0[,](π΄ + 1)) β©
β)(logβπ)) |
63 | 54, 55, 62 | 3syl 18 |
. 2
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (ΞΈβ(π΄ +
1)) = Ξ£π β
((0[,](π΄ + 1)) β©
β)(logβπ)) |
64 | | chtval 26475 |
. . 3
β’ (π΄ β β β
(ΞΈβπ΄) =
Ξ£π β ((0[,]π΄) β© β)(logβπ)) |
65 | 54, 64 | syl 17 |
. 2
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (ΞΈβπ΄) =
Ξ£π β ((0[,]π΄) β© β)(logβπ)) |
66 | 61, 63, 65 | 3eqtr4d 2783 |
1
β’ ((π΄ β β€ β§ Β¬
(π΄ + 1) β β)
β (ΞΈβ(π΄ +
1)) = (ΞΈβπ΄)) |