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

Metamath Proof Explorer

Theorem prmone0

Description: The primorial function is nonzero. (Contributed by AV, 28-Aug-2020)

Ref Expression
Assertion prmone0 ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 prmocl ⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ∈ ℕ )
2 1 nnne0d ⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ≠ 0 )