Metamath Proof Explorer

Theorem 4fppr1

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

Ref Expression
Assertion 4fppr1 
|- 4 e. ( FPPr ` 1 )

Proof

Step Hyp Ref Expression
1 4z 
 |-  4 e. ZZ
2 uzid 
 |-  ( 4 e. ZZ -> 4 e. ( ZZ>= ` 4 ) )
3 1 2 ax-mp 
 |-  4 e. ( ZZ>= ` 4 )
4 4nprm 
 |-  -. 4 e. Prime
5 4 nelir 
 |-  4 e/ Prime
6 4m1e3 
 |-  ( 4 - 1 ) = 3
7 6 oveq2i 
 |-  ( 1 ^ ( 4 - 1 ) ) = ( 1 ^ 3 )
8 3z 
 |-  3 e. ZZ
9 1exp 
 |-  ( 3 e. ZZ -> ( 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 e. RR
14 1lt4 
 |-  1 < 4
15 1mod 
 |-  ( ( 4 e. RR /\ 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 e. NN
19 fpprel 
 |-  ( 1 e. NN -> ( 4 e. ( FPPr ` 1 ) <-> ( 4 e. ( ZZ>= ` 4 ) /\ 4 e/ Prime /\ ( ( 1 ^ ( 4 - 1 ) ) mod 4 ) = 1 ) ) )
20 18 19 ax-mp 
 |-  ( 4 e. ( FPPr ` 1 ) <-> ( 4 e. ( ZZ>= ` 4 ) /\ 4 e/ Prime /\ ( ( 1 ^ ( 4 - 1 ) ) mod 4 ) = 1 ) )
21 3 5 17 20 mpbir3an 
 |-  4 e. ( FPPr ` 1 )