Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> A e. RR+ ) |
2 |
1
|
rprege0d |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( A e. RR /\ 0 <_ A ) ) |
3 |
|
flge0nn0 |
|- ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 ) |
4 |
2 3
|
syl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( |_ ` A ) e. NN0 ) |
5 |
4
|
faccld |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ! ` ( |_ ` A ) ) e. NN ) |
6 |
5
|
nnrpd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ! ` ( |_ ` A ) ) e. RR+ ) |
7 |
|
relogcl |
|- ( ( ! ` ( |_ ` A ) ) e. RR+ -> ( log ` ( ! ` ( |_ ` A ) ) ) e. RR ) |
8 |
6 7
|
syl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( log ` ( ! ` ( |_ ` A ) ) ) e. RR ) |
9 |
|
rpre |
|- ( A e. RR+ -> A e. RR ) |
10 |
9
|
adantr |
|- ( ( A e. RR+ /\ 1 <_ A ) -> A e. RR ) |
11 |
|
relogcl |
|- ( A e. RR+ -> ( log ` A ) e. RR ) |
12 |
11
|
adantr |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( log ` A ) e. RR ) |
13 |
|
peano2rem |
|- ( ( log ` A ) e. RR -> ( ( log ` A ) - 1 ) e. RR ) |
14 |
12 13
|
syl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( log ` A ) - 1 ) e. RR ) |
15 |
10 14
|
remulcld |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( A x. ( ( log ` A ) - 1 ) ) e. RR ) |
16 |
8 15
|
resubcld |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) e. RR ) |
17 |
16
|
recnd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) e. CC ) |
18 |
17
|
abscld |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) e. RR ) |
19 |
|
peano2rem |
|- ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) e. RR -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 ) e. RR ) |
20 |
18 19
|
syl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 ) e. RR ) |
21 |
|
ax-1cn |
|- 1 e. CC |
22 |
|
subcl |
|- ( ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) e. CC /\ 1 e. CC ) -> ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) e. CC ) |
23 |
17 21 22
|
sylancl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) e. CC ) |
24 |
23
|
abscld |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) e. RR ) |
25 |
|
abs1 |
|- ( abs ` 1 ) = 1 |
26 |
25
|
oveq2i |
|- ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - ( abs ` 1 ) ) = ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 ) |
27 |
|
abs2dif |
|- ( ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) e. CC /\ 1 e. CC ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - ( abs ` 1 ) ) <_ ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) ) |
28 |
17 21 27
|
sylancl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - ( abs ` 1 ) ) <_ ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) ) |
29 |
26 28
|
eqbrtrrid |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 ) <_ ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) ) |
30 |
|
fveq2 |
|- ( x = A -> ( |_ ` x ) = ( |_ ` A ) ) |
31 |
30
|
oveq2d |
|- ( x = A -> ( 1 ... ( |_ ` x ) ) = ( 1 ... ( |_ ` A ) ) ) |
32 |
31
|
sumeq1d |
|- ( x = A -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) ) |
33 |
|
id |
|- ( x = A -> x = A ) |
34 |
|
fveq2 |
|- ( x = A -> ( log ` x ) = ( log ` A ) ) |
35 |
34
|
oveq1d |
|- ( x = A -> ( ( log ` x ) - 1 ) = ( ( log ` A ) - 1 ) ) |
36 |
33 35
|
oveq12d |
|- ( x = A -> ( x x. ( ( log ` x ) - 1 ) ) = ( A x. ( ( log ` A ) - 1 ) ) ) |
37 |
32 36
|
oveq12d |
|- ( x = A -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) |
38 |
|
eqid |
|- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) |
39 |
|
ovex |
|- ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) e. _V |
40 |
37 38 39
|
fvmpt3i |
|- ( A e. RR+ -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) |
41 |
40
|
adantr |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) |
42 |
|
logfac |
|- ( ( |_ ` A ) e. NN0 -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) ) |
43 |
4 42
|
syl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) ) |
44 |
43
|
oveq1d |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) |
45 |
41 44
|
eqtr4d |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) = ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) |
46 |
|
1rp |
|- 1 e. RR+ |
47 |
|
fveq2 |
|- ( x = 1 -> ( |_ ` x ) = ( |_ ` 1 ) ) |
48 |
|
1z |
|- 1 e. ZZ |
49 |
|
flid |
|- ( 1 e. ZZ -> ( |_ ` 1 ) = 1 ) |
50 |
48 49
|
ax-mp |
|- ( |_ ` 1 ) = 1 |
51 |
47 50
|
eqtrdi |
|- ( x = 1 -> ( |_ ` x ) = 1 ) |
52 |
51
|
oveq2d |
|- ( x = 1 -> ( 1 ... ( |_ ` x ) ) = ( 1 ... 1 ) ) |
53 |
52
|
sumeq1d |
|- ( x = 1 -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) = sum_ n e. ( 1 ... 1 ) ( log ` n ) ) |
54 |
|
0cn |
|- 0 e. CC |
55 |
|
fveq2 |
|- ( n = 1 -> ( log ` n ) = ( log ` 1 ) ) |
56 |
|
log1 |
|- ( log ` 1 ) = 0 |
57 |
55 56
|
eqtrdi |
|- ( n = 1 -> ( log ` n ) = 0 ) |
58 |
57
|
fsum1 |
|- ( ( 1 e. ZZ /\ 0 e. CC ) -> sum_ n e. ( 1 ... 1 ) ( log ` n ) = 0 ) |
59 |
48 54 58
|
mp2an |
|- sum_ n e. ( 1 ... 1 ) ( log ` n ) = 0 |
60 |
53 59
|
eqtrdi |
|- ( x = 1 -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) = 0 ) |
61 |
|
id |
|- ( x = 1 -> x = 1 ) |
62 |
|
fveq2 |
|- ( x = 1 -> ( log ` x ) = ( log ` 1 ) ) |
63 |
62 56
|
eqtrdi |
|- ( x = 1 -> ( log ` x ) = 0 ) |
64 |
63
|
oveq1d |
|- ( x = 1 -> ( ( log ` x ) - 1 ) = ( 0 - 1 ) ) |
65 |
61 64
|
oveq12d |
|- ( x = 1 -> ( x x. ( ( log ` x ) - 1 ) ) = ( 1 x. ( 0 - 1 ) ) ) |
66 |
54 21
|
subcli |
|- ( 0 - 1 ) e. CC |
67 |
66
|
mulid2i |
|- ( 1 x. ( 0 - 1 ) ) = ( 0 - 1 ) |
68 |
65 67
|
eqtrdi |
|- ( x = 1 -> ( x x. ( ( log ` x ) - 1 ) ) = ( 0 - 1 ) ) |
69 |
60 68
|
oveq12d |
|- ( x = 1 -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) = ( 0 - ( 0 - 1 ) ) ) |
70 |
|
nncan |
|- ( ( 0 e. CC /\ 1 e. CC ) -> ( 0 - ( 0 - 1 ) ) = 1 ) |
71 |
54 21 70
|
mp2an |
|- ( 0 - ( 0 - 1 ) ) = 1 |
72 |
69 71
|
eqtrdi |
|- ( x = 1 -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) = 1 ) |
73 |
72 38 39
|
fvmpt3i |
|- ( 1 e. RR+ -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` 1 ) = 1 ) |
74 |
46 73
|
mp1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` 1 ) = 1 ) |
75 |
45 74
|
oveq12d |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) - ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` 1 ) ) = ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) |
76 |
75
|
fveq2d |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) - ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` 1 ) ) ) = ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) ) |
77 |
|
ioorp |
|- ( 0 (,) +oo ) = RR+ |
78 |
77
|
eqcomi |
|- RR+ = ( 0 (,) +oo ) |
79 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
80 |
48
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 e. ZZ ) |
81 |
|
1re |
|- 1 e. RR |
82 |
81
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 e. RR ) |
83 |
|
pnfxr |
|- +oo e. RR* |
84 |
83
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> +oo e. RR* ) |
85 |
|
1nn0 |
|- 1 e. NN0 |
86 |
81 85
|
nn0addge1i |
|- 1 <_ ( 1 + 1 ) |
87 |
86
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 <_ ( 1 + 1 ) ) |
88 |
|
0red |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 0 e. RR ) |
89 |
|
rpre |
|- ( x e. RR+ -> x e. RR ) |
90 |
89
|
adantl |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> x e. RR ) |
91 |
|
relogcl |
|- ( x e. RR+ -> ( log ` x ) e. RR ) |
92 |
91
|
adantl |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( log ` x ) e. RR ) |
93 |
|
peano2rem |
|- ( ( log ` x ) e. RR -> ( ( log ` x ) - 1 ) e. RR ) |
94 |
92 93
|
syl |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( log ` x ) - 1 ) e. RR ) |
95 |
90 94
|
remulcld |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( x x. ( ( log ` x ) - 1 ) ) e. RR ) |
96 |
|
nnrp |
|- ( x e. NN -> x e. RR+ ) |
97 |
96 92
|
sylan2 |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. NN ) -> ( log ` x ) e. RR ) |
98 |
|
advlog |
|- ( RR _D ( x e. RR+ |-> ( x x. ( ( log ` x ) - 1 ) ) ) ) = ( x e. RR+ |-> ( log ` x ) ) |
99 |
98
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> ( x x. ( ( log ` x ) - 1 ) ) ) ) = ( x e. RR+ |-> ( log ` x ) ) ) |
100 |
|
fveq2 |
|- ( x = n -> ( log ` x ) = ( log ` n ) ) |
101 |
|
simp32 |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> x <_ n ) |
102 |
|
logleb |
|- ( ( x e. RR+ /\ n e. RR+ ) -> ( x <_ n <-> ( log ` x ) <_ ( log ` n ) ) ) |
103 |
102
|
3ad2ant2 |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( x <_ n <-> ( log ` x ) <_ ( log ` n ) ) ) |
104 |
101 103
|
mpbid |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( log ` x ) <_ ( log ` n ) ) |
105 |
|
simprr |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x ) |
106 |
|
simprl |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR+ ) |
107 |
|
logleb |
|- ( ( 1 e. RR+ /\ x e. RR+ ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) ) |
108 |
46 106 107
|
sylancr |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) ) |
109 |
105 108
|
mpbid |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` 1 ) <_ ( log ` x ) ) |
110 |
56 109
|
eqbrtrrid |
|- ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( log ` x ) ) |
111 |
46
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 e. RR+ ) |
112 |
|
1le1 |
|- 1 <_ 1 |
113 |
112
|
a1i |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 <_ 1 ) |
114 |
|
simpr |
|- ( ( A e. RR+ /\ 1 <_ A ) -> 1 <_ A ) |
115 |
10
|
rexrd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> A e. RR* ) |
116 |
|
pnfge |
|- ( A e. RR* -> A <_ +oo ) |
117 |
115 116
|
syl |
|- ( ( A e. RR+ /\ 1 <_ A ) -> A <_ +oo ) |
118 |
78 79 80 82 84 87 88 95 92 97 99 100 104 38 110 111 1 113 114 117 34
|
dvfsum2 |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) - ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` 1 ) ) ) <_ ( log ` A ) ) |
119 |
76 118
|
eqbrtrrd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) <_ ( log ` A ) ) |
120 |
20 24 12 29 119
|
letrd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 ) <_ ( log ` A ) ) |
121 |
18 82 12
|
lesubaddd |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 ) <_ ( log ` A ) <-> ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) <_ ( ( log ` A ) + 1 ) ) ) |
122 |
120 121
|
mpbid |
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) <_ ( ( log ` A ) + 1 ) ) |