Metamath Proof Explorer

Theorem fmtno5lem1

Description: Lemma 1 for fmtno5 . (Contributed by AV, 22-Jul-2021)

Ref Expression
Assertion fmtno5lem1 
|- ( ; ; ; ; 6 5 5 3 6 x. 6 ) = ; ; ; ; ; 3 9 3 2 1 6

Proof

Step Hyp Ref Expression
1 6nn0 
 |-  6 e. NN0
2 5nn0 
 |-  5 e. NN0
3 1 2 deccl 
 |-  ; 6 5 e. NN0
4 3 2 deccl 
 |-  ; ; 6 5 5 e. NN0
5 3nn0 
 |-  3 e. NN0
6 4 5 deccl 
 |-  ; ; ; 6 5 5 3 e. NN0
7 eqid 
 |-  ; ; ; ; 6 5 5 3 6 = ; ; ; ; 6 5 5 3 6
8 9nn0 
 |-  9 e. NN0
9 5 8 deccl 
 |-  ; 3 9 e. NN0
10 9 5 deccl 
 |-  ; ; 3 9 3 e. NN0
11 1nn0 
 |-  1 e. NN0
12 10 11 deccl 
 |-  ; ; ; 3 9 3 1 e. NN0
13 8nn0 
 |-  8 e. NN0
14 eqid 
 |-  ; ; ; 6 5 5 3 = ; ; ; 6 5 5 3
15 0nn0 
 |-  0 e. NN0
16 0p1e1 
 |-  ( 0 + 1 ) = 1
17 eqid 
 |-  ; ; 6 5 5 = ; ; 6 5 5
18 eqid 
 |-  ; 6 5 = ; 6 5
19 6t6e36 
 |-  ( 6 x. 6 ) = ; 3 6
20 6p3e9 
 |-  ( 6 + 3 ) = 9
21 5 1 5 19 20 decaddi 
 |-  ( ( 6 x. 6 ) + 3 ) = ; 3 9
22 6cn 
 |-  6 e. CC
23 5cn 
 |-  5 e. CC
24 6t5e30 
 |-  ( 6 x. 5 ) = ; 3 0
25 22 23 24 mulcomli 
 |-  ( 5 x. 6 ) = ; 3 0
26 1 1 2 18 15 5 21 25 decmul1c 
 |-  ( ; 6 5 x. 6 ) = ; ; 3 9 0
27 3cn 
 |-  3 e. CC
28 27 addid2i 
 |-  ( 0 + 3 ) = 3
29 9 15 5 26 28 decaddi 
 |-  ( ( ; 6 5 x. 6 ) + 3 ) = ; ; 3 9 3
30 1 3 2 17 15 5 29 25 decmul1c 
 |-  ( ; ; 6 5 5 x. 6 ) = ; ; ; 3 9 3 0
31 10 15 16 30 decsuc 
 |-  ( ( ; ; 6 5 5 x. 6 ) + 1 ) = ; ; ; 3 9 3 1
32 6t3e18 
 |-  ( 6 x. 3 ) = ; 1 8
33 22 27 32 mulcomli 
 |-  ( 3 x. 6 ) = ; 1 8
34 1 4 5 14 13 11 31 33 decmul1c 
 |-  ( ; ; ; 6 5 5 3 x. 6 ) = ; ; ; ; 3 9 3 1 8
35 1p1e2 
 |-  ( 1 + 1 ) = 2
36 eqid 
 |-  ; ; ; 3 9 3 1 = ; ; ; 3 9 3 1
37 10 11 35 36 decsuc 
 |-  ( ; ; ; 3 9 3 1 + 1 ) = ; ; ; 3 9 3 2
38 8p3e11 
 |-  ( 8 + 3 ) = ; 1 1
39 12 13 5 34 37 11 38 decaddci 
 |-  ( ( ; ; ; 6 5 5 3 x. 6 ) + 3 ) = ; ; ; ; 3 9 3 2 1
40 1 6 1 7 1 5 39 19 decmul1c 
 |-  ( ; ; ; ; 6 5 5 3 6 x. 6 ) = ; ; ; ; ; 3 9 3 2 1 6