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	⊢ ∃ 𝑎 ∈ ℤ ∃ 𝑝 ∈ ( ℤ≥ ‘ 3 ) ¬ ( ( ( 𝑎 ↑ 𝑝 ) mod 𝑝 ) = ( 𝑎 mod 𝑝 ) → 𝑝 ∈ ℙ )

Proof

Step	Hyp	Ref	Expression
1		8nn	⊢ 8 ∈ ℕ
2	1	elexi	⊢ 8 ∈ V
3		eleq1	⊢ ( 𝑎 = 8 → ( 𝑎 ∈ ℤ ↔ 8 ∈ ℤ ) )
4		oveq1	⊢ ( 𝑎 = 8 → ( 𝑎 ↑ 𝑝 ) = ( 8 ↑ 𝑝 ) )
5	4	oveq1d	⊢ ( 𝑎 = 8 → ( ( 𝑎 ↑ 𝑝 ) mod 𝑝 ) = ( ( 8 ↑ 𝑝 ) mod 𝑝 ) )
6		oveq1	⊢ ( 𝑎 = 8 → ( 𝑎 mod 𝑝 ) = ( 8 mod 𝑝 ) )
7	5 6	eqeq12d	⊢ ( 𝑎 = 8 → ( ( ( 𝑎 ↑ 𝑝 ) mod 𝑝 ) = ( 𝑎 mod 𝑝 ) ↔ ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) ) )
8	7	imbi1d	⊢ ( 𝑎 = 8 → ( ( ( ( 𝑎 ↑ 𝑝 ) mod 𝑝 ) = ( 𝑎 mod 𝑝 ) → 𝑝 ∈ ℙ ) ↔ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ ) ) )
9	8	notbid	⊢ ( 𝑎 = 8 → ( ¬ ( ( ( 𝑎 ↑ 𝑝 ) mod 𝑝 ) = ( 𝑎 mod 𝑝 ) → 𝑝 ∈ ℙ ) ↔ ¬ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ ) ) )
10	9	rexbidv	⊢ ( 𝑎 = 8 → ( ∃ 𝑝 ∈ ( ℤ≥ ‘ 3 ) ¬ ( ( ( 𝑎 ↑ 𝑝 ) mod 𝑝 ) = ( 𝑎 mod 𝑝 ) → 𝑝 ∈ ℙ ) ↔ ∃ 𝑝 ∈ ( ℤ≥ ‘ 3 ) ¬ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ ) ) )
11	3 10	anbi12d	⊢ ( 𝑎 = 8 → ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑝 ∈ ( ℤ≥ ‘ 3 ) ¬ ( ( ( 𝑎 ↑ 𝑝 ) mod 𝑝 ) = ( 𝑎 mod 𝑝 ) → 𝑝 ∈ ℙ ) ) ↔ ( 8 ∈ ℤ ∧ ∃ 𝑝 ∈ ( ℤ≥ ‘ 3 ) ¬ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ ) ) ) )
12	1	nnzi	⊢ 8 ∈ ℤ
13		nfermltl8rev	⊢ ∃ 𝑝 ∈ ( ℤ≥ ‘ 3 ) ¬ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ )
14	12 13	pm3.2i	⊢ ( 8 ∈ ℤ ∧ ∃ 𝑝 ∈ ( ℤ≥ ‘ 3 ) ¬ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ ) )
15	2 11 14	ceqsexv2d	⊢ ∃ 𝑎 ( 𝑎 ∈ ℤ ∧ ∃ 𝑝 ∈ ( ℤ≥ ‘ 3 ) ¬ ( ( ( 𝑎 ↑ 𝑝 ) mod 𝑝 ) = ( 𝑎 mod 𝑝 ) → 𝑝 ∈ ℙ ) )
16		df-rex	⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑝 ∈ ( ℤ≥ ‘ 3 ) ¬ ( ( ( 𝑎 ↑ 𝑝 ) mod 𝑝 ) = ( 𝑎 mod 𝑝 ) → 𝑝 ∈ ℙ ) ↔ ∃ 𝑎 ( 𝑎 ∈ ℤ ∧ ∃ 𝑝 ∈ ( ℤ≥ ‘ 3 ) ¬ ( ( ( 𝑎 ↑ 𝑝 ) mod 𝑝 ) = ( 𝑎 mod 𝑝 ) → 𝑝 ∈ ℙ ) ) )
17	15 16	mpbir	⊢ ∃ 𝑎 ∈ ℤ ∃ 𝑝 ∈ ( ℤ≥ ‘ 3 ) ¬ ( ( ( 𝑎 ↑ 𝑝 ) mod 𝑝 ) = ( 𝑎 mod 𝑝 ) → 𝑝 ∈ ℙ )