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		simpll	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P \in ℙ$
19		simplr1	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to A \in ℤ$
20		simpr	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to A \neq 0$
21		pczdvds	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0)) \to P^{P pCnt A} ∥ A$
22	18 19 20 21	syl12anc	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P^{P pCnt A} ∥ A$
23		simplr3	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to A ∥ B$
24		prmnn	$⊢ P \in ℙ \to P \in ℕ$
25	24	ad2antrr	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P \in ℕ$
26		pczcl	$⊢ (P \in ℙ \land (A \in ℤ \land A \neq 0)) \to P pCnt A \in ℕ_{0}$
27	18 19 20 26	syl12anc	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P pCnt A \in ℕ_{0}$
28	25 27	nnexpcld	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P^{P pCnt A} \in ℕ$
29	28	nnzd	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P^{P pCnt A} \in ℤ$
30		simplr2	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to B \in ℤ$
31		dvdstr	$⊢ (P^{P pCnt A} \in ℤ \land A \in ℤ \land B \in ℤ) \to ((P^{P pCnt A} ∥ A \land A ∥ B) \to P^{P pCnt A} ∥ B)$
32	29 19 30 31	syl3anc	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to ((P^{P pCnt A} ∥ A \land A ∥ B) \to P^{P pCnt A} ∥ B)$
33	22 23 32	mp2and	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P^{P pCnt A} ∥ B$
34		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)$
35	18 30 27 34	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)$
36	33 35	mpbird	$⊢ ((P \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \land A \neq 0) \to P pCnt A \leq P pCnt B$
37	17 36	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