Theorem pcidlem

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

	Ref	Expression
Assertion	pcidlem	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 𝑃 ∈ ℙ )
2		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
3	1 2	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 𝑃 ∈ ℕ )
4		simpr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 𝐴 ∈ ℕ0 )
5	3 4	nnexpcld	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐴 ) ∈ ℕ )
6	1 5	pccld	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ0 )
7	6	nn0red	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ∈ ℝ )
8	7	leidd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ≤ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) )
9	5	nnzd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐴 ) ∈ ℤ )
10		pcdvdsb	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 ↑ 𝐴 ) ∈ ℤ ∧ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ0 ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ≤ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ∥ ( 𝑃 ↑ 𝐴 ) ) )
11	1 9 6 10	syl3anc	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ≤ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ∥ ( 𝑃 ↑ 𝐴 ) ) )
12	8 11	mpbid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ∥ ( 𝑃 ↑ 𝐴 ) )
13	3 6	nnexpcld	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ∈ ℕ )
14	13	nnzd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ∈ ℤ )
15		dvdsle	⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ∈ ℤ ∧ ( 𝑃 ↑ 𝐴 ) ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ∥ ( 𝑃 ↑ 𝐴 ) → ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ≤ ( 𝑃 ↑ 𝐴 ) ) )
16	14 5 15	syl2anc	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ∥ ( 𝑃 ↑ 𝐴 ) → ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ≤ ( 𝑃 ↑ 𝐴 ) ) )
17	12 16	mpd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ≤ ( 𝑃 ↑ 𝐴 ) )
18	3	nnred	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 𝑃 ∈ ℝ )
19	6	nn0zd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ∈ ℤ )
20		nn0z	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
21	20	adantl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 𝐴 ∈ ℤ )
22		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
23		eluz2gt1	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑃 )
24	1 22 23	3syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 1 < 𝑃 )
25	18 19 21 24	leexp2d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ≤ 𝐴 ↔ ( 𝑃 ↑ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ≤ ( 𝑃 ↑ 𝐴 ) ) )
26	17 25	mpbird	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ≤ 𝐴 )
27		iddvds	⊢ ( ( 𝑃 ↑ 𝐴 ) ∈ ℤ → ( 𝑃 ↑ 𝐴 ) ∥ ( 𝑃 ↑ 𝐴 ) )
28	9 27	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐴 ) ∥ ( 𝑃 ↑ 𝐴 ) )
29		pcdvdsb	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 ↑ 𝐴 ) ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( 𝐴 ≤ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ↔ ( 𝑃 ↑ 𝐴 ) ∥ ( 𝑃 ↑ 𝐴 ) ) )
30	1 9 4 29	syl3anc	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝐴 ≤ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ↔ ( 𝑃 ↑ 𝐴 ) ∥ ( 𝑃 ↑ 𝐴 ) ) )
31	28 30	mpbird	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 𝐴 ≤ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) )
32		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
33	32	adantl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
34	7 33	letri3d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) = 𝐴 ↔ ( ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ≤ 𝐴 ∧ 𝐴 ≤ ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) ) )
35	26 31 34	mpbir2and	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) = 𝐴 )