Metamath Proof Explorer

Theorem advlogexp

Description: The antiderivative of a power of the logarithm. (Set A = 1 and multiply by ( -u 1 ) ^ N x. N ! to get the antiderivative of log ( x ) ^ N itself.) (Contributed by Mario Carneiro, 22-May-2016)

Ref Expression
Assertion advlogexp 
|- ( ( A e. RR+ /\ N e. NN0 ) -> ( RR _D ( x e. RR+ |-> ( x x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) ) ) = ( x e. RR+ |-> ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) ) )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( 0 ... N ) e. Fin )
2 rpcn 
 |-  ( x e. RR+ -> x e. CC )
3 2 adantl 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> x e. CC )
4 rpdivcl 
 |-  ( ( A e. RR+ /\ x e. RR+ ) -> ( A / x ) e. RR+ )
5 4 adantlr 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( A / x ) e. RR+ )
6 5 relogcld 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( log ` ( A / x ) ) e. RR )
7 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
8 reexpcl 
 |-  ( ( ( log ` ( A / x ) ) e. RR /\ k e. NN0 ) -> ( ( log ` ( A / x ) ) ^ k ) e. RR )
9 6 7 8 syl2an 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( log ` ( A / x ) ) ^ k ) e. RR )
10 7 adantl 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> k e. NN0 )
11 10 faccld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. NN )
12 9 11 nndivred 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) e. RR )
13 12 recnd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) e. CC )
14 1 3 13 fsummulc2 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( x x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) = sum_ k e. ( 0 ... N ) ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) )
15 simplr 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> N e. NN0 )
16 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
17 15 16 eleqtrdi 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> N e. ( ZZ>= ` 0 ) )
18 3 adantr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> x e. CC )
19 18 13 mulcld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ k e. ( 0 ... N ) ) -> ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) e. CC )
20 oveq2 
 |-  ( k = 0 -> ( ( log ` ( A / x ) ) ^ k ) = ( ( log ` ( A / x ) ) ^ 0 ) )
21 fveq2 
 |-  ( k = 0 -> ( ! ` k ) = ( ! ` 0 ) )
22 fac0 
 |-  ( ! ` 0 ) = 1
23 21 22 eqtrdi 
 |-  ( k = 0 -> ( ! ` k ) = 1 )
24 20 23 oveq12d 
 |-  ( k = 0 -> ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) = ( ( ( log ` ( A / x ) ) ^ 0 ) / 1 ) )
25 24 oveq2d 
 |-  ( k = 0 -> ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) = ( x x. ( ( ( log ` ( A / x ) ) ^ 0 ) / 1 ) ) )
26 17 19 25 fsum1p 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> sum_ k e. ( 0 ... N ) ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) = ( ( x x. ( ( ( log ` ( A / x ) ) ^ 0 ) / 1 ) ) + sum_ k e. ( ( 0 + 1 ) ... N ) ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) ) )
27 6 recnd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( log ` ( A / x ) ) e. CC )
28 27 exp0d 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( ( log ` ( A / x ) ) ^ 0 ) = 1 )
29 28 oveq1d 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( ( ( log ` ( A / x ) ) ^ 0 ) / 1 ) = ( 1 / 1 ) )
30 1div1e1 
 |-  ( 1 / 1 ) = 1
31 29 30 eqtrdi 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( ( ( log ` ( A / x ) ) ^ 0 ) / 1 ) = 1 )
32 31 oveq2d 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( x x. ( ( ( log ` ( A / x ) ) ^ 0 ) / 1 ) ) = ( x x. 1 ) )
33 3 mulridd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( x x. 1 ) = x )
34 32 33 eqtrd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( x x. ( ( ( log ` ( A / x ) ) ^ 0 ) / 1 ) ) = x )
35 1zzd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> 1 e. ZZ )
36 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
37 36 ad2antlr 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> N e. ZZ )
38 fz1ssfz0 
 |-  ( 1 ... N ) C_ ( 0 ... N )
39 38 sseli 
 |-  ( k e. ( 1 ... N ) -> k e. ( 0 ... N ) )
