chtnprm

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

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

Proof

Step	Hyp	Ref	Expression
1		simprr	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in ((2 \dots A + 1) \cap ℙ)$
2	1	elin2d	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in ℙ$
3		simprl	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to \neg A + 1 \in ℙ$
4		nelne2	$⊢ (x \in ℙ \land \neg A + 1 \in ℙ) \to x \neq A + 1$
5	2 3 4	syl2anc	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \neq A + 1$
6		velsn	$⊢ x \in \{A + 1\} \leftrightarrow x = A + 1$
7	6	necon3bbii	$⊢ \neg x \in \{A + 1\} \leftrightarrow x \neq A + 1$
8	5 7	sylibr	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to \neg x \in \{A + 1\}$
9	1	elin1d	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in (2 \dots A + 1)$
10		2z	$⊢ 2 \in ℤ$
11		zcn	$⊢ A \in ℤ \to A \in ℂ$
12	11	adantr	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to A \in ℂ$
13		ax-1cn	$⊢ 1 \in ℂ$
14		pncan	$⊢ (A \in ℂ \land 1 \in ℂ) \to A + 1 - 1 = A$
15	12 13 14	sylancl	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to A + 1 - 1 = A$
16		elfzuz2	$⊢ x \in (2 \dots A + 1) \to A + 1 \in ℤ_{\geq 2}$
17		uz2m1nn	$⊢ A + 1 \in ℤ_{\geq 2} \to A + 1 - 1 \in ℕ$
18	9 16 17	3syl	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to A + 1 - 1 \in ℕ$
19	15 18	eqeltrrd	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to A \in ℕ$
20		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
21		2m1e1	$⊢ 2 - 1 = 1$
22	21	fveq2i	$⊢ ℤ_{\geq (2 - 1)} = ℤ_{\geq 1}$
23	20 22	eqtr4i	$⊢ ℕ = ℤ_{\geq (2 - 1)}$
24	19 23	eleqtrdi	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to A \in ℤ_{\geq (2 - 1)}$
25		fzsuc2	$⊢ (2 \in ℤ \land A \in ℤ_{\geq (2 - 1)}) \to (2 \dots A + 1) = (2 \dots A) \cup \{A + 1\}$
26	10 24 25	sylancr	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to (2 \dots A + 1) = (2 \dots A) \cup \{A + 1\}$
27	9 26	eleqtrd	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in ((2 \dots A) \cup \{A + 1\})$
28		elun	$⊢ x \in ((2 \dots A) \cup \{A + 1\}) \leftrightarrow (x \in (2 \dots A) \lor x \in \{A + 1\})$
29	27 28	sylib	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to (x \in (2 \dots A) \lor x \in \{A + 1\})$
30	29	ord	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to (\neg x \in (2 \dots A) \to x \in \{A + 1\})$
31	8 30	mt3d	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in (2 \dots A)$
32	31 2	elind	$⊢ (A \in ℤ \land (\neg A + 1 \in ℙ \land x \in ((2 \dots A + 1) \cap ℙ))) \to x \in ((2 \dots A) \cap ℙ)$
33	32	expr	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (x \in ((2 \dots A + 1) \cap ℙ) \to x \in ((2 \dots A) \cap ℙ))$
34	33	ssrdv	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (2 \dots A + 1) \cap ℙ \subseteq (2 \dots A) \cap ℙ$
35		uzid	$⊢ A \in ℤ \to A \in ℤ_{\geq A}$
36	35	adantr	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to A \in ℤ_{\geq A}$
37		peano2uz	$⊢ A \in ℤ_{\geq A} \to A + 1 \in ℤ_{\geq A}$
38		fzss2	$⊢ A + 1 \in ℤ_{\geq A} \to (2 \dots A) \subseteq (2 \dots A + 1)$
39		ssrin	$⊢ (2 \dots A) \subseteq (2 \dots A + 1) \to (2 \dots A) \cap ℙ \subseteq (2 \dots A + 1) \cap ℙ$
40	36 37 38 39	4syl	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (2 \dots A) \cap ℙ \subseteq (2 \dots A + 1) \cap ℙ$
41	34 40	eqssd	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (2 \dots A + 1) \cap ℙ = (2 \dots A) \cap ℙ$
42		peano2z	$⊢ A \in ℤ \to A + 1 \in ℤ$
43	42	adantr	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to A + 1 \in ℤ$
44		flid	$⊢ A + 1 \in ℤ \to ⌊A + 1⌋ = A + 1$
45	43 44	syl	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to ⌊A + 1⌋ = A + 1$
46	45	oveq2d	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (2 \dots ⌊A + 1⌋) = (2 \dots A + 1)$
47	46	ineq1d	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (2 \dots ⌊A + 1⌋) \cap ℙ = (2 \dots A + 1) \cap ℙ$
48		flid	$⊢ A \in ℤ \to ⌊A⌋ = A$
49	48	adantr	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to ⌊A⌋ = A$
50	49	oveq2d	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (2 \dots ⌊A⌋) = (2 \dots A)$
51	50	ineq1d	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (2 \dots ⌊A⌋) \cap ℙ = (2 \dots A) \cap ℙ$
52	41 47 51	3eqtr4d	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to (2 \dots ⌊A + 1⌋) \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
53		zre	$⊢ A \in ℤ \to A \in ℝ$
54	53	adantr	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to A \in ℝ$
55		peano2re	$⊢ A \in ℝ \to A + 1 \in ℝ$
56		ppisval	$⊢ A + 1 \in ℝ \to [0, A + 1] \cap ℙ = (2 \dots ⌊A + 1⌋) \cap ℙ$
57	54 55 56	3syl	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to [0, A + 1] \cap ℙ = (2 \dots ⌊A + 1⌋) \cap ℙ$
58		ppisval	$⊢ A \in ℝ \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
59	54 58	syl	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
60	52 57 59	3eqtr4d	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to [0, A + 1] \cap ℙ = [0, A] \cap ℙ$
61	60	sumeq1d	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to \sum_{p \in [0, A + 1] \cap ℙ} \log p = \sum_{p \in [0, A] \cap ℙ} \log p$
62		chtval	$⊢ A + 1 \in ℝ \to θ (A + 1) = \sum_{p \in [0, A + 1] \cap ℙ} \log p$
63	54 55 62	3syl	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to θ (A + 1) = \sum_{p \in [0, A + 1] \cap ℙ} \log p$
64		chtval	$⊢ A \in ℝ \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
65	54 64	syl	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
66	61 63 65	3eqtr4d	$⊢ (A \in ℤ \land \neg A + 1 \in ℙ) \to θ (A + 1) = θ (A)$

Metamath Proof Explorer

Theorem chtnprm

Proof