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