Theorem pczcl

Description: Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Assertion	pczcl	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ sup ( { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 } , ℝ , < ) = sup ( { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 } , ℝ , < )
2	1	pczpre	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) = sup ( { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 } , ℝ , < ) )
3		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
4		eqid	⊢ { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 } = { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 }
5	4 1	pcprecl	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( sup ( { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 } , ℝ , < ) ∈ ℕ0 ∧ ( 𝑃 ↑ sup ( { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 } , ℝ , < ) ) ∥ 𝑁 ) )
6	3 5	sylan	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( sup ( { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 } , ℝ , < ) ∈ ℕ0 ∧ ( 𝑃 ↑ sup ( { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 } , ℝ , < ) ) ∥ 𝑁 ) )
7	6	simpld	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → sup ( { 𝑥 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑥 ) ∥ 𝑁 } , ℝ , < ) ∈ ℕ0 )
8	2 7	eqeltrd	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )