Metamath Proof Explorer

Theorem fmtno5lem2

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

Ref Expression
Assertion fmtno5lem2 
|- ( ; ; ; ; 6 5 5 3 6 x. 5 ) = ; ; ; ; ; 3 2 7 6 8 0

Proof

Step Hyp Ref Expression
1 5nn0 
 |-  5 e. NN0
2 6nn0 
 |-  6 e. NN0
3 2 1 deccl 
 |-  ; 6 5 e. NN0
4 3 1 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 0nn0 
 |-  0 e. NN0
9 2nn0 
 |-  2 e. NN0
10 5 9 deccl 
 |-  ; 3 2 e. NN0
11 7nn0 
 |-  7 e. NN0
12 10 11 deccl 
 |-  ; ; 3 2 7 e. NN0
13 12 2 deccl 
 |-  ; ; ; 3 2 7 6 e. NN0
14 eqid 
 |-  ; ; ; 6 5 5 3 = ; ; ; 6 5 5 3
15 1nn0 
 |-  1 e. NN0
16 5p1e6 
 |-  ( 5 + 1 ) = 6
17 eqid 
 |-  ; ; 6 5 5 = ; ; 6 5 5
18 eqid 
 |-  ; 6 5 = ; 6 5
19 6t5e30 
 |-  ( 6 x. 5 ) = ; 3 0
20 2cn 
 |-  2 e. CC
21 20 addid2i 
 |-  ( 0 + 2 ) = 2
22 5 8 9 19 21 decaddi 
 |-  ( ( 6 x. 5 ) + 2 ) = ; 3 2
23 5t5e25 
 |-  ( 5 x. 5 ) = ; 2 5
24 1 2 1 18 1 9 22 23 decmul1c 
 |-  ( ; 6 5 x. 5 ) = ; ; 3 2 5
25 5p2e7 
 |-  ( 5 + 2 ) = 7
26 10 1 9 24 25 decaddi 
 |-  ( ( ; 6 5 x. 5 ) + 2 ) = ; ; 3 2 7
27 1 3 1 17 1 9 26 23 decmul1c 
 |-  ( ; ; 6 5 5 x. 5 ) = ; ; ; 3 2 7 5
28 12 1 16 27 decsuc 
 |-  ( ( ; ; 6 5 5 x. 5 ) + 1 ) = ; ; ; 3 2 7 6
29 5cn 
 |-  5 e. CC
30 3cn 
 |-  3 e. CC
31 5t3e15 
 |-  ( 5 x. 3 ) = ; 1 5
32 29 30 31 mulcomli 
 |-  ( 3 x. 5 ) = ; 1 5
33 1 4 5 14 1 15 28 32 decmul1c 
 |-  ( ; ; ; 6 5 5 3 x. 5 ) = ; ; ; ; 3 2 7 6 5
34 5p3e8 
 |-  ( 5 + 3 ) = 8
35 13 1 5 33 34 decaddi 
 |-  ( ( ; ; ; 6 5 5 3 x. 5 ) + 3 ) = ; ; ; ; 3 2 7 6 8
36 1 6 2 7 8 5 35 19 decmul1c 
 |-  ( ; ; ; ; 6 5 5 3 6 x. 5 ) = ; ; ; ; ; 3 2 7 6 8 0