Metamath Proof Explorer


Theorem fmtnofac1

Description: Divisor of Fermat number (Euler's Result), see ProofWiki "Divisor of Fermat Number/Euler's Result", 24-Jul-2021, https://proofwiki.org/wiki/Divisor_of_Fermat_Number/Euler's_Result ): "Let F_n be a Fermat number. Let m be divisor of F_n. Then m is in the form: k*2^(n+1)+1 where k is a positive integer." Here, however, k must be a nonnegative integer, because k must be 0 to represent 1 (which is a divisor of F_n ).

Historical Note: In 1747, Leonhard Paul Euler proved that a divisor of a Fermat number F_n is always in the form kx2^(n+1)+1. This was later refined to k*2^(n+2)+1 by François Édouard Anatole Lucas, see fmtnofac2 . (Contributed by AV, 30-Jul-2021)

Ref Expression
Assertion fmtnofac1 N M M FermatNo N k 0 M = k 2 N + 1 + 1

Proof

Step Hyp Ref Expression
1 elnn1uz2 N N = 1 N 2
2 5prm 5
3 dvdsprime 5 M M 5 M = 5 M = 1
4 2 3 mpan M M 5 M = 5 M = 1
5 1nn0 1 0
6 5 a1i M = 5 1 0
7 simpl M = 5 k = 1 M = 5
8 oveq1 k = 1 k 4 = 1 4
9 8 oveq1d k = 1 k 4 + 1 = 1 4 + 1
10 9 adantl M = 5 k = 1 k 4 + 1 = 1 4 + 1
11 7 10 eqeq12d M = 5 k = 1 M = k 4 + 1 5 = 1 4 + 1
12 df-5 5 = 4 + 1
13 4cn 4
14 13 mulid2i 1 4 = 4
15 14 eqcomi 4 = 1 4
16 15 oveq1i 4 + 1 = 1 4 + 1
17 12 16 eqtri 5 = 1 4 + 1
18 17 a1i M = 5 5 = 1 4 + 1
19 6 11 18 rspcedvd M = 5 k 0 M = k 4 + 1
20 0nn0 0 0
21 20 a1i M = 1 0 0
22 simpl M = 1 k = 0 M = 1
23 oveq1 k = 0 k 4 = 0 4
24 23 oveq1d k = 0 k 4 + 1 = 0 4 + 1
25 24 adantl M = 1 k = 0 k 4 + 1 = 0 4 + 1
26 22 25 eqeq12d M = 1 k = 0 M = k 4 + 1 1 = 0 4 + 1
27 13 mul02i 0 4 = 0
28 27 oveq1i 0 4 + 1 = 0 + 1
29 0p1e1 0 + 1 = 1
30 28 29 eqtri 0 4 + 1 = 1
31 30 eqcomi 1 = 0 4 + 1
32 31 a1i M = 1 1 = 0 4 + 1
33 21 26 32 rspcedvd M = 1 k 0 M = k 4 + 1
34 19 33 jaoi M = 5 M = 1 k 0 M = k 4 + 1
35 4 34 syl6bi M M 5 k 0 M = k 4 + 1
36 fveq2 N = 1 FermatNo N = FermatNo 1
37 fmtno1 FermatNo 1 = 5
38 36 37 eqtrdi N = 1 FermatNo N = 5
39 38 breq2d N = 1 M FermatNo N M 5
40 oveq1 N = 1 N + 1 = 1 + 1
41 1p1e2 1 + 1 = 2
42 40 41 eqtrdi N = 1 N + 1 = 2
43 42 oveq2d N = 1 2 N + 1 = 2 2
44 sq2 2 2 = 4
45 43 44 eqtrdi N = 1 2 N + 1 = 4
46 45 oveq2d N = 1 k 2 N + 1 = k 4
47 46 oveq1d N = 1 k 2 N + 1 + 1 = k 4 + 1
48 47 eqeq2d N = 1 M = k 2 N + 1 + 1 M = k 4 + 1
49 48 rexbidv N = 1 k 0 M = k 2 N + 1 + 1 k 0 M = k 4 + 1
50 39 49 imbi12d N = 1 M FermatNo N k 0 M = k 2 N + 1 + 1 M 5 k 0 M = k 4 + 1
51 35 50 syl5ibr N = 1 M M FermatNo N k 0 M = k 2 N + 1 + 1
52 fmtnofac2 N 2 M M FermatNo N n 0 M = n 2 N + 2 + 1
53 id n 0 n 0
54 2nn0 2 0
55 54 a1i n 0 2 0
56 53 55 nn0mulcld n 0 n 2 0
57 56 adantl N 2 M M FermatNo N n 0 n 2 0
58 57 adantr N 2 M M FermatNo N n 0 M = n 2 N + 2 + 1 n 2 0
59 simpr N 2 M M FermatNo N n 0 M = n 2 N + 2 + 1 M = n 2 N + 2 + 1
60 oveq1 k = n 2 k 2 N + 1 = n 2 2 N + 1
61 60 oveq1d k = n 2 k 2 N + 1 + 1 = n 2 2 N + 1 + 1
62 59 61 eqeqan12d N 2 M M FermatNo N n 0 M = n 2 N + 2 + 1 k = n 2 M = k 2 N + 1 + 1 n 2 N + 2 + 1 = n 2 2 N + 1 + 1
63 eluzge2nn0 N 2 N 0
64 63 nn0cnd N 2 N
65 add1p1 N N + 1 + 1 = N + 2
66 64 65 syl N 2 N + 1 + 1 = N + 2
67 66 eqcomd N 2 N + 2 = N + 1 + 1
68 67 oveq2d N 2 2 N + 2 = 2 N + 1 + 1
69 2cnd N 2 2
70 peano2nn0 N 0 N + 1 0
71 63 70 syl N 2 N + 1 0
72 69 71 expp1d N 2 2 N + 1 + 1 = 2 N + 1 2
73 54 a1i N 2 2 0
74 73 71 nn0expcld N 2 2 N + 1 0
75 74 nn0cnd N 2 2 N + 1
76 75 69 mulcomd N 2 2 N + 1 2 = 2 2 N + 1
77 68 72 76 3eqtrd N 2 2 N + 2 = 2 2 N + 1
78 77 adantr N 2 n 0 2 N + 2 = 2 2 N + 1
79 78 oveq2d N 2 n 0 n 2 N + 2 = n 2 2 N + 1
80 nn0cn n 0 n
81 80 adantl N 2 n 0 n
82 2cnd N 2 n 0 2
83 75 adantr N 2 n 0 2 N + 1
84 81 82 83 mulassd N 2 n 0 n 2 2 N + 1 = n 2 2 N + 1
85 79 84 eqtr4d N 2 n 0 n 2 N + 2 = n 2 2 N + 1
86 85 3ad2antl1 N 2 M M FermatNo N n 0 n 2 N + 2 = n 2 2 N + 1
87 86 adantr N 2 M M FermatNo N n 0 M = n 2 N + 2 + 1 n 2 N + 2 = n 2 2 N + 1
88 87 oveq1d N 2 M M FermatNo N n 0 M = n 2 N + 2 + 1 n 2 N + 2 + 1 = n 2 2 N + 1 + 1
89 58 62 88 rspcedvd N 2 M M FermatNo N n 0 M = n 2 N + 2 + 1 k 0 M = k 2 N + 1 + 1
90 89 rexlimdva2 N 2 M M FermatNo N n 0 M = n 2 N + 2 + 1 k 0 M = k 2 N + 1 + 1
91 52 90 mpd N 2 M M FermatNo N k 0 M = k 2 N + 1 + 1
92 91 3exp N 2 M M FermatNo N k 0 M = k 2 N + 1 + 1
93 51 92 jaoi N = 1 N 2 M M FermatNo N k 0 M = k 2 N + 1 + 1
94 1 93 sylbi N M M FermatNo N k 0 M = k 2 N + 1 + 1
95 94 3imp N M M FermatNo N k 0 M = k 2 N + 1 + 1