Theorem cht3

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

	Ref	Expression
Assertion	cht3	$$⊢\theta \left(3\right)=\log 6$$

Proof

Step	Hyp	Ref	Expression
1		df-3	$$⊢3=2+1$$
2	1	fveq2i	$$⊢\theta \left(3\right)=\theta \left(2+1\right)$$
3		2z	$$⊢2\in \mathbb{Z}$$
4		3prm	$$⊢3\in \mathbb{P}$$
5	1 4	eqeltrri	$$⊢2+1\in \mathbb{P}$$
6		chtprm	$$⊢\left(2\in \mathbb{Z}\wedge 2+1\in \mathbb{P}\right)\to \theta \left(2+1\right)=\theta \left(2\right)+\log \left(2+1\right)$$
7	3 5 6	mp2an	$$⊢\theta \left(2+1\right)=\theta \left(2\right)+\log \left(2+1\right)$$
8		2rp	$$⊢2\in {ℝ}^{+}$$
9		3rp	$$⊢3\in {ℝ}^{+}$$
10		relogmul	$$⊢\left(2\in {ℝ}^{+}\wedge 3\in {ℝ}^{+}\right)\to \log 2\cdot 3=\log 2+\log 3$$
11	8 9 10	mp2an	$$⊢\log 2\cdot 3=\log 2+\log 3$$
12		2t3e6	$$⊢2\cdot 3=6$$
13	12	fveq2i	$$⊢\log 2\cdot 3=\log 6$$
14		cht2	$$⊢\theta \left(2\right)=\log 2$$
15	14	eqcomi	$$⊢\log 2=\theta \left(2\right)$$
16	1	fveq2i	$$⊢\log 3=\log \left(2+1\right)$$
17	15 16	oveq12i	$$⊢\log 2+\log 3=\theta \left(2\right)+\log \left(2+1\right)$$
18	11 13 17	3eqtr3ri	$$⊢\theta \left(2\right)+\log \left(2+1\right)=\log 6$$
19	2 7 18	3eqtri	$$⊢\theta \left(3\right)=\log 6$$