40 39 19 sylan2 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ k e. ( 1 ... N ) ) -> ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) e. CC )
41 oveq2 
 |-  ( k = ( j + 1 ) -> ( ( log ` ( A / x ) ) ^ k ) = ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) )
42 fveq2 
 |-  ( k = ( j + 1 ) -> ( ! ` k ) = ( ! ` ( j + 1 ) ) )
43 41 42 oveq12d 
 |-  ( k = ( j + 1 ) -> ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) = ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) )
44 43 oveq2d 
 |-  ( k = ( j + 1 ) -> ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) = ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) )
45 35 35 37 40 44 fsumshftm 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> sum_ k e. ( 1 ... N ) ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) = sum_ j e. ( ( 1 - 1 ) ... ( N - 1 ) ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) )
46 0p1e1 
 |-  ( 0 + 1 ) = 1
47 46 oveq1i 
 |-  ( ( 0 + 1 ) ... N ) = ( 1 ... N )
48 47 sumeq1i 
 |-  sum_ k e. ( ( 0 + 1 ) ... N ) ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) = sum_ k e. ( 1 ... N ) ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) )
49 48 a1i 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> sum_ k e. ( ( 0 + 1 ) ... N ) ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) = sum_ k e. ( 1 ... N ) ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) )
50 1m1e0 
 |-  ( 1 - 1 ) = 0
51 50 oveq1i 
 |-  ( ( 1 - 1 ) ..^ N ) = ( 0 ..^ N )
52 fzoval 
 |-  ( N e. ZZ -> ( ( 1 - 1 ) ..^ N ) = ( ( 1 - 1 ) ... ( N - 1 ) ) )
53 37 52 syl 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( ( 1 - 1 ) ..^ N ) = ( ( 1 - 1 ) ... ( N - 1 ) ) )
54 51 53 eqtr3id 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( 0 ..^ N ) = ( ( 1 - 1 ) ... ( N - 1 ) ) )
55 54 sumeq1d 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> sum_ j e. ( 0 ..^ N ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) = sum_ j e. ( ( 1 - 1 ) ... ( N - 1 ) ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) )
56 45 49 55 3eqtr4d 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> sum_ k e. ( ( 0 + 1 ) ... N ) ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) = sum_ j e. ( 0 ..^ N ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) )
57 34 56 oveq12d 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( ( x x. ( ( ( log ` ( A / x ) ) ^ 0 ) / 1 ) ) + sum_ k e. ( ( 0 + 1 ) ... N ) ( x x. ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) ) = ( x + sum_ j e. ( 0 ..^ N ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) )
58 14 26 57 3eqtrd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( x x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) = ( x + sum_ j e. ( 0 ..^ N ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) )
59 58 mpteq2dva 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( x e. RR+ |-> ( x x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) ) = ( x e. RR+ |-> ( x + sum_ j e. ( 0 ..^ N ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) ) )
60 59 oveq2d 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( RR _D ( x e. RR+ |-> ( x x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) ) ) = ( RR _D ( x e. RR+ |-> ( x + sum_ j e. ( 0 ..^ N ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) ) ) )
61 reelprrecn 
 |-  RR e. { RR , CC }
62 61 a1i 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> RR e. { RR , CC } )
63 1cnd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> 1 e. CC )
64 recn 
 |-  ( x e. RR -> x e. CC )
65 64 adantl 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR ) -> x e. CC )
66 1cnd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR ) -> 1 e. CC )
67 62 dvmptid 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( RR _D ( x e. RR |-> x ) ) = ( x e. RR |-> 1 ) )
68 rpssre 
 |-  RR+ C_ RR
69 68 a1i 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> RR+ C_ RR )
70 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
71 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
72 ioorp 
 |-  ( 0 (,) +oo ) = RR+
73 iooretop 
 |-  ( 0 (,) +oo ) e. ( topGen ` ran (,) )
74 72 73 eqeltrri 
 |-  RR+ e. ( topGen ` ran (,) )
75 74 a1i 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> RR+ e. ( topGen ` ran (,) ) )
76 62 65 66 67 69 70 71 75 dvmptres 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( RR _D ( x e. RR+ |-> x ) ) = ( x e. RR+ |-> 1 ) )
77 fzofi 
 |-  ( 0 ..^ N ) e. Fin
78 77 a1i 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( 0 ..^ N ) e. Fin )
79 3 adantr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> x e. CC )
80 elfzonn0 
 |-  ( j e. ( 0 ..^ N ) -> j e. NN0 )
81 peano2nn0 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN0 )
82 80 81 syl 
 |-  ( j e. ( 0 ..^ N ) -> ( j + 1 ) e. NN0 )
83 reexpcl 
 |-  ( ( ( log ` ( A / x ) ) e. RR /\ ( j + 1 ) e. NN0 ) -> ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) e. RR )
