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 |
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 |