Step | Hyp | Ref
| Expression |
1 | | fzfid 13937 |
. . . . 5
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
(1...(ββ((logβπ΄) / (logβπ)))) β Fin) |
2 | | simpr 485 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β ((0[,]π΄) β© β)) |
3 | 2 | elin2d 4199 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
4 | | prmnn 16610 |
. . . . . . . . 9
β’ (π β β β π β
β) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
6 | 5 | nnrpd 13013 |
. . . . . . 7
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β+) |
7 | 6 | relogcld 26130 |
. . . . . 6
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (logβπ) β
β) |
8 | 7 | recnd 11241 |
. . . . 5
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (logβπ) β
β) |
9 | | fsumconst 15735 |
. . . . 5
β’
(((1...(ββ((logβπ΄) / (logβπ)))) β Fin β§ (logβπ) β β) β
Ξ£π β
(1...(ββ((logβπ΄) / (logβπ))))(logβπ) =
((β―β(1...(ββ((logβπ΄) / (logβπ))))) Β· (logβπ))) |
10 | 1, 8, 9 | syl2anc 584 |
. . . 4
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β Ξ£π β
(1...(ββ((logβπ΄) / (logβπ))))(logβπ) =
((β―β(1...(ββ((logβπ΄) / (logβπ))))) Β· (logβπ))) |
11 | | simpl 483 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π΄ β β) |
12 | | 1red 11214 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 1 β
β) |
13 | 5 | nnred 12226 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
14 | | prmuz2 16632 |
. . . . . . . . . . . . 13
β’ (π β β β π β
(β€β₯β2)) |
15 | 3, 14 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β
(β€β₯β2)) |
16 | | eluz2gt1 12903 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β2) β 1 < π) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 1 < π) |
18 | 2 | elin1d 4198 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β (0[,]π΄)) |
19 | | 0re 11215 |
. . . . . . . . . . . . . 14
β’ 0 β
β |
20 | | elicc2 13388 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ π΄
β β) β (π
β (0[,]π΄) β
(π β β β§ 0
β€ π β§ π β€ π΄))) |
21 | 19, 11, 20 | sylancr 587 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (π β (0[,]π΄) β (π β β β§ 0 β€ π β§ π β€ π΄))) |
22 | 18, 21 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (π β β β§ 0 β€ π β§ π β€ π΄)) |
23 | 22 | simp3d 1144 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β€ π΄) |
24 | 12, 13, 11, 17, 23 | ltletrd 11373 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 1 < π΄) |
25 | 11, 24 | rplogcld 26136 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (logβπ΄) β
β+) |
26 | 13, 17 | rplogcld 26136 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β (logβπ) β
β+) |
27 | 25, 26 | rpdivcld 13032 |
. . . . . . . 8
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β ((logβπ΄) / (logβπ)) β
β+) |
28 | 27 | rpred 13015 |
. . . . . . 7
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β ((logβπ΄) / (logβπ)) β
β) |
29 | 27 | rpge0d 13019 |
. . . . . . 7
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 0 β€
((logβπ΄) /
(logβπ))) |
30 | | flge0nn0 13784 |
. . . . . . 7
β’
((((logβπ΄) /
(logβπ)) β
β β§ 0 β€ ((logβπ΄) / (logβπ))) β (ββ((logβπ΄) / (logβπ))) β
β0) |
31 | 28, 29, 30 | syl2anc 584 |
. . . . . 6
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
(ββ((logβπ΄) / (logβπ))) β
β0) |
32 | | hashfz1 14305 |
. . . . . 6
β’
((ββ((logβπ΄) / (logβπ))) β β0 β
(β―β(1...(ββ((logβπ΄) / (logβπ))))) = (ββ((logβπ΄) / (logβπ)))) |
33 | 31, 32 | syl 17 |
. . . . 5
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
(β―β(1...(ββ((logβπ΄) / (logβπ))))) = (ββ((logβπ΄) / (logβπ)))) |
34 | 33 | oveq1d 7423 |
. . . 4
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
((β―β(1...(ββ((logβπ΄) / (logβπ))))) Β· (logβπ)) = ((ββ((logβπ΄) / (logβπ))) Β· (logβπ))) |
35 | 28 | flcld 13762 |
. . . . . 6
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
(ββ((logβπ΄) / (logβπ))) β β€) |
36 | 35 | zcnd 12666 |
. . . . 5
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
(ββ((logβπ΄) / (logβπ))) β β) |
37 | 36, 8 | mulcomd 11234 |
. . . 4
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β
((ββ((logβπ΄) / (logβπ))) Β· (logβπ)) = ((logβπ) Β· (ββ((logβπ΄) / (logβπ))))) |
38 | 10, 34, 37 | 3eqtrrd 2777 |
. . 3
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β ((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) = Ξ£π β (1...(ββ((logβπ΄) / (logβπ))))(logβπ)) |
39 | 38 | sumeq2dv 15648 |
. 2
β’ (π΄ β β β
Ξ£π β ((0[,]π΄) β©
β)((logβπ)
Β· (ββ((logβπ΄) / (logβπ)))) = Ξ£π β ((0[,]π΄) β© β)Ξ£π β (1...(ββ((logβπ΄) / (logβπ))))(logβπ)) |
40 | | chpval2 26718 |
. 2
β’ (π΄ β β β
(Οβπ΄) =
Ξ£π β ((0[,]π΄) β©
β)((logβπ)
Β· (ββ((logβπ΄) / (logβπ))))) |
41 | | simpl 483 |
. . . . . 6
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β π΄ β
β) |
42 | | 0red 11216 |
. . . . . . 7
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 0 β β) |
43 | | 1red 11214 |
. . . . . . . 8
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 1 β β) |
44 | | 0lt1 11735 |
. . . . . . . . 9
β’ 0 <
1 |
45 | 44 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 0 < 1) |
46 | | elfzuz2 13505 |
. . . . . . . . 9
β’ (π β
(1...(ββπ΄))
β (ββπ΄)
β (β€β₯β1)) |
47 | | eluzle 12834 |
. . . . . . . . . . 11
β’
((ββπ΄)
β (β€β₯β1) β 1 β€ (ββπ΄)) |
48 | 47 | adantl 482 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(β€β₯β1)) β 1 β€ (ββπ΄)) |
49 | | simpl 483 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(β€β₯β1)) β π΄ β β) |
50 | | 1z 12591 |
. . . . . . . . . . 11
β’ 1 β
β€ |
51 | | flge 13769 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ 1 β
β€) β (1 β€ π΄
β 1 β€ (ββπ΄))) |
52 | 49, 50, 51 | sylancl 586 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β
(β€β₯β1)) β (1 β€ π΄ β 1 β€ (ββπ΄))) |
53 | 48, 52 | mpbird 256 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β
(β€β₯β1)) β 1 β€ π΄) |
54 | 46, 53 | sylan2 593 |
. . . . . . . 8
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 1 β€ π΄) |
55 | 42, 43, 41, 45, 54 | ltletrd 11373 |
. . . . . . 7
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 0 < π΄) |
56 | 42, 41, 55 | ltled 11361 |
. . . . . 6
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β 0 β€ π΄) |
57 | | elfznn 13529 |
. . . . . . . 8
β’ (π β
(1...(ββπ΄))
β π β
β) |
58 | 57 | adantl 482 |
. . . . . . 7
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β π β
β) |
59 | 58 | nnrecred 12262 |
. . . . . 6
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β (1 / π) β
β) |
60 | 41, 56, 59 | recxpcld 26230 |
. . . . 5
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β (π΄βπ(1 / π)) β
β) |
61 | | chtval 26611 |
. . . . 5
β’ ((π΄βπ(1 /
π)) β β β
(ΞΈβ(π΄βπ(1 / π))) = Ξ£π β ((0[,](π΄βπ(1 / π))) β©
β)(logβπ)) |
62 | 60, 61 | syl 17 |
. . . 4
β’ ((π΄ β β β§ π β
(1...(ββπ΄)))
β (ΞΈβ(π΄βπ(1 / π))) = Ξ£π β ((0[,](π΄βπ(1 / π))) β©
β)(logβπ)) |
63 | 62 | sumeq2dv 15648 |
. . 3
β’ (π΄ β β β
Ξ£π β
(1...(ββπ΄))(ΞΈβ(π΄βπ(1 / π))) = Ξ£π β (1...(ββπ΄))Ξ£π β ((0[,](π΄βπ(1 / π))) β©
β)(logβπ)) |
64 | | ppifi 26607 |
. . . 4
β’ (π΄ β β β
((0[,]π΄) β© β)
β Fin) |
65 | | fzfid 13937 |
. . . 4
β’ (π΄ β β β
(1...(ββπ΄))
β Fin) |
66 | | elinel2 4196 |
. . . . . . . 8
β’ (π β ((0[,]π΄) β© β) β π β β) |
67 | | elfznn 13529 |
. . . . . . . 8
β’ (π β
(1...(ββ((logβπ΄) / (logβπ)))) β π β β) |
68 | 66, 67 | anim12i 613 |
. . . . . . 7
β’ ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β β β§ π β β)) |
69 | 68 | a1i 11 |
. . . . . 6
β’ (π΄ β β β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β β β§ π β β))) |
70 | | 0red 11216 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 0 β
β) |
71 | | inss2 4229 |
. . . . . . . . . . . . 13
β’
((0[,]π΄) β©
β) β β |
72 | 71 | a1i 11 |
. . . . . . . . . . . 12
β’ (π΄ β β β
((0[,]π΄) β© β)
β β) |
73 | 72 | sselda 3982 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
74 | 73, 4 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
75 | 74 | nnred 12226 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β π β β) |
76 | 74 | nngt0d 12260 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 0 < π) |
77 | 70, 75, 11, 76, 23 | ltletrd 11373 |
. . . . . . . 8
β’ ((π΄ β β β§ π β ((0[,]π΄) β© β)) β 0 < π΄) |
78 | 77 | ex 413 |
. . . . . . 7
β’ (π΄ β β β (π β ((0[,]π΄) β© β) β 0 < π΄)) |
79 | 78 | adantrd 492 |
. . . . . 6
β’ (π΄ β β β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β 0 < π΄)) |
80 | 69, 79 | jcad 513 |
. . . . 5
β’ (π΄ β β β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β ((π β β β§ π β β) β§ 0 <
π΄))) |
81 | | elinel2 4196 |
. . . . . . . 8
β’ (π β ((0[,](π΄βπ(1 / π))) β© β) β π β
β) |
82 | 57, 81 | anim12ci 614 |
. . . . . . 7
β’ ((π β
(1...(ββπ΄))
β§ π β ((0[,](π΄βπ(1 /
π))) β© β)) β
(π β β β§
π β
β)) |
83 | 82 | a1i 11 |
. . . . . 6
β’ (π΄ β β β ((π β
(1...(ββπ΄))
β§ π β ((0[,](π΄βπ(1 /
π))) β© β)) β
(π β β β§
π β
β))) |
84 | 55 | ex 413 |
. . . . . . 7
β’ (π΄ β β β (π β
(1...(ββπ΄))
β 0 < π΄)) |
85 | 84 | adantrd 492 |
. . . . . 6
β’ (π΄ β β β ((π β
(1...(ββπ΄))
β§ π β ((0[,](π΄βπ(1 /
π))) β© β)) β
0 < π΄)) |
86 | 83, 85 | jcad 513 |
. . . . 5
β’ (π΄ β β β ((π β
(1...(ββπ΄))
β§ π β ((0[,](π΄βπ(1 /
π))) β© β)) β
((π β β β§
π β β) β§ 0
< π΄))) |
87 | | elin 3964 |
. . . . . . . . 9
β’ (π β ((0[,]π΄) β© β) β (π β (0[,]π΄) β§ π β β)) |
88 | | simprll 777 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
89 | 88 | biantrud 532 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β (0[,]π΄) β (π β (0[,]π΄) β§ π β β))) |
90 | | 0red 11216 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 0 β
β) |
91 | | simpl 483 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π΄ β
β) |
92 | 88, 4 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
93 | 92 | nnred 12226 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
94 | 92 | nnnn0d 12531 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β0) |
95 | 94 | nn0ge0d 12534 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 0 β€ π) |
96 | | df-3an 1089 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 0 β€
π β§ π β€ π΄) β ((π β β β§ 0 β€ π) β§ π β€ π΄)) |
97 | 20, 96 | bitrdi 286 |
. . . . . . . . . . . 12
β’ ((0
β β β§ π΄
β β) β (π
β (0[,]π΄) β
((π β β β§ 0
β€ π) β§ π β€ π΄))) |
98 | 97 | baibd 540 |
. . . . . . . . . . 11
β’ (((0
β β β§ π΄
β β) β§ (π
β β β§ 0 β€ π)) β (π β (0[,]π΄) β π β€ π΄)) |
99 | 90, 91, 93, 95, 98 | syl22anc 837 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β (0[,]π΄) β π β€ π΄)) |
100 | 89, 99 | bitr3d 280 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β (0[,]π΄) β§ π β β) β π β€ π΄)) |
101 | 87, 100 | bitrid 282 |
. . . . . . . 8
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β ((0[,]π΄) β© β) β π β€ π΄)) |
102 | | simprr 771 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 0 < π΄) |
103 | 91, 102 | elrpd 13012 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π΄ β
β+) |
104 | 103 | relogcld 26130 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (logβπ΄) β
β) |
105 | 88, 14 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
(β€β₯β2)) |
106 | 105, 16 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 1 < π) |
107 | 93, 106 | rplogcld 26136 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (logβπ) β
β+) |
108 | 104, 107 | rerpdivcld 13046 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β
((logβπ΄) /
(logβπ)) β
β) |
109 | | simprlr 778 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
110 | 109 | nnzd 12584 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β€) |
111 | | flge 13769 |
. . . . . . . . . 10
β’
((((logβπ΄) /
(logβπ)) β
β β§ π β
β€) β (π β€
((logβπ΄) /
(logβπ)) β π β€
(ββ((logβπ΄) / (logβπ))))) |
112 | 108, 110,
111 | syl2anc 584 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β€ ((logβπ΄) / (logβπ)) β π β€ (ββ((logβπ΄) / (logβπ))))) |
113 | 109 | nnnn0d 12531 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β0) |
114 | 92, 113 | nnexpcld 14207 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβπ) β β) |
115 | 114 | nnrpd 13013 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβπ) β
β+) |
116 | 115, 103 | logled 26134 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β (logβ(πβπ)) β€ (logβπ΄))) |
117 | 92 | nnrpd 13013 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β+) |
118 | | relogexp 26103 |
. . . . . . . . . . . 12
β’ ((π β β+
β§ π β β€)
β (logβ(πβπ)) = (π Β· (logβπ))) |
119 | 117, 110,
118 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β
(logβ(πβπ)) = (π Β· (logβπ))) |
120 | 119 | breq1d 5158 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β
((logβ(πβπ)) β€ (logβπ΄) β (π Β· (logβπ)) β€ (logβπ΄))) |
121 | 109 | nnred 12226 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
122 | 121, 104,
107 | lemuldivd 13064 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π Β· (logβπ)) β€ (logβπ΄) β π β€ ((logβπ΄) / (logβπ)))) |
123 | 116, 120,
122 | 3bitrd 304 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β π β€ ((logβπ΄) / (logβπ)))) |
124 | | nnuz 12864 |
. . . . . . . . . . 11
β’ β =
(β€β₯β1) |
125 | 109, 124 | eleqtrdi 2843 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
(β€β₯β1)) |
126 | 108 | flcld 13762 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β
(ββ((logβπ΄) / (logβπ))) β β€) |
127 | | elfz5 13492 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β1) β§ (ββ((logβπ΄) / (logβπ))) β β€) β
(π β
(1...(ββ((logβπ΄) / (logβπ)))) β π β€ (ββ((logβπ΄) / (logβπ))))) |
128 | 125, 126,
127 | syl2anc 584 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β
(1...(ββ((logβπ΄) / (logβπ)))) β π β€ (ββ((logβπ΄) / (logβπ))))) |
129 | 112, 123,
128 | 3bitr4rd 311 |
. . . . . . . 8
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β
(1...(ββ((logβπ΄) / (logβπ)))) β (πβπ) β€ π΄)) |
130 | 101, 129 | anbi12d 631 |
. . . . . . 7
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β€ π΄ β§ (πβπ) β€ π΄))) |
131 | 91 | flcld 13762 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β
(ββπ΄) β
β€) |
132 | | elfz5 13492 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯β1) β§ (ββπ΄) β β€) β (π β (1...(ββπ΄)) β π β€ (ββπ΄))) |
133 | 125, 131,
132 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β
(1...(ββπ΄))
β π β€
(ββπ΄))) |
134 | | flge 13769 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π β β€) β (π β€ π΄ β π β€ (ββπ΄))) |
135 | 91, 110, 134 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β€ π΄ β π β€ (ββπ΄))) |
136 | 133, 135 | bitr4d 281 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β
(1...(ββπ΄))
β π β€ π΄)) |
137 | | elin 3964 |
. . . . . . . . . 10
β’ (π β ((0[,](π΄βπ(1 / π))) β© β) β (π β (0[,](π΄βπ(1 / π))) β§ π β β)) |
138 | 88 | biantrud 532 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β (0[,](π΄βπ(1 / π))) β (π β (0[,](π΄βπ(1 / π))) β§ π β β))) |
139 | 103 | rpge0d 13019 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 0 β€ π΄) |
140 | 109 | nnrecred 12262 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (1 / π) β
β) |
141 | 91, 139, 140 | recxpcld 26230 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π΄βπ(1 /
π)) β
β) |
142 | | elicc2 13388 |
. . . . . . . . . . . . . . 15
β’ ((0
β β β§ (π΄βπ(1 / π)) β β) β (π β (0[,](π΄βπ(1 / π))) β (π β β β§ 0 β€ π β§ π β€ (π΄βπ(1 / π))))) |
143 | | df-3an 1089 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ 0 β€
π β§ π β€ (π΄βπ(1 / π))) β ((π β β β§ 0 β€ π) β§ π β€ (π΄βπ(1 / π)))) |
144 | 142, 143 | bitrdi 286 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ (π΄βπ(1 / π)) β β) β (π β (0[,](π΄βπ(1 / π))) β ((π β β β§ 0 β€ π) β§ π β€ (π΄βπ(1 / π))))) |
145 | 144 | baibd 540 |
. . . . . . . . . . . . 13
β’ (((0
β β β§ (π΄βπ(1 / π)) β β) β§ (π β β β§ 0 β€
π)) β (π β (0[,](π΄βπ(1 / π))) β π β€ (π΄βπ(1 / π)))) |
146 | 90, 141, 93, 95, 145 | syl22anc 837 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β (0[,](π΄βπ(1 / π))) β π β€ (π΄βπ(1 / π)))) |
147 | 138, 146 | bitr3d 280 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β (0[,](π΄βπ(1 / π))) β§ π β β) β π β€ (π΄βπ(1 / π)))) |
148 | 91, 139, 140 | cxpge0d 26231 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 0 β€ (π΄βπ(1 /
π))) |
149 | 109 | nnrpd 13013 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β+) |
150 | 93, 95, 141, 148, 149 | cxple2d 26234 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β€ (π΄βπ(1 / π)) β (πβππ) β€ ((π΄βπ(1 / π))βππ))) |
151 | 92 | nncnd 12227 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
152 | | cxpexp 26175 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β0)
β (πβππ) = (πβπ)) |
153 | 151, 113,
152 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβππ) = (πβπ)) |
154 | 109 | nncnd 12227 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β
β) |
155 | 109 | nnne0d 12261 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β 0) |
156 | 154, 155 | recid2d 11985 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((1 / π) Β· π) = 1) |
157 | 156 | oveq2d 7424 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π΄βπ((1 /
π) Β· π)) = (π΄βπ1)) |
158 | 103, 140,
154 | cxpmuld 26243 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π΄βπ((1 /
π) Β· π)) = ((π΄βπ(1 / π))βππ)) |
159 | 91 | recnd 11241 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π΄ β
β) |
160 | 159 | cxp1d 26213 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π΄βπ1) =
π΄) |
161 | 157, 158,
160 | 3eqtr3d 2780 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π΄βπ(1 /
π))βππ) = π΄) |
162 | 153, 161 | breq12d 5161 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβππ) β€ ((π΄βπ(1 / π))βππ) β (πβπ) β€ π΄)) |
163 | 147, 150,
162 | 3bitrd 304 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β (0[,](π΄βπ(1 / π))) β§ π β β) β (πβπ) β€ π΄)) |
164 | 137, 163 | bitrid 282 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (π β ((0[,](π΄βπ(1 / π))) β© β) β (πβπ) β€ π΄)) |
165 | 136, 164 | anbi12d 631 |
. . . . . . . 8
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β
(1...(ββπ΄))
β§ π β ((0[,](π΄βπ(1 /
π))) β© β)) β
(π β€ π΄ β§ (πβπ) β€ π΄))) |
166 | 114 | nnred 12226 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβπ) β β) |
167 | | bernneq3 14193 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β2) β§ π β β0) β π < (πβπ)) |
168 | 105, 113,
167 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π < (πβπ)) |
169 | 121, 166,
168 | ltled 11361 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β€ (πβπ)) |
170 | | letr 11307 |
. . . . . . . . . . 11
β’ ((π β β β§ (πβπ) β β β§ π΄ β β) β ((π β€ (πβπ) β§ (πβπ) β€ π΄) β π β€ π΄)) |
171 | 121, 166,
91, 170 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β€ (πβπ) β§ (πβπ) β€ π΄) β π β€ π΄)) |
172 | 169, 171 | mpand 693 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β π β€ π΄)) |
173 | 172 | pm4.71rd 563 |
. . . . . . . 8
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β (π β€ π΄ β§ (πβπ) β€ π΄))) |
174 | 151 | exp1d 14105 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβ1) = π) |
175 | 92 | nnge1d 12259 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β 1 β€ π) |
176 | 93, 175, 125 | leexp2ad 14216 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β (πβ1) β€ (πβπ)) |
177 | 174, 176 | eqbrtrrd 5172 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β π β€ (πβπ)) |
178 | | letr 11307 |
. . . . . . . . . . 11
β’ ((π β β β§ (πβπ) β β β§ π΄ β β) β ((π β€ (πβπ) β§ (πβπ) β€ π΄) β π β€ π΄)) |
179 | 93, 166, 91, 178 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β€ (πβπ) β§ (πβπ) β€ π΄) β π β€ π΄)) |
180 | 177, 179 | mpand 693 |
. . . . . . . . 9
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β π β€ π΄)) |
181 | 180 | pm4.71rd 563 |
. . . . . . . 8
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((πβπ) β€ π΄ β (π β€ π΄ β§ (πβπ) β€ π΄))) |
182 | 165, 173,
181 | 3bitr2rd 307 |
. . . . . . 7
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β€ π΄ β§ (πβπ) β€ π΄) β (π β (1...(ββπ΄)) β§ π β ((0[,](π΄βπ(1 / π))) β©
β)))) |
183 | 130, 182 | bitrd 278 |
. . . . . 6
β’ ((π΄ β β β§ ((π β β β§ π β β) β§ 0 <
π΄)) β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β (1...(ββπ΄)) β§ π β ((0[,](π΄βπ(1 / π))) β©
β)))) |
184 | 183 | ex 413 |
. . . . 5
β’ (π΄ β β β (((π β β β§ π β β) β§ 0 <
π΄) β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β (1...(ββπ΄)) β§ π β ((0[,](π΄βπ(1 / π))) β©
β))))) |
185 | 80, 86, 184 | pm5.21ndd 380 |
. . . 4
β’ (π΄ β β β ((π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ))))) β (π β (1...(ββπ΄)) β§ π β ((0[,](π΄βπ(1 / π))) β©
β)))) |
186 | 8 | adantrr 715 |
. . . 4
β’ ((π΄ β β β§ (π β ((0[,]π΄) β© β) β§ π β (1...(ββ((logβπ΄) / (logβπ)))))) β (logβπ) β
β) |
187 | 64, 65, 1, 185, 186 | fsumcom2 15719 |
. . 3
β’ (π΄ β β β
Ξ£π β ((0[,]π΄) β© β)Ξ£π β
(1...(ββ((logβπ΄) / (logβπ))))(logβπ) = Ξ£π β (1...(ββπ΄))Ξ£π β ((0[,](π΄βπ(1 / π))) β©
β)(logβπ)) |
188 | 63, 187 | eqtr4d 2775 |
. 2
β’ (π΄ β β β
Ξ£π β
(1...(ββπ΄))(ΞΈβ(π΄βπ(1 / π))) = Ξ£π β ((0[,]π΄) β© β)Ξ£π β (1...(ββ((logβπ΄) / (logβπ))))(logβπ)) |
189 | 39, 40, 188 | 3eqtr4d 2782 |
1
β’ (π΄ β β β
(Οβπ΄) =
Ξ£π β
(1...(ββπ΄))(ΞΈβ(π΄βπ(1 / π)))) |