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