84 6 82 83 syl2an 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) e. RR )
85 82 adantl 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( j + 1 ) e. NN0 )
86 85 faccld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ! ` ( j + 1 ) ) e. NN )
87 84 86 nndivred 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) e. RR )
88 87 recnd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) e. CC )
89 79 88 mulcld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) e. CC )
90 78 89 fsumcl 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> sum_ j e. ( 0 ..^ N ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) e. CC )
91 6 15 reexpcld 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( ( log ` ( A / x ) ) ^ N ) e. RR )
92 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
93 92 ad2antlr 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( ! ` N ) e. NN )
94 91 93 nndivred 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) e. RR )
95 94 recnd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) e. CC )
96 ax-1cn 
 |-  1 e. CC
97 subcl 
 |-  ( ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) e. CC /\ 1 e. CC ) -> ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - 1 ) e. CC )
98 95 96 97 sylancl 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - 1 ) e. CC )
99 77 a1i 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( 0 ..^ N ) e. Fin )
100 89 an32s 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) e. CC )
101 100 3impa 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) /\ x e. RR+ ) -> ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) e. CC )
102 reexpcl 
 |-  ( ( ( log ` ( A / x ) ) e. RR /\ j e. NN0 ) -> ( ( log ` ( A / x ) ) ^ j ) e. RR )
103 6 80 102 syl2an 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( log ` ( A / x ) ) ^ j ) e. RR )
104 80 adantl 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> j e. NN0 )
105 104 faccld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ! ` j ) e. NN )
106 103 105 nndivred 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) e. RR )
107 106 recnd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) e. CC )
108 88 107 subcld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) e. CC )
109 108 an32s 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) e. CC )
110 109 3impa 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) /\ x e. RR+ ) -> ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) e. CC )
111 61 a1i 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> RR e. { RR , CC } )
112 2 adantl 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> x e. CC )
113 1cnd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> 1 e. CC )
114 76 adantr 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR+ |-> x ) ) = ( x e. RR+ |-> 1 ) )
115 88 an32s 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) e. CC )
116 negex 
 |-  -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) e. _V
117 116 a1i 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) e. _V )
118 cnelprrecn 
 |-  CC e. { RR , CC }
119 118 a1i 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> CC e. { RR , CC } )
120 27 adantlr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( log ` ( A / x ) ) e. CC )
121 negex 
 |-  -u ( 1 / x ) e. _V
122 121 a1i 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> -u ( 1 / x ) e. _V )
123 id 
 |-  ( y e. CC -> y e. CC )
124 80 adantl 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> j e. NN0 )
125 124 81 syl 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( j + 1 ) e. NN0 )
126 expcl 
 |-  ( ( y e. CC /\ ( j + 1 ) e. NN0 ) -> ( y ^ ( j + 1 ) ) e. CC )
