Theorem chpp1

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

	Ref	Expression
Assertion	chpp1	$$⊢A\in {\mathbb{N}}_0\to \psi \left(A+1\right)=\psi \left(A\right)+\Lambda \left(A+1\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0p1nn	$$⊢A\in {\mathbb{N}}_0\to A+1\in \mathbb{N}$$
2		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
3	1 2	eleqtrdi	$$⊢A\in {\mathbb{N}}_0\to A+1\in {\mathbb{Z}}_{\ge 1}$$
4		elfznn	$$⊢n\in \left(1\dots A+1\right)\to n\in \mathbb{N}$$
5	4	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge n\in \left(1\dots A+1\right)\right)\to n\in \mathbb{N}$$
6		vmacl	$$⊢n\in \mathbb{N}\to \Lambda \left(n\right)\in ℝ$$
7	5 6	syl	$$⊢\left(A\in {\mathbb{N}}_0\wedge n\in \left(1\dots A+1\right)\right)\to \Lambda \left(n\right)\in ℝ$$
8	7	recnd	$$⊢\left(A\in {\mathbb{N}}_0\wedge n\in \left(1\dots A+1\right)\right)\to \Lambda \left(n\right)\in ℂ$$
9		fveq2	$$⊢n=A+1\to \Lambda \left(n\right)=\Lambda \left(A+1\right)$$
10	3 8 9	fsumm1	$$⊢A\in {\mathbb{N}}_0\to \sum _{n=1}^{A+1}\Lambda \left(n\right)=\sum _{n=1}^{A+1-1}\Lambda \left(n\right)+\Lambda \left(A+1\right)$$
11		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
12		peano2re	$$⊢A\in ℝ\to A+1\in ℝ$$
13		chpval	$$⊢A+1\in ℝ\to \psi \left(A+1\right)=\sum _{n=1}^{⌊A+1⌋}\Lambda \left(n\right)$$
14	11 12 13	3syl	$$⊢A\in {\mathbb{N}}_0\to \psi \left(A+1\right)=\sum _{n=1}^{⌊A+1⌋}\Lambda \left(n\right)$$
15		nn0z	$$⊢A\in {\mathbb{N}}_0\to A\in \mathbb{Z}$$
16	15	peano2zd	$$⊢A\in {\mathbb{N}}_0\to A+1\in \mathbb{Z}$$
17		flid	$$⊢A+1\in \mathbb{Z}\to ⌊A+1⌋=A+1$$
18	16 17	syl	$$⊢A\in {\mathbb{N}}_0\to ⌊A+1⌋=A+1$$
19	18	oveq2d	$$⊢A\in {\mathbb{N}}_0\to \left(1\dots ⌊A+1⌋\right)=\left(1\dots A+1\right)$$
20	19	sumeq1d	$$⊢A\in {\mathbb{N}}_0\to \sum _{n=1}^{⌊A+1⌋}\Lambda \left(n\right)=\sum _{n=1}^{A+1}\Lambda \left(n\right)$$
21	14 20	eqtrd	$$⊢A\in {\mathbb{N}}_0\to \psi \left(A+1\right)=\sum _{n=1}^{A+1}\Lambda \left(n\right)$$
22		chpval	$$⊢A\in ℝ\to \psi \left(A\right)=\sum _{n=1}^{⌊A⌋}\Lambda \left(n\right)$$
23	11 22	syl	$$⊢A\in {\mathbb{N}}_0\to \psi \left(A\right)=\sum _{n=1}^{⌊A⌋}\Lambda \left(n\right)$$
24		flid	$$⊢A\in \mathbb{Z}\to ⌊A⌋=A$$
25	15 24	syl	$$⊢A\in {\mathbb{N}}_0\to ⌊A⌋=A$$
26		nn0cn	$$⊢A\in {\mathbb{N}}_0\to A\in ℂ$$
27		ax-1cn	$$⊢1\in ℂ$$
28		pncan	$$⊢\left(A\in ℂ\wedge 1\in ℂ\right)\to A+1-1=A$$
29	26 27 28	sylancl	$$⊢A\in {\mathbb{N}}_0\to A+1-1=A$$
30	25 29	eqtr4d	$$⊢A\in {\mathbb{N}}_0\to ⌊A⌋=A+1-1$$
31	30	oveq2d	$$⊢A\in {\mathbb{N}}_0\to \left(1\dots ⌊A⌋\right)=\left(1\dots A+1-1\right)$$
32	31	sumeq1d	$$⊢A\in {\mathbb{N}}_0\to \sum _{n=1}^{⌊A⌋}\Lambda \left(n\right)=\sum _{n=1}^{A+1-1}\Lambda \left(n\right)$$
33	23 32	eqtrd	$$⊢A\in {\mathbb{N}}_0\to \psi \left(A\right)=\sum _{n=1}^{A+1-1}\Lambda \left(n\right)$$
34	33	oveq1d	$$⊢A\in {\mathbb{N}}_0\to \psi \left(A\right)+\Lambda \left(A+1\right)=\sum _{n=1}^{A+1-1}\Lambda \left(n\right)+\Lambda \left(A+1\right)$$
35	10 21 34	3eqtr4d	$$⊢A\in {\mathbb{N}}_0\to \psi \left(A+1\right)=\psi \left(A\right)+\Lambda \left(A+1\right)$$