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

Metamath Proof Explorer

Theorem 11multnc

Description: The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021)

Ref Expression
Hypothesis 11multnc.n ⊢ 𝑁 ∈ ℕ0
Assertion 11multnc ( 𝑁 · 1 1 ) = 𝑁 𝑁

Proof

Step Hyp Ref Expression
1 11multnc.n ⊢ 𝑁 ∈ ℕ0
2 1nn0 ⊢ 1 ∈ ℕ0
3 1 2 2 decmulnc ⊢ ( 𝑁 · 1 1 ) = ( 𝑁 · 1 ) ( 𝑁 · 1 )
4 1 nn0cni ⊢ 𝑁 ∈ ℂ
5 4 mulridi ⊢ ( 𝑁 · 1 ) = 𝑁
6 5 5 deceq12i ⊢ ( 𝑁 · 1 ) ( 𝑁 · 1 ) = 𝑁 𝑁
7 3 6 eqtri ⊢ ( 𝑁 · 1 1 ) = 𝑁 𝑁