fmtno4prm

Description: The 4-th Fermat number (65537) is a prime (thefifth Fermat prime). (Contributed by AV, 28-Jul-2021)

		Ref	Expression
	Assertion	fmtno4prm	$⊢ FermatNo (4) \in ℙ$

Proof

Step	Hyp	Ref	Expression
1		4nn0	$⊢ 4 \in ℕ_{0}$
2		fmtno	$⊢ 4 \in ℕ_{0} \to FermatNo (4) = 2^{2^{4}} + 1$
3	1 2	ax-mp	$⊢ FermatNo (4) = 2^{2^{4}} + 1$
4		2nn	$⊢ 2 \in ℕ$
5		2nn0	$⊢ 2 \in ℕ_{0}$
6	5 1	nn0expcli	$⊢ 2^{4} \in ℕ_{0}$
7		nnexpcl	$⊢ (2 \in ℕ \land 2^{4} \in ℕ_{0}) \to 2^{2^{4}} \in ℕ$
8	4 6 7	mp2an	$⊢ 2^{2^{4}} \in ℕ$
9		2re	$⊢ 2 \in ℝ$
10		nnexpcl	$⊢ (2 \in ℕ \land 4 \in ℕ_{0}) \to 2^{4} \in ℕ$
11	4 1 10	mp2an	$⊢ 2^{4} \in ℕ$
12		1lt2	$⊢ 1 < 2$
13		expgt1	$⊢ (2 \in ℝ \land 2^{4} \in ℕ \land 1 < 2) \to 1 < 2^{2^{4}}$
14	9 11 12 13	mp3an	$⊢ 1 < 2^{2^{4}}$
15		eluz2b2	$⊢ 2^{2^{4}} \in ℤ_{\geq 2} \leftrightarrow (2^{2^{4}} \in ℕ \land 1 < 2^{2^{4}})$
16	8 14 15	mpbir2an	$⊢ 2^{2^{4}} \in ℤ_{\geq 2}$
17		peano2uz	$⊢ 2^{2^{4}} \in ℤ_{\geq 2} \to 2^{2^{4}} + 1 \in ℤ_{\geq 2}$
18	16 17	ax-mp	$⊢ 2^{2^{4}} + 1 \in ℤ_{\geq 2}$
19	3 18	eqeltri	$⊢ FermatNo (4) \in ℤ_{\geq 2}$
20		elinel2	$⊢ p \in ((2 \dots ⌊\sqrt{FermatNo (4)}⌋) \cap ℙ) \to p \in ℙ$
21	20	adantr	$⊢ (p \in ((2 \dots ⌊\sqrt{FermatNo (4)}⌋) \cap ℙ) \land p ∥ FermatNo (4)) \to p \in ℙ$
22		simpr	$⊢ (p \in ((2 \dots ⌊\sqrt{FermatNo (4)}⌋) \cap ℙ) \land p ∥ FermatNo (4)) \to p ∥ FermatNo (4)$
23		elinel1	$⊢ p \in ((2 \dots ⌊\sqrt{FermatNo (4)}⌋) \cap ℙ) \to p \in (2 \dots ⌊\sqrt{FermatNo (4)}⌋)$
24		elfzle2	$⊢ p \in (2 \dots ⌊\sqrt{FermatNo (4)}⌋) \to p \leq ⌊\sqrt{FermatNo (4)}⌋$
25	23 24	syl	$⊢ p \in ((2 \dots ⌊\sqrt{FermatNo (4)}⌋) \cap ℙ) \to p \leq ⌊\sqrt{FermatNo (4)}⌋$
26	25	adantr	$⊢ (p \in ((2 \dots ⌊\sqrt{FermatNo (4)}⌋) \cap ℙ) \land p ∥ FermatNo (4)) \to p \leq ⌊\sqrt{FermatNo (4)}⌋$
27		fmtno4prmfac193	$⊢ (p \in ℙ \land p ∥ FermatNo (4) \land p \leq ⌊\sqrt{FermatNo (4)}⌋) \to p = 193$
28	21 22 26 27	syl3anc	$⊢ (p \in ((2 \dots ⌊\sqrt{FermatNo (4)}⌋) \cap ℙ) \land p ∥ FermatNo (4)) \to p = 193$
29		fmtno4nprmfac193	$⊢ \neg 193 ∥ FermatNo (4)$
30		breq1	$⊢ p = 193 \to (p ∥ FermatNo (4) \leftrightarrow 193 ∥ FermatNo (4))$
31	29 30	mtbiri	$⊢ p = 193 \to \neg p ∥ FermatNo (4)$
32	28 31	syl	$⊢ (p \in ((2 \dots ⌊\sqrt{FermatNo (4)}⌋) \cap ℙ) \land p ∥ FermatNo (4)) \to \neg p ∥ FermatNo (4)$
33	32	pm2.01da	$⊢ p \in ((2 \dots ⌊\sqrt{FermatNo (4)}⌋) \cap ℙ) \to \neg p ∥ FermatNo (4)$
34	33	rgen	$⊢ \forall p \in ((2 \dots ⌊\sqrt{FermatNo (4)}⌋) \cap ℙ) \neg p ∥ FermatNo (4)$
35		isprm7	$⊢ FermatNo (4) \in ℙ \leftrightarrow (FermatNo (4) \in ℤ_{\geq 2} \land \forall p \in ((2 \dots ⌊\sqrt{FermatNo (4)}⌋) \cap ℙ) \neg p ∥ FermatNo (4))$
36	19 34 35	mpbir2an	$⊢ FermatNo (4) \in ℙ$

Metamath Proof Explorer

Theorem fmtno4prm

Proof