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	$⊢ \exists a \in ℤ \exists p \in ℤ_{\geq 3} \neg (a^{p} \mod p = a \mod p \to p \in ℙ)$

Proof

Step	Hyp	Ref	Expression
1		8nn	$⊢ 8 \in ℕ$
2	1	elexi	$⊢ 8 \in V$
3		eleq1	$⊢ a = 8 \to (a \in ℤ \leftrightarrow 8 \in ℤ)$
4		oveq1	$⊢ a = 8 \to a^{p} = 8^{p}$
5	4	oveq1d	$⊢ a = 8 \to a^{p} \mod p = 8^{p} \mod p$
6		oveq1	$⊢ a = 8 \to a \mod p = 8 \mod p$
7	5 6	eqeq12d	$⊢ a = 8 \to (a^{p} \mod p = a \mod p \leftrightarrow 8^{p} \mod p = 8 \mod p)$
8	7	imbi1d	$⊢ a = 8 \to ((a^{p} \mod p = a \mod p \to p \in ℙ) \leftrightarrow (8^{p} \mod p = 8 \mod p \to p \in ℙ))$
9	8	notbid	$⊢ a = 8 \to (\neg (a^{p} \mod p = a \mod p \to p \in ℙ) \leftrightarrow \neg (8^{p} \mod p = 8 \mod p \to p \in ℙ))$
10	9	rexbidv	$⊢ a = 8 \to (\exists p \in ℤ_{\geq 3} \neg (a^{p} \mod p = a \mod p \to p \in ℙ) \leftrightarrow \exists p \in ℤ_{\geq 3} \neg (8^{p} \mod p = 8 \mod p \to p \in ℙ))$
11	3 10	anbi12d	$⊢ a = 8 \to ((a \in ℤ \land \exists p \in ℤ_{\geq 3} \neg (a^{p} \mod p = a \mod p \to p \in ℙ)) \leftrightarrow (8 \in ℤ \land \exists p \in ℤ_{\geq 3} \neg (8^{p} \mod p = 8 \mod p \to p \in ℙ)))$
12	1	nnzi	$⊢ 8 \in ℤ$
13		nfermltl8rev	$⊢ \exists p \in ℤ_{\geq 3} \neg (8^{p} \mod p = 8 \mod p \to p \in ℙ)$
14	12 13	pm3.2i	$⊢ (8 \in ℤ \land \exists p \in ℤ_{\geq 3} \neg (8^{p} \mod p = 8 \mod p \to p \in ℙ))$
15	2 11 14	ceqsexv2d	$⊢ \exists a (a \in ℤ \land \exists p \in ℤ_{\geq 3} \neg (a^{p} \mod p = a \mod p \to p \in ℙ))$
16		df-rex	$⊢ \exists a \in ℤ \exists p \in ℤ_{\geq 3} \neg (a^{p} \mod p = a \mod p \to p \in ℙ) \leftrightarrow \exists a (a \in ℤ \land \exists p \in ℤ_{\geq 3} \neg (a^{p} \mod p = a \mod p \to p \in ℙ))$
17	15 16	mpbir	$⊢ \exists a \in ℤ \exists p \in ℤ_{\geq 3} \neg (a^{p} \mod p = a \mod p \to p \in ℙ)$