Theorem fmtno4prm

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

	Ref	Expression
Assertion	fmtno4prm	$$⊢\mathrm{FermatNo}\left(4\right)\in \mathbb{P}$$

Proof

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