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 · 7 1 1 ) = 1 6 7 0 8 5

Proof

Step Hyp Ref Expression
1 2nn0 2 ∈ ℕ0
2 3nn0 3 ∈ ℕ0
3 1 2 deccl 2 3 ∈ ℕ0
4 5nn0 5 ∈ ℕ0
5 7nn0 7 ∈ ℕ0
6 1nn0 1 ∈ ℕ0
7 5 6 deccl 7 1 ∈ ℕ0
8 eqid 7 1 = 7 1
9 6nn0 6 ∈ ℕ0
10 6 9 deccl 1 6 ∈ ℕ0
11 eqid 2 3 = 2 3
12 4nn0 4 ∈ ℕ0
13 7cn 7 ∈ ℂ
14 2cn 2 ∈ ℂ
15 7t2e14 ( 7 · 2 ) = 1 4
16 13 14 15 mulcomli ( 2 · 7 ) = 1 4
17 4p2e6 ( 4 + 2 ) = 6
18 6 12 1 16 17 decaddi ( ( 2 · 7 ) + 2 ) = 1 6
19 3cn 3 ∈ ℂ
20 7t3e21 ( 7 · 3 ) = 2 1
21 13 19 20 mulcomli ( 3 · 7 ) = 2 1
22 5 1 2 11 6 1 18 21 decmul1c ( 2 3 · 7 ) = 1 6 1
23 1p2e3 ( 1 + 2 ) = 3
24 10 6 1 22 23 decaddi ( ( 2 3 · 7 ) + 2 ) = 1 6 3
25 3 nn0cni 2 3 ∈ ℂ
26 25 mulid1i ( 2 3 · 1 ) = 2 3
27 3 5 6 8 2 1 24 26 decmul2c ( 2 3 · 7 1 ) = 1 6 3 3
28 2 4 deccl 3 5 ∈ ℕ0
29 7 nn0cni 7 1 ∈ ℂ
30 5cn 5 ∈ ℂ
31 7t5e35 ( 7 · 5 ) = 3 5
32 30 mulid2i ( 1 · 5 ) = 5
33 4 5 6 8 31 32 decmul1 ( 7 1 · 5 ) = 3 5 5
34 29 30 33 mulcomli ( 5 · 7 1 ) = 3 5 5
35 28 nn0cni 3 5 ∈ ℂ
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 · 1 ) + ( 5 · 7 1 ) ) = 3 7 8
43 30 mulid1i ( 5 · 1 ) = 5
44 4 dec0h 5 = 0 5
45 43 44 eqtri ( 5 · 1 ) = 0 5
46 10 2 deccl 1 6 3 ∈ ℕ0
47 46 2 deccl 1 6 3 3 ∈ ℕ0
48 0nn0 0 ∈ ℕ0
49 2 5 deccl 3 7 ∈ ℕ0
50 8nn0 8 ∈ ℕ0
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 ∈ ℂ
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 · 7 1 1 ) = 1 6 7 0 8 5