Metamath Proof Explorer

Theorem fmtno5lem3

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

Ref Expression
Assertion fmtno5lem3 
|- ( ; ; ; ; 6 5 5 3 6 x. 3 ) = ; ; ; ; ; 1 9 6 6 0 8

Proof

Step Hyp Ref Expression
1 3nn0 
 |-  3 e. NN0
2 6nn0 
 |-  6 e. NN0
3 5nn0 
 |-  5 e. NN0
4 2 3 deccl 
 |-  ; 6 5 e. NN0
5 4 3 deccl 
 |-  ; ; 6 5 5 e. NN0
6 5 1 deccl 
 |-  ; ; ; 6 5 5 3 e. NN0
7 eqid 
 |-  ; ; ; ; 6 5 5 3 6 = ; ; ; ; 6 5 5 3 6
8 8nn0 
 |-  8 e. NN0
9 1nn0 
 |-  1 e. NN0
10 9nn0 
 |-  9 e. NN0
11 9 10 deccl 
 |-  ; 1 9 e. NN0
12 11 2 deccl 
 |-  ; ; 1 9 6 e. NN0
13 12 3 deccl 
 |-  ; ; ; 1 9 6 5 e. NN0
14 5p1e6 
 |-  ( 5 + 1 ) = 6
15 eqid 
 |-  ; ; ; 1 9 6 5 = ; ; ; 1 9 6 5
16 12 3 14 15 decsuc 
 |-  ( ; ; ; 1 9 6 5 + 1 ) = ; ; ; 1 9 6 6
17 eqid 
 |-  ; ; ; 6 5 5 3 = ; ; ; 6 5 5 3
18 eqid 
 |-  ; ; 6 5 5 = ; ; 6 5 5
19 eqid 
 |-  ; 6 5 = ; 6 5
20 8p1e9 
 |-  ( 8 + 1 ) = 9
21 6t3e18 
 |-  ( 6 x. 3 ) = ; 1 8
22 9 8 20 21 decsuc 
 |-  ( ( 6 x. 3 ) + 1 ) = ; 1 9
23 5t3e15 
 |-  ( 5 x. 3 ) = ; 1 5
24 1 2 3 19 3 9 22 23 decmul1c 
 |-  ( ; 6 5 x. 3 ) = ; ; 1 9 5
25 11 3 14 24 decsuc 
 |-  ( ( ; 6 5 x. 3 ) + 1 ) = ; ; 1 9 6
26 1 4 3 18 3 9 25 23 decmul1c 
 |-  ( ; ; 6 5 5 x. 3 ) = ; ; ; 1 9 6 5
27 3t3e9 
 |-  ( 3 x. 3 ) = 9
28 1 5 1 17 26 27 decmul1 
 |-  ( ; ; ; 6 5 5 3 x. 3 ) = ; ; ; ; 1 9 6 5 9
29 13 16 28 decsucc 
 |-  ( ( ; ; ; 6 5 5 3 x. 3 ) + 1 ) = ; ; ; ; 1 9 6 6 0
30 1 6 2 7 8 9 29 21 decmul1c 
 |-  ( ; ; ; ; 6 5 5 3 6 x. 3 ) = ; ; ; ; ; 1 9 6 6 0 8