Metamath Proof Explorer

Theorem fmtno5lem1

Description: Lemma 1 for fmtno5 . (Contributed by AV, 22-Jul-2021)

Ref Expression
Assertion fmtno5lem1 ( 6 5 5 3 6 · 6 ) = 3 9 3 2 1 6

Proof

Step Hyp Ref Expression
1 6nn0 ⊢ 6 ∈ ℕ0
2 5nn0 ⊢ 5 ∈ ℕ0
3 1 2 deccl ⊢ 6 5 ∈ ℕ0
4 3 2 deccl ⊢ 6 5 5 ∈ ℕ0
5 3nn0 ⊢ 3 ∈ ℕ0
6 4 5 deccl ⊢ 6 5 5 3 ∈ ℕ0
7 eqid ⊢ 6 5 5 3 6 = 6 5 5 3 6
8 9nn0 ⊢ 9 ∈ ℕ0
9 5 8 deccl ⊢ 3 9 ∈ ℕ0
10 9 5 deccl ⊢ 3 9 3 ∈ ℕ0
11 1nn0 ⊢ 1 ∈ ℕ0
12 10 11 deccl ⊢ 3 9 3 1 ∈ ℕ0
13 8nn0 ⊢ 8 ∈ ℕ0
14 eqid ⊢ 6 5 5 3 = 6 5 5 3
15 0nn0 ⊢ 0 ∈ ℕ0
16 0p1e1 ⊢ ( 0 + 1 ) = 1
17 eqid ⊢ 6 5 5 = 6 5 5
18 eqid ⊢ 6 5 = 6 5
19 6t6e36 ⊢ ( 6 · 6 ) = 3 6
20 6p3e9 ⊢ ( 6 + 3 ) = 9
21 5 1 5 19 20 decaddi ⊢ ( ( 6 · 6 ) + 3 ) = 3 9
22 6cn ⊢ 6 ∈ ℂ
23 5cn ⊢ 5 ∈ ℂ
24 6t5e30 ⊢ ( 6 · 5 ) = 3 0
25 22 23 24 mulcomli ⊢ ( 5 · 6 ) = 3 0
26 1 1 2 18 15 5 21 25 decmul1c ⊢ ( 6 5 · 6 ) = 3 9 0
27 3cn ⊢ 3 ∈ ℂ
28 27 addid2i ⊢ ( 0 + 3 ) = 3
29 9 15 5 26 28 decaddi ⊢ ( ( 6 5 · 6 ) + 3 ) = 3 9 3
30 1 3 2 17 15 5 29 25 decmul1c ⊢ ( 6 5 5 · 6 ) = 3 9 3 0
31 10 15 16 30 decsuc ⊢ ( ( 6 5 5 · 6 ) + 1 ) = 3 9 3 1
32 6t3e18 ⊢ ( 6 · 3 ) = 1 8
33 22 27 32 mulcomli ⊢ ( 3 · 6 ) = 1 8
34 1 4 5 14 13 11 31 33 decmul1c ⊢ ( 6 5 5 3 · 6 ) = 3 9 3 1 8
35 1p1e2 ⊢ ( 1 + 1 ) = 2
36 eqid ⊢ 3 9 3 1 = 3 9 3 1
37 10 11 35 36 decsuc ⊢ ( 3 9 3 1 + 1 ) = 3 9 3 2
38 8p3e11 ⊢ ( 8 + 3 ) = 1 1
39 12 13 5 34 37 11 38 decaddci ⊢ ( ( 6 5 5 3 · 6 ) + 3 ) = 3 9 3 2 1
40 1 6 1 7 1 5 39 19 decmul1c ⊢ ( 6 5 5 3 6 · 6 ) = 3 9 3 2 1 6