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 a p 3 ¬ a p mod p = a mod p p

Proof

Step Hyp Ref Expression
1 8nn 8
2 1 elexi 8 V
3 eleq1 a = 8 a 8
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 8 p mod p = 8 mod p p
9 8 notbid a = 8 ¬ a p mod p = a mod p p ¬ 8 p mod p = 8 mod p p
10 9 rexbidv a = 8 p 3 ¬ a p mod p = a mod p p p 3 ¬ 8 p mod p = 8 mod p p
11 3 10 anbi12d a = 8 a p 3 ¬ a p mod p = a mod p p 8 p 3 ¬ 8 p mod p = 8 mod p p
12 1 nnzi 8
13 nfermltl8rev p 3 ¬ 8 p mod p = 8 mod p p
14 12 13 pm3.2i 8 p 3 ¬ 8 p mod p = 8 mod p p
15 2 11 14 ceqsexv2d a a p 3 ¬ a p mod p = a mod p p
16 df-rex a p 3 ¬ a p mod p = a mod p p a a p 3 ¬ a p mod p = a mod p p
17 15 16 mpbir a p 3 ¬ a p mod p = a mod p p