pcidlem

Description: The prime count of a prime power. (Contributed by Mario Carneiro, 12-Mar-2014)

		Ref	Expression
	Assertion	pcidlem	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P pCnt P^{A} = A$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P \in ℙ$
2		prmnn	$⊢ P \in ℙ \to P \in ℕ$
3	1 2	syl	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P \in ℕ$
4		simpr	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to A \in ℕ_{0}$
5	3 4	nnexpcld	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P^{A} \in ℕ$
6	1 5	pccld	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P pCnt P^{A} \in ℕ_{0}$
7	6	nn0red	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P pCnt P^{A} \in ℝ$
8	7	leidd	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P pCnt P^{A} \leq P pCnt P^{A}$
9	5	nnzd	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P^{A} \in ℤ$
10		pcdvdsb	$⊢ (P \in ℙ \land P^{A} \in ℤ \land P pCnt P^{A} \in ℕ_{0}) \to (P pCnt P^{A} \leq P pCnt P^{A} \leftrightarrow P^{P pCnt P^{A}} ∥ P^{A})$
11	1 9 6 10	syl3anc	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to (P pCnt P^{A} \leq P pCnt P^{A} \leftrightarrow P^{P pCnt P^{A}} ∥ P^{A})$
12	8 11	mpbid	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P^{P pCnt P^{A}} ∥ P^{A}$
13	3 6	nnexpcld	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P^{P pCnt P^{A}} \in ℕ$
14	13	nnzd	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P^{P pCnt P^{A}} \in ℤ$
15		dvdsle	$⊢ (P^{P pCnt P^{A}} \in ℤ \land P^{A} \in ℕ) \to (P^{P pCnt P^{A}} ∥ P^{A} \to P^{P pCnt P^{A}} \leq P^{A})$
16	14 5 15	syl2anc	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to (P^{P pCnt P^{A}} ∥ P^{A} \to P^{P pCnt P^{A}} \leq P^{A})$
17	12 16	mpd	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P^{P pCnt P^{A}} \leq P^{A}$
18	3	nnred	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P \in ℝ$
19	6	nn0zd	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P pCnt P^{A} \in ℤ$
20		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
21	20	adantl	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to A \in ℤ$
22		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
23		eluz2gt1	$⊢ P \in ℤ_{\geq 2} \to 1 < P$
24	1 22 23	3syl	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to 1 < P$
25	18 19 21 24	leexp2d	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to (P pCnt P^{A} \leq A \leftrightarrow P^{P pCnt P^{A}} \leq P^{A})$
26	17 25	mpbird	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P pCnt P^{A} \leq A$
27		iddvds	$⊢ P^{A} \in ℤ \to P^{A} ∥ P^{A}$
28	9 27	syl	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P^{A} ∥ P^{A}$
29		pcdvdsb	$⊢ (P \in ℙ \land P^{A} \in ℤ \land A \in ℕ_{0}) \to (A \leq P pCnt P^{A} \leftrightarrow P^{A} ∥ P^{A})$
30	1 9 4 29	syl3anc	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to (A \leq P pCnt P^{A} \leftrightarrow P^{A} ∥ P^{A})$
31	28 30	mpbird	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to A \leq P pCnt P^{A}$
32		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
33	32	adantl	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to A \in ℝ$
34	7 33	letri3d	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to (P pCnt P^{A} = A \leftrightarrow (P pCnt P^{A} \leq A \land A \leq P pCnt P^{A}))$
35	26 31 34	mpbir2and	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P pCnt P^{A} = A$

Metamath Proof Explorer

Theorem pcidlem

Proof