Theorem 4fppr1

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

	Ref	Expression
Assertion	4fppr1	⊢ 4 ∈ ( FPPr ‘ 1 )

Proof

Step	Hyp	Ref	Expression
1		4z	⊢ 4 ∈ ℤ
2		uzid	⊢ ( 4 ∈ ℤ → 4 ∈ ( ℤ≥ ‘ 4 ) )
3	1 2	ax-mp	⊢ 4 ∈ ( ℤ≥ ‘ 4 )
4		4nprm	⊢ ¬ 4 ∈ ℙ
5	4	nelir	⊢ 4 ∉ ℙ
6		4m1e3	⊢ ( 4 − 1 ) = 3
7	6	oveq2i	⊢ ( 1 ↑ ( 4 − 1 ) ) = ( 1 ↑ 3 )
8		3z	⊢ 3 ∈ ℤ
9		1exp	⊢ ( 3 ∈ ℤ → ( 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 ) ) mod 4 ) = ( 1 mod 4 )
13		4re	⊢ 4 ∈ ℝ
14		1lt4	⊢ 1 < 4
15		1mod	⊢ ( ( 4 ∈ ℝ ∧ 1 < 4 ) → ( 1 mod 4 ) = 1 )
16	13 14 15	mp2an	⊢ ( 1 mod 4 ) = 1
17	12 16	eqtri	⊢ ( ( 1 ↑ ( 4 − 1 ) ) mod 4 ) = 1
18		1nn	⊢ 1 ∈ ℕ
19		fpprel	⊢ ( 1 ∈ ℕ → ( 4 ∈ ( FPPr ‘ 1 ) ↔ ( 4 ∈ ( ℤ≥ ‘ 4 ) ∧ 4 ∉ ℙ ∧ ( ( 1 ↑ ( 4 − 1 ) ) mod 4 ) = 1 ) ) )
20	18 19	ax-mp	⊢ ( 4 ∈ ( FPPr ‘ 1 ) ↔ ( 4 ∈ ( ℤ≥ ‘ 4 ) ∧ 4 ∉ ℙ ∧ ( ( 1 ↑ ( 4 − 1 ) ) mod 4 ) = 1 ) )
21	3 5 17 20	mpbir3an	⊢ 4 ∈ ( FPPr ‘ 1 )