127 123 125 126 syl2anr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( y ^ ( j + 1 ) ) e. CC )
128 125 faccld 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( ! ` ( j + 1 ) ) e. NN )
129 128 nncnd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( ! ` ( j + 1 ) ) e. CC )
130 129 adantr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ! ` ( j + 1 ) ) e. CC )
131 128 nnne0d 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( ! ` ( j + 1 ) ) =/= 0 )
132 131 adantr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ! ` ( j + 1 ) ) =/= 0 )
133 127 130 132 divcld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ( y ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) e. CC )
134 expcl 
 |-  ( ( y e. CC /\ j e. NN0 ) -> ( y ^ j ) e. CC )
135 123 124 134 syl2anr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( y ^ j ) e. CC )
136 124 faccld 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( ! ` j ) e. NN )
137 136 nncnd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( ! ` j ) e. CC )
138 137 adantr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ! ` j ) e. CC )
139 124 adantr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> j e. NN0 )
140 139 faccld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ! ` j ) e. NN )
141 140 nnne0d 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ! ` j ) =/= 0 )
142 135 138 141 divcld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ( y ^ j ) / ( ! ` j ) ) e. CC )
143 simplll 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> A e. RR+ )
144 simpr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> x e. RR+ )
145 143 144 relogdivd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( log ` ( A / x ) ) = ( ( log ` A ) - ( log ` x ) ) )
146 145 mpteq2dva 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( x e. RR+ |-> ( log ` ( A / x ) ) ) = ( x e. RR+ |-> ( ( log ` A ) - ( log ` x ) ) ) )
147 146 oveq2d 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR+ |-> ( log ` ( A / x ) ) ) ) = ( RR _D ( x e. RR+ |-> ( ( log ` A ) - ( log ` x ) ) ) ) )
148 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
149 148 ad2antrr 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( log ` A ) e. RR )
150 149 recnd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( log ` A ) e. CC )
151 150 adantr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( log ` A ) e. CC )
152 0cnd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> 0 e. CC )
153 150 adantr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR ) -> ( log ` A ) e. CC )
154 0cnd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR ) -> 0 e. CC )
155 111 150 dvmptc 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR |-> ( log ` A ) ) ) = ( x e. RR |-> 0 ) )
156 68 a1i 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> RR+ C_ RR )
157 74 a1i 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> RR+ e. ( topGen ` ran (,) ) )
158 111 153 154 155 156 70 71 157 dvmptres 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR+ |-> ( log ` A ) ) ) = ( x e. RR+ |-> 0 ) )
159 144 relogcld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( log ` x ) e. RR )
160 159 recnd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( log ` x ) e. CC )
161 144 rpreccld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( 1 / x ) e. RR+ )
162 relogf1o 
 |-  ( log |` RR+ ) : RR+ -1-1-onto-> RR
163 f1of 
 |-  ( ( log |` RR+ ) : RR+ -1-1-onto-> RR -> ( log |` RR+ ) : RR+ --> RR )
164 162 163 mp1i 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( log |` RR+ ) : RR+ --> RR )
165 164 feqmptd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( log |` RR+ ) = ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) )
166 fvres 
 |-  ( x e. RR+ -> ( ( log |` RR+ ) ` x ) = ( log ` x ) )
167 166 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) = ( x e. RR+ |-> ( log ` x ) )
168 165 167 eqtrdi 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( log |` RR+ ) = ( x e. RR+ |-> ( log ` x ) ) )
169 168 oveq2d 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( log |` RR+ ) ) = ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) )
170 dvrelog 
 |-  ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )
171 169 170 eqtr3di 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) = ( x e. RR+ |-> ( 1 / x ) ) )
172 111 151 152 158 160 161 171 dvmptsub 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR+ |-> ( ( log ` A ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> ( 0 - ( 1 / x ) ) ) )
173 147 172 eqtrd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR+ |-> ( log ` ( A / x ) ) ) ) = ( x e. RR+ |-> ( 0 - ( 1 / x ) ) ) )
174 df-neg 
 |-  -u ( 1 / x ) = ( 0 - ( 1 / x ) )
175 174 mpteq2i 
 |-  ( x e. RR+ |-> -u ( 1 / x ) ) = ( x e. RR+ |-> ( 0 - ( 1 / x ) ) )
176 173 175 eqtr4di 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR+ |-> ( log ` ( A / x ) ) ) ) = ( x e. RR+ |-> -u ( 1 / x ) ) )
177 ovexd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ( j + 1 ) x. ( y ^ ( ( j + 1 ) - 1 ) ) ) e. _V )
178 nn0p1nn 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN )
179 124 178 syl 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( j + 1 ) e. NN )
180 dvexp 
 |-  ( ( j + 1 ) e. NN -> ( CC _D ( y e. CC |-> ( y ^ ( j + 1 ) ) ) ) = ( y e. CC |-> ( ( j + 1 ) x. ( y ^ ( ( j + 1 ) - 1 ) ) ) ) )
