This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑃 ↑ 𝐴 ) ) = 𝐴 )