fmtnoprmfac2

Description: Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 ): 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+2)+1 where k is a positive integer. (Contributed by AV, 26-Jul-2021)

		Ref	Expression
	Assertion	fmtnoprmfac2	$⊢ (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N)) \to \exists k \in ℕ P = k 2^{N + 2} + 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 ℤ_{\geq 2}) \to (P ∥ FermatNo (N) \leftrightarrow 2 ∥ FermatNo (N))$
3		eluzge2nn0	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ_{0}$
4		fmtnoodd	$⊢ N \in ℕ_{0} \to \neg 2 ∥ FermatNo (N)$
5	3 4	syl	$⊢ N \in ℤ_{\geq 2} \to \neg 2 ∥ FermatNo (N)$
6	5	adantl	$⊢ (P = 2 \land N \in ℤ_{\geq 2}) \to \neg 2 ∥ FermatNo (N)$
7	6	pm2.21d	$⊢ (P = 2 \land N \in ℤ_{\geq 2}) \to (2 ∥ FermatNo (N) \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
8	2 7	sylbid	$⊢ (P = 2 \land N \in ℤ_{\geq 2}) \to (P ∥ FermatNo (N) \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
9	8	a1d	$⊢ (P = 2 \land N \in ℤ_{\geq 2}) \to (P \in ℙ \to (P ∥ FermatNo (N) \to \exists k \in ℕ P = k 2^{N + 2} + 1))$
10	9	ex	$⊢ P = 2 \to (N \in ℤ_{\geq 2} \to (P \in ℙ \to (P ∥ FermatNo (N) \to \exists k \in ℕ P = k 2^{N + 2} + 1)))$
11	10	3impd	$⊢ P = 2 \to ((N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N)) \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
12		simpr1	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to N \in ℤ_{\geq 2}$
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 ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N)) \to (\neg P = 2 \to P \in (ℙ ∖ \{2\}))$
19	18	impcom	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to P \in (ℙ ∖ \{2\})$
20		simpr3	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to P ∥ FermatNo (N)$
21		fmtnoprmfac2lem1	$⊢ (N \in ℤ_{\geq 2} \land P \in (ℙ ∖ \{2\}) \land P ∥ FermatNo (N)) \to 2^{\frac{P - 1}{2}} \mod P = 1$
22	12 19 20 21	syl3anc	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to 2^{\frac{P - 1}{2}} \mod P = 1$
23		simpl	$⊢ (P \in ℙ \land \neg P = 2) \to P \in ℙ$
24		2nn	$⊢ 2 \in ℕ$
25	24	a1i	$⊢ (P \in ℙ \land \neg P = 2) \to 2 \in ℕ$
26		oddprm	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℕ$
27	16 26	syl	$⊢ (P \in ℙ \land \neg P = 2) \to \frac{P - 1}{2} \in ℕ$
28	27	nnnn0d	$⊢ (P \in ℙ \land \neg P = 2) \to \frac{P - 1}{2} \in ℕ_{0}$
29	25 28	nnexpcld	$⊢ (P \in ℙ \land \neg P = 2) \to 2^{\frac{P - 1}{2}} \in ℕ$
30	29	nnzd	$⊢ (P \in ℙ \land \neg P = 2) \to 2^{\frac{P - 1}{2}} \in ℤ$
31	23 30	jca	$⊢ (P \in ℙ \land \neg P = 2) \to (P \in ℙ \land 2^{\frac{P - 1}{2}} \in ℤ)$
32	31	ex	$⊢ P \in ℙ \to (\neg P = 2 \to (P \in ℙ \land 2^{\frac{P - 1}{2}} \in ℤ))$
33	32	3ad2ant2	$⊢ (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N)) \to (\neg P = 2 \to (P \in ℙ \land 2^{\frac{P - 1}{2}} \in ℤ))$
34	33	impcom	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to (P \in ℙ \land 2^{\frac{P - 1}{2}} \in ℤ)$
35		modprm1div	$⊢ (P \in ℙ \land 2^{\frac{P - 1}{2}} \in ℤ) \to (2^{\frac{P - 1}{2}} \mod P = 1 \leftrightarrow P ∥ (2^{\frac{P - 1}{2}} - 1))$
36	34 35	syl	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to (2^{\frac{P - 1}{2}} \mod P = 1 \leftrightarrow P ∥ (2^{\frac{P - 1}{2}} - 1))$
37		prmnn	$⊢ P \in ℙ \to P \in ℕ$
38	37	adantr	$⊢ (P \in ℙ \land \neg P = 2) \to P \in ℕ$
39		2z	$⊢ 2 \in ℤ$
40	39	a1i	$⊢ (P \in ℙ \land \neg P = 2) \to 2 \in ℤ$
41	13	necomd	$⊢ \neg P = 2 \to 2 \neq P$
42	41	adantl	$⊢ (P \in ℙ \land \neg P = 2) \to 2 \neq P$
43		2prm	$⊢ 2 \in ℙ$
44	43	a1i	$⊢ \neg P = 2 \to 2 \in ℙ$
45	44	anim2i	$⊢ (P \in ℙ \land \neg P = 2) \to (P \in ℙ \land 2 \in ℙ)$
46	45	ancomd	$⊢ (P \in ℙ \land \neg P = 2) \to (2 \in ℙ \land P \in ℙ)$
47		prmrp	$⊢ (2 \in ℙ \land P \in ℙ) \to (2 \gcd P = 1 \leftrightarrow 2 \neq P)$
48	46 47	syl	$⊢ (P \in ℙ \land \neg P = 2) \to (2 \gcd P = 1 \leftrightarrow 2 \neq P)$
49	42 48	mpbird	$⊢ (P \in ℙ \land \neg P = 2) \to 2 \gcd P = 1$
50	38 40 49	3jca	$⊢ (P \in ℙ \land \neg P = 2) \to (P \in ℕ \land 2 \in ℤ \land 2 \gcd P = 1)$
51	50 28	jca	$⊢ (P \in ℙ \land \neg P = 2) \to ((P \in ℕ \land 2 \in ℤ \land 2 \gcd P = 1) \land \frac{P - 1}{2} \in ℕ_{0})$
52	51	ex	$⊢ P \in ℙ \to (\neg P = 2 \to ((P \in ℕ \land 2 \in ℤ \land 2 \gcd P = 1) \land \frac{P - 1}{2} \in ℕ_{0}))$
53	52	3ad2ant2	$⊢ (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N)) \to (\neg P = 2 \to ((P \in ℕ \land 2 \in ℤ \land 2 \gcd P = 1) \land \frac{P - 1}{2} \in ℕ_{0}))$
54	53	impcom	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to ((P \in ℕ \land 2 \in ℤ \land 2 \gcd P = 1) \land \frac{P - 1}{2} \in ℕ_{0})$
55		odzdvds	$⊢ ((P \in ℕ \land 2 \in ℤ \land 2 \gcd P = 1) \land \frac{P - 1}{2} \in ℕ_{0}) \to (P ∥ (2^{\frac{P - 1}{2}} - 1) \leftrightarrow {od}_{ℤ} (P) (2) ∥ (\frac{P - 1}{2}))$
56	54 55	syl	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to (P ∥ (2^{\frac{P - 1}{2}} - 1) \leftrightarrow {od}_{ℤ} (P) (2) ∥ (\frac{P - 1}{2}))$
57		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
58	57	3ad2ant1	$⊢ (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N)) \to N \in ℕ$
59	58	adantl	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to N \in ℕ$
60		fmtnoprmfac1lem	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\}) \land P ∥ FermatNo (N)) \to {od}_{ℤ} (P) (2) = 2^{N + 1}$
61	59 19 20 60	syl3anc	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to {od}_{ℤ} (P) (2) = 2^{N + 1}$
62		breq1	$⊢ {od}_{ℤ} (P) (2) = 2^{N + 1} \to ({od}_{ℤ} (P) (2) ∥ (\frac{P - 1}{2}) \leftrightarrow 2^{N + 1} ∥ (\frac{P - 1}{2}))$
63	62	adantl	$⊢ ((\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \land {od}_{ℤ} (P) (2) = 2^{N + 1}) \to ({od}_{ℤ} (P) (2) ∥ (\frac{P - 1}{2}) \leftrightarrow 2^{N + 1} ∥ (\frac{P - 1}{2}))$
64	24	a1i	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℕ$
65		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
66	57 65	syl	$⊢ N \in ℤ_{\geq 2} \to N + 1 \in ℕ$
67	66	nnnn0d	$⊢ N \in ℤ_{\geq 2} \to N + 1 \in ℕ_{0}$
68	64 67	nnexpcld	$⊢ N \in ℤ_{\geq 2} \to 2^{N + 1} \in ℕ$
69		nndivides	$⊢ (2^{N + 1} \in ℕ \land \frac{P - 1}{2} \in ℕ) \to (2^{N + 1} ∥ (\frac{P - 1}{2}) \leftrightarrow \exists k \in ℕ k 2^{N + 1} = \frac{P - 1}{2})$
70	68 27 69	syl2an	$⊢ (N \in ℤ_{\geq 2} \land (P \in ℙ \land \neg P = 2)) \to (2^{N + 1} ∥ (\frac{P - 1}{2}) \leftrightarrow \exists k \in ℕ k 2^{N + 1} = \frac{P - 1}{2})$
71		eqcom	$⊢ k 2^{N + 1} = \frac{P - 1}{2} \leftrightarrow \frac{P - 1}{2} = k 2^{N + 1}$
72	71	a1i	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to (k 2^{N + 1} = \frac{P - 1}{2} \leftrightarrow \frac{P - 1}{2} = k 2^{N + 1})$
73	37	nncnd	$⊢ P \in ℙ \to P \in ℂ$
74		peano2cnm	$⊢ P \in ℂ \to P - 1 \in ℂ$
75	73 74	syl	$⊢ P \in ℙ \to P - 1 \in ℂ$
76	75	adantl	$⊢ (N \in ℤ_{\geq 2} \land P \in ℙ) \to P - 1 \in ℂ$
77	76	adantr	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to P - 1 \in ℂ$
78		simpr	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to k \in ℕ$
79	68	ad2antrr	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to 2^{N + 1} \in ℕ$
80	78 79	nnmulcld	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to k 2^{N + 1} \in ℕ$
81	80	nncnd	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to k 2^{N + 1} \in ℂ$
82		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
83	82	a1i	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to (2 \in ℂ \land 2 \neq 0)$
84		divmul3	$⊢ (P - 1 \in ℂ \land k 2^{N + 1} \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to (\frac{P - 1}{2} = k 2^{N + 1} \leftrightarrow P - 1 = k 2^{N + 1} \cdot 2)$
85	77 81 83 84	syl3anc	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to (\frac{P - 1}{2} = k 2^{N + 1} \leftrightarrow P - 1 = k 2^{N + 1} \cdot 2)$
86		nncn	$⊢ k \in ℕ \to k \in ℂ$
87	86	adantl	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to k \in ℂ$
88	68	nncnd	$⊢ N \in ℤ_{\geq 2} \to 2^{N + 1} \in ℂ$
89	88	ad2antrr	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to 2^{N + 1} \in ℂ$
90		2cnd	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to 2 \in ℂ$
91	87 89 90	mulassd	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to k 2^{N + 1} \cdot 2 = k 2^{N + 1} \cdot 2$
92		2cnd	$⊢ N \in ℕ \to 2 \in ℂ$
93	65	nnnn0d	$⊢ N \in ℕ \to N + 1 \in ℕ_{0}$
94	92 93	expp1d	$⊢ N \in ℕ \to 2^{N + 1 + 1} = 2^{N + 1} \cdot 2$
95		nncn	$⊢ N \in ℕ \to N \in ℂ$
96		add1p1	$⊢ N \in ℂ \to N + 1 + 1 = N + 2$
97	95 96	syl	$⊢ N \in ℕ \to N + 1 + 1 = N + 2$
98	97	oveq2d	$⊢ N \in ℕ \to 2^{N + 1 + 1} = 2^{N + 2}$
99	94 98	eqtr3d	$⊢ N \in ℕ \to 2^{N + 1} \cdot 2 = 2^{N + 2}$
100	57 99	syl	$⊢ N \in ℤ_{\geq 2} \to 2^{N + 1} \cdot 2 = 2^{N + 2}$
101	100	ad2antrr	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to 2^{N + 1} \cdot 2 = 2^{N + 2}$
102	101	oveq2d	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to k 2^{N + 1} \cdot 2 = k 2^{N + 2}$
103	91 102	eqtrd	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to k 2^{N + 1} \cdot 2 = k 2^{N + 2}$
104	103	eqeq2d	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to (P - 1 = k 2^{N + 1} \cdot 2 \leftrightarrow P - 1 = k 2^{N + 2})$
105	73	adantl	$⊢ (N \in ℤ_{\geq 2} \land P \in ℙ) \to P \in ℂ$
106	105	adantr	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to P \in ℂ$
107		1cnd	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to 1 \in ℂ$
108		id	$⊢ N \in ℕ \to N \in ℕ$
109	24	a1i	$⊢ N \in ℕ \to 2 \in ℕ$
110	108 109	nnaddcld	$⊢ N \in ℕ \to N + 2 \in ℕ$
111	110	nnnn0d	$⊢ N \in ℕ \to N + 2 \in ℕ_{0}$
112	57 111	syl	$⊢ N \in ℤ_{\geq 2} \to N + 2 \in ℕ_{0}$
113	64 112	nnexpcld	$⊢ N \in ℤ_{\geq 2} \to 2^{N + 2} \in ℕ$
114	113	nncnd	$⊢ N \in ℤ_{\geq 2} \to 2^{N + 2} \in ℂ$
115	114	ad2antrr	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to 2^{N + 2} \in ℂ$
116	87 115	mulcld	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to k 2^{N + 2} \in ℂ$
117	106 107 116	subadd2d	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to (P - 1 = k 2^{N + 2} \leftrightarrow k 2^{N + 2} + 1 = P)$
118		eqcom	$⊢ k 2^{N + 2} + 1 = P \leftrightarrow P = k 2^{N + 2} + 1$
119	118	a1i	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to (k 2^{N + 2} + 1 = P \leftrightarrow P = k 2^{N + 2} + 1)$
120	104 117 119	3bitrd	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to (P - 1 = k 2^{N + 1} \cdot 2 \leftrightarrow P = k 2^{N + 2} + 1)$
121	72 85 120	3bitrd	$⊢ ((N \in ℤ_{\geq 2} \land P \in ℙ) \land k \in ℕ) \to (k 2^{N + 1} = \frac{P - 1}{2} \leftrightarrow P = k 2^{N + 2} + 1)$
122	121	rexbidva	$⊢ (N \in ℤ_{\geq 2} \land P \in ℙ) \to (\exists k \in ℕ k 2^{N + 1} = \frac{P - 1}{2} \leftrightarrow \exists k \in ℕ P = k 2^{N + 2} + 1)$
123	122	biimpd	$⊢ (N \in ℤ_{\geq 2} \land P \in ℙ) \to (\exists k \in ℕ k 2^{N + 1} = \frac{P - 1}{2} \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
124	123	adantrr	$⊢ (N \in ℤ_{\geq 2} \land (P \in ℙ \land \neg P = 2)) \to (\exists k \in ℕ k 2^{N + 1} = \frac{P - 1}{2} \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
125	70 124	sylbid	$⊢ (N \in ℤ_{\geq 2} \land (P \in ℙ \land \neg P = 2)) \to (2^{N + 1} ∥ (\frac{P - 1}{2}) \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
126	125	expr	$⊢ (N \in ℤ_{\geq 2} \land P \in ℙ) \to (\neg P = 2 \to (2^{N + 1} ∥ (\frac{P - 1}{2}) \to \exists k \in ℕ P = k 2^{N + 2} + 1))$
127	126	3adant3	$⊢ (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N)) \to (\neg P = 2 \to (2^{N + 1} ∥ (\frac{P - 1}{2}) \to \exists k \in ℕ P = k 2^{N + 2} + 1))$
128	127	impcom	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to (2^{N + 1} ∥ (\frac{P - 1}{2}) \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
129	128	adantr	$⊢ ((\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \land {od}_{ℤ} (P) (2) = 2^{N + 1}) \to (2^{N + 1} ∥ (\frac{P - 1}{2}) \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
130	63 129	sylbid	$⊢ ((\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \land {od}_{ℤ} (P) (2) = 2^{N + 1}) \to ({od}_{ℤ} (P) (2) ∥ (\frac{P - 1}{2}) \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
131	130	ex	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to ({od}_{ℤ} (P) (2) = 2^{N + 1} \to ({od}_{ℤ} (P) (2) ∥ (\frac{P - 1}{2}) \to \exists k \in ℕ P = k 2^{N + 2} + 1))$
132	61 131	mpd	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to ({od}_{ℤ} (P) (2) ∥ (\frac{P - 1}{2}) \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
133	56 132	sylbid	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to (P ∥ (2^{\frac{P - 1}{2}} - 1) \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
134	36 133	sylbid	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to (2^{\frac{P - 1}{2}} \mod P = 1 \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
135	22 134	mpd	$⊢ (\neg P = 2 \land (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N))) \to \exists k \in ℕ P = k 2^{N + 2} + 1$
136	135	ex	$⊢ \neg P = 2 \to ((N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N)) \to \exists k \in ℕ P = k 2^{N + 2} + 1)$
137	11 136	pm2.61i	$⊢ (N \in ℤ_{\geq 2} \land P \in ℙ \land P ∥ FermatNo (N)) \to \exists k \in ℕ P = k 2^{N + 2} + 1$

Metamath Proof Explorer

Theorem fmtnoprmfac2

Proof