Theorem fmtno5nprm

Description: The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021)

	Ref	Expression
Assertion	fmtno5nprm	$$⊢\mathrm{FermatNo}\left(5\right)\notin \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		6nn0	$$⊢6\in {\mathbb{N}}_0$$
2		7nn0	$$⊢7\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢67\in {\mathbb{N}}_0$$
4		0nn0	$$⊢0\in {\mathbb{N}}_0$$
5	3 4	deccl	$$⊢670\in {\mathbb{N}}_0$$
6	5 4	deccl	$$⊢6700\in {\mathbb{N}}_0$$
7		4nn0	$$⊢4\in {\mathbb{N}}_0$$
8	6 7	deccl	$$⊢67004\in {\mathbb{N}}_0$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10	8 9	deccl	$$⊢670041\in {\mathbb{N}}_0$$
11		7nn	$$⊢7\in \mathbb{N}$$
12	10 11	decnncl	$$⊢6700417\in \mathbb{N}$$
13	1 7	deccl	$$⊢64\in {\mathbb{N}}_0$$
14		1nn	$$⊢1\in \mathbb{N}$$
15	13 14	decnncl	$$⊢641\in \mathbb{N}$$
16	8 14	decnncl	$$⊢670041\in \mathbb{N}$$
17		1lt10	$$⊢1<10$$
18	16 2 9 17	declti	$$⊢1<6700417$$
19		4nn	$$⊢4\in \mathbb{N}$$
20	1 19	decnncl	$$⊢64\in \mathbb{N}$$
21	20 9 9 17	declti	$$⊢1<641$$
22		fmtno5fac	$$⊢\mathrm{FermatNo}\left(5\right)=6700417\cdot 641$$
23	22	eqcomi	$$⊢6700417\cdot 641=\mathrm{FermatNo}\left(5\right)$$
24	12 15 18 21 23	nprmi	$$⊢\neg \mathrm{FermatNo}\left(5\right)\in \mathbb{P}$$
25	24	nelir	$$⊢\mathrm{FermatNo}\left(5\right)\notin \mathbb{P}$$