chtprm

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

		Ref	Expression
	Assertion	chtprm	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to θ (A + 1) = θ (A) + \log (A + 1)$

Proof

Step	Hyp	Ref	Expression
1		peano2z	$⊢ A \in ℤ \to A + 1 \in ℤ$
2	1	adantr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 \in ℤ$
3		zre	$⊢ A + 1 \in ℤ \to A + 1 \in ℝ$
4	2 3	syl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 \in ℝ$
5		chtval	$⊢ A + 1 \in ℝ \to θ (A + 1) = \sum_{p \in [0, A + 1] \cap ℙ} \log p$
6	4 5	syl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to θ (A + 1) = \sum_{p \in [0, A + 1] \cap ℙ} \log p$
7		ppisval	$⊢ A + 1 \in ℝ \to [0, A + 1] \cap ℙ = (2 \dots ⌊A + 1⌋) \cap ℙ$
8	4 7	syl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to [0, A + 1] \cap ℙ = (2 \dots ⌊A + 1⌋) \cap ℙ$
9		flid	$⊢ A + 1 \in ℤ \to ⌊A + 1⌋ = A + 1$
10	2 9	syl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to ⌊A + 1⌋ = A + 1$
11	10	oveq2d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots ⌊A + 1⌋) = (2 \dots A + 1)$
12	11	ineq1d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots ⌊A + 1⌋) \cap ℙ = (2 \dots A + 1) \cap ℙ$
13	8 12	eqtrd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to [0, A + 1] \cap ℙ = (2 \dots A + 1) \cap ℙ$
14	13	sumeq1d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \sum_{p \in [0, A + 1] \cap ℙ} \log p = \sum_{p \in (2 \dots A + 1) \cap ℙ} \log p$
15	6 14	eqtrd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to θ (A + 1) = \sum_{p \in (2 \dots A + 1) \cap ℙ} \log p$
16		zre	$⊢ A \in ℤ \to A \in ℝ$
17	16	adantr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A \in ℝ$
18	17	ltp1d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A < A + 1$
19	17 4	ltnled	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (A < A + 1 \leftrightarrow \neg A + 1 \leq A)$
20	18 19	mpbid	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \neg A + 1 \leq A$
21		elinel1	$⊢ A + 1 \in ((2 \dots A) \cap ℙ) \to A + 1 \in (2 \dots A)$
22		elfzle2	$⊢ A + 1 \in (2 \dots A) \to A + 1 \leq A$
23	21 22	syl	$⊢ A + 1 \in ((2 \dots A) \cap ℙ) \to A + 1 \leq A$
24	20 23	nsyl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \neg A + 1 \in ((2 \dots A) \cap ℙ)$
25		disjsn	$⊢ ((2 \dots A) \cap ℙ) \cap \{A + 1\} = \emptyset \leftrightarrow \neg A + 1 \in ((2 \dots A) \cap ℙ)$
26	24 25	sylibr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to ((2 \dots A) \cap ℙ) \cap \{A + 1\} = \emptyset$
27		2z	$⊢ 2 \in ℤ$
28		zcn	$⊢ A \in ℤ \to A \in ℂ$
29	28	adantr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A \in ℂ$
30		ax-1cn	$⊢ 1 \in ℂ$
31		pncan	$⊢ (A \in ℂ \land 1 \in ℂ) \to A + 1 - 1 = A$
32	29 30 31	sylancl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 - 1 = A$
33		prmuz2	$⊢ A + 1 \in ℙ \to A + 1 \in ℤ_{\geq 2}$
34	33	adantl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 \in ℤ_{\geq 2}$
35		uz2m1nn	$⊢ A + 1 \in ℤ_{\geq 2} \to A + 1 - 1 \in ℕ$
36	34 35	syl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 - 1 \in ℕ$
37	32 36	eqeltrrd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A \in ℕ$
38		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
39		2m1e1	$⊢ 2 - 1 = 1$
40	39	fveq2i	$⊢ ℤ_{\geq (2 - 1)} = ℤ_{\geq 1}$
41	38 40	eqtr4i	$⊢ ℕ = ℤ_{\geq (2 - 1)}$
42	37 41	eleqtrdi	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A \in ℤ_{\geq (2 - 1)}$
43		fzsuc2	$⊢ (2 \in ℤ \land A \in ℤ_{\geq (2 - 1)}) \to (2 \dots A + 1) = (2 \dots A) \cup \{A + 1\}$
44	27 42 43	sylancr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A + 1) = (2 \dots A) \cup \{A + 1\}$
45	44	ineq1d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A + 1) \cap ℙ = ((2 \dots A) \cup \{A + 1\}) \cap ℙ$
46		indir	$⊢ ((2 \dots A) \cup \{A + 1\}) \cap ℙ = ((2 \dots A) \cap ℙ) \cup (\{A + 1\} \cap ℙ)$
47	45 46	eqtrdi	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A + 1) \cap ℙ = ((2 \dots A) \cap ℙ) \cup (\{A + 1\} \cap ℙ)$
48		simpr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 \in ℙ$
49	48	snssd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \{A + 1\} \subseteq ℙ$
50		df-ss	$⊢ \{A + 1\} \subseteq ℙ \leftrightarrow \{A + 1\} \cap ℙ = \{A + 1\}$
51	49 50	sylib	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \{A + 1\} \cap ℙ = \{A + 1\}$
52	51	uneq2d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to ((2 \dots A) \cap ℙ) \cup (\{A + 1\} \cap ℙ) = ((2 \dots A) \cap ℙ) \cup \{A + 1\}$
53	47 52	eqtrd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A + 1) \cap ℙ = ((2 \dots A) \cap ℙ) \cup \{A + 1\}$
54		fzfid	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A + 1) \in Fin$
55		inss1	$⊢ (2 \dots A + 1) \cap ℙ \subseteq (2 \dots A + 1)$
56		ssfi	$⊢ ((2 \dots A + 1) \in Fin \land (2 \dots A + 1) \cap ℙ \subseteq (2 \dots A + 1)) \to (2 \dots A + 1) \cap ℙ \in Fin$
57	54 55 56	sylancl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots A + 1) \cap ℙ \in Fin$
58		simpr	$⊢ ((A \in ℤ \land A + 1 \in ℙ) \land p \in ((2 \dots A + 1) \cap ℙ)) \to p \in ((2 \dots A + 1) \cap ℙ)$
59	58	elin2d	$⊢ ((A \in ℤ \land A + 1 \in ℙ) \land p \in ((2 \dots A + 1) \cap ℙ)) \to p \in ℙ$
60		prmnn	$⊢ p \in ℙ \to p \in ℕ$
61	59 60	syl	$⊢ ((A \in ℤ \land A + 1 \in ℙ) \land p \in ((2 \dots A + 1) \cap ℙ)) \to p \in ℕ$
62	61	nnrpd	$⊢ ((A \in ℤ \land A + 1 \in ℙ) \land p \in ((2 \dots A + 1) \cap ℙ)) \to p \in ℝ^{+}$
63	62	relogcld	$⊢ ((A \in ℤ \land A + 1 \in ℙ) \land p \in ((2 \dots A + 1) \cap ℙ)) \to \log p \in ℝ$
64	63	recnd	$⊢ ((A \in ℤ \land A + 1 \in ℙ) \land p \in ((2 \dots A + 1) \cap ℙ)) \to \log p \in ℂ$
65	26 53 57 64	fsumsplit	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \sum_{p \in (2 \dots A + 1) \cap ℙ} \log p = \sum_{p \in (2 \dots A) \cap ℙ} \log p + \sum_{p \in \{A + 1\}} \log p$
66		chtval	$⊢ A \in ℝ \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
67	17 66	syl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
68		ppisval	$⊢ A \in ℝ \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
69	17 68	syl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
70		flid	$⊢ A \in ℤ \to ⌊A⌋ = A$
71	70	adantr	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to ⌊A⌋ = A$
72	71	oveq2d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots ⌊A⌋) = (2 \dots A)$
73	72	ineq1d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to (2 \dots ⌊A⌋) \cap ℙ = (2 \dots A) \cap ℙ$
74	69 73	eqtrd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to [0, A] \cap ℙ = (2 \dots A) \cap ℙ$
75	74	sumeq1d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \sum_{p \in [0, A] \cap ℙ} \log p = \sum_{p \in (2 \dots A) \cap ℙ} \log p$
76	67 75	eqtr2d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \sum_{p \in (2 \dots A) \cap ℙ} \log p = θ (A)$
77		prmnn	$⊢ A + 1 \in ℙ \to A + 1 \in ℕ$
78	77	adantl	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 \in ℕ$
79	78	nnrpd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to A + 1 \in ℝ^{+}$
80	79	relogcld	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \log (A + 1) \in ℝ$
81	80	recnd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \log (A + 1) \in ℂ$
82		fveq2	$⊢ p = A + 1 \to \log p = \log (A + 1)$
83	82	sumsn	$⊢ (A + 1 \in ℕ \land \log (A + 1) \in ℂ) \to \sum_{p \in \{A + 1\}} \log p = \log (A + 1)$
84	78 81 83	syl2anc	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \sum_{p \in \{A + 1\}} \log p = \log (A + 1)$
85	76 84	oveq12d	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to \sum_{p \in (2 \dots A) \cap ℙ} \log p + \sum_{p \in \{A + 1\}} \log p = θ (A) + \log (A + 1)$
86	15 65 85	3eqtrd	$⊢ (A \in ℤ \land A + 1 \in ℙ) \to θ (A + 1) = θ (A) + \log (A + 1)$

Metamath Proof Explorer

Theorem chtprm

Proof