2pwp1prmfmtno

Description: Every prime number of the form ( ( 2 ^ k ) + 1 ) must be a Fermat number. (Contributed by AV, 7-Aug-2021)

		Ref	Expression
	Assertion	2pwp1prmfmtno	$⊢ (K \in ℕ \land P = 2^{K} + 1 \land P \in ℙ) \to \exists n \in ℕ_{0} P = FermatNo (n)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (K \in ℕ \land P = 2^{K} + 1 \land P \in ℙ) \to K \in ℕ$
2		eleq1	$⊢ P = 2^{K} + 1 \to (P \in ℙ \leftrightarrow 2^{K} + 1 \in ℙ)$
3	2	biimpa	$⊢ (P = 2^{K} + 1 \land P \in ℙ) \to 2^{K} + 1 \in ℙ$
4	3	3adant1	$⊢ (K \in ℕ \land P = 2^{K} + 1 \land P \in ℙ) \to 2^{K} + 1 \in ℙ$
5		2pwp1prm	$⊢ (K \in ℕ \land 2^{K} + 1 \in ℙ) \to \exists n \in ℕ_{0} K = 2^{n}$
6	1 4 5	syl2anc	$⊢ (K \in ℕ \land P = 2^{K} + 1 \land P \in ℙ) \to \exists n \in ℕ_{0} K = 2^{n}$
7		simpl	$⊢ (P = 2^{K} + 1 \land K = 2^{n}) \to P = 2^{K} + 1$
8		oveq2	$⊢ K = 2^{n} \to 2^{K} = 2^{2^{n}}$
9	8	oveq1d	$⊢ K = 2^{n} \to 2^{K} + 1 = 2^{2^{n}} + 1$
10	9	adantl	$⊢ (P = 2^{K} + 1 \land K = 2^{n}) \to 2^{K} + 1 = 2^{2^{n}} + 1$
11	7 10	eqtrd	$⊢ (P = 2^{K} + 1 \land K = 2^{n}) \to P = 2^{2^{n}} + 1$
12		fmtno	$⊢ n \in ℕ_{0} \to FermatNo (n) = 2^{2^{n}} + 1$
13	12	eqcomd	$⊢ n \in ℕ_{0} \to 2^{2^{n}} + 1 = FermatNo (n)$
14	11 13	sylan9eqr	$⊢ (n \in ℕ_{0} \land (P = 2^{K} + 1 \land K = 2^{n})) \to P = FermatNo (n)$
15	14	exp32	$⊢ n \in ℕ_{0} \to (P = 2^{K} + 1 \to (K = 2^{n} \to P = FermatNo (n)))$
16	15	com12	$⊢ P = 2^{K} + 1 \to (n \in ℕ_{0} \to (K = 2^{n} \to P = FermatNo (n)))$
17	16	3ad2ant2	$⊢ (K \in ℕ \land P = 2^{K} + 1 \land P \in ℙ) \to (n \in ℕ_{0} \to (K = 2^{n} \to P = FermatNo (n)))$
18	17	imp	$⊢ ((K \in ℕ \land P = 2^{K} + 1 \land P \in ℙ) \land n \in ℕ_{0}) \to (K = 2^{n} \to P = FermatNo (n))$
19	18	reximdva	$⊢ (K \in ℕ \land P = 2^{K} + 1 \land P \in ℙ) \to (\exists n \in ℕ_{0} K = 2^{n} \to \exists n \in ℕ_{0} P = FermatNo (n))$
20	6 19	mpd	$⊢ (K \in ℕ \land P = 2^{K} + 1 \land P \in ℙ) \to \exists n \in ℕ_{0} P = FermatNo (n)$

Metamath Proof Explorer

Theorem 2pwp1prmfmtno

Proof