fmtnofac2

Description: Divisor of Fermat number (Euler's Result refined by François Édouard Anatole Lucas), see fmtnofac1 : Let F_n be a Fermat number. Let m be divisor of F_n. Then m is in the form: k*2^(n+2)+1 where k is a nonnegative integer. (Contributed by AV, 30-Jul-2021)

		Ref	Expression
	Assertion	fmtnofac2	$⊢ (N \in ℤ_{\geq 2} \land M \in ℕ \land M ∥ FermatNo (N)) \to \exists k \in ℕ_{0} M = k 2^{N + 2} + 1$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ x = 1 \to (x ∥ FermatNo (N) \leftrightarrow 1 ∥ FermatNo (N))$
2	1	anbi2d	$⊢ x = 1 \to ((N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \leftrightarrow (N \in ℤ_{\geq 2} \land 1 ∥ FermatNo (N)))$
3		eqeq1	$⊢ x = 1 \to (x = k 2^{N + 2} + 1 \leftrightarrow 1 = k 2^{N + 2} + 1)$
4	3	rexbidv	$⊢ x = 1 \to (\exists k \in ℕ_{0} x = k 2^{N + 2} + 1 \leftrightarrow \exists k \in ℕ_{0} 1 = k 2^{N + 2} + 1)$
5	2 4	imbi12d	$⊢ x = 1 \to (((N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \to \exists k \in ℕ_{0} x = k 2^{N + 2} + 1) \leftrightarrow ((N \in ℤ_{\geq 2} \land 1 ∥ FermatNo (N)) \to \exists k \in ℕ_{0} 1 = k 2^{N + 2} + 1))$
6		breq1	$⊢ x = y \to (x ∥ FermatNo (N) \leftrightarrow y ∥ FermatNo (N))$
7	6	anbi2d	$⊢ x = y \to ((N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \leftrightarrow (N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)))$
8		eqeq1	$⊢ x = y \to (x = k 2^{N + 2} + 1 \leftrightarrow y = k 2^{N + 2} + 1)$
9	8	rexbidv	$⊢ x = y \to (\exists k \in ℕ_{0} x = k 2^{N + 2} + 1 \leftrightarrow \exists k \in ℕ_{0} y = k 2^{N + 2} + 1)$
10	7 9	imbi12d	$⊢ x = y \to (((N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \to \exists k \in ℕ_{0} x = k 2^{N + 2} + 1) \leftrightarrow ((N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1))$
11		breq1	$⊢ x = z \to (x ∥ FermatNo (N) \leftrightarrow z ∥ FermatNo (N))$
12	11	anbi2d	$⊢ x = z \to ((N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \leftrightarrow (N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)))$
13		eqeq1	$⊢ x = z \to (x = k 2^{N + 2} + 1 \leftrightarrow z = k 2^{N + 2} + 1)$
14	13	rexbidv	$⊢ x = z \to (\exists k \in ℕ_{0} x = k 2^{N + 2} + 1 \leftrightarrow \exists k \in ℕ_{0} z = k 2^{N + 2} + 1)$
15	12 14	imbi12d	$⊢ x = z \to (((N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \to \exists k \in ℕ_{0} x = k 2^{N + 2} + 1) \leftrightarrow ((N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1))$
16		breq1	$⊢ x = y z \to (x ∥ FermatNo (N) \leftrightarrow y z ∥ FermatNo (N))$
17	16	anbi2d	$⊢ x = y z \to ((N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \leftrightarrow (N \in ℤ_{\geq 2} \land y z ∥ FermatNo (N)))$
18		eqeq1	$⊢ x = y z \to (x = k 2^{N + 2} + 1 \leftrightarrow y z = k 2^{N + 2} + 1)$
19	18	rexbidv	$⊢ x = y z \to (\exists k \in ℕ_{0} x = k 2^{N + 2} + 1 \leftrightarrow \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1)$
20	17 19	imbi12d	$⊢ x = y z \to (((N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \to \exists k \in ℕ_{0} x = k 2^{N + 2} + 1) \leftrightarrow ((N \in ℤ_{\geq 2} \land y z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$
21		breq1	$⊢ x = M \to (x ∥ FermatNo (N) \leftrightarrow M ∥ FermatNo (N))$
22	21	anbi2d	$⊢ x = M \to ((N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \leftrightarrow (N \in ℤ_{\geq 2} \land M ∥ FermatNo (N)))$
23		eqeq1	$⊢ x = M \to (x = k 2^{N + 2} + 1 \leftrightarrow M = k 2^{N + 2} + 1)$
24	23	rexbidv	$⊢ x = M \to (\exists k \in ℕ_{0} x = k 2^{N + 2} + 1 \leftrightarrow \exists k \in ℕ_{0} M = k 2^{N + 2} + 1)$
25	22 24	imbi12d	$⊢ x = M \to (((N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \to \exists k \in ℕ_{0} x = k 2^{N + 2} + 1) \leftrightarrow ((N \in ℤ_{\geq 2} \land M ∥ FermatNo (N)) \to \exists k \in ℕ_{0} M = k 2^{N + 2} + 1))$
26		0nn0	$⊢ 0 \in ℕ_{0}$
27	26	a1i	$⊢ N \in ℤ_{\geq 2} \to 0 \in ℕ_{0}$
28		oveq1	$⊢ k = 0 \to k 2^{N + 2} = 0 \cdot 2^{N + 2}$
29	28	oveq1d	$⊢ k = 0 \to k 2^{N + 2} + 1 = 0 \cdot 2^{N + 2} + 1$
30	29	eqeq2d	$⊢ k = 0 \to (1 = k 2^{N + 2} + 1 \leftrightarrow 1 = 0 \cdot 2^{N + 2} + 1)$
31	30	adantl	$⊢ (N \in ℤ_{\geq 2} \land k = 0) \to (1 = k 2^{N + 2} + 1 \leftrightarrow 1 = 0 \cdot 2^{N + 2} + 1)$
32		2nn0	$⊢ 2 \in ℕ_{0}$
33	32	a1i	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℕ_{0}$
34		eluzge2nn0	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ_{0}$
35	34 33	nn0addcld	$⊢ N \in ℤ_{\geq 2} \to N + 2 \in ℕ_{0}$
36	33 35	nn0expcld	$⊢ N \in ℤ_{\geq 2} \to 2^{N + 2} \in ℕ_{0}$
37	36	nn0cnd	$⊢ N \in ℤ_{\geq 2} \to 2^{N + 2} \in ℂ$
38	37	mul02d	$⊢ N \in ℤ_{\geq 2} \to 0 \cdot 2^{N + 2} = 0$
39	38	oveq1d	$⊢ N \in ℤ_{\geq 2} \to 0 \cdot 2^{N + 2} + 1 = 0 + 1$
40		0p1e1	$⊢ 0 + 1 = 1$
41	39 40	eqtr2di	$⊢ N \in ℤ_{\geq 2} \to 1 = 0 \cdot 2^{N + 2} + 1$
42	27 31 41	rspcedvd	$⊢ N \in ℤ_{\geq 2} \to \exists k \in ℕ_{0} 1 = k 2^{N + 2} + 1$
43	42	adantr	$⊢ (N \in ℤ_{\geq 2} \land 1 ∥ FermatNo (N)) \to \exists k \in ℕ_{0} 1 = k 2^{N + 2} + 1$
44		simpl	$⊢ (N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \to N \in ℤ_{\geq 2}$
45	44	adantl	$⊢ (x \in ℙ \land (N \in ℤ_{\geq 2} \land x ∥ FermatNo (N))) \to N \in ℤ_{\geq 2}$
46		simpl	$⊢ (x \in ℙ \land (N \in ℤ_{\geq 2} \land x ∥ FermatNo (N))) \to x \in ℙ$
47		simprr	$⊢ (x \in ℙ \land (N \in ℤ_{\geq 2} \land x ∥ FermatNo (N))) \to x ∥ FermatNo (N)$
48		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
49		fmtnoprmfac2	$⊢ (N \in ℤ_{\geq 2} \land x \in ℙ \land x ∥ FermatNo (N)) \to \exists k \in ℕ x = k 2^{N + 2} + 1$
50		ssrexv	$⊢ ℕ \subseteq ℕ_{0} \to (\exists k \in ℕ x = k 2^{N + 2} + 1 \to \exists k \in ℕ_{0} x = k 2^{N + 2} + 1)$
51	48 49 50	mpsyl	$⊢ (N \in ℤ_{\geq 2} \land x \in ℙ \land x ∥ FermatNo (N)) \to \exists k \in ℕ_{0} x = k 2^{N + 2} + 1$
52	45 46 47 51	syl3anc	$⊢ (x \in ℙ \land (N \in ℤ_{\geq 2} \land x ∥ FermatNo (N))) \to \exists k \in ℕ_{0} x = k 2^{N + 2} + 1$
53	52	ex	$⊢ x \in ℙ \to ((N \in ℤ_{\geq 2} \land x ∥ FermatNo (N)) \to \exists k \in ℕ_{0} x = k 2^{N + 2} + 1)$
54		fmtnofac2lem	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to ((((N \in ℤ_{\geq 2} \land y ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y = k 2^{N + 2} + 1) \land ((N \in ℤ_{\geq 2} \land z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} z = k 2^{N + 2} + 1)) \to ((N \in ℤ_{\geq 2} \land y z ∥ FermatNo (N)) \to \exists k \in ℕ_{0} y z = k 2^{N + 2} + 1))$
55	5 10 15 20 25 43 53 54	prmind	$⊢ M \in ℕ \to ((N \in ℤ_{\geq 2} \land M ∥ FermatNo (N)) \to \exists k \in ℕ_{0} M = k 2^{N + 2} + 1)$
56	55	expd	$⊢ M \in ℕ \to (N \in ℤ_{\geq 2} \to (M ∥ FermatNo (N) \to \exists k \in ℕ_{0} M = k 2^{N + 2} + 1))$
57	56	3imp21	$⊢ (N \in ℤ_{\geq 2} \land M \in ℕ \land M ∥ FermatNo (N)) \to \exists k \in ℕ_{0} M = k 2^{N + 2} + 1$

Metamath Proof Explorer

Theorem fmtnofac2

Proof