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 
|- N e. NN0
Assertion 11multnc 
|- ( N x. ; 1 1 ) = ; N N

Proof

Step Hyp Ref Expression
1 11multnc.n 
 |-  N e. NN0
2 1nn0 
 |-  1 e. NN0
3 1 2 2 decmulnc 
 |-  ( N x. ; 1 1 ) = ; ( N x. 1 ) ( N x. 1 )
4 1 nn0cni 
 |-  N e. CC
5 4 mulid1i 
 |-  ( N x. 1 ) = N
6 5 5 deceq12i 
 |-  ; ( N x. 1 ) ( N x. 1 ) = ; N N
7 3 6 eqtri 
 |-  ( N x. ; 1 1 ) = ; N N