Theorem cht2

Description: The Chebyshev function at 2 . (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	cht2	$$⊢\theta \left(2\right)=\log 2$$

Proof

Step	Hyp	Ref	Expression
1		df-2	$$⊢2=1+1$$
2	1	fveq2i	$$⊢\theta \left(2\right)=\theta \left(1+1\right)$$
3		1z	$$⊢1\in \mathbb{Z}$$
4		2prm	$$⊢2\in \mathbb{P}$$
5	1 4	eqeltrri	$$⊢1+1\in \mathbb{P}$$
6		chtprm	$$⊢\left(1\in \mathbb{Z}\wedge 1+1\in \mathbb{P}\right)\to \theta \left(1+1\right)=\theta \left(1\right)+\log \left(1+1\right)$$
7	3 5 6	mp2an	$$⊢\theta \left(1+1\right)=\theta \left(1\right)+\log \left(1+1\right)$$
8		cht1	$$⊢\theta \left(1\right)=0$$
9	8	eqcomi	$$⊢0=\theta \left(1\right)$$
10	1	fveq2i	$$⊢\log 2=\log \left(1+1\right)$$
11	9 10	oveq12i	$$⊢0+\log 2=\theta \left(1\right)+\log \left(1+1\right)$$
12		2rp	$$⊢2\in {ℝ}^{+}$$
13		relogcl	$$⊢2\in {ℝ}^{+}\to \log 2\in ℝ$$
14	12 13	ax-mp	$$⊢\log 2\in ℝ$$
15	14	recni	$$⊢\log 2\in ℂ$$
16	15	addid2i	$$⊢0+\log 2=\log 2$$
17	11 16	eqtr3i	$$⊢\theta \left(1\right)+\log \left(1+1\right)=\log 2$$
18	2 7 17	3eqtri	$$⊢\theta \left(2\right)=\log 2$$