Metamath Proof Explorer

Theorem fmtno5faclem3

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

Ref Expression
Assertion fmtno5faclem3 ( 4 0 2 0 2 5 0 2 0 + 2 6 8 0 1 6 6 8 ) = 4 2 8 8 2 6 6 8 8

Proof

Step Hyp Ref Expression
1 4nn0 ⊢ 4 ∈ ℕ0
2 0nn0 ⊢ 0 ∈ ℕ0
3 1 2 deccl ⊢ 4 0 ∈ ℕ0
4 2nn0 ⊢ 2 ∈ ℕ0
5 3 4 deccl ⊢ 4 0 2 ∈ ℕ0
6 5 2 deccl ⊢ 4 0 2 0 ∈ ℕ0
7 6 4 deccl ⊢ 4 0 2 0 2 ∈ ℕ0
8 5nn0 ⊢ 5 ∈ ℕ0
9 7 8 deccl ⊢ 4 0 2 0 2 5 ∈ ℕ0
10 9 2 deccl ⊢ 4 0 2 0 2 5 0 ∈ ℕ0
11 10 4 deccl ⊢ 4 0 2 0 2 5 0 2 ∈ ℕ0
12 6nn0 ⊢ 6 ∈ ℕ0
13 4 12 deccl ⊢ 2 6 ∈ ℕ0
14 8nn0 ⊢ 8 ∈ ℕ0
15 13 14 deccl ⊢ 2 6 8 ∈ ℕ0
16 15 2 deccl ⊢ 2 6 8 0 ∈ ℕ0
17 1nn0 ⊢ 1 ∈ ℕ0
18 16 17 deccl ⊢ 2 6 8 0 1 ∈ ℕ0
19 18 12 deccl ⊢ 2 6 8 0 1 6 ∈ ℕ0
20 19 12 deccl ⊢ 2 6 8 0 1 6 6 ∈ ℕ0
21 eqid ⊢ 4 0 2 0 2 5 0 2 0 = 4 0 2 0 2 5 0 2 0
22 eqid ⊢ 2 6 8 0 1 6 6 8 = 2 6 8 0 1 6 6 8
23 eqid ⊢ 4 0 2 0 2 5 0 2 = 4 0 2 0 2 5 0 2
24 eqid ⊢ 2 6 8 0 1 6 6 = 2 6 8 0 1 6 6
25 eqid ⊢ 4 0 2 0 2 5 0 = 4 0 2 0 2 5 0
26 eqid ⊢ 2 6 8 0 1 6 = 2 6 8 0 1 6
27 eqid ⊢ 4 0 2 0 2 5 = 4 0 2 0 2 5
28 eqid ⊢ 2 6 8 0 1 = 2 6 8 0 1
29 eqid ⊢ 4 0 2 0 2 = 4 0 2 0 2
30 eqid ⊢ 2 6 8 0 = 2 6 8 0
31 eqid ⊢ 4 0 2 0 = 4 0 2 0
32 eqid ⊢ 2 6 8 = 2 6 8
33 eqid ⊢ 4 0 2 = 4 0 2
34 eqid ⊢ 2 6 = 2 6
35 eqid ⊢ 4 0 = 4 0
36 2cn ⊢ 2 ∈ ℂ
37 36 addlidi ⊢ ( 0 + 2 ) = 2
38 1 2 4 35 37 decaddi ⊢ ( 4 0 + 2 ) = 4 2
39 6cn ⊢ 6 ∈ ℂ
40 6p2e8 ⊢ ( 6 + 2 ) = 8
41 39 36 40 addcomli ⊢ ( 2 + 6 ) = 8
42 3 4 4 12 33 34 38 41 decadd ⊢ ( 4 0 2 + 2 6 ) = 4 2 8
43 8cn ⊢ 8 ∈ ℂ
44 43 addlidi ⊢ ( 0 + 8 ) = 8
45 5 2 13 14 31 32 42 44 decadd ⊢ ( 4 0 2 0 + 2 6 8 ) = 4 2 8 8
46 36 addridi ⊢ ( 2 + 0 ) = 2
47 6 4 15 2 29 30 45 46 decadd ⊢ ( 4 0 2 0 2 + 2 6 8 0 ) = 4 2 8 8 2
48 5p1e6 ⊢ ( 5 + 1 ) = 6
49 7 8 16 17 27 28 47 48 decadd ⊢ ( 4 0 2 0 2 5 + 2 6 8 0 1 ) = 4 2 8 8 2 6
50 39 addlidi ⊢ ( 0 + 6 ) = 6
51 9 2 18 12 25 26 49 50 decadd ⊢ ( 4 0 2 0 2 5 0 + 2 6 8 0 1 6 ) = 4 2 8 8 2 6 6
52 10 4 19 12 23 24 51 41 decadd ⊢ ( 4 0 2 0 2 5 0 2 + 2 6 8 0 1 6 6 ) = 4 2 8 8 2 6 6 8
53 11 2 20 14 21 22 52 44 decadd ⊢ ( 4 0 2 0 2 5 0 2 0 + 2 6 8 0 1 6 6 8 ) = 4 2 8 8 2 6 6 8 8