Metamath Proof Explorer

Theorem fmtno5lem2

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

Ref Expression
Assertion fmtno5lem2 ( 6 5 5 3 6 · 5 ) = 3 2 7 6 8 0

Proof

Step Hyp Ref Expression
1 5nn0 ⊢ 5 ∈ ℕ0
2 6nn0 ⊢ 6 ∈ ℕ0
3 2 1 deccl ⊢ 6 5 ∈ ℕ0
4 3 1 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 0nn0 ⊢ 0 ∈ ℕ0
9 2nn0 ⊢ 2 ∈ ℕ0
10 5 9 deccl ⊢ 3 2 ∈ ℕ0
11 7nn0 ⊢ 7 ∈ ℕ0
12 10 11 deccl ⊢ 3 2 7 ∈ ℕ0
13 12 2 deccl ⊢ 3 2 7 6 ∈ ℕ0
14 eqid ⊢ 6 5 5 3 = 6 5 5 3
15 1nn0 ⊢ 1 ∈ ℕ0
16 5p1e6 ⊢ ( 5 + 1 ) = 6
17 eqid ⊢ 6 5 5 = 6 5 5
18 eqid ⊢ 6 5 = 6 5
19 6t5e30 ⊢ ( 6 · 5 ) = 3 0
20 2cn ⊢ 2 ∈ ℂ
21 20 addid2i ⊢ ( 0 + 2 ) = 2
22 5 8 9 19 21 decaddi ⊢ ( ( 6 · 5 ) + 2 ) = 3 2
23 5t5e25 ⊢ ( 5 · 5 ) = 2 5
24 1 2 1 18 1 9 22 23 decmul1c ⊢ ( 6 5 · 5 ) = 3 2 5
25 5p2e7 ⊢ ( 5 + 2 ) = 7
26 10 1 9 24 25 decaddi ⊢ ( ( 6 5 · 5 ) + 2 ) = 3 2 7
27 1 3 1 17 1 9 26 23 decmul1c ⊢ ( 6 5 5 · 5 ) = 3 2 7 5
28 12 1 16 27 decsuc ⊢ ( ( 6 5 5 · 5 ) + 1 ) = 3 2 7 6
29 5cn ⊢ 5 ∈ ℂ
30 3cn ⊢ 3 ∈ ℂ
31 5t3e15 ⊢ ( 5 · 3 ) = 1 5
32 29 30 31 mulcomli ⊢ ( 3 · 5 ) = 1 5
33 1 4 5 14 1 15 28 32 decmul1c ⊢ ( 6 5 5 3 · 5 ) = 3 2 7 6 5
34 5p3e8 ⊢ ( 5 + 3 ) = 8
35 13 1 5 33 34 decaddi ⊢ ( ( 6 5 5 3 · 5 ) + 3 ) = 3 2 7 6 8
36 1 6 2 7 8 5 35 19 decmul1c ⊢ ( 6 5 5 3 6 · 5 ) = 3 2 7 6 8 0