Metamath Proof Explorer

Theorem fmtno5faclem2

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

Ref Expression
Assertion fmtno5faclem2 ( 6 7 0 0 4 1 7 · 6 ) = 4 0 2 0 2 5 0 2

Proof

Step Hyp Ref Expression
1 6nn0 ⊢ 6 ∈ ℕ0
2 7nn0 ⊢ 7 ∈ ℕ0
3 1 2 deccl ⊢ 6 7 ∈ ℕ0
4 0nn0 ⊢ 0 ∈ ℕ0
5 3 4 deccl ⊢ 6 7 0 ∈ ℕ0
6 5 4 deccl ⊢ 6 7 0 0 ∈ ℕ0
7 4nn0 ⊢ 4 ∈ ℕ0
8 6 7 deccl ⊢ 6 7 0 0 4 ∈ ℕ0
9 1nn0 ⊢ 1 ∈ ℕ0
10 8 9 deccl ⊢ 6 7 0 0 4 1 ∈ ℕ0
11 eqid ⊢ 6 7 0 0 4 1 7 = 6 7 0 0 4 1 7
12 2nn0 ⊢ 2 ∈ ℕ0
13 7 4 deccl ⊢ 4 0 ∈ ℕ0
14 13 12 deccl ⊢ 4 0 2 ∈ ℕ0
15 14 4 deccl ⊢ 4 0 2 0 ∈ ℕ0
16 15 12 deccl ⊢ 4 0 2 0 2 ∈ ℕ0
17 16 7 deccl ⊢ 4 0 2 0 2 4 ∈ ℕ0
18 eqid ⊢ 6 7 0 0 4 1 = 6 7 0 0 4 1
19 eqid ⊢ 6 7 0 0 4 = 6 7 0 0 4
20 eqid ⊢ 6 7 0 0 = 6 7 0 0
21 eqid ⊢ 6 7 0 = 6 7 0
22 eqid ⊢ 6 7 = 6 7
23 3nn0 ⊢ 3 ∈ ℕ0
24 6t6e36 ⊢ ( 6 · 6 ) = 3 6
25 3p1e4 ⊢ ( 3 + 1 ) = 4
26 6p4e10 ⊢ ( 6 + 4 ) = 1 0
27 23 1 7 24 25 26 decaddci2 ⊢ ( ( 6 · 6 ) + 4 ) = 4 0
28 7t6e42 ⊢ ( 7 · 6 ) = 4 2
29 1 1 2 22 12 7 27 28 decmul1c ⊢ ( 6 7 · 6 ) = 4 0 2
30 6cn ⊢ 6 ∈ ℂ
31 30 mul02i ⊢ ( 0 · 6 ) = 0
32 1 3 4 21 29 31 decmul1 ⊢ ( 6 7 0 · 6 ) = 4 0 2 0
33 1 5 4 20 32 31 decmul1 ⊢ ( 6 7 0 0 · 6 ) = 4 0 2 0 0
34 2cn ⊢ 2 ∈ ℂ
35 34 addid2i ⊢ ( 0 + 2 ) = 2
36 15 4 12 33 35 decaddi ⊢ ( ( 6 7 0 0 · 6 ) + 2 ) = 4 0 2 0 2
37 4cn ⊢ 4 ∈ ℂ
38 6t4e24 ⊢ ( 6 · 4 ) = 2 4
39 30 37 38 mulcomli ⊢ ( 4 · 6 ) = 2 4
40 1 6 7 19 7 12 36 39 decmul1c ⊢ ( 6 7 0 0 4 · 6 ) = 4 0 2 0 2 4
41 30 mulid2i ⊢ ( 1 · 6 ) = 6
42 1 8 9 18 40 41 decmul1 ⊢ ( 6 7 0 0 4 1 · 6 ) = 4 0 2 0 2 4 6
43 eqid ⊢ 4 0 2 0 2 4 = 4 0 2 0 2 4
44 4p1e5 ⊢ ( 4 + 1 ) = 5
45 16 7 9 43 44 decaddi ⊢ ( 4 0 2 0 2 4 + 1 ) = 4 0 2 0 2 5
46 17 1 7 42 45 26 decaddci2 ⊢ ( ( 6 7 0 0 4 1 · 6 ) + 4 ) = 4 0 2 0 2 5 0
47 1 10 2 11 12 7 46 28 decmul1c ⊢ ( 6 7 0 0 4 1 7 · 6 ) = 4 0 2 0 2 5 0 2