181 179 180 syl 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( CC _D ( y e. CC |-> ( y ^ ( j + 1 ) ) ) ) = ( y e. CC |-> ( ( j + 1 ) x. ( y ^ ( ( j + 1 ) - 1 ) ) ) ) )
182 119 127 177 181 129 131 dvmptdivc 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( CC _D ( y e. CC |-> ( ( y ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) = ( y e. CC |-> ( ( ( j + 1 ) x. ( y ^ ( ( j + 1 ) - 1 ) ) ) / ( ! ` ( j + 1 ) ) ) ) )
183 124 nn0cnd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> j e. CC )
184 183 adantr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> j e. CC )
185 pncan 
 |-  ( ( j e. CC /\ 1 e. CC ) -> ( ( j + 1 ) - 1 ) = j )
186 184 96 185 sylancl 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ( j + 1 ) - 1 ) = j )
187 186 oveq2d 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( y ^ ( ( j + 1 ) - 1 ) ) = ( y ^ j ) )
188 187 oveq2d 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ( j + 1 ) x. ( y ^ ( ( j + 1 ) - 1 ) ) ) = ( ( j + 1 ) x. ( y ^ j ) ) )
189 facp1 
 |-  ( j e. NN0 -> ( ! ` ( j + 1 ) ) = ( ( ! ` j ) x. ( j + 1 ) ) )
190 139 189 syl 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ! ` ( j + 1 ) ) = ( ( ! ` j ) x. ( j + 1 ) ) )
191 peano2cn 
 |-  ( j e. CC -> ( j + 1 ) e. CC )
192 184 191 syl 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( j + 1 ) e. CC )
193 138 192 mulcomd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ( ! ` j ) x. ( j + 1 ) ) = ( ( j + 1 ) x. ( ! ` j ) ) )
194 190 193 eqtrd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ! ` ( j + 1 ) ) = ( ( j + 1 ) x. ( ! ` j ) ) )
195 188 194 oveq12d 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ( ( j + 1 ) x. ( y ^ ( ( j + 1 ) - 1 ) ) ) / ( ! ` ( j + 1 ) ) ) = ( ( ( j + 1 ) x. ( y ^ j ) ) / ( ( j + 1 ) x. ( ! ` j ) ) ) )
196 179 nnne0d 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( j + 1 ) =/= 0 )
197 196 adantr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( j + 1 ) =/= 0 )
198 135 138 192 141 197 divcan5d 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ( ( j + 1 ) x. ( y ^ j ) ) / ( ( j + 1 ) x. ( ! ` j ) ) ) = ( ( y ^ j ) / ( ! ` j ) ) )
199 195 198 eqtrd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ y e. CC ) -> ( ( ( j + 1 ) x. ( y ^ ( ( j + 1 ) - 1 ) ) ) / ( ! ` ( j + 1 ) ) ) = ( ( y ^ j ) / ( ! ` j ) ) )
200 199 mpteq2dva 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( y e. CC |-> ( ( ( j + 1 ) x. ( y ^ ( ( j + 1 ) - 1 ) ) ) / ( ! ` ( j + 1 ) ) ) ) = ( y e. CC |-> ( ( y ^ j ) / ( ! ` j ) ) ) )
201 182 200 eqtrd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( CC _D ( y e. CC |-> ( ( y ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) = ( y e. CC |-> ( ( y ^ j ) / ( ! ` j ) ) ) )
202 oveq1 
 |-  ( y = ( log ` ( A / x ) ) -> ( y ^ ( j + 1 ) ) = ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) )
203 202 oveq1d 
 |-  ( y = ( log ` ( A / x ) ) -> ( ( y ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) = ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) )
204 oveq1 
 |-  ( y = ( log ` ( A / x ) ) -> ( y ^ j ) = ( ( log ` ( A / x ) ) ^ j ) )
205 204 oveq1d 
 |-  ( y = ( log ` ( A / x ) ) -> ( ( y ^ j ) / ( ! ` j ) ) = ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) )
206 111 119 120 122 133 142 176 201 203 205 dvmptco 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR+ |-> ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) = ( x e. RR+ |-> ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) x. -u ( 1 / x ) ) ) )
207 107 an32s 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) e. CC )
208 161 rpcnd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( 1 / x ) e. CC )
209 207 208 mulneg2d 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) x. -u ( 1 / x ) ) = -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) x. ( 1 / x ) ) )
210 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
211 210 adantl 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> x =/= 0 )
212 207 112 211 divrecd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) = ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) x. ( 1 / x ) ) )
213 212 negeqd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) = -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) x. ( 1 / x ) ) )
214 209 213 eqtr4d 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) x. -u ( 1 / x ) ) = -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) )
215 214 mpteq2dva 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( x e. RR+ |-> ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) x. -u ( 1 / x ) ) ) = ( x e. RR+ |-> -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) ) )
216 206 215 eqtrd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR+ |-> ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) = ( x e. RR+ |-> -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) ) )
217 111 112 113 114 115 117 216 dvmptmul 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR+ |-> ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) ) = ( x e. RR+ |-> ( ( 1 x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) + ( -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) x. x ) ) ) )
218 88 mullidd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( 1 x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) = ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) )
219 simplr 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> x e. RR+ )
220 106 219 rerpdivcld 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) e. RR )
221 220 recnd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) e. CC )
222 221 79 mulneg1d 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) x. x ) = -u ( ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) x. x ) )
223 211 an32s 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> x =/= 0 )
224 107 79 223 divcan1d 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) x. x ) = ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) )
225 224 negeqd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> -u ( ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) x. x ) = -u ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) )
226 222 225 eqtrd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) x. x ) = -u ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) )
227 218 226 oveq12d 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( 1 x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) + ( -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) x. x ) ) = ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) + -u ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) )
228 88 107 negsubd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) + -u ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) = ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) )
229 227 228 eqtrd 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) /\ j e. ( 0 ..^ N ) ) -> ( ( 1 x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) + ( -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) x. x ) ) = ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) )
230 229 an32s 
 |-  ( ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) /\ x e. RR+ ) -> ( ( 1 x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) + ( -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) x. x ) ) = ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) )
