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

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 ( 𝑃 ∈ ℙ → ( 𝑃 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 ) = +∞ )