Metamath Proof Explorer

Theorem 11t31e341

Description: 341 is the product of 11 and 31. (Contributed by AV, 3-Jun-2023)

Ref Expression
Assertion 11t31e341 
|- ( ; 1 1 x. ; 3 1 ) = ; ; 3 4 1

Proof

Step Hyp Ref Expression
1 3nn0 
 |-  3 e. NN0
2 1nn0 
 |-  1 e. NN0
3 1 2 deccl 
 |-  ; 3 1 e. NN0
4 eqid 
 |-  ; 1 1 = ; 1 1
5 3 nn0cni 
 |-  ; 3 1 e. CC
6 5 mulid2i 
 |-  ( 1 x. ; 3 1 ) = ; 3 1
7 3cn 
 |-  3 e. CC
8 ax-1cn 
 |-  1 e. CC
9 3p1e4 
 |-  ( 3 + 1 ) = 4
10 7 8 9 addcomli 
 |-  ( 1 + 3 ) = 4
11 1 2 1 6 10 decaddi 
 |-  ( ( 1 x. ; 3 1 ) + 3 ) = ; 3 4
12 3 2 2 4 2 1 11 6 decmul1c 
 |-  ( ; 1 1 x. ; 3 1 ) = ; ; 3 4 1