Theorem pc0

Description: The value of the prime power function at zero. (Contributed by Mario Carneiro, 3-Oct-2014)

	Ref	Expression
Assertion	pc0	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 0 ) = +∞ )

Proof

Step	Hyp	Ref	Expression
1		0z	⊢ 0 ∈ ℤ
2		zq	⊢ ( 0 ∈ ℤ → 0 ∈ ℚ )
3	1 2	ax-mp	⊢ 0 ∈ ℚ
4		iftrue	⊢ ( 𝑟 = 0 → if ( 𝑟 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) ) = +∞ )
5	4	adantl	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑟 = 0 ) → if ( 𝑟 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) ) = +∞ )
6		df-pc	⊢ pCnt = ( 𝑝 ∈ ℙ , 𝑟 ∈ ℚ ↦ if ( 𝑟 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) ) )
7		pnfex	⊢ +∞ ∈ V
8	5 6 7	ovmpoa	⊢ ( ( 𝑃 ∈ ℙ ∧ 0 ∈ ℚ ) → ( 𝑃 pCnt 0 ) = +∞ )
9	3 8	mpan2	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 0 ) = +∞ )