Metamath Proof Explorer

Theorem fmtno5fac

Description: The factorisation of the 5 th Fermat number, see remark in ApostolNT p. 7. (Contributed by AV, 22-Jul-2021)

Ref Expression
Assertion fmtno5fac ( FermatNo ‘ 5 ) = ( 6 7 0 0 4 1 7 · 6 4 1 )

Proof

Step Hyp Ref Expression
1 4nn0 ⊢ 4 ∈ ℕ0
2 2nn0 ⊢ 2 ∈ ℕ0
3 1 2 deccl ⊢ 4 2 ∈ ℕ0
4 8nn0 ⊢ 8 ∈ ℕ0
5 3 4 deccl ⊢ 4 2 8 ∈ ℕ0
6 5 4 deccl ⊢ 4 2 8 8 ∈ ℕ0
7 6 2 deccl ⊢ 4 2 8 8 2 ∈ ℕ0
8 6nn0 ⊢ 6 ∈ ℕ0
9 7 8 deccl ⊢ 4 2 8 8 2 6 ∈ ℕ0
10 9 8 deccl ⊢ 4 2 8 8 2 6 6 ∈ ℕ0
11 10 4 deccl ⊢ 4 2 8 8 2 6 6 8 ∈ ℕ0
12 11 4 deccl ⊢ 4 2 8 8 2 6 6 8 8 ∈ ℕ0
13 0nn0 ⊢ 0 ∈ ℕ0
14 7nn0 ⊢ 7 ∈ ℕ0
15 8 14 deccl ⊢ 6 7 ∈ ℕ0
16 15 13 deccl ⊢ 6 7 0 ∈ ℕ0
17 16 13 deccl ⊢ 6 7 0 0 ∈ ℕ0
18 17 1 deccl ⊢ 6 7 0 0 4 ∈ ℕ0
19 1nn0 ⊢ 1 ∈ ℕ0
20 18 19 deccl ⊢ 6 7 0 0 4 1 ∈ ℕ0
21 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
22 21 deceq1i ⊢ ( 4 0 2 0 2 5 0 2 0 + 2 6 8 0 1 6 6 8 ) 0 = 4 2 8 8 2 6 6 8 8 0
23 eqid ⊢ 6 7 0 0 4 1 7 = 6 7 0 0 4 1 7
24 eqid ⊢ 4 2 8 8 2 6 6 8 8 = 4 2 8 8 2 6 6 8 8
25 eqid ⊢ 6 7 0 0 4 1 = 6 7 0 0 4 1
26 eqid ⊢ 4 2 8 8 2 6 6 8 = 4 2 8 8 2 6 6 8
27 eqid ⊢ 6 7 0 0 4 = 6 7 0 0 4
28 9nn0 ⊢ 9 ∈ ℕ0
29 3 28 deccl ⊢ 4 2 9 ∈ ℕ0
30 29 1 deccl ⊢ 4 2 9 4 ∈ ℕ0
31 30 28 deccl ⊢ 4 2 9 4 9 ∈ ℕ0
32 31 8 deccl ⊢ 4 2 9 4 9 6 ∈ ℕ0
33 6p1e7 ⊢ ( 6 + 1 ) = 7
34 eqid ⊢ 4 2 8 8 2 6 6 = 4 2 8 8 2 6 6
35 eqid ⊢ 6 7 0 0 = 6 7 0 0
36 eqid ⊢ 4 2 8 8 2 6 = 4 2 8 8 2 6
37 eqid ⊢ 6 7 0 = 6 7 0
38 eqid ⊢ 4 2 8 8 2 = 4 2 8 8 2
39 eqid ⊢ 6 7 = 6 7
40 eqid ⊢ 4 2 8 8 = 4 2 8 8
41 8p1e9 ⊢ ( 8 + 1 ) = 9
42 eqid ⊢ 4 2 8 = 4 2 8
43 3 4 41 42 decsuc ⊢ ( 4 2 8 + 1 ) = 4 2 9
44 8p6e14 ⊢ ( 8 + 6 ) = 1 4
45 5 4 8 40 43 1 44 decaddci ⊢ ( 4 2 8 8 + 6 ) = 4 2 9 4
46 7cn ⊢ 7 ∈ ℂ
47 2cn ⊢ 2 ∈ ℂ
48 7p2e9 ⊢ ( 7 + 2 ) = 9
49 46 47 48 addcomli ⊢ ( 2 + 7 ) = 9
50 6 2 8 14 38 39 45 49 decadd ⊢ ( 4 2 8 8 2 + 6 7 ) = 4 2 9 4 9
51 6cn ⊢ 6 ∈ ℂ
52 51 addid1i ⊢ ( 6 + 0 ) = 6
53 7 8 15 13 36 37 50 52 decadd ⊢ ( 4 2 8 8 2 6 + 6 7 0 ) = 4 2 9 4 9 6
54 9 8 16 13 34 35 53 52 decadd ⊢ ( 4 2 8 8 2 6 6 + 6 7 0 0 ) = 4 2 9 4 9 6 6
55 32 8 33 54 decsuc ⊢ ( ( 4 2 8 8 2 6 6 + 6 7 0 0 ) + 1 ) = 4 2 9 4 9 6 7
56 8p4e12 ⊢ ( 8 + 4 ) = 1 2
57 10 4 17 1 26 27 55 2 56 decaddc ⊢ ( 4 2 8 8 2 6 6 8 + 6 7 0 0 4 ) = 4 2 9 4 9 6 7 2
58 11 4 18 19 24 25 57 41 decadd ⊢ ( 4 2 8 8 2 6 6 8 8 + 6 7 0 0 4 1 ) = 4 2 9 4 9 6 7 2 9
59 46 addid2i ⊢ ( 0 + 7 ) = 7
60 12 13 20 14 22 23 58 59 decadd ⊢ ( ( 4 0 2 0 2 5 0 2 0 + 2 6 8 0 1 6 6 8 ) 0 + 6 7 0 0 4 1 7 ) = 4 2 9 4 9 6 7 2 9 7
61 8 1 deccl ⊢ 6 4 ∈ ℕ0
62 20 14 deccl ⊢ 6 7 0 0 4 1 7 ∈ ℕ0
63 fmtno5faclem2 ⊢ ( 6 7 0 0 4 1 7 · 6 ) = 4 0 2 0 2 5 0 2
64 63 eqcomi ⊢ 4 0 2 0 2 5 0 2 = ( 6 7 0 0 4 1 7 · 6 )
65 fmtno5faclem1 ⊢ ( 6 7 0 0 4 1 7 · 4 ) = 2 6 8 0 1 6 6 8
66 65 eqcomi ⊢ 2 6 8 0 1 6 6 8 = ( 6 7 0 0 4 1 7 · 4 )
67 8 1 62 64 66 decmul10add ⊢ ( 6 7 0 0 4 1 7 · 6 4 ) = ( 4 0 2 0 2 5 0 2 0 + 2 6 8 0 1 6 6 8 )
68 67 eqcomi ⊢ ( 4 0 2 0 2 5 0 2 0 + 2 6 8 0 1 6 6 8 ) = ( 6 7 0 0 4 1 7 · 6 4 )
69 62 nn0cni ⊢ 6 7 0 0 4 1 7 ∈ ℂ
70 69 mulid1i ⊢ ( 6 7 0 0 4 1 7 · 1 ) = 6 7 0 0 4 1 7
71 70 eqcomi ⊢ 6 7 0 0 4 1 7 = ( 6 7 0 0 4 1 7 · 1 )
72 61 19 62 68 71 decmul10add ⊢ ( 6 7 0 0 4 1 7 · 6 4 1 ) = ( ( 4 0 2 0 2 5 0 2 0 + 2 6 8 0 1 6 6 8 ) 0 + 6 7 0 0 4 1 7 )
73 fmtno5 ⊢ ( FermatNo ‘ 5 ) = 4 2 9 4 9 6 7 2 9 7
74 60 72 73 3eqtr4ri ⊢ ( FermatNo ‘ 5 ) = ( 6 7 0 0 4 1 7 · 6 4 1 )