ppiwordi

Description: The prime-counting function ppi is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014)

		Ref	Expression
	Assertion	ppiwordi	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \underline{π} (A) \leq \underline{π} (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		0red	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to 0 \in ℝ$
5		0le0	$⊢ 0 \leq 0$
6	5	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to 0 \leq 0$
7		simp3	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to A \leq B$
8		iccss	$⊢ ((0 \in ℝ \land B \in ℝ) \land (0 \leq 0 \land A \leq B)) \to [0, A] \subseteq [0, B]$
9	4 1 6 7 8	syl22anc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to [0, A] \subseteq [0, B]$
10	9	ssrind	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to [0, A] \cap ℙ \subseteq [0, B] \cap ℙ$
11		ssdomg	$⊢ [0, B] \cap ℙ \in Fin \to ([0, A] \cap ℙ \subseteq [0, B] \cap ℙ \to ([0, A] \cap ℙ) ≼ ([0, B] \cap ℙ))$
12	3 10 11	sylc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to ([0, A] \cap ℙ) ≼ ([0, B] \cap ℙ)$
13		ppifi	$⊢ A \in ℝ \to [0, A] \cap ℙ \in Fin$
14	13	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to [0, A] \cap ℙ \in Fin$
15		hashdom	$⊢ ([0, A] \cap ℙ \in Fin \land [0, B] \cap ℙ \in Fin) \to (\|[0, A] \cap ℙ\| \leq \|[0, B] \cap ℙ\| \leftrightarrow ([0, A] \cap ℙ) ≼ ([0, B] \cap ℙ))$
16	14 3 15	syl2anc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to (\|[0, A] \cap ℙ\| \leq \|[0, B] \cap ℙ\| \leftrightarrow ([0, A] \cap ℙ) ≼ ([0, B] \cap ℙ))$
17	12 16	mpbird	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \|[0, A] \cap ℙ\| \leq \|[0, B] \cap ℙ\|$
18		ppival	$⊢ A \in ℝ \to \underline{π} (A) = \|[0, A] \cap ℙ\|$
19	18	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \underline{π} (A) = \|[0, A] \cap ℙ\|$
20		ppival	$⊢ B \in ℝ \to \underline{π} (B) = \|[0, B] \cap ℙ\|$
21	1 20	syl	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \underline{π} (B) = \|[0, B] \cap ℙ\|$
22	17 19 21	3brtr4d	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \underline{π} (A) \leq \underline{π} (B)$

Metamath Proof Explorer

Theorem ppiwordi

Proof