Metamath Proof Explorer

Theorem nfermltlrev

Description: Fermat's little theorem reversed is not generally true: There are integers a and p so that " p is prime" does not follow from a ^ p == a (mod p ). (Contributed by AV, 3-Jun-2023)

Ref Expression
Assertion nfermltlrev 
|- E. a e. ZZ E. p e. ( ZZ>= ` 3 ) -. ( ( ( a ^ p ) mod p ) = ( a mod p ) -> p e. Prime )

Proof

Step Hyp Ref Expression
1 8nn 
 |-  8 e. NN
2 1 elexi 
 |-  8 e. _V
3 eleq1 
 |-  ( a = 8 -> ( a e. ZZ <-> 8 e. ZZ ) )
4 oveq1 
 |-  ( a = 8 -> ( a ^ p ) = ( 8 ^ p ) )
5 4 oveq1d 
 |-  ( a = 8 -> ( ( a ^ p ) mod p ) = ( ( 8 ^ p ) mod p ) )
6 oveq1 
 |-  ( a = 8 -> ( a mod p ) = ( 8 mod p ) )
7 5 6 eqeq12d 
 |-  ( a = 8 -> ( ( ( a ^ p ) mod p ) = ( a mod p ) <-> ( ( 8 ^ p ) mod p ) = ( 8 mod p ) ) )
8 7 imbi1d 
 |-  ( a = 8 -> ( ( ( ( a ^ p ) mod p ) = ( a mod p ) -> p e. Prime ) <-> ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime ) ) )
9 8 notbid 
 |-  ( a = 8 -> ( -. ( ( ( a ^ p ) mod p ) = ( a mod p ) -> p e. Prime ) <-> -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime ) ) )
10 9 rexbidv 
 |-  ( a = 8 -> ( E. p e. ( ZZ>= ` 3 ) -. ( ( ( a ^ p ) mod p ) = ( a mod p ) -> p e. Prime ) <-> E. p e. ( ZZ>= ` 3 ) -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime ) ) )
11 3 10 anbi12d 
 |-  ( a = 8 -> ( ( a e. ZZ /\ E. p e. ( ZZ>= ` 3 ) -. ( ( ( a ^ p ) mod p ) = ( a mod p ) -> p e. Prime ) ) <-> ( 8 e. ZZ /\ E. p e. ( ZZ>= ` 3 ) -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime ) ) ) )
12 1 nnzi 
 |-  8 e. ZZ
13 nfermltl8rev 
 |-  E. p e. ( ZZ>= ` 3 ) -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime )
14 12 13 pm3.2i 
 |-  ( 8 e. ZZ /\ E. p e. ( ZZ>= ` 3 ) -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime ) )
15 2 11 14 ceqsexv2d 
 |-  E. a ( a e. ZZ /\ E. p e. ( ZZ>= ` 3 ) -. ( ( ( a ^ p ) mod p ) = ( a mod p ) -> p e. Prime ) )
16 df-rex 
 |-  ( E. a e. ZZ E. p e. ( ZZ>= ` 3 ) -. ( ( ( a ^ p ) mod p ) = ( a mod p ) -> p e. Prime ) <-> E. a ( a e. ZZ /\ E. p e. ( ZZ>= ` 3 ) -. ( ( ( a ^ p ) mod p ) = ( a mod p ) -> p e. Prime ) ) )
17 15 16 mpbir 
 |-  E. a e. ZZ E. p e. ( ZZ>= ` 3 ) -. ( ( ( a ^ p ) mod p ) = ( a mod p ) -> p e. Prime )