Step |
Hyp |
Ref |
Expression |
1 |
|
rpcn |
|- ( A e. RR+ -> A e. CC ) |
2 |
1
|
times2d |
|- ( A e. RR+ -> ( A x. 2 ) = ( A + A ) ) |
3 |
2
|
oveq2d |
|- ( A e. RR+ -> ( ( A x. ( log ` A ) ) - ( A x. 2 ) ) = ( ( A x. ( log ` A ) ) - ( A + A ) ) ) |
4 |
|
relogcl |
|- ( A e. RR+ -> ( log ` A ) e. RR ) |
5 |
4
|
recnd |
|- ( A e. RR+ -> ( log ` A ) e. CC ) |
6 |
|
2cnd |
|- ( A e. RR+ -> 2 e. CC ) |
7 |
1 5 6
|
subdid |
|- ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) = ( ( A x. ( log ` A ) ) - ( A x. 2 ) ) ) |
8 |
|
rpre |
|- ( A e. RR+ -> A e. RR ) |
9 |
8 4
|
remulcld |
|- ( A e. RR+ -> ( A x. ( log ` A ) ) e. RR ) |
10 |
9
|
recnd |
|- ( A e. RR+ -> ( A x. ( log ` A ) ) e. CC ) |
11 |
10 1 1
|
subsub4d |
|- ( A e. RR+ -> ( ( ( A x. ( log ` A ) ) - A ) - A ) = ( ( A x. ( log ` A ) ) - ( A + A ) ) ) |
12 |
3 7 11
|
3eqtr4d |
|- ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) = ( ( ( A x. ( log ` A ) ) - A ) - A ) ) |
13 |
9 8
|
resubcld |
|- ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) e. RR ) |
14 |
|
fzfid |
|- ( A e. RR+ -> ( 1 ... ( |_ ` A ) ) e. Fin ) |
15 |
|
fzfid |
|- ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... n ) e. Fin ) |
16 |
|
elfznn |
|- ( d e. ( 1 ... n ) -> d e. NN ) |
17 |
16
|
adantl |
|- ( ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. ( 1 ... n ) ) -> d e. NN ) |
18 |
17
|
nnrecred |
|- ( ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. ( 1 ... n ) ) -> ( 1 / d ) e. RR ) |
19 |
15 18
|
fsumrecl |
|- ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> sum_ d e. ( 1 ... n ) ( 1 / d ) e. RR ) |
20 |
14 19
|
fsumrecl |
|- ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) e. RR ) |
21 |
|
rprege0 |
|- ( A e. RR+ -> ( A e. RR /\ 0 <_ A ) ) |
22 |
|
flge0nn0 |
|- ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 ) |
23 |
21 22
|
syl |
|- ( A e. RR+ -> ( |_ ` A ) e. NN0 ) |
24 |
23
|
faccld |
|- ( A e. RR+ -> ( ! ` ( |_ ` A ) ) e. NN ) |
25 |
24
|
nnrpd |
|- ( A e. RR+ -> ( ! ` ( |_ ` A ) ) e. RR+ ) |
26 |
25
|
relogcld |
|- ( A e. RR+ -> ( log ` ( ! ` ( |_ ` A ) ) ) e. RR ) |
27 |
26 8
|
readdcld |
|- ( A e. RR+ -> ( ( log ` ( ! ` ( |_ ` A ) ) ) + A ) e. RR ) |
28 |
|
elfznn |
|- ( d e. ( 1 ... ( |_ ` A ) ) -> d e. NN ) |
29 |
28
|
adantl |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. NN ) |
30 |
29
|
nnrecred |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / d ) e. RR ) |
31 |
14 30
|
fsumrecl |
|- ( A e. RR+ -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) e. RR ) |
32 |
8 31
|
remulcld |
|- ( A e. RR+ -> ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) e. RR ) |
33 |
|
reflcl |
|- ( A e. RR -> ( |_ ` A ) e. RR ) |
34 |
8 33
|
syl |
|- ( A e. RR+ -> ( |_ ` A ) e. RR ) |
35 |
32 34
|
resubcld |
|- ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) - ( |_ ` A ) ) e. RR ) |
36 |
|
harmoniclbnd |
|- ( A e. RR+ -> ( log ` A ) <_ sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) |
37 |
|
rpregt0 |
|- ( A e. RR+ -> ( A e. RR /\ 0 < A ) ) |
38 |
|
lemul2 |
|- ( ( ( log ` A ) e. RR /\ sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( log ` A ) <_ sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) <-> ( A x. ( log ` A ) ) <_ ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) ) ) |
39 |
4 31 37 38
|
syl3anc |
|- ( A e. RR+ -> ( ( log ` A ) <_ sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) <-> ( A x. ( log ` A ) ) <_ ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) ) ) |
40 |
36 39
|
mpbid |
|- ( A e. RR+ -> ( A x. ( log ` A ) ) <_ ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) ) |
41 |
|
flle |
|- ( A e. RR -> ( |_ ` A ) <_ A ) |
42 |
8 41
|
syl |
|- ( A e. RR+ -> ( |_ ` A ) <_ A ) |
43 |
9 34 32 8 40 42
|
le2subd |
|- ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) <_ ( ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) - ( |_ ` A ) ) ) |
44 |
28
|
nnrecred |
|- ( d e. ( 1 ... ( |_ ` A ) ) -> ( 1 / d ) e. RR ) |
45 |
|
remulcl |
|- ( ( A e. RR /\ ( 1 / d ) e. RR ) -> ( A x. ( 1 / d ) ) e. RR ) |
46 |
8 44 45
|
syl2an |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( A x. ( 1 / d ) ) e. RR ) |
47 |
|
peano2rem |
|- ( ( A x. ( 1 / d ) ) e. RR -> ( ( A x. ( 1 / d ) ) - 1 ) e. RR ) |
48 |
46 47
|
syl |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - 1 ) e. RR ) |
49 |
|
fzfid |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( d ... ( |_ ` A ) ) e. Fin ) |
50 |
30
|
adantr |
|- ( ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ n e. ( d ... ( |_ ` A ) ) ) -> ( 1 / d ) e. RR ) |
51 |
49 50
|
fsumrecl |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) e. RR ) |
52 |
8
|
adantr |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> A e. RR ) |
53 |
52 33
|
syl |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( |_ ` A ) e. RR ) |
54 |
|
peano2re |
|- ( ( |_ ` A ) e. RR -> ( ( |_ ` A ) + 1 ) e. RR ) |
55 |
53 54
|
syl |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( |_ ` A ) + 1 ) e. RR ) |
56 |
29
|
nnred |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. RR ) |
57 |
|
fllep1 |
|- ( A e. RR -> A <_ ( ( |_ ` A ) + 1 ) ) |
58 |
8 57
|
syl |
|- ( A e. RR+ -> A <_ ( ( |_ ` A ) + 1 ) ) |
59 |
58
|
adantr |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> A <_ ( ( |_ ` A ) + 1 ) ) |
60 |
52 55 56 59
|
lesub1dd |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( A - d ) <_ ( ( ( |_ ` A ) + 1 ) - d ) ) |
61 |
52 56
|
resubcld |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( A - d ) e. RR ) |
62 |
55 56
|
resubcld |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( ( |_ ` A ) + 1 ) - d ) e. RR ) |
63 |
29
|
nnrpd |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. RR+ ) |
64 |
63
|
rpreccld |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / d ) e. RR+ ) |
65 |
61 62 64
|
lemul1d |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A - d ) <_ ( ( ( |_ ` A ) + 1 ) - d ) <-> ( ( A - d ) x. ( 1 / d ) ) <_ ( ( ( ( |_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) ) ) |
66 |
60 65
|
mpbid |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A - d ) x. ( 1 / d ) ) <_ ( ( ( ( |_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) ) |
67 |
1
|
adantr |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> A e. CC ) |
68 |
29
|
nncnd |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. CC ) |
69 |
30
|
recnd |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / d ) e. CC ) |
70 |
67 68 69
|
subdird |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A - d ) x. ( 1 / d ) ) = ( ( A x. ( 1 / d ) ) - ( d x. ( 1 / d ) ) ) ) |
71 |
29
|
nnne0d |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d =/= 0 ) |
72 |
68 71
|
recidd |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( d x. ( 1 / d ) ) = 1 ) |
73 |
72
|
oveq2d |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - ( d x. ( 1 / d ) ) ) = ( ( A x. ( 1 / d ) ) - 1 ) ) |
74 |
70 73
|
eqtr2d |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - 1 ) = ( ( A - d ) x. ( 1 / d ) ) ) |
75 |
|
fsumconst |
|- ( ( ( d ... ( |_ ` A ) ) e. Fin /\ ( 1 / d ) e. CC ) -> sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) = ( ( # ` ( d ... ( |_ ` A ) ) ) x. ( 1 / d ) ) ) |
76 |
49 69 75
|
syl2anc |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) = ( ( # ` ( d ... ( |_ ` A ) ) ) x. ( 1 / d ) ) ) |
77 |
|
elfzuz3 |
|- ( d e. ( 1 ... ( |_ ` A ) ) -> ( |_ ` A ) e. ( ZZ>= ` d ) ) |
78 |
77
|
adantl |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( |_ ` A ) e. ( ZZ>= ` d ) ) |
79 |
|
hashfz |
|- ( ( |_ ` A ) e. ( ZZ>= ` d ) -> ( # ` ( d ... ( |_ ` A ) ) ) = ( ( ( |_ ` A ) - d ) + 1 ) ) |
80 |
78 79
|
syl |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( # ` ( d ... ( |_ ` A ) ) ) = ( ( ( |_ ` A ) - d ) + 1 ) ) |
81 |
34
|
recnd |
|- ( A e. RR+ -> ( |_ ` A ) e. CC ) |
82 |
81
|
adantr |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( |_ ` A ) e. CC ) |
83 |
|
1cnd |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> 1 e. CC ) |
84 |
82 83 68
|
addsubd |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( ( |_ ` A ) + 1 ) - d ) = ( ( ( |_ ` A ) - d ) + 1 ) ) |
85 |
80 84
|
eqtr4d |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( # ` ( d ... ( |_ ` A ) ) ) = ( ( ( |_ ` A ) + 1 ) - d ) ) |
86 |
85
|
oveq1d |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( # ` ( d ... ( |_ ` A ) ) ) x. ( 1 / d ) ) = ( ( ( ( |_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) ) |
87 |
76 86
|
eqtrd |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) = ( ( ( ( |_ ` A ) + 1 ) - d ) x. ( 1 / d ) ) ) |
88 |
66 74 87
|
3brtr4d |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A x. ( 1 / d ) ) - 1 ) <_ sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) ) |
89 |
14 48 51 88
|
fsumle |
|- ( A e. RR+ -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( A x. ( 1 / d ) ) - 1 ) <_ sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) ) |
90 |
14 1 69
|
fsummulc2 |
|- ( A e. RR+ -> ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( A x. ( 1 / d ) ) ) |
91 |
|
ax-1cn |
|- 1 e. CC |
92 |
|
fsumconst |
|- ( ( ( 1 ... ( |_ ` A ) ) e. Fin /\ 1 e. CC ) -> sum_ d e. ( 1 ... ( |_ ` A ) ) 1 = ( ( # ` ( 1 ... ( |_ ` A ) ) ) x. 1 ) ) |
93 |
14 91 92
|
sylancl |
|- ( A e. RR+ -> sum_ d e. ( 1 ... ( |_ ` A ) ) 1 = ( ( # ` ( 1 ... ( |_ ` A ) ) ) x. 1 ) ) |
94 |
|
hashfz1 |
|- ( ( |_ ` A ) e. NN0 -> ( # ` ( 1 ... ( |_ ` A ) ) ) = ( |_ ` A ) ) |
95 |
23 94
|
syl |
|- ( A e. RR+ -> ( # ` ( 1 ... ( |_ ` A ) ) ) = ( |_ ` A ) ) |
96 |
95
|
oveq1d |
|- ( A e. RR+ -> ( ( # ` ( 1 ... ( |_ ` A ) ) ) x. 1 ) = ( ( |_ ` A ) x. 1 ) ) |
97 |
81
|
mulid1d |
|- ( A e. RR+ -> ( ( |_ ` A ) x. 1 ) = ( |_ ` A ) ) |
98 |
93 96 97
|
3eqtrrd |
|- ( A e. RR+ -> ( |_ ` A ) = sum_ d e. ( 1 ... ( |_ ` A ) ) 1 ) |
99 |
90 98
|
oveq12d |
|- ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) - ( |_ ` A ) ) = ( sum_ d e. ( 1 ... ( |_ ` A ) ) ( A x. ( 1 / d ) ) - sum_ d e. ( 1 ... ( |_ ` A ) ) 1 ) ) |
100 |
46
|
recnd |
|- ( ( A e. RR+ /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( A x. ( 1 / d ) ) e. CC ) |
101 |
14 100 83
|
fsumsub |
|- ( A e. RR+ -> sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( A x. ( 1 / d ) ) - 1 ) = ( sum_ d e. ( 1 ... ( |_ ` A ) ) ( A x. ( 1 / d ) ) - sum_ d e. ( 1 ... ( |_ ` A ) ) 1 ) ) |
102 |
99 101
|
eqtr4d |
|- ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) - ( |_ ` A ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( A x. ( 1 / d ) ) - 1 ) ) |
103 |
|
eqid |
|- ( ZZ>= ` 1 ) = ( ZZ>= ` 1 ) |
104 |
103
|
uztrn2 |
|- ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) -> n e. ( ZZ>= ` 1 ) ) |
105 |
104
|
adantl |
|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> n e. ( ZZ>= ` 1 ) ) |
106 |
105
|
biantrurd |
|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( |_ ` A ) e. ( ZZ>= ` n ) <-> ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) ) |
107 |
|
uzss |
|- ( n e. ( ZZ>= ` d ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` d ) ) |
108 |
107
|
ad2antll |
|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` d ) ) |
109 |
108
|
sseld |
|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( |_ ` A ) e. ( ZZ>= ` n ) -> ( |_ ` A ) e. ( ZZ>= ` d ) ) ) |
110 |
109
|
pm4.71rd |
|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( |_ ` A ) e. ( ZZ>= ` n ) <-> ( ( |_ ` A ) e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) ) |
111 |
106 110
|
bitr3d |
|- ( ( A e. RR+ /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) -> ( ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) <-> ( ( |_ ` A ) e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) ) |
112 |
111
|
pm5.32da |
|- ( A e. RR+ -> ( ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( ( |_ ` A ) e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) ) ) |
113 |
|
ancom |
|- ( ( ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) ) |
114 |
|
an4 |
|- ( ( ( d e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) /\ ( ( |_ ` A ) e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) ) |
115 |
112 113 114
|
3bitr4g |
|- ( A e. RR+ -> ( ( ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) ) ) |
116 |
|
elfzuzb |
|- ( n e. ( 1 ... ( |_ ` A ) ) <-> ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) |
117 |
|
elfzuzb |
|- ( d e. ( 1 ... n ) <-> ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) |
118 |
116 117
|
anbi12i |
|- ( ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. ( 1 ... n ) ) <-> ( ( n e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) /\ ( d e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` d ) ) ) ) |
119 |
|
elfzuzb |
|- ( d e. ( 1 ... ( |_ ` A ) ) <-> ( d e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` d ) ) ) |
120 |
|
elfzuzb |
|- ( n e. ( d ... ( |_ ` A ) ) <-> ( n e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) |
121 |
119 120
|
anbi12i |
|- ( ( d e. ( 1 ... ( |_ ` A ) ) /\ n e. ( d ... ( |_ ` A ) ) ) <-> ( ( d e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` d ) ) /\ ( n e. ( ZZ>= ` d ) /\ ( |_ ` A ) e. ( ZZ>= ` n ) ) ) ) |
122 |
115 118 121
|
3bitr4g |
|- ( A e. RR+ -> ( ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. ( 1 ... n ) ) <-> ( d e. ( 1 ... ( |_ ` A ) ) /\ n e. ( d ... ( |_ ` A ) ) ) ) ) |
123 |
18
|
recnd |
|- ( ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. ( 1 ... n ) ) -> ( 1 / d ) e. CC ) |
124 |
123
|
anasss |
|- ( ( A e. RR+ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. ( 1 ... n ) ) ) -> ( 1 / d ) e. CC ) |
125 |
14 14 15 122 124
|
fsumcom2 |
|- ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) = sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ n e. ( d ... ( |_ ` A ) ) ( 1 / d ) ) |
126 |
89 102 125
|
3brtr4d |
|- ( A e. RR+ -> ( ( A x. sum_ d e. ( 1 ... ( |_ ` A ) ) ( 1 / d ) ) - ( |_ ` A ) ) <_ sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) ) |
127 |
13 35 20 43 126
|
letrd |
|- ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) <_ sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) ) |
128 |
26 34
|
readdcld |
|- ( A e. RR+ -> ( ( log ` ( ! ` ( |_ ` A ) ) ) + ( |_ ` A ) ) e. RR ) |
129 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN ) |
130 |
129
|
adantl |
|- ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN ) |
131 |
130
|
nnrpd |
|- ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. RR+ ) |
132 |
131
|
relogcld |
|- ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` n ) e. RR ) |
133 |
|
peano2re |
|- ( ( log ` n ) e. RR -> ( ( log ` n ) + 1 ) e. RR ) |
134 |
132 133
|
syl |
|- ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( log ` n ) + 1 ) e. RR ) |
135 |
|
nnz |
|- ( n e. NN -> n e. ZZ ) |
136 |
|
flid |
|- ( n e. ZZ -> ( |_ ` n ) = n ) |
137 |
135 136
|
syl |
|- ( n e. NN -> ( |_ ` n ) = n ) |
138 |
137
|
oveq2d |
|- ( n e. NN -> ( 1 ... ( |_ ` n ) ) = ( 1 ... n ) ) |
139 |
138
|
sumeq1d |
|- ( n e. NN -> sum_ d e. ( 1 ... ( |_ ` n ) ) ( 1 / d ) = sum_ d e. ( 1 ... n ) ( 1 / d ) ) |
140 |
|
nnre |
|- ( n e. NN -> n e. RR ) |
141 |
|
nnge1 |
|- ( n e. NN -> 1 <_ n ) |
142 |
|
harmonicubnd |
|- ( ( n e. RR /\ 1 <_ n ) -> sum_ d e. ( 1 ... ( |_ ` n ) ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) ) |
143 |
140 141 142
|
syl2anc |
|- ( n e. NN -> sum_ d e. ( 1 ... ( |_ ` n ) ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) ) |
144 |
139 143
|
eqbrtrrd |
|- ( n e. NN -> sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) ) |
145 |
130 144
|
syl |
|- ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` n ) + 1 ) ) |
146 |
14 19 134 145
|
fsumle |
|- ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) <_ sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) + 1 ) ) |
147 |
132
|
recnd |
|- ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` n ) e. CC ) |
148 |
|
1cnd |
|- ( ( A e. RR+ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> 1 e. CC ) |
149 |
14 147 148
|
fsumadd |
|- ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) + 1 ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) + sum_ n e. ( 1 ... ( |_ ` A ) ) 1 ) ) |
150 |
|
logfac |
|- ( ( |_ ` A ) e. NN0 -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) ) |
151 |
23 150
|
syl |
|- ( A e. RR+ -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) ) |
152 |
|
fsumconst |
|- ( ( ( 1 ... ( |_ ` A ) ) e. Fin /\ 1 e. CC ) -> sum_ n e. ( 1 ... ( |_ ` A ) ) 1 = ( ( # ` ( 1 ... ( |_ ` A ) ) ) x. 1 ) ) |
153 |
14 91 152
|
sylancl |
|- ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) 1 = ( ( # ` ( 1 ... ( |_ ` A ) ) ) x. 1 ) ) |
154 |
153 96 97
|
3eqtrrd |
|- ( A e. RR+ -> ( |_ ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) 1 ) |
155 |
151 154
|
oveq12d |
|- ( A e. RR+ -> ( ( log ` ( ! ` ( |_ ` A ) ) ) + ( |_ ` A ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) + sum_ n e. ( 1 ... ( |_ ` A ) ) 1 ) ) |
156 |
149 155
|
eqtr4d |
|- ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) + 1 ) = ( ( log ` ( ! ` ( |_ ` A ) ) ) + ( |_ ` A ) ) ) |
157 |
146 156
|
breqtrd |
|- ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` ( ! ` ( |_ ` A ) ) ) + ( |_ ` A ) ) ) |
158 |
34 8 26 42
|
leadd2dd |
|- ( A e. RR+ -> ( ( log ` ( ! ` ( |_ ` A ) ) ) + ( |_ ` A ) ) <_ ( ( log ` ( ! ` ( |_ ` A ) ) ) + A ) ) |
159 |
20 128 27 157 158
|
letrd |
|- ( A e. RR+ -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. ( 1 ... n ) ( 1 / d ) <_ ( ( log ` ( ! ` ( |_ ` A ) ) ) + A ) ) |
160 |
13 20 27 127 159
|
letrd |
|- ( A e. RR+ -> ( ( A x. ( log ` A ) ) - A ) <_ ( ( log ` ( ! ` ( |_ ` A ) ) ) + A ) ) |
161 |
13 8 26
|
lesubaddd |
|- ( A e. RR+ -> ( ( ( ( A x. ( log ` A ) ) - A ) - A ) <_ ( log ` ( ! ` ( |_ ` A ) ) ) <-> ( ( A x. ( log ` A ) ) - A ) <_ ( ( log ` ( ! ` ( |_ ` A ) ) ) + A ) ) ) |
162 |
160 161
|
mpbird |
|- ( A e. RR+ -> ( ( ( A x. ( log ` A ) ) - A ) - A ) <_ ( log ` ( ! ` ( |_ ` A ) ) ) ) |
163 |
12 162
|
eqbrtrd |
|- ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) <_ ( log ` ( ! ` ( |_ ` A ) ) ) ) |