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	$$⊢\left(N\in \mathbb{N}\wedge M\in \mathbb{N}\wedge M\parallel \mathrm{FermatNo}\left(N\right)\right)\to \exists k\in {\mathbb{N}}_{0}M=k{2}^{N+1}+1$$

Proof

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