fmtnoprmfac1

Description: Divisor of Fermat number (special form of Euler's result, see fmtnofac1 ): Let F_n be a Fermat number. Let p be a prime divisor of F_n. Then p is in the form: k*2^(n+1)+1 where k is a positive integer. (Contributed by AV, 25-Jul-2021)

		Ref	Expression
	Assertion	fmtnoprmfac1	$⊢ (N \in ℕ \land P \in ℙ \land P ∥ FermatNo (N)) \to \exists k \in ℕ P = k 2^{N + 1} + 1$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ P = 2 \to (P ∥ FermatNo (N) \leftrightarrow 2 ∥ FermatNo (N))$
2	1	adantr	$⊢ (P = 2 \land N \in ℕ) \to (P ∥ FermatNo (N) \leftrightarrow 2 ∥ FermatNo (N))$
3		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
4		fmtnoodd	$⊢ N \in ℕ_{0} \to \neg 2 ∥ FermatNo (N)$
5	3 4	syl	$⊢ N \in ℕ \to \neg 2 ∥ FermatNo (N)$
6	5	adantl	$⊢ (P = 2 \land N \in ℕ) \to \neg 2 ∥ FermatNo (N)$
7	6	pm2.21d	$⊢ (P = 2 \land N \in ℕ) \to (2 ∥ FermatNo (N) \to \exists k \in ℕ P = k 2^{N + 1} + 1)$
8	2 7	sylbid	$⊢ (P = 2 \land N \in ℕ) \to (P ∥ FermatNo (N) \to \exists k \in ℕ P = k 2^{N + 1} + 1)$
9	8	a1d	$⊢ (P = 2 \land N \in ℕ) \to (P \in ℙ \to (P ∥ FermatNo (N) \to \exists k \in ℕ P = k 2^{N + 1} + 1))$
10	9	ex	$⊢ P = 2 \to (N \in ℕ \to (P \in ℙ \to (P ∥ FermatNo (N) \to \exists k \in ℕ P = k 2^{N + 1} + 1)))$
11	10	3impd	$⊢ P = 2 \to ((N \in ℕ \land P \in ℙ \land P ∥ FermatNo (N)) \to \exists k \in ℕ P = k 2^{N + 1} + 1)$
12		simpr1	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ \land P ∥ FermatNo (N))) \to N \in ℕ$
13		neqne	$⊢ \neg P = 2 \to P \neq 2$
14	13	anim2i	$⊢ (P \in ℙ \land \neg P = 2) \to (P \in ℙ \land P \neq 2)$
15		eldifsn	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land P \neq 2)$
16	14 15	sylibr	$⊢ (P \in ℙ \land \neg P = 2) \to P \in (ℙ ∖ \{2\})$
17	16	ex	$⊢ P \in ℙ \to (\neg P = 2 \to P \in (ℙ ∖ \{2\}))$
18	17	3ad2ant2	$⊢ (N \in ℕ \land P \in ℙ \land P ∥ FermatNo (N)) \to (\neg P = 2 \to P \in (ℙ ∖ \{2\}))$
19	18	impcom	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ \land P ∥ FermatNo (N))) \to P \in (ℙ ∖ \{2\})$
20		simpr3	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ \land P ∥ FermatNo (N))) \to P ∥ FermatNo (N)$
21		fmtnoprmfac1lem	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\}) \land P ∥ FermatNo (N)) \to {od}_{ℤ} (P) (2) = 2^{N + 1}$
22	12 19 20 21	syl3anc	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ \land P ∥ FermatNo (N))) \to {od}_{ℤ} (P) (2) = 2^{N + 1}$
23		prmnn	$⊢ P \in ℙ \to P \in ℕ$
24	23	ad2antll	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to P \in ℕ$
25		2z	$⊢ 2 \in ℤ$
26	25	a1i	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to 2 \in ℤ$
27	13	necomd	$⊢ \neg P = 2 \to 2 \neq P$
28	27	adantr	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to 2 \neq P$
29		2prm	$⊢ 2 \in ℙ$
30	29	a1i	$⊢ N \in ℕ \to 2 \in ℙ$
31	30	anim1i	$⊢ (N \in ℕ \land P \in ℙ) \to (2 \in ℙ \land P \in ℙ)$
32	31	adantl	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to (2 \in ℙ \land P \in ℙ)$
33		prmrp	$⊢ (2 \in ℙ \land P \in ℙ) \to (2 \gcd P = 1 \leftrightarrow 2 \neq P)$
34	32 33	syl	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to (2 \gcd P = 1 \leftrightarrow 2 \neq P)$
35	28 34	mpbird	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to 2 \gcd P = 1$
36		odzphi	$⊢ (P \in ℕ \land 2 \in ℤ \land 2 \gcd P = 1) \to {od}_{ℤ} (P) (2) ∥ ϕ (P)$
37	24 26 35 36	syl3anc	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to {od}_{ℤ} (P) (2) ∥ ϕ (P)$
38		phiprm	$⊢ P \in ℙ \to ϕ (P) = P - 1$
39	38	ad2antll	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to ϕ (P) = P - 1$
40	39	breq2d	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to ({od}_{ℤ} (P) (2) ∥ ϕ (P) \leftrightarrow {od}_{ℤ} (P) (2) ∥ (P - 1))$
41		breq1	$⊢ {od}_{ℤ} (P) (2) = 2^{N + 1} \to ({od}_{ℤ} (P) (2) ∥ (P - 1) \leftrightarrow 2^{N + 1} ∥ (P - 1))$
42	41	adantl	$⊢ ((\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \land {od}_{ℤ} (P) (2) = 2^{N + 1}) \to ({od}_{ℤ} (P) (2) ∥ (P - 1) \leftrightarrow 2^{N + 1} ∥ (P - 1))$
43		2nn	$⊢ 2 \in ℕ$
44	43	a1i	$⊢ N \in ℕ \to 2 \in ℕ$
45		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
46	45	nnnn0d	$⊢ N \in ℕ \to N + 1 \in ℕ_{0}$
47	44 46	nnexpcld	$⊢ N \in ℕ \to 2^{N + 1} \in ℕ$
48	23	nnnn0d	$⊢ P \in ℙ \to P \in ℕ_{0}$
49		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
50		eluzle	$⊢ P \in ℤ_{\geq 2} \to 2 \leq P$
51	49 50	syl	$⊢ P \in ℙ \to 2 \leq P$
52		nn0ge2m1nn	$⊢ (P \in ℕ_{0} \land 2 \leq P) \to P - 1 \in ℕ$
53	48 51 52	syl2anc	$⊢ P \in ℙ \to P - 1 \in ℕ$
54	47 53	anim12i	$⊢ (N \in ℕ \land P \in ℙ) \to (2^{N + 1} \in ℕ \land P - 1 \in ℕ)$
55	54	adantl	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to (2^{N + 1} \in ℕ \land P - 1 \in ℕ)$
56		nndivides	$⊢ (2^{N + 1} \in ℕ \land P - 1 \in ℕ) \to (2^{N + 1} ∥ (P - 1) \leftrightarrow \exists k \in ℕ k 2^{N + 1} = P - 1)$
57	55 56	syl	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to (2^{N + 1} ∥ (P - 1) \leftrightarrow \exists k \in ℕ k 2^{N + 1} = P - 1)$
58		eqcom	$⊢ k 2^{N + 1} = P - 1 \leftrightarrow P - 1 = k 2^{N + 1}$
59	58	a1i	$⊢ ((\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \land k \in ℕ) \to (k 2^{N + 1} = P - 1 \leftrightarrow P - 1 = k 2^{N + 1})$
60	23	nncnd	$⊢ P \in ℙ \to P \in ℂ$
61	60	adantl	$⊢ (N \in ℕ \land P \in ℙ) \to P \in ℂ$
62	61	adantr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in ℕ) \to P \in ℂ$
63		1cnd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in ℕ) \to 1 \in ℂ$
64		nncn	$⊢ k \in ℕ \to k \in ℂ$
65	64	adantl	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in ℕ) \to k \in ℂ$
66		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
67	3 66	syl	$⊢ N \in ℕ \to N + 1 \in ℕ_{0}$
68	44 67	nnexpcld	$⊢ N \in ℕ \to 2^{N + 1} \in ℕ$
69	68	nncnd	$⊢ N \in ℕ \to 2^{N + 1} \in ℂ$
70	69	adantr	$⊢ (N \in ℕ \land P \in ℙ) \to 2^{N + 1} \in ℂ$
71	70	adantr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in ℕ) \to 2^{N + 1} \in ℂ$
72	65 71	mulcld	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in ℕ) \to k 2^{N + 1} \in ℂ$
73	62 63 72	subadd2d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in ℕ) \to (P - 1 = k 2^{N + 1} \leftrightarrow k 2^{N + 1} + 1 = P)$
74	73	adantll	$⊢ ((\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \land k \in ℕ) \to (P - 1 = k 2^{N + 1} \leftrightarrow k 2^{N + 1} + 1 = P)$
75		eqcom	$⊢ k 2^{N + 1} + 1 = P \leftrightarrow P = k 2^{N + 1} + 1$
76	75	a1i	$⊢ ((\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \land k \in ℕ) \to (k 2^{N + 1} + 1 = P \leftrightarrow P = k 2^{N + 1} + 1)$
77	59 74 76	3bitrd	$⊢ ((\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \land k \in ℕ) \to (k 2^{N + 1} = P - 1 \leftrightarrow P = k 2^{N + 1} + 1)$
78	77	rexbidva	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to (\exists k \in ℕ k 2^{N + 1} = P - 1 \leftrightarrow \exists k \in ℕ P = k 2^{N + 1} + 1)$
79	78	biimpd	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to (\exists k \in ℕ k 2^{N + 1} = P - 1 \to \exists k \in ℕ P = k 2^{N + 1} + 1)$
80	57 79	sylbid	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to (2^{N + 1} ∥ (P - 1) \to \exists k \in ℕ P = k 2^{N + 1} + 1)$
81	80	adantr	$⊢ ((\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \land {od}_{ℤ} (P) (2) = 2^{N + 1}) \to (2^{N + 1} ∥ (P - 1) \to \exists k \in ℕ P = k 2^{N + 1} + 1)$
82	42 81	sylbid	$⊢ ((\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \land {od}_{ℤ} (P) (2) = 2^{N + 1}) \to ({od}_{ℤ} (P) (2) ∥ (P - 1) \to \exists k \in ℕ P = k 2^{N + 1} + 1)$
83	82	ex	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to ({od}_{ℤ} (P) (2) = 2^{N + 1} \to ({od}_{ℤ} (P) (2) ∥ (P - 1) \to \exists k \in ℕ P = k 2^{N + 1} + 1))$
84	83	com23	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to ({od}_{ℤ} (P) (2) ∥ (P - 1) \to ({od}_{ℤ} (P) (2) = 2^{N + 1} \to \exists k \in ℕ P = k 2^{N + 1} + 1))$
85	40 84	sylbid	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to ({od}_{ℤ} (P) (2) ∥ ϕ (P) \to ({od}_{ℤ} (P) (2) = 2^{N + 1} \to \exists k \in ℕ P = k 2^{N + 1} + 1))$
86	37 85	mpd	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ)) \to ({od}_{ℤ} (P) (2) = 2^{N + 1} \to \exists k \in ℕ P = k 2^{N + 1} + 1)$
87	86	3adantr3	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ \land P ∥ FermatNo (N))) \to ({od}_{ℤ} (P) (2) = 2^{N + 1} \to \exists k \in ℕ P = k 2^{N + 1} + 1)$
88	22 87	mpd	$⊢ (\neg P = 2 \land (N \in ℕ \land P \in ℙ \land P ∥ FermatNo (N))) \to \exists k \in ℕ P = k 2^{N + 1} + 1$
89	88	ex	$⊢ \neg P = 2 \to ((N \in ℕ \land P \in ℙ \land P ∥ FermatNo (N)) \to \exists k \in ℕ P = k 2^{N + 1} + 1)$
90	11 89	pm2.61i	$⊢ (N \in ℕ \land P \in ℙ \land P ∥ FermatNo (N)) \to \exists k \in ℕ P = k 2^{N + 1} + 1$

Metamath Proof Explorer

Theorem fmtnoprmfac1

Proof