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 x. ; ; 6 4 1 )

Proof

Step Hyp Ref Expression
1 4nn0 
 |-  4 e. NN0
2 2nn0 
 |-  2 e. NN0
3 1 2 deccl 
 |-  ; 4 2 e. NN0
4 8nn0 
 |-  8 e. NN0
5 3 4 deccl 
 |-  ; ; 4 2 8 e. NN0
6 5 4 deccl 
 |-  ; ; ; 4 2 8 8 e. NN0
7 6 2 deccl 
 |-  ; ; ; ; 4 2 8 8 2 e. NN0
8 6nn0 
 |-  6 e. NN0
9 7 8 deccl 
 |-  ; ; ; ; ; 4 2 8 8 2 6 e. NN0
10 9 8 deccl 
 |-  ; ; ; ; ; ; 4 2 8 8 2 6 6 e. NN0
11 10 4 deccl 
 |-  ; ; ; ; ; ; ; 4 2 8 8 2 6 6 8 e. NN0
12 11 4 deccl 
 |-  ; ; ; ; ; ; ; ; 4 2 8 8 2 6 6 8 8 e. NN0
13 0nn0 
 |-  0 e. NN0
14 7nn0 
 |-  7 e. NN0
15 8 14 deccl 
 |-  ; 6 7 e. NN0
16 15 13 deccl 
 |-  ; ; 6 7 0 e. NN0
17 16 13 deccl 
 |-  ; ; ; 6 7 0 0 e. NN0
18 17 1 deccl 
 |-  ; ; ; ; 6 7 0 0 4 e. NN0
19 1nn0 
 |-  1 e. NN0
20 18 19 deccl 
 |-  ; ; ; ; ; 6 7 0 0 4 1 e. NN0
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 e. NN0
29 3 28 deccl 
 |-  ; ; 4 2 9 e. NN0
30 29 1 deccl 
 |-  ; ; ; 4 2 9 4 e. NN0
31 30 28 deccl 
 |-  ; ; ; ; 4 2 9 4 9 e. NN0
32 31 8 deccl 
 |-  ; ; ; ; ; 4 2 9 4 9 6 e. NN0
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 e. CC
47 2cn 
 |-  2 e. CC
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 e. CC
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 e. NN0
62 20 14 deccl 
 |-  ; ; ; ; ; ; 6 7 0 0 4 1 7 e. NN0
63 fmtno5faclem2 
 |-  ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. 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 x. 6 )
65 fmtno5faclem1 
 |-  ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. 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 x. 4 )
67 8 1 62 64 66 decmul10add 
 |-  ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. ; 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 x. ; 6 4 )
69 62 nn0cni 
 |-  ; ; ; ; ; ; 6 7 0 0 4 1 7 e. CC
70 69 mulid1i 
 |-  ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. 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 x. 1 )
72 61 19 62 68 71 decmul10add 
 |-  ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. ; ; 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 x. ; ; 6 4 1 )