Metamath Proof Explorer

Theorem pc0

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

Ref Expression
Assertion pc0 ⊢ P ∈ ℙ → P pCnt 0 = +∞

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 zq ⊢ 0 ∈ ℤ → 0 ∈ ℚ
3 1 2 ax-mp ⊢ 0 ∈ ℚ
4 iftrue ⊢ r = 0 → if r = 0 +∞ ι z | ∃ x ∈ ℤ ∃ y ∈ ℕ r = x y ∧ z = sup n ∈ ℕ 0 | p n ∥ x ℝ < − sup n ∈ ℕ 0 | p n ∥ y ℝ < = +∞
5 4 adantl ⊢ p = P ∧ r = 0 → if r = 0 +∞ ι z | ∃ x ∈ ℤ ∃ y ∈ ℕ r = x y ∧ z = sup n ∈ ℕ 0 | p n ∥ x ℝ < − sup n ∈ ℕ 0 | p n ∥ y ℝ < = +∞
6 df-pc ⊢ pCnt = p ∈ ℙ , r ∈ ℚ ⟼ if r = 0 +∞ ι z | ∃ x ∈ ℤ ∃ y ∈ ℕ r = x y ∧ z = sup n ∈ ℕ 0 | p n ∥ x ℝ < − sup n ∈ ℕ 0 | p n ∥ y ℝ <
7 pnfex ⊢ +∞ ∈ V
8 5 6 7 ovmpoa ⊢ P ∈ ℙ ∧ 0 ∈ ℚ → P pCnt 0 = +∞
9 3 8 mpan2 ⊢ P ∈ ℙ → P pCnt 0 = +∞