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		3cn	$$⊢3\in ℂ$$
13		2cn	$$⊢2\in ℂ$$
14		3t2e6	$$⊢3\cdot 2=6$$
15	12 13 14	mulcomli	$$⊢2\cdot 3=6$$
16	15	fveq2i	$$⊢\log 2\cdot 3=\log 6$$
17		cht2	$$⊢\theta \left(2\right)=\log 2$$
18	17	eqcomi	$$⊢\log 2=\theta \left(2\right)$$
19	1	fveq2i	$$⊢\log 3=\log \left(2+1\right)$$
20	18 19	oveq12i	$$⊢\log 2+\log 3=\theta \left(2\right)+\log \left(2+1\right)$$
21	11 16 20	3eqtr3ri	$$⊢\theta \left(2\right)+\log \left(2+1\right)=\log 6$$
22	2 7 21	3eqtri	$$⊢\theta \left(3\right)=\log 6$$