Step | Hyp | Ref
| Expression |
1 | | fzfid 13938 |
. . . . 5
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
(1...(ββ((logβπ΄) / (logβπ)))) β Fin) |
2 | | simpr 486 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β ((0[,]π΄) β© β)) |
3 | 2 | elin2d 4200 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
4 | | prmnn 16611 |
. . . . . . . . 9
β’ (π β β β π β
β) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
6 | 5 | nnrpd 13014 |
. . . . . . 7
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β+) |
7 | 6 | relogcld 26131 |
. . . . . 6
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (logβπ) β
β) |
8 | 7 | recnd 11242 |
. . . . 5
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (logβπ) β
β) |
9 | | fsumconst 15736 |
. . . . 5
β’
(((1...(ββ((logβπ΄) / (logβπ)))) β Fin β§ (logβπ) β β) β
Ξ£π β
(1...(ββ((logβπ΄) / (logβπ))))(logβπ) =
((β―β(1...(ββ((logβπ΄) / (logβπ))))) Β· (logβπ))) |
10 | 1, 8, 9 | syl2anc 585 |
. . . 4
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β Ξ£π β
(1...(ββ((logβπ΄) / (logβπ))))(logβπ) =
((β―β(1...(ββ((logβπ΄) / (logβπ))))) Β· (logβπ))) |
11 | | simpl 484 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π΄ β β) |
12 | | 1red 11215 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 1 β
β) |
13 | 5 | nnred 12227 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
14 | | prmuz2 16633 |
. . . . . . . . . . . . 13
β’ (π β β β π β
(β€β₯β2)) |
15 | 3, 14 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β
(β€β₯β2)) |
16 | | eluz2gt1 12904 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β2) β 1 < π) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 1 < π) |
18 | 2 | elin1d 4199 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β (0[,]π΄)) |
19 | | 0re 11216 |
. . . . . . . . . . . . . 14
β’ 0 β
β |
20 | | elicc2 13389 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ π΄
β β) β (π
β (0[,]π΄) β
(π β β β§ 0
β€ π β§ π β€ π΄))) |
21 | 19, 11, 20 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (π β (0[,]π΄) β (π β β β§ 0 β€ π β§ π β€ π΄))) |
22 | 18, 21 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (π β β β§ 0 β€ π β§ π β€ π΄)) |
23 | 22 | simp3d 1145 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β€ π΄) |
24 | 12, 13, 11, 17, 23 | ltletrd 11374 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 1 < π΄) |
25 | 11, 24 | rplogcld 26137 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (logβπ΄) β
β+) |
26 | 13, 17 | rplogcld 26137 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (logβπ) β
β+) |
27 | 25, 26 | rpdivcld 13033 |
. . . . . . . 8
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β ((logβπ΄) / (logβπ)) β
β+) |
28 | 27 | rpred 13016 |
. . . . . . 7
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β ((logβπ΄) / (logβπ)) β
β) |
29 | 27 | rpge0d 13020 |
. . . . . . 7
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 0 β€
((logβπ΄) /
(logβπ))) |
30 | | flge0nn0 13785 |
. . . . . . 7
β’
((((logβπ΄) /
(logβπ)) β
β β§ 0 β€ ((logβπ΄) / (logβπ))) β (ββ((logβπ΄) / (logβπ))) β
β0) |
31 | 28, 29, 30 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
(ββ((logβπ΄) / (logβπ))) β
β0) |
32 | | hashfz1 14306 |
. . . . . 6
β’
((ββ((logβπ΄) / (logβπ))) β β0 β
(β―β(1...(ββ((logβπ΄) / (logβπ))))) = (ββ((logβπ΄) / (logβπ)))) |
33 | 31, 32 | syl 17 |
. . . . 5
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
(β―β(1...(ββ((logβπ΄) / (logβπ))))) = (ββ((logβπ΄) / (logβπ)))) |
34 | 33 | oveq1d 7424 |
. . . 4
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
((β―β(1...(ββ((logβπ΄) / (logβπ))))) Β· (logβπ)) = ((ββ((logβπ΄) / (logβπ))) Β· (logβπ))) |
35 | 28 | flcld 13763 |
. . . . . 6
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
(ββ((logβπ΄) / (logβπ))) β β€) |
36 | 35 | zcnd 12667 |
. . . . 5
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
(ββ((logβπ΄) / (logβπ))) β β) |
37 | 36, 8 | mulcomd 11235 |
. . . 4
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
((ββ((logβπ΄) / (logβπ))) Β· (logβπ)) = ((logβπ) Β· (ββ((logβπ΄) / (logβπ))))) |
38 | 10, 34, 37 | 3eqtrrd 2778 |
. . 3
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β ((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) = Ξ£π β (1...(ββ((logβπ΄) / (logβπ))))(logβπ)) |
39 | 38 | sumeq2dv 15649 |
. 2
β’ (π΄ β β β
Ξ£π β ((0[,]π΄) β©
β)((logβπ)
Β· (ββ((logβπ΄) / (logβπ)))) = Ξ£π β ((0[,]π΄) β© β)Ξ£π β (1...(ββ((logβπ΄) / (logβπ))))(logβπ)) |
40 | | chpval2 26721 |
. 2
β’ (π΄ β β β
(Οβπ΄) =
Ξ£π β ((0[,]π΄) β©
β)((logβπ)
Β· (ββ((logβπ΄) / (logβπ))))) |
41 | | simpl 484 |
. . . . . 6
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β π΄ β
β) |
42 | | 0red 11217 |
. . . . . . 7
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 0 β β) |
43 | | 1red 11215 |
. . . . . . . 8
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 1 β β) |
44 | | 0lt1 11736 |
. . . . . . . . 9
β’ 0 <
1 |
45 | 44 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 0 < 1) |
46 | | elfzuz2 13506 |
. . . . . . . . 9
β’ (π β
(1...(ββπ΄))
β (ββπ΄)
β (β€β₯β1)) |
47 | | eluzle 12835 |
. . . . . . . . . . 11
β’
((ββπ΄)
β (β€β₯β1) β 1 β€ (ββπ΄)) |
48 | 47 | adantl 483 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(β€β₯β1)) β 1 β€ (ββπ΄)) |
49 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(β€β₯β1)) β π΄ β β) |
50 | | 1z 12592 |
. . . . . . . . . . 11
β’ 1 β
β€ |
51 | | flge 13770 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ 1 β
β€) β (1 β€ π΄
β 1 β€ (ββπ΄))) |
52 | 49, 50, 51 | sylancl 587 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(β€β₯β1)) β (1 β€ π΄ β 1 β€ (ββπ΄))) |
53 | 48, 52 | mpbird 257 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(β€β₯β1)) β 1 β€ π΄) |
54 | 46, 53 | sylan2 594 |
. . . . . . . 8
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 1 β€ π΄) |
55 | 42, 43, 41, 45, 54 | ltletrd 11374 |
. . . . . . 7
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 0 < π΄) |
56 | 42, 41, 55 | ltled 11362 |
. . . . . 6
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 0 β€ π΄) |
57 | | elfznn 13530 |
. . . . . . . 8
β’ (π β
(1...(ββπ΄))
β π β
β) |
58 | 57 | adantl 483 |
. . . . . . 7
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β π β
β) |
59 | 58 | nnrecred 12263 |
. . . . . 6
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β (1 / π) β
β) |
60 | 41, 56, 59 | recxpcld 26231 |
. . . . 5
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β (π΄βπ(1 / π)) β
β) |
61 | | chtval 26614 |
. . . . 5
β’ ((π΄βπ(1 /
π)) β β β
(ΞΈβ(π΄βπ(1 / π))) = Ξ£π β ((0[,](π΄βπ(1 / π))) β©
β)(logβπ)) |
62 | 60, 61 | syl 17 |
. . . 4
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β (ΞΈβ(π΄βπ(1 / π))) = Ξ£π β ((0[,](π΄βπ(1 / π))) β©
β)(logβπ)) |
63 | 62 | sumeq2dv 15649 |
. . 3
β’ (π΄ β β β
Ξ£π β
(1...(ββπ΄))(ΞΈβ(π΄βπ(1 / π))) = Ξ£π β (1...(ββπ΄))Ξ£π β ((0[,](π΄βπ(1 / π))) β©
β)(logβπ)) |
64 | | ppifi 26610 |
. . . 4
β’ (π΄ β β β
((0[,]π΄) β© β)
β Fin) |
65 | | fzfid 13938 |
. . . 4
β’ (π΄ β β β
(1...(ββπ΄))
β Fin) |
66 | | elinel2 4197 |
. . . . . . . 8
β’ (π β ((0[,]π΄) β© β) β π β β) |
67 | | elfznn 13530 |
. . . . . . . 8
β’ (π β
(1...(ββ((logβπ΄) / (logβπ)))) β π β β) |
68 | 66, 67 | anim12i 614 |
. . . . . . 7
β’ ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β β β§ π β β)) |
69 | 68 | a1i 11 |
. . . . . 6
β’ (π΄ β β β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β β β§ π β β))) |
70 | | 0red 11217 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 0 β
β) |
71 | | inss2 4230 |
. . . . . . . . . . . . 13
β’
((0[,]π΄) β©
β) β β |
72 | 71 | a1i 11 |
. . . . . . . . . . . 12
β’ (π΄ β β β
((0[,]π΄) β© β)
β β) |
73 | 72 | sselda 3983 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
74 | 73, 4 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
75 | 74 | nnred 12227 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
76 | 74 | nngt0d 12261 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 0 < π) |
77 | 70, 75, 11, 76, 23 | ltletrd 11374 |
. . . . . . . 8
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 0 < π΄) |
78 | 77 | ex 414 |
. . . . . . 7
β’ (π΄ β β β (π β ((0[,]π΄) β© β) β 0 < π΄)) |
79 | 78 | adantrd 493 |
. . . . . 6
β’ (π΄ β β β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β 0 < π΄)) |
80 | 69, 79 | jcad 514 |
. . . . 5
β’ (π΄ β β β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β ((π β β β§ π β β) β§ 0 <
π΄))) |
81 | | elinel2 4197 |
. . . . . . . 8
β’ (π β ((0[,](π΄βπ(1 / π))) β© β) β π β
β) |
82 | 57, 81 | anim12ci 615 |
. . . . . . 7
β’ ((π β
(1...(ββπ΄))
β§ π β ((0[,](π΄βπ(1 /
π))) β© β)) β
(π β β β§
π β
β)) |
83 | 82 | a1i 11 |
. . . . . 6
β’ (π΄ β β β ((π β
(1...(ββπ΄))
β§ π β ((0[,](π΄βπ(1 /
π))) β© β)) β
(π β β β§
π β
β))) |
84 | 55 | ex 414 |
. . . . . . 7
β’ (π΄ β β β (π β
(1...(ββπ΄))
β 0 < π΄)) |
85 | 84 | adantrd 493 |
. . . . . 6
β’ (π΄ β β β ((π β
(1...(ββπ΄))
β§ π β ((0[,](π΄βπ(1 /
π))) β© β)) β
0 < π΄)) |
86 | 83, 85 | jcad 514 |
. . . . 5
β’ (π΄ β β β ((π β
(1...(ββπ΄))
β§ π β ((0[,](π΄βπ(1 /
π))) β© β)) β
((π β β β§
π β β) β§ 0
< π΄))) |
87 | | elin 3965 |
. . . . . . . . 9
β’ (π β ((0[,]π΄) β© β) β (π β (0[,]π΄) β§ π β β)) |
88 | | simprll 778 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
89 | 88 | biantrud 533 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β (0[,]π΄) β (π β (0[,]π΄) β§ π β β))) |
90 | | 0red 11217 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 0 β
β) |
91 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π΄ β
β) |
92 | 88, 4 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
93 | 92 | nnred 12227 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
94 | 92 | nnnn0d 12532 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β0) |
95 | 94 | nn0ge0d 12535 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 0 β€ π) |
96 | | df-3an 1090 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 0 β€
π β§ π β€ π΄) β ((π β β β§ 0 β€ π) β§ π β€ π΄)) |
97 | 20, 96 | bitrdi 287 |
. . . . . . . . . . . 12
β’ ((0
β β β§ π΄
β β) β (π
β (0[,]π΄) β
((π β β β§ 0
β€ π) β§ π β€ π΄))) |
98 | 97 | baibd 541 |
. . . . . . . . . . 11
β’ (((0
β β β§ π΄
β β) β§ (π
β β β§ 0 β€ π)) β (π β (0[,]π΄) β π β€ π΄)) |
99 | 90, 91, 93, 95, 98 | syl22anc 838 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β (0[,]π΄) β π β€ π΄)) |
100 | 89, 99 | bitr3d 281 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β (0[,]π΄) β§ π β β) β π β€ π΄)) |
101 | 87, 100 | bitrid 283 |
. . . . . . . 8
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β ((0[,]π΄) β© β) β π β€ π΄)) |
102 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 0 < π΄) |
103 | 91, 102 | elrpd 13013 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π΄ β
β+) |
104 | 103 | relogcld 26131 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (logβπ΄) β
β) |
105 | 88, 14 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
(β€β₯β2)) |
106 | 105, 16 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 1 < π) |
107 | 93, 106 | rplogcld 26137 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (logβπ) β
β+) |
108 | 104, 107 | rerpdivcld 13047 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β
((logβπ΄) /
(logβπ)) β
β) |
109 | | simprlr 779 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
110 | 109 | nnzd 12585 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β€) |
111 | | flge 13770 |
. . . . . . . . . 10
β’
((((logβπ΄) /
(logβπ)) β
β β§ π β
β€) β (π β€
((logβπ΄) /
(logβπ)) β π β€
(ββ((logβπ΄) / (logβπ))))) |
112 | 108, 110,
111 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β€ ((logβπ΄) / (logβπ)) β π β€ (ββ((logβπ΄) / (logβπ))))) |
113 | 109 | nnnn0d 12532 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β0) |
114 | 92, 113 | nnexpcld 14208 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβπ) β β) |
115 | 114 | nnrpd 13014 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβπ) β
β+) |
116 | 115, 103 | logled 26135 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β (logβ(πβπ)) β€ (logβπ΄))) |
117 | 92 | nnrpd 13014 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β+) |
118 | | relogexp 26104 |
. . . . . . . . . . . 12
β’ ((π β β+
β§ π β β€)
β (logβ(πβπ)) = (π Β· (logβπ))) |
119 | 117, 110,
118 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β
(logβ(πβπ)) = (π Β· (logβπ))) |
120 | 119 | breq1d 5159 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β
((logβ(πβπ)) β€ (logβπ΄) β (π Β· (logβπ)) β€ (logβπ΄))) |
121 | 109 | nnred 12227 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
122 | 121, 104,
107 | lemuldivd 13065 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π Β· (logβπ)) β€ (logβπ΄) β π β€ ((logβπ΄) / (logβπ)))) |
123 | 116, 120,
122 | 3bitrd 305 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β π β€ ((logβπ΄) / (logβπ)))) |
124 | | nnuz 12865 |
. . . . . . . . . . 11
β’ β =
(β€β₯β1) |
125 | 109, 124 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
(β€β₯β1)) |
126 | 108 | flcld 13763 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β
(ββ((logβπ΄) / (logβπ))) β β€) |
127 | | elfz5 13493 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β1) β§ (ββ((logβπ΄) / (logβπ))) β β€) β
(π β
(1...(ββ((logβπ΄) / (logβπ)))) β π β€ (ββ((logβπ΄) / (logβπ))))) |
128 | 125, 126,
127 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β
(1...(ββ((logβπ΄) / (logβπ)))) β π β€ (ββ((logβπ΄) / (logβπ))))) |
129 | 112, 123,
128 | 3bitr4rd 312 |
. . . . . . . 8
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β
(1...(ββ((logβπ΄) / (logβπ)))) β (πβπ) β€ π΄)) |
130 | 101, 129 | anbi12d 632 |
. . . . . . 7
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β€ π΄ β§ (πβπ) β€ π΄))) |
131 | 91 | flcld 13763 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β
(ββπ΄) β
β€) |
132 | | elfz5 13493 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯β1) β§ (ββπ΄) β β€) β (π β (1...(ββπ΄)) β π β€ (ββπ΄))) |
133 | 125, 131,
132 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β
(1...(ββπ΄))
β π β€
(ββπ΄))) |
134 | | flge 13770 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β β€) β (π β€ π΄ β π β€ (ββπ΄))) |
135 | 91, 110, 134 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β€ π΄ β π β€ (ββπ΄))) |
136 | 133, 135 | bitr4d 282 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β
(1...(ββπ΄))
β π β€ π΄)) |
137 | | elin 3965 |
. . . . . . . . . 10
β’ (π β ((0[,](π΄βπ(1 / π))) β© β) β (π β (0[,](π΄βπ(1 / π))) β§ π β β)) |
138 | 88 | biantrud 533 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β (0[,](π΄βπ(1 / π))) β (π β (0[,](π΄βπ(1 / π))) β§ π β β))) |
139 | 103 | rpge0d 13020 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 0 β€ π΄) |
140 | 109 | nnrecred 12263 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (1 / π) β
β) |
141 | 91, 139, 140 | recxpcld 26231 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π΄βπ(1 /
π)) β
β) |
142 | | elicc2 13389 |
. . . . . . . . . . . . . . 15
β’ ((0
β β β§ (π΄βπ(1 / π)) β β) β (π β (0[,](π΄βπ(1 / π))) β (π β β β§ 0 β€ π β§ π β€ (π΄βπ(1 / π))))) |
143 | | df-3an 1090 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ 0 β€
π β§ π β€ (π΄βπ(1 / π))) β ((π β β β§ 0 β€ π) β§ π β€ (π΄βπ(1 / π)))) |
144 | 142, 143 | bitrdi 287 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ (π΄βπ(1 / π)) β β) β (π β (0[,](π΄βπ(1 / π))) β ((π β β β§ 0 β€ π) β§ π β€ (π΄βπ(1 / π))))) |
145 | 144 | baibd 541 |
. . . . . . . . . . . . 13
β’ (((0
β β β§ (π΄βπ(1 / π)) β β) β§ (π β β β§ 0 β€
π)) β (π β (0[,](π΄βπ(1 / π))) β π β€ (π΄βπ(1 / π)))) |
146 | 90, 141, 93, 95, 145 | syl22anc 838 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β (0[,](π΄βπ(1 / π))) β π β€ (π΄βπ(1 / π)))) |
147 | 138, 146 | bitr3d 281 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β (0[,](π΄βπ(1 / π))) β§ π β β) β π β€ (π΄βπ(1 / π)))) |
148 | 91, 139, 140 | cxpge0d 26232 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 0 β€ (π΄βπ(1 /
π))) |
149 | 109 | nnrpd 13014 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β+) |
150 | 93, 95, 141, 148, 149 | cxple2d 26235 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β€ (π΄βπ(1 / π)) β (πβππ) β€ ((π΄βπ(1 / π))βππ))) |
151 | 92 | nncnd 12228 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
152 | | cxpexp 26176 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β0)
β (πβππ) = (πβπ)) |
153 | 151, 113,
152 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβππ) = (πβπ)) |
154 | 109 | nncnd 12228 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
155 | 109 | nnne0d 12262 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β 0) |
156 | 154, 155 | recid2d 11986 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((1 / π) Β· π) = 1) |
157 | 156 | oveq2d 7425 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π΄βπ((1 /
π) Β· π)) = (π΄βπ1)) |
158 | 103, 140,
154 | cxpmuld 26245 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π΄βπ((1 /
π) Β· π)) = ((π΄βπ(1 / π))βππ)) |
159 | 91 | recnd 11242 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π΄ β
β) |
160 | 159 | cxp1d 26214 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π΄βπ1) =
π΄) |
161 | 157, 158,
160 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π΄βπ(1 /
π))βππ) = π΄) |
162 | 153, 161 | breq12d 5162 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβππ) β€ ((π΄βπ(1 / π))βππ) β (πβπ) β€ π΄)) |
163 | 147, 150,
162 | 3bitrd 305 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β (0[,](π΄βπ(1 / π))) β§ π β β) β (πβπ) β€ π΄)) |
164 | 137, 163 | bitrid 283 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β ((0[,](π΄βπ(1 / π))) β© β) β (πβπ) β€ π΄)) |
165 | 136, 164 | anbi12d 632 |
. . . . . . . 8
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β
(1...(ββπ΄))
β§ π β ((0[,](π΄βπ(1 /
π))) β© β)) β
(π β€ π΄ β§ (πβπ) β€ π΄))) |
166 | 114 | nnred 12227 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβπ) β β) |
167 | | bernneq3 14194 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β2) β§ π β β0) β π < (πβπ)) |
168 | 105, 113,
167 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π < (πβπ)) |
169 | 121, 166,
168 | ltled 11362 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β€ (πβπ)) |
170 | | letr 11308 |
. . . . . . . . . . 11
β’ ((π β β β§ (πβπ) β β β§ π΄ β β) β ((π β€ (πβπ) β§ (πβπ) β€ π΄) β π β€ π΄)) |
171 | 121, 166,
91, 170 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β€ (πβπ) β§ (πβπ) β€ π΄) β π β€ π΄)) |
172 | 169, 171 | mpand 694 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β π β€ π΄)) |
173 | 172 | pm4.71rd 564 |
. . . . . . . 8
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β (π β€ π΄ β§ (πβπ) β€ π΄))) |
174 | 151 | exp1d 14106 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβ1) = π) |
175 | 92 | nnge1d 12260 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 1 β€ π) |
176 | 93, 175, 125 | leexp2ad 14217 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβ1) β€ (πβπ)) |
177 | 174, 176 | eqbrtrrd 5173 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β€ (πβπ)) |
178 | | letr 11308 |
. . . . . . . . . . 11
β’ ((π β β β§ (πβπ) β β β§ π΄ β β) β ((π β€ (πβπ) β§ (πβπ) β€ π΄) β π β€ π΄)) |
179 | 93, 166, 91, 178 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β€ (πβπ) β§ (πβπ) β€ π΄) β π β€ π΄)) |
180 | 177, 179 | mpand 694 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β π β€ π΄)) |
181 | 180 | pm4.71rd 564 |
. . . . . . . 8
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β (π β€ π΄ β§ (πβπ) β€ π΄))) |
182 | 165, 173,
181 | 3bitr2rd 308 |
. . . . . . 7
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β€ π΄ β§ (πβπ) β€ π΄) β (π β (1...(ββπ΄)) β§ π β ((0[,](π΄βπ(1 / π))) β©
β)))) |
183 | 130, 182 | bitrd 279 |
. . . . . 6
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β (1...(ββπ΄)) β§ π β ((0[,](π΄βπ(1 / π))) β©
β)))) |
184 | 183 | ex 414 |
. . . . 5
β’ (π΄ β β β (((π β β β§ π β β) β§ 0 <
π΄) β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β (1...(ββπ΄)) β§ π β ((0[,](π΄βπ(1 / π))) β©
β))))) |
185 | 80, 86, 184 | pm5.21ndd 381 |
. . . 4
β’ (π΄ β β β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β (1...(ββπ΄)) β§ π β ((0[,](π΄βπ(1 / π))) β©
β)))) |
186 | 8 | adantrr 716 |
. . . 4
β’ ((π΄ β β β§ (π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ)))))) β (logβπ) β
β) |
187 | 64, 65, 1, 185, 186 | fsumcom2 15720 |
. . 3
β’ (π΄ β β β
Ξ£π β ((0[,]π΄) β© β)Ξ£π β
(1...(ββ((logβπ΄) / (logβπ))))(logβπ) = Ξ£π β (1...(ββπ΄))Ξ£π β ((0[,](π΄βπ(1 / π))) β©
β)(logβπ)) |
188 | 63, 187 | eqtr4d 2776 |
. 2
β’ (π΄ β β β
Ξ£π β
(1...(ββπ΄))(ΞΈβ(π΄βπ(1 / π))) = Ξ£π β ((0[,]π΄) β© β)Ξ£π β (1...(ββ((logβπ΄) / (logβπ))))(logβπ)) |
189 | 39, 40, 188 | 3eqtr4d 2783 |
1
β’ (π΄ β β β
(Οβπ΄) =
Ξ£π β
(1...(ββπ΄))(ΞΈβ(π΄βπ(1 / π)))) |