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

Metamath Proof Explorer

Theorem numnncl2

Description: Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses numnncl2.1 ⊢ 𝑇 ∈ ℕ
numnncl2.2 ⊢ 𝐴 ∈ ℕ
Assertion numnncl2 ( ( 𝑇 · 𝐴 ) + 0 ) ∈ ℕ

Proof

Step Hyp Ref Expression
1 numnncl2.1 ⊢ 𝑇 ∈ ℕ
2 numnncl2.2 ⊢ 𝐴 ∈ ℕ
3 1 2 nnmulcli ⊢ ( 𝑇 · 𝐴 ) ∈ ℕ
4 3 nncni ⊢ ( 𝑇 · 𝐴 ) ∈ ℂ
5 4 addridi ⊢ ( ( 𝑇 · 𝐴 ) + 0 ) = ( 𝑇 · 𝐴 )
6 5 3 eqeltri ⊢ ( ( 𝑇 · 𝐴 ) + 0 ) ∈ ℕ