Metamath Proof Explorer

Theorem fmtno5lem3

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

Ref Expression
Assertion fmtno5lem3 ( 6 5 5 3 6 · 3 ) = 1 9 6 6 0 8

Proof

Step Hyp Ref Expression
1 3nn0 ⊢ 3 ∈ ℕ0
2 6nn0 ⊢ 6 ∈ ℕ0
3 5nn0 ⊢ 5 ∈ ℕ0
4 2 3 deccl ⊢ 6 5 ∈ ℕ0
5 4 3 deccl ⊢ 6 5 5 ∈ ℕ0
6 5 1 deccl ⊢ 6 5 5 3 ∈ ℕ0
7 eqid ⊢ 6 5 5 3 6 = 6 5 5 3 6
8 8nn0 ⊢ 8 ∈ ℕ0
9 1nn0 ⊢ 1 ∈ ℕ0
10 9nn0 ⊢ 9 ∈ ℕ0
11 9 10 deccl ⊢ 1 9 ∈ ℕ0
12 11 2 deccl ⊢ 1 9 6 ∈ ℕ0
13 12 3 deccl ⊢ 1 9 6 5 ∈ ℕ0
14 5p1e6 ⊢ ( 5 + 1 ) = 6
15 eqid ⊢ 1 9 6 5 = 1 9 6 5
16 12 3 14 15 decsuc ⊢ ( 1 9 6 5 + 1 ) = 1 9 6 6
17 eqid ⊢ 6 5 5 3 = 6 5 5 3
18 eqid ⊢ 6 5 5 = 6 5 5
19 eqid ⊢ 6 5 = 6 5
20 8p1e9 ⊢ ( 8 + 1 ) = 9
21 6t3e18 ⊢ ( 6 · 3 ) = 1 8
22 9 8 20 21 decsuc ⊢ ( ( 6 · 3 ) + 1 ) = 1 9
23 5t3e15 ⊢ ( 5 · 3 ) = 1 5
24 1 2 3 19 3 9 22 23 decmul1c ⊢ ( 6 5 · 3 ) = 1 9 5
25 11 3 14 24 decsuc ⊢ ( ( 6 5 · 3 ) + 1 ) = 1 9 6
26 1 4 3 18 3 9 25 23 decmul1c ⊢ ( 6 5 5 · 3 ) = 1 9 6 5
27 3t3e9 ⊢ ( 3 · 3 ) = 9
28 1 5 1 17 26 27 decmul1 ⊢ ( 6 5 5 3 · 3 ) = 1 9 6 5 9
29 13 16 28 decsucc ⊢ ( ( 6 5 5 3 · 3 ) + 1 ) = 1 9 6 6 0
30 1 6 2 7 8 9 29 21 decmul1c ⊢ ( 6 5 5 3 6 · 3 ) = 1 9 6 6 0 8