231 230 mpteq2dva 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( x e. RR+ |-> ( ( 1 x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) + ( -u ( ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) / x ) x. x ) ) ) = ( x e. RR+ |-> ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) ) )
232 217 231 eqtrd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( x e. RR+ |-> ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) ) = ( x e. RR+ |-> ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) ) )
233 70 71 62 75 99 101 110 232 dvmptfsum 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( RR _D ( x e. RR+ |-> sum_ j e. ( 0 ..^ N ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) ) = ( x e. RR+ |-> sum_ j e. ( 0 ..^ N ) ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) ) )
234 oveq2 
 |-  ( k = j -> ( ( log ` ( A / x ) ) ^ k ) = ( ( log ` ( A / x ) ) ^ j ) )
235 fveq2 
 |-  ( k = j -> ( ! ` k ) = ( ! ` j ) )
236 234 235 oveq12d 
 |-  ( k = j -> ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) = ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) )
237 oveq2 
 |-  ( k = N -> ( ( log ` ( A / x ) ) ^ k ) = ( ( log ` ( A / x ) ) ^ N ) )
238 fveq2 
 |-  ( k = N -> ( ! ` k ) = ( ! ` N ) )
239 237 238 oveq12d 
 |-  ( k = N -> ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) = ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) )
240 236 43 24 239 17 13 telfsumo2 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> sum_ j e. ( 0 ..^ N ) ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) = ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - ( ( ( log ` ( A / x ) ) ^ 0 ) / 1 ) ) )
241 31 oveq2d 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - ( ( ( log ` ( A / x ) ) ^ 0 ) / 1 ) ) = ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - 1 ) )
242 240 241 eqtrd 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> sum_ j e. ( 0 ..^ N ) ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) = ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - 1 ) )
243 242 mpteq2dva 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( x e. RR+ |-> sum_ j e. ( 0 ..^ N ) ( ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) - ( ( ( log ` ( A / x ) ) ^ j ) / ( ! ` j ) ) ) ) = ( x e. RR+ |-> ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - 1 ) ) )
244 233 243 eqtrd 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( RR _D ( x e. RR+ |-> sum_ j e. ( 0 ..^ N ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) ) = ( x e. RR+ |-> ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - 1 ) ) )
245 62 3 63 76 90 98 244 dvmptadd 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( RR _D ( x e. RR+ |-> ( x + sum_ j e. ( 0 ..^ N ) ( x x. ( ( ( log ` ( A / x ) ) ^ ( j + 1 ) ) / ( ! ` ( j + 1 ) ) ) ) ) ) ) = ( x e. RR+ |-> ( 1 + ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - 1 ) ) ) )
246 pncan3 
 |-  ( ( 1 e. CC /\ ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) e. CC ) -> ( 1 + ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - 1 ) ) = ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) )
247 96 95 246 sylancr 
 |-  ( ( ( A e. RR+ /\ N e. NN0 ) /\ x e. RR+ ) -> ( 1 + ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - 1 ) ) = ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) )
248 247 mpteq2dva 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( x e. RR+ |-> ( 1 + ( ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) - 1 ) ) ) = ( x e. RR+ |-> ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) ) )
249 60 245 248 3eqtrd 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( RR _D ( x e. RR+ |-> ( x x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) ) ) = ( x e. RR+ |-> ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) ) )