pcdvdstr

Description: The prime count increases under the divisibility relation. (Contributed by Mario Carneiro, 13-Mar-2014)

		Ref	Expression
	Assertion	pcdvdstr	$⊢ (P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \to P pCnt A \leq P pCnt B$

Proof

Step	Hyp	Ref	Expression
1		0z	$⊢ 0 \in ℤ$
2		zq	$⊢ 0 \in ℤ \to 0 \in ℚ$
3	1 2	ax-mp	$⊢ 0 \in ℚ$
4		pcxcl	$⊢ (P \in ℙ \land 0 \in ℚ) \to P pCnt 0 \in ℝ^{*}$
5	3 4	mpan2	$⊢ P \in ℙ \to P pCnt 0 \in ℝ^{*}$
6	5	xrleidd	$⊢ P \in ℙ \to P pCnt 0 \leq P pCnt 0$
7	6	ad2antrr	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A = 0) \to P pCnt 0 \leq P pCnt 0$
8		simpr	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A = 0) \to A = 0$
9	8	oveq2d	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A = 0) \to P pCnt A = P pCnt 0$
10		simplr3	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A = 0) \to A ∥ B$
11	8 10	eqbrtrrd	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A = 0) \to 0 ∥ B$
12		simplr2	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A = 0) \to B \in ℤ$
13		0dvds	$⊢ B \in ℤ \to (0 ∥ B \leftrightarrow B = 0)$
14	12 13	syl	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A = 0) \to (0 ∥ B \leftrightarrow B = 0)$
15	11 14	mpbid	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A = 0) \to B = 0$
16	15	oveq2d	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A = 0) \to P pCnt B = P pCnt 0$
17	7 9 16	3brtr4d	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A = 0) \to P pCnt A \leq P pCnt B$
18		prmnn	$⊢ P \in ℙ \to P \in ℕ$
19	18	ad2antrr	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P \in ℕ$
20		simpll	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P \in ℙ$
21		simplr1	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to A \in ℤ$
22		simpr	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to A \neq 0$
23		pczcl	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0)) \to P pCnt A \in ℕ_{0}$
24	20 21 22 23	syl12anc	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P pCnt A \in ℕ_{0}$
25	19 24	nnexpcld	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P^{P pCnt A} \in ℕ$
26	25	nnzd	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P^{P pCnt A} \in ℤ$
27		simplr2	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to B \in ℤ$
28		pczdvds	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0)) \to P^{P pCnt A} ∥ A$
29	20 21 22 28	syl12anc	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P^{P pCnt A} ∥ A$
30		simplr3	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to A ∥ B$
31	26 21 27 29 30	dvdstrd	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P^{P pCnt A} ∥ B$
32		pcdvdsb	$⊢ (P \in ℙ \land B \in ℤ \land P pCnt A \in ℕ_{0}) \to (P pCnt A \leq P pCnt B \leftrightarrow P^{P pCnt A} ∥ B)$
33	20 27 24 32	syl3anc	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to (P pCnt A \leq P pCnt B \leftrightarrow P^{P pCnt A} ∥ B)$
34	31 33	mpbird	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P pCnt A \leq P pCnt B$
35	17 34	pm2.61dane	$⊢ (P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \to P pCnt A \leq P pCnt B$

Metamath Proof Explorer

Theorem pcdvdstr

Proof