Theorem chpp1

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

	Ref	Expression
Assertion	chpp1	⊢ ( 𝐴 ∈ ℕ0 → ( ψ ‘ ( 𝐴 + 1 ) ) = ( ( ψ ‘ 𝐴 ) + ( Λ ‘ ( 𝐴 + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0p1nn	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 + 1 ) ∈ ℕ )
2		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
3	1 2	eleqtrdi	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
4		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( 𝐴 + 1 ) ) → 𝑛 ∈ ℕ )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑛 ∈ ( 1 ... ( 𝐴 + 1 ) ) ) → 𝑛 ∈ ℕ )
6		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
7	5 6	syl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑛 ∈ ( 1 ... ( 𝐴 + 1 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
8	7	recnd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑛 ∈ ( 1 ... ( 𝐴 + 1 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
9		fveq2	⊢ ( 𝑛 = ( 𝐴 + 1 ) → ( Λ ‘ 𝑛 ) = ( Λ ‘ ( 𝐴 + 1 ) ) )
10	3 8 9	fsumm1	⊢ ( 𝐴 ∈ ℕ0 → Σ 𝑛 ∈ ( 1 ... ( 𝐴 + 1 ) ) ( Λ ‘ 𝑛 ) = ( Σ 𝑛 ∈ ( 1 ... ( ( 𝐴 + 1 ) − 1 ) ) ( Λ ‘ 𝑛 ) + ( Λ ‘ ( 𝐴 + 1 ) ) ) )
11		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
12		peano2re	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
13		chpval	⊢ ( ( 𝐴 + 1 ) ∈ ℝ → ( ψ ‘ ( 𝐴 + 1 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ( Λ ‘ 𝑛 ) )
14	11 12 13	3syl	⊢ ( 𝐴 ∈ ℕ0 → ( ψ ‘ ( 𝐴 + 1 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ( Λ ‘ 𝑛 ) )
15		nn0z	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
16	15	peano2zd	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 + 1 ) ∈ ℤ )
17		flid	⊢ ( ( 𝐴 + 1 ) ∈ ℤ → ( ⌊ ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) )
18	16 17	syl	⊢ ( 𝐴 ∈ ℕ0 → ( ⌊ ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) )
19	18	oveq2d	⊢ ( 𝐴 ∈ ℕ0 → ( 1 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) = ( 1 ... ( 𝐴 + 1 ) ) )
20	19	sumeq1d	⊢ ( 𝐴 ∈ ℕ0 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 + 1 ) ) ) ( Λ ‘ 𝑛 ) = Σ 𝑛 ∈ ( 1 ... ( 𝐴 + 1 ) ) ( Λ ‘ 𝑛 ) )
21	14 20	eqtrd	⊢ ( 𝐴 ∈ ℕ0 → ( ψ ‘ ( 𝐴 + 1 ) ) = Σ 𝑛 ∈ ( 1 ... ( 𝐴 + 1 ) ) ( Λ ‘ 𝑛 ) )
22		chpval	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) )
23	11 22	syl	⊢ ( 𝐴 ∈ ℕ0 → ( ψ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) )
24		flid	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 )
25	15 24	syl	⊢ ( 𝐴 ∈ ℕ0 → ( ⌊ ‘ 𝐴 ) = 𝐴 )
26		nn0cn	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ )
27		ax-1cn	⊢ 1 ∈ ℂ
28		pncan	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
29	26 27 28	sylancl	⊢ ( 𝐴 ∈ ℕ0 → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
30	25 29	eqtr4d	⊢ ( 𝐴 ∈ ℕ0 → ( ⌊ ‘ 𝐴 ) = ( ( 𝐴 + 1 ) − 1 ) )
31	30	oveq2d	⊢ ( 𝐴 ∈ ℕ0 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) = ( 1 ... ( ( 𝐴 + 1 ) − 1 ) ) )
32	31	sumeq1d	⊢ ( 𝐴 ∈ ℕ0 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) = Σ 𝑛 ∈ ( 1 ... ( ( 𝐴 + 1 ) − 1 ) ) ( Λ ‘ 𝑛 ) )
33	23 32	eqtrd	⊢ ( 𝐴 ∈ ℕ0 → ( ψ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ( 𝐴 + 1 ) − 1 ) ) ( Λ ‘ 𝑛 ) )
34	33	oveq1d	⊢ ( 𝐴 ∈ ℕ0 → ( ( ψ ‘ 𝐴 ) + ( Λ ‘ ( 𝐴 + 1 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ( 𝐴 + 1 ) − 1 ) ) ( Λ ‘ 𝑛 ) + ( Λ ‘ ( 𝐴 + 1 ) ) ) )
35	10 21 34	3eqtr4d	⊢ ( 𝐴 ∈ ℕ0 → ( ψ ‘ ( 𝐴 + 1 ) ) = ( ( ψ ‘ 𝐴 ) + ( Λ ‘ ( 𝐴 + 1 ) ) ) )