Metamath Proof Explorer

Theorem fmtno5faclem3

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

Ref Expression
Assertion fmtno5faclem3 
|- ( ; ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 0 + ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8 ) = ; ; ; ; ; ; ; ; 4 2 8 8 2 6 6 8 8

Proof

Step Hyp Ref Expression
1 4nn0 
 |-  4 e. NN0
2 0nn0 
 |-  0 e. NN0
3 1 2 deccl 
 |-  ; 4 0 e. NN0
4 2nn0 
 |-  2 e. NN0
5 3 4 deccl 
 |-  ; ; 4 0 2 e. NN0
6 5 2 deccl 
 |-  ; ; ; 4 0 2 0 e. NN0
7 6 4 deccl 
 |-  ; ; ; ; 4 0 2 0 2 e. NN0
8 5nn0 
 |-  5 e. NN0
9 7 8 deccl 
 |-  ; ; ; ; ; 4 0 2 0 2 5 e. NN0
10 9 2 deccl 
 |-  ; ; ; ; ; ; 4 0 2 0 2 5 0 e. NN0
11 10 4 deccl 
 |-  ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 e. NN0
12 6nn0 
 |-  6 e. NN0
13 4 12 deccl 
 |-  ; 2 6 e. NN0
14 8nn0 
 |-  8 e. NN0
15 13 14 deccl 
 |-  ; ; 2 6 8 e. NN0
16 15 2 deccl 
 |-  ; ; ; 2 6 8 0 e. NN0
17 1nn0 
 |-  1 e. NN0
18 16 17 deccl 
 |-  ; ; ; ; 2 6 8 0 1 e. NN0
19 18 12 deccl 
 |-  ; ; ; ; ; 2 6 8 0 1 6 e. NN0
20 19 12 deccl 
 |-  ; ; ; ; ; ; 2 6 8 0 1 6 6 e. NN0
21 eqid 
 |-  ; ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 0 = ; ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 0
22 eqid 
 |-  ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8 = ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8
23 eqid 
 |-  ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 = ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2
24 eqid 
 |-  ; ; ; ; ; ; 2 6 8 0 1 6 6 = ; ; ; ; ; ; 2 6 8 0 1 6 6
25 eqid 
 |-  ; ; ; ; ; ; 4 0 2 0 2 5 0 = ; ; ; ; ; ; 4 0 2 0 2 5 0
26 eqid 
 |-  ; ; ; ; ; 2 6 8 0 1 6 = ; ; ; ; ; 2 6 8 0 1 6
27 eqid 
 |-  ; ; ; ; ; 4 0 2 0 2 5 = ; ; ; ; ; 4 0 2 0 2 5
28 eqid 
 |-  ; ; ; ; 2 6 8 0 1 = ; ; ; ; 2 6 8 0 1
29 eqid 
 |-  ; ; ; ; 4 0 2 0 2 = ; ; ; ; 4 0 2 0 2
30 eqid 
 |-  ; ; ; 2 6 8 0 = ; ; ; 2 6 8 0
31 eqid 
 |-  ; ; ; 4 0 2 0 = ; ; ; 4 0 2 0
32 eqid 
 |-  ; ; 2 6 8 = ; ; 2 6 8
33 eqid 
 |-  ; ; 4 0 2 = ; ; 4 0 2
34 eqid 
 |-  ; 2 6 = ; 2 6
35 eqid 
 |-  ; 4 0 = ; 4 0
36 2cn 
 |-  2 e. CC
37 36 addid2i 
 |-  ( 0 + 2 ) = 2
38 1 2 4 35 37 decaddi 
 |-  ( ; 4 0 + 2 ) = ; 4 2
39 6cn 
 |-  6 e. CC
40 6p2e8 
 |-  ( 6 + 2 ) = 8
41 39 36 40 addcomli 
 |-  ( 2 + 6 ) = 8
42 3 4 4 12 33 34 38 41 decadd 
 |-  ( ; ; 4 0 2 + ; 2 6 ) = ; ; 4 2 8
43 8cn 
 |-  8 e. CC
44 43 addid2i 
 |-  ( 0 + 8 ) = 8
45 5 2 13 14 31 32 42 44 decadd 
 |-  ( ; ; ; 4 0 2 0 + ; ; 2 6 8 ) = ; ; ; 4 2 8 8
46 36 addid1i 
 |-  ( 2 + 0 ) = 2
47 6 4 15 2 29 30 45 46 decadd 
 |-  ( ; ; ; ; 4 0 2 0 2 + ; ; ; 2 6 8 0 ) = ; ; ; ; 4 2 8 8 2
48 5p1e6 
 |-  ( 5 + 1 ) = 6
49 7 8 16 17 27 28 47 48 decadd 
 |-  ( ; ; ; ; ; 4 0 2 0 2 5 + ; ; ; ; 2 6 8 0 1 ) = ; ; ; ; ; 4 2 8 8 2 6
50 39 addid2i 
 |-  ( 0 + 6 ) = 6
51 9 2 18 12 25 26 49 50 decadd 
 |-  ( ; ; ; ; ; ; 4 0 2 0 2 5 0 + ; ; ; ; ; 2 6 8 0 1 6 ) = ; ; ; ; ; ; 4 2 8 8 2 6 6
52 10 4 19 12 23 24 51 41 decadd 
 |-  ( ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 + ; ; ; ; ; ; 2 6 8 0 1 6 6 ) = ; ; ; ; ; ; ; 4 2 8 8 2 6 6 8
53 11 2 20 14 21 22 52 44 decadd 
 |-  ( ; ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 0 + ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8 ) = ; ; ; ; ; ; ; ; 4 2 8 8 2 6 6 8 8