Theorem fmtno5faclem1

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

	Ref	Expression
Assertion	fmtno5faclem1	⊢ ( ; ; ; ; ; ; 6 7 0 0 4 1 7 · 4 ) = ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8

Proof

Step	Hyp	Ref	Expression
1		4nn0	⊢ 4 ∈ ℕ0
2		6nn0	⊢ 6 ∈ ℕ0
3		7nn0	⊢ 7 ∈ ℕ0
4	2 3	deccl	⊢ ; 6 7 ∈ ℕ0
5		0nn0	⊢ 0 ∈ ℕ0
6	4 5	deccl	⊢ ; ; 6 7 0 ∈ ℕ0
7	6 5	deccl	⊢ ; ; ; 6 7 0 0 ∈ ℕ0
8	7 1	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		8nn0	⊢ 8 ∈ ℕ0
13		2nn0	⊢ 2 ∈ ℕ0
14	13 2	deccl	⊢ ; 2 6 ∈ ℕ0
15	14 12	deccl	⊢ ; ; 2 6 8 ∈ ℕ0
16	15 5	deccl	⊢ ; ; ; 2 6 8 0 ∈ ℕ0
17	16 9	deccl	⊢ ; ; ; ; 2 6 8 0 1 ∈ ℕ0
18	17 2	deccl	⊢ ; ; ; ; ; 2 6 8 0 1 6 ∈ ℕ0
19		eqid	⊢ ; ; ; ; ; 6 7 0 0 4 1 = ; ; ; ; ; 6 7 0 0 4 1
20		eqid	⊢ ; ; ; ; 6 7 0 0 4 = ; ; ; ; 6 7 0 0 4
21		eqid	⊢ ; ; ; 6 7 0 0 = ; ; ; 6 7 0 0
22		eqid	⊢ ; ; 6 7 0 = ; ; 6 7 0
23		eqid	⊢ ; 6 7 = ; 6 7
24		6t4e24	⊢ ( 6 · 4 ) = ; 2 4
25		4p2e6	⊢ ( 4 + 2 ) = 6
26	13 1 13 24 25	decaddi	⊢ ( ( 6 · 4 ) + 2 ) = ; 2 6
27		7t4e28	⊢ ( 7 · 4 ) = ; 2 8
28	1 2 3 23 12 13 26 27	decmul1c	⊢ ( ; 6 7 · 4 ) = ; ; 2 6 8
29		4cn	⊢ 4 ∈ ℂ
30	29	mul02i	⊢ ( 0 · 4 ) = 0
31	1 4 5 22 28 30	decmul1	⊢ ( ; ; 6 7 0 · 4 ) = ; ; ; 2 6 8 0
32	1 6 5 21 31 30	decmul1	⊢ ( ; ; ; 6 7 0 0 · 4 ) = ; ; ; ; 2 6 8 0 0
33		0p1e1	⊢ ( 0 + 1 ) = 1
34	16 5 9 32 33	decaddi	⊢ ( ( ; ; ; 6 7 0 0 · 4 ) + 1 ) = ; ; ; ; 2 6 8 0 1
35		4t4e16	⊢ ( 4 · 4 ) = ; 1 6
36	1 7 1 20 2 9 34 35	decmul1c	⊢ ( ; ; ; ; 6 7 0 0 4 · 4 ) = ; ; ; ; ; 2 6 8 0 1 6
37	29	mulid2i	⊢ ( 1 · 4 ) = 4
38	1 8 9 19 36 37	decmul1	⊢ ( ; ; ; ; ; 6 7 0 0 4 1 · 4 ) = ; ; ; ; ; ; 2 6 8 0 1 6 4
39	18 1 13 38 25	decaddi	⊢ ( ( ; ; ; ; ; 6 7 0 0 4 1 · 4 ) + 2 ) = ; ; ; ; ; ; 2 6 8 0 1 6 6
40	1 10 3 11 12 13 39 27	decmul1c	⊢ ( ; ; ; ; ; ; 6 7 0 0 4 1 7 · 4 ) = ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8