This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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