chtwordi

Description: The Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 22-Sep-2014)

		Ref	Expression
	Assertion	chtwordi	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to θ (A) \leq θ (B)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to B \in ℝ$
2		ppifi	$⊢ B \in ℝ \to [0, B] \cap ℙ \in Fin$
3	1 2	syl	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to [0, B] \cap ℙ \in Fin$
4		simpr	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land p \in ([0, B] \cap ℙ)) \to p \in ([0, B] \cap ℙ)$
5	4	elin2d	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land p \in ([0, B] \cap ℙ)) \to p \in ℙ$
6		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
7	5 6	syl	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land p \in ([0, B] \cap ℙ)) \to p \in ℤ_{\geq 2}$
8		eluz2b2	$⊢ p \in ℤ_{\geq 2} \leftrightarrow (p \in ℕ \land 1 < p)$
9	7 8	sylib	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land p \in ([0, B] \cap ℙ)) \to (p \in ℕ \land 1 < p)$
10	9	simpld	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land p \in ([0, B] \cap ℙ)) \to p \in ℕ$
11	10	nnred	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land p \in ([0, B] \cap ℙ)) \to p \in ℝ$
12	9	simprd	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land p \in ([0, B] \cap ℙ)) \to 1 < p$
13	11 12	rplogcld	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land p \in ([0, B] \cap ℙ)) \to \log p \in ℝ^{+}$
14	13	rpred	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land p \in ([0, B] \cap ℙ)) \to \log p \in ℝ$
15	13	rpge0d	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land p \in ([0, B] \cap ℙ)) \to 0 \leq \log p$
16		0red	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to 0 \in ℝ$
17		0le0	$⊢ 0 \leq 0$
18	17	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to 0 \leq 0$
19		simp3	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to A \leq B$
20		iccss	$⊢ ((0 \in ℝ \land B \in ℝ) \land (0 \leq 0 \land A \leq B)) \to [0, A] \subseteq [0, B]$
21	16 1 18 19 20	syl22anc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to [0, A] \subseteq [0, B]$
22	21	ssrind	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to [0, A] \cap ℙ \subseteq [0, B] \cap ℙ$
23	3 14 15 22	fsumless	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \sum_{p \in [0, A] \cap ℙ} \log p \leq \sum_{p \in [0, B] \cap ℙ} \log p$
24		chtval	$⊢ A \in ℝ \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
25	24	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
26		chtval	$⊢ B \in ℝ \to θ (B) = \sum_{p \in [0, B] \cap ℙ} \log p$
27	1 26	syl	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to θ (B) = \sum_{p \in [0, B] \cap ℙ} \log p$
28	23 25 27	3brtr4d	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to θ (A) \leq θ (B)$

Metamath Proof Explorer

Theorem chtwordi

Proof