Theorem pczdvds

Description: Defining property of the prime count function. (Contributed by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Assertion	pczdvds	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 )

Proof

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