Step |
Hyp |
Ref |
Expression |
1 |
|
nn0p1nn |
|- ( A e. NN0 -> ( A + 1 ) e. NN ) |
2 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
3 |
1 2
|
eleqtrdi |
|- ( A e. NN0 -> ( A + 1 ) e. ( ZZ>= ` 1 ) ) |
4 |
|
elfznn |
|- ( n e. ( 1 ... ( A + 1 ) ) -> n e. NN ) |
5 |
4
|
adantl |
|- ( ( A e. NN0 /\ n e. ( 1 ... ( A + 1 ) ) ) -> n e. NN ) |
6 |
|
vmacl |
|- ( n e. NN -> ( Lam ` n ) e. RR ) |
7 |
5 6
|
syl |
|- ( ( A e. NN0 /\ n e. ( 1 ... ( A + 1 ) ) ) -> ( Lam ` n ) e. RR ) |
8 |
7
|
recnd |
|- ( ( A e. NN0 /\ n e. ( 1 ... ( A + 1 ) ) ) -> ( Lam ` n ) e. CC ) |
9 |
|
fveq2 |
|- ( n = ( A + 1 ) -> ( Lam ` n ) = ( Lam ` ( A + 1 ) ) ) |
10 |
3 8 9
|
fsumm1 |
|- ( A e. NN0 -> sum_ n e. ( 1 ... ( A + 1 ) ) ( Lam ` n ) = ( sum_ n e. ( 1 ... ( ( A + 1 ) - 1 ) ) ( Lam ` n ) + ( Lam ` ( A + 1 ) ) ) ) |
11 |
|
nn0re |
|- ( A e. NN0 -> A e. RR ) |
12 |
|
peano2re |
|- ( A e. RR -> ( A + 1 ) e. RR ) |
13 |
|
chpval |
|- ( ( A + 1 ) e. RR -> ( psi ` ( A + 1 ) ) = sum_ n e. ( 1 ... ( |_ ` ( A + 1 ) ) ) ( Lam ` n ) ) |
14 |
11 12 13
|
3syl |
|- ( A e. NN0 -> ( psi ` ( A + 1 ) ) = sum_ n e. ( 1 ... ( |_ ` ( A + 1 ) ) ) ( Lam ` n ) ) |
15 |
|
nn0z |
|- ( A e. NN0 -> A e. ZZ ) |
16 |
15
|
peano2zd |
|- ( A e. NN0 -> ( A + 1 ) e. ZZ ) |
17 |
|
flid |
|- ( ( A + 1 ) e. ZZ -> ( |_ ` ( A + 1 ) ) = ( A + 1 ) ) |
18 |
16 17
|
syl |
|- ( A e. NN0 -> ( |_ ` ( A + 1 ) ) = ( A + 1 ) ) |
19 |
18
|
oveq2d |
|- ( A e. NN0 -> ( 1 ... ( |_ ` ( A + 1 ) ) ) = ( 1 ... ( A + 1 ) ) ) |
20 |
19
|
sumeq1d |
|- ( A e. NN0 -> sum_ n e. ( 1 ... ( |_ ` ( A + 1 ) ) ) ( Lam ` n ) = sum_ n e. ( 1 ... ( A + 1 ) ) ( Lam ` n ) ) |
21 |
14 20
|
eqtrd |
|- ( A e. NN0 -> ( psi ` ( A + 1 ) ) = sum_ n e. ( 1 ... ( A + 1 ) ) ( Lam ` n ) ) |
22 |
|
chpval |
|- ( A e. RR -> ( psi ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) ) |
23 |
11 22
|
syl |
|- ( A e. NN0 -> ( psi ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) ) |
24 |
|
flid |
|- ( A e. ZZ -> ( |_ ` A ) = A ) |
25 |
15 24
|
syl |
|- ( A e. NN0 -> ( |_ ` A ) = A ) |
26 |
|
nn0cn |
|- ( A e. NN0 -> A e. CC ) |
27 |
|
ax-1cn |
|- 1 e. CC |
28 |
|
pncan |
|- ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - 1 ) = A ) |
29 |
26 27 28
|
sylancl |
|- ( A e. NN0 -> ( ( A + 1 ) - 1 ) = A ) |
30 |
25 29
|
eqtr4d |
|- ( A e. NN0 -> ( |_ ` A ) = ( ( A + 1 ) - 1 ) ) |
31 |
30
|
oveq2d |
|- ( A e. NN0 -> ( 1 ... ( |_ ` A ) ) = ( 1 ... ( ( A + 1 ) - 1 ) ) ) |
32 |
31
|
sumeq1d |
|- ( A e. NN0 -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) = sum_ n e. ( 1 ... ( ( A + 1 ) - 1 ) ) ( Lam ` n ) ) |
33 |
23 32
|
eqtrd |
|- ( A e. NN0 -> ( psi ` A ) = sum_ n e. ( 1 ... ( ( A + 1 ) - 1 ) ) ( Lam ` n ) ) |
34 |
33
|
oveq1d |
|- ( A e. NN0 -> ( ( psi ` A ) + ( Lam ` ( A + 1 ) ) ) = ( sum_ n e. ( 1 ... ( ( A + 1 ) - 1 ) ) ( Lam ` n ) + ( Lam ` ( A + 1 ) ) ) ) |
35 |
10 21 34
|
3eqtr4d |
|- ( A e. NN0 -> ( psi ` ( A + 1 ) ) = ( ( psi ` A ) + ( Lam ` ( A + 1 ) ) ) ) |