Step |
Hyp |
Ref |
Expression |
1 |
|
rpdmgm |
|- ( A e. RR+ -> A e. ( CC \ ( ZZ \ NN ) ) ) |
2 |
|
lgamcl |
|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` A ) e. CC ) |
3 |
1 2
|
syl |
|- ( A e. RR+ -> ( log_G ` A ) e. CC ) |
4 |
|
relogcl |
|- ( A e. RR+ -> ( log ` A ) e. RR ) |
5 |
4
|
recnd |
|- ( A e. RR+ -> ( log ` A ) e. CC ) |
6 |
3 5
|
pncand |
|- ( A e. RR+ -> ( ( ( log_G ` A ) + ( log ` A ) ) - ( log ` A ) ) = ( log_G ` A ) ) |
7 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
8 |
|
1zzd |
|- ( A e. RR+ -> 1 e. ZZ ) |
9 |
|
eqid |
|- ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) = ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) |
10 |
9 1
|
lgamcvg |
|- ( A e. RR+ -> seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) ~~> ( ( log_G ` A ) + ( log ` A ) ) ) |
11 |
|
simpl |
|- ( ( A e. RR+ /\ m e. NN ) -> A e. RR+ ) |
12 |
11
|
rpred |
|- ( ( A e. RR+ /\ m e. NN ) -> A e. RR ) |
13 |
|
simpr |
|- ( ( A e. RR+ /\ m e. NN ) -> m e. NN ) |
14 |
13
|
peano2nnd |
|- ( ( A e. RR+ /\ m e. NN ) -> ( m + 1 ) e. NN ) |
15 |
14
|
nnrpd |
|- ( ( A e. RR+ /\ m e. NN ) -> ( m + 1 ) e. RR+ ) |
16 |
13
|
nnrpd |
|- ( ( A e. RR+ /\ m e. NN ) -> m e. RR+ ) |
17 |
15 16
|
rpdivcld |
|- ( ( A e. RR+ /\ m e. NN ) -> ( ( m + 1 ) / m ) e. RR+ ) |
18 |
17
|
relogcld |
|- ( ( A e. RR+ /\ m e. NN ) -> ( log ` ( ( m + 1 ) / m ) ) e. RR ) |
19 |
12 18
|
remulcld |
|- ( ( A e. RR+ /\ m e. NN ) -> ( A x. ( log ` ( ( m + 1 ) / m ) ) ) e. RR ) |
20 |
11 16
|
rpdivcld |
|- ( ( A e. RR+ /\ m e. NN ) -> ( A / m ) e. RR+ ) |
21 |
|
1rp |
|- 1 e. RR+ |
22 |
21
|
a1i |
|- ( ( A e. RR+ /\ m e. NN ) -> 1 e. RR+ ) |
23 |
20 22
|
rpaddcld |
|- ( ( A e. RR+ /\ m e. NN ) -> ( ( A / m ) + 1 ) e. RR+ ) |
24 |
23
|
relogcld |
|- ( ( A e. RR+ /\ m e. NN ) -> ( log ` ( ( A / m ) + 1 ) ) e. RR ) |
25 |
19 24
|
resubcld |
|- ( ( A e. RR+ /\ m e. NN ) -> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) e. RR ) |
26 |
25
|
fmpttd |
|- ( A e. RR+ -> ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) : NN --> RR ) |
27 |
26
|
ffvelrnda |
|- ( ( A e. RR+ /\ n e. NN ) -> ( ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ` n ) e. RR ) |
28 |
7 8 27
|
serfre |
|- ( A e. RR+ -> seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) : NN --> RR ) |
29 |
28
|
ffvelrnda |
|- ( ( A e. RR+ /\ n e. NN ) -> ( seq 1 ( + , ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) ) ` n ) e. RR ) |
30 |
7 8 10 29
|
climrecl |
|- ( A e. RR+ -> ( ( log_G ` A ) + ( log ` A ) ) e. RR ) |
31 |
30 4
|
resubcld |
|- ( A e. RR+ -> ( ( ( log_G ` A ) + ( log ` A ) ) - ( log ` A ) ) e. RR ) |
32 |
6 31
|
eqeltrrd |
|- ( A e. RR+ -> ( log_G ` A ) e. RR ) |