chtleppi

Description: Upper bound on the theta function. (Contributed by Mario Carneiro, 22-Sep-2014)

		Ref	Expression
	Assertion	chtleppi	$⊢ A \in ℝ^{+} \to θ (A) \leq \underline{π} (A) \log A$

Proof

Step	Hyp	Ref	Expression
1		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
2		ppifi	$⊢ A \in ℝ \to [0, A] \cap ℙ \in Fin$
3	1 2	syl	$⊢ A \in ℝ^{+} \to [0, A] \cap ℙ \in Fin$
4		simpr	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to p \in ([0, A] \cap ℙ)$
5	4	elin2d	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to p \in ℙ$
6		prmnn	$⊢ p \in ℙ \to p \in ℕ$
7	5 6	syl	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to p \in ℕ$
8	7	nnrpd	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to p \in ℝ^{+}$
9	8	relogcld	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to \log p \in ℝ$
10		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
11	10	adantr	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to \log A \in ℝ$
12	4	elin1d	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to p \in [0, A]$
13		0re	$⊢ 0 \in ℝ$
14		elicc2	$⊢ (0 \in ℝ \land A \in ℝ) \to (p \in [0, A] \leftrightarrow (p \in ℝ \land 0 \leq p \land p \leq A))$
15	13 1 14	sylancr	$⊢ A \in ℝ^{+} \to (p \in [0, A] \leftrightarrow (p \in ℝ \land 0 \leq p \land p \leq A))$
16	15	biimpa	$⊢ (A \in ℝ^{+} \land p \in [0, A]) \to (p \in ℝ \land 0 \leq p \land p \leq A)$
17	12 16	syldan	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to (p \in ℝ \land 0 \leq p \land p \leq A)$
18	17	simp3d	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to p \leq A$
19	8	reeflogd	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to e^{\log p} = p$
20		reeflog	$⊢ A \in ℝ^{+} \to e^{\log A} = A$
21	20	adantr	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to e^{\log A} = A$
22	18 19 21	3brtr4d	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to e^{\log p} \leq e^{\log A}$
23		efle	$⊢ (\log p \in ℝ \land \log A \in ℝ) \to (\log p \leq \log A \leftrightarrow e^{\log p} \leq e^{\log A})$
24	9 11 23	syl2anc	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to (\log p \leq \log A \leftrightarrow e^{\log p} \leq e^{\log A})$
25	22 24	mpbird	$⊢ (A \in ℝ^{+} \land p \in ([0, A] \cap ℙ)) \to \log p \leq \log A$
26	3 9 11 25	fsumle	$⊢ A \in ℝ^{+} \to \sum_{p \in [0, A] \cap ℙ} \log p \leq \sum_{p \in [0, A] \cap ℙ} \log A$
27		chtval	$⊢ A \in ℝ \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
28	1 27	syl	$⊢ A \in ℝ^{+} \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
29		ppival	$⊢ A \in ℝ \to \underline{π} (A) = \|[0, A] \cap ℙ\|$
30	1 29	syl	$⊢ A \in ℝ^{+} \to \underline{π} (A) = \|[0, A] \cap ℙ\|$
31	30	oveq1d	$⊢ A \in ℝ^{+} \to \underline{π} (A) \log A = \|[0, A] \cap ℙ\| \log A$
32	10	recnd	$⊢ A \in ℝ^{+} \to \log A \in ℂ$
33		fsumconst	$⊢ ([0, A] \cap ℙ \in Fin \land \log A \in ℂ) \to \sum_{p \in [0, A] \cap ℙ} \log A = \|[0, A] \cap ℙ\| \log A$
34	3 32 33	syl2anc	$⊢ A \in ℝ^{+} \to \sum_{p \in [0, A] \cap ℙ} \log A = \|[0, A] \cap ℙ\| \log A$
35	31 34	eqtr4d	$⊢ A \in ℝ^{+} \to \underline{π} (A) \log A = \sum_{p \in [0, A] \cap ℙ} \log A$
36	26 28 35	3brtr4d	$⊢ A \in ℝ^{+} \to θ (A) \leq \underline{π} (A) \log A$

Metamath Proof Explorer

Theorem chtleppi

Proof