Metamath Proof Explorer


Theorem chpp1

Description: The second Chebyshev function at a successor. (Contributed by Mario Carneiro, 11-Apr-2016)

Ref Expression
Assertion chpp1
|- ( A e. NN0 -> ( psi ` ( A + 1 ) ) = ( ( psi ` A ) + ( Lam ` ( A + 1 ) ) ) )

Proof

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 ) ) ) )