Theorem 4fppr1

Description: 4 is the (smallest) Fermat pseudoprime to the base 1. (Contributed by AV, 3-Jun-2023)

	Ref	Expression
Assertion	4fppr1	$$⊢4\in \mathrm{FPPr}\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		4z	$$⊢4\in \mathbb{Z}$$
2		uzid	$$⊢4\in \mathbb{Z}\to 4\in {\mathbb{Z}}_{\ge 4}$$
3	1 2	ax-mp	$$⊢4\in {\mathbb{Z}}_{\ge 4}$$
4		4nprm	$$⊢\neg 4\in \mathbb{P}$$
5	4	nelir	$$⊢4\notin \mathbb{P}$$
6		4m1e3	$$⊢4-1=3$$
7	6	oveq2i	$$⊢1^{4-1}=1^3$$
8		3z	$$⊢3\in \mathbb{Z}$$
9		1exp	$$⊢3\in \mathbb{Z}\to 1^3=1$$
10	8 9	ax-mp	$$⊢1^3=1$$
11	7 10	eqtri	$$⊢1^{4-1}=1$$
12	11	oveq1i	$$⊢1^{4-1}\mathrm{mod}4=1\mathrm{mod}4$$
13		4re	$$⊢4\in ℝ$$
14		1lt4	$$⊢1<4$$
15		1mod	$$⊢\left(4\in ℝ\wedge 1<4\right)\to 1\mathrm{mod}4=1$$
16	13 14 15	mp2an	$$⊢1\mathrm{mod}4=1$$
17	12 16	eqtri	$$⊢1^{4-1}\mathrm{mod}4=1$$
18		1nn	$$⊢1\in \mathbb{N}$$
19		fpprel	$$⊢1\in \mathbb{N}\to \left(4\in \mathrm{FPPr}\left(1\right)\leftrightarrow \left(4\in {\mathbb{Z}}_{\ge 4}\wedge 4\notin \mathbb{P}\wedge 1^{4-1}\mathrm{mod}4=1\right)\right)$$
20	18 19	ax-mp	$$⊢4\in \mathrm{FPPr}\left(1\right)\leftrightarrow \left(4\in {\mathbb{Z}}_{\ge 4}\wedge 4\notin \mathbb{P}\wedge 1^{4-1}\mathrm{mod}4=1\right)$$
21	3 5 17 20	mpbir3an	$$⊢4\in \mathrm{FPPr}\left(1\right)$$