Metamath Proof Explorer

Theorem ex-decpmul

Description: Example usage of decpmul . This proof is significantly longer than 235t711 . There is more unnecessary carrying compared to 235t711 . Although saving 5 visual steps, using mulcomli early on increases the compressed proof length. (Contributed by Steven Nguyen, 10-Dec-2022) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 3nn0 
 |-  3 e. NN0
3 1 2 deccl 
 |-  ; 2 3 e. NN0
4 5nn0 
 |-  5 e. NN0
5 7nn0 
 |-  7 e. NN0
6 1nn0 
 |-  1 e. NN0
7 5 6 deccl 
 |-  ; 7 1 e. NN0
8 eqid 
 |-  ; 7 1 = ; 7 1
9 6nn0 
 |-  6 e. NN0
10 6 9 deccl 
 |-  ; 1 6 e. NN0
11 eqid 
 |-  ; 2 3 = ; 2 3
12 4nn0 
 |-  4 e. NN0
13 7cn 
 |-  7 e. CC
14 2cn 
 |-  2 e. CC
15 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
16 13 14 15 mulcomli 
 |-  ( 2 x. 7 ) = ; 1 4
17 4p2e6 
 |-  ( 4 + 2 ) = 6
18 6 12 1 16 17 decaddi 
 |-  ( ( 2 x. 7 ) + 2 ) = ; 1 6
19 3cn 
 |-  3 e. CC
20 7t3e21 
 |-  ( 7 x. 3 ) = ; 2 1
21 13 19 20 mulcomli 
 |-  ( 3 x. 7 ) = ; 2 1
22 5 1 2 11 6 1 18 21 decmul1c 
 |-  ( ; 2 3 x. 7 ) = ; ; 1 6 1
23 1p2e3 
 |-  ( 1 + 2 ) = 3
24 10 6 1 22 23 decaddi 
 |-  ( ( ; 2 3 x. 7 ) + 2 ) = ; ; 1 6 3
25 3 nn0cni 
 |-  ; 2 3 e. CC
26 25 mulid1i 
 |-  ( ; 2 3 x. 1 ) = ; 2 3
27 3 5 6 8 2 1 24 26 decmul2c 
 |-  ( ; 2 3 x. ; 7 1 ) = ; ; ; 1 6 3 3
28 2 4 deccl 
 |-  ; 3 5 e. NN0
29 7 nn0cni 
 |-  ; 7 1 e. CC
30 5cn 
 |-  5 e. CC
31 7t5e35 
 |-  ( 7 x. 5 ) = ; 3 5
32 30 mulid2i 
 |-  ( 1 x. 5 ) = 5
33 4 5 6 8 31 32 decmul1 
 |-  ( ; 7 1 x. 5 ) = ; ; 3 5 5
34 29 30 33 mulcomli 
 |-  ( 5 x. ; 7 1 ) = ; ; 3 5 5
35 28 nn0cni 
 |-  ; 3 5 e. CC
36 eqid 
 |-  ; 3 5 = ; 3 5
37 5p2e7 
 |-  ( 5 + 2 ) = 7
38 2 4 1 36 37 decaddi 
 |-  ( ; 3 5 + 2 ) = ; 3 7
39 35 14 38 addcomli 
 |-  ( 2 + ; 3 5 ) = ; 3 7
40 5p3e8 
 |-  ( 5 + 3 ) = 8
41 30 19 40 addcomli 
 |-  ( 3 + 5 ) = 8
42 1 2 28 4 26 34 39 41 decadd 
 |-  ( ( ; 2 3 x. 1 ) + ( 5 x. ; 7 1 ) ) = ; ; 3 7 8
43 30 mulid1i 
 |-  ( 5 x. 1 ) = 5
44 4 dec0h 
 |-  5 = ; 0 5
45 43 44 eqtri 
 |-  ( 5 x. 1 ) = ; 0 5
46 10 2 deccl 
 |-  ; ; 1 6 3 e. NN0
47 46 2 deccl 
 |-  ; ; ; 1 6 3 3 e. NN0
48 0nn0 
 |-  0 e. NN0
49 2 5 deccl 
 |-  ; 3 7 e. NN0
50 8nn0 
 |-  8 e. NN0
51 eqid 
 |-  ; ; ; ; 1 6 3 3 0 = ; ; ; ; 1 6 3 3 0
52 eqid 
 |-  ; ; 3 7 8 = ; ; 3 7 8
53 eqid 
 |-  ; ; ; 1 6 3 3 = ; ; ; 1 6 3 3
54 eqid 
 |-  ; 3 7 = ; 3 7
55 eqid 
 |-  ; ; 1 6 3 = ; ; 1 6 3
56 3p3e6 
 |-  ( 3 + 3 ) = 6
57 10 2 2 55 56 decaddi 
 |-  ( ; ; 1 6 3 + 3 ) = ; ; 1 6 6
58 6p1e7 
 |-  ( 6 + 1 ) = 7
59 10 9 6 57 58 decaddi 
 |-  ( ( ; ; 1 6 3 + 3 ) + 1 ) = ; ; 1 6 7
60 7p3e10 
 |-  ( 7 + 3 ) = ; 1 0
61 13 19 60 addcomli 
 |-  ( 3 + 7 ) = ; 1 0
62 46 2 2 5 53 54 59 61 decaddc2 
 |-  ( ; ; ; 1 6 3 3 + ; 3 7 ) = ; ; ; 1 6 7 0
63 8cn 
 |-  8 e. CC
64 63 addid2i 
 |-  ( 0 + 8 ) = 8
65 47 48 49 50 51 52 62 64 decadd 
 |-  ( ; ; ; ; 1 6 3 3 0 + ; ; 3 7 8 ) = ; ; ; ; 1 6 7 0 8
66 3 4 7 6 27 42 45 65 48 4 decpmul 
 |-  ( ; ; 2 3 5 x. ; ; 7 1 1 ) = ; ; ; ; ; 1 6 7 0 8 5