nfermltl2rev

Description: Fermat's little theorem with base 2 reversed is not generally true: There is an integer p (for example 341, see 341fppr2 ) so that " p is prime" does not follow from 2 ^ p == 2 (mod p ). (Contributed by AV, 3-Jun-2023)

		Ref	Expression
	Assertion	nfermltl2rev	$⊢ \exists p \in ℤ_{\geq 3} \neg (2^{p} \mod p = 2 \mod p \to p \in ℙ)$

Proof

Step	Hyp	Ref	Expression
1		decex	$⊢ 341 \in V$
2		eleq1	$⊢ p = 341 \to (p \in ℤ_{\geq 3} \leftrightarrow 341 \in ℤ_{\geq 3})$
3		oveq2	$⊢ p = 341 \to 2^{p} = 2^{341}$
4		id	$⊢ p = 341 \to p = 341$
5	3 4	oveq12d	$⊢ p = 341 \to 2^{p} \mod p = 2^{341} \mod 341$
6		oveq2	$⊢ p = 341 \to 2 \mod p = 2 \mod 341$
7	5 6	eqeq12d	$⊢ p = 341 \to (2^{p} \mod p = 2 \mod p \leftrightarrow 2^{341} \mod 341 = 2 \mod 341)$
8		eleq1	$⊢ p = 341 \to (p \in ℙ \leftrightarrow 341 \in ℙ)$
9	7 8	imbi12d	$⊢ p = 341 \to ((2^{p} \mod p = 2 \mod p \to p \in ℙ) \leftrightarrow (2^{341} \mod 341 = 2 \mod 341 \to 341 \in ℙ))$
10	9	notbid	$⊢ p = 341 \to (\neg (2^{p} \mod p = 2 \mod p \to p \in ℙ) \leftrightarrow \neg (2^{341} \mod 341 = 2 \mod 341 \to 341 \in ℙ))$
11	2 10	anbi12d	$⊢ p = 341 \to ((p \in ℤ_{\geq 3} \land \neg (2^{p} \mod p = 2 \mod p \to p \in ℙ)) \leftrightarrow (341 \in ℤ_{\geq 3} \land \neg (2^{341} \mod 341 = 2 \mod 341 \to 341 \in ℙ)))$
12		3z	$⊢ 3 \in ℤ$
13		3nn0	$⊢ 3 \in ℕ_{0}$
14		4nn0	$⊢ 4 \in ℕ_{0}$
15	13 14	deccl	$⊢ 34 \in ℕ_{0}$
16		1nn0	$⊢ 1 \in ℕ_{0}$
17	15 16	deccl	$⊢ 341 \in ℕ_{0}$
18	17	nn0zi	$⊢ 341 \in ℤ$
19	13	dec0h	$⊢ 3 = 03$
20		0nn0	$⊢ 0 \in ℕ_{0}$
21		3re	$⊢ 3 \in ℝ$
22		9re	$⊢ 9 \in ℝ$
23		3lt9	$⊢ 3 < 9$
24	21 22 23	ltleii	$⊢ 3 \leq 9$
25		3nn	$⊢ 3 \in ℕ$
26		0re	$⊢ 0 \in ℝ$
27		9pos	$⊢ 0 < 9$
28	26 22 27	ltleii	$⊢ 0 \leq 9$
29	25 14 20 28	decltdi	$⊢ 0 < 34$
30	20 15 13 16 24 29	decleh	$⊢ 03 \leq 341$
31	19 30	eqbrtri	$⊢ 3 \leq 341$
32		eluz2	$⊢ 341 \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land 341 \in ℤ \land 3 \leq 341)$
33	12 18 31 32	mpbir3an	$⊢ 341 \in ℤ_{\geq 3}$
34		341fppr2	$⊢ 341 \in FPPr (2)$
35		fpprwppr	$⊢ 341 \in FPPr (2) \to 2^{341} \mod 341 = 2 \mod 341$
36	34 35	ax-mp	$⊢ 2^{341} \mod 341 = 2 \mod 341$
37		11t31e341	$⊢ 11 \cdot 31 = 341$
38	37	eqcomi	$⊢ 341 = 11 \cdot 31$
39		2z	$⊢ 2 \in ℤ$
40	16 16	deccl	$⊢ 11 \in ℕ_{0}$
41	40	nn0zi	$⊢ 11 \in ℤ$
42		2nn0	$⊢ 2 \in ℕ_{0}$
43	42	dec0h	$⊢ 2 = 02$
44		2re	$⊢ 2 \in ℝ$
45		2lt9	$⊢ 2 < 9$
46	44 22 45	ltleii	$⊢ 2 \leq 9$
47		0lt1	$⊢ 0 < 1$
48	20 16 42 16 46 47	decleh	$⊢ 02 \leq 11$
49	43 48	eqbrtri	$⊢ 2 \leq 11$
50		eluz2	$⊢ 11 \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land 11 \in ℤ \land 2 \leq 11)$
51	39 41 49 50	mpbir3an	$⊢ 11 \in ℤ_{\geq 2}$
52	13 16	deccl	$⊢ 31 \in ℕ_{0}$
53	52	nn0zi	$⊢ 31 \in ℤ$
54		3pos	$⊢ 0 < 3$
55	20 13 42 16 46 54	decleh	$⊢ 02 \leq 31$
56	43 55	eqbrtri	$⊢ 2 \leq 31$
57		eluz2	$⊢ 31 \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land 31 \in ℤ \land 2 \leq 31)$
58	39 53 56 57	mpbir3an	$⊢ 31 \in ℤ_{\geq 2}$
59		nprm	$⊢ (11 \in ℤ_{\geq 2} \land 31 \in ℤ_{\geq 2}) \to \neg 11 \cdot 31 \in ℙ$
60	51 58 59	mp2an	$⊢ \neg 11 \cdot 31 \in ℙ$
61	38 60	eqneltri	$⊢ \neg 341 \in ℙ$
62	36 61	pm3.2i	$⊢ (2^{341} \mod 341 = 2 \mod 341 \land \neg 341 \in ℙ)$
63		annim	$⊢ (2^{341} \mod 341 = 2 \mod 341 \land \neg 341 \in ℙ) \leftrightarrow \neg (2^{341} \mod 341 = 2 \mod 341 \to 341 \in ℙ)$
64	62 63	mpbi	$⊢ \neg (2^{341} \mod 341 = 2 \mod 341 \to 341 \in ℙ)$
65	33 64	pm3.2i	$⊢ (341 \in ℤ_{\geq 3} \land \neg (2^{341} \mod 341 = 2 \mod 341 \to 341 \in ℙ))$
66	1 11 65	ceqsexv2d	$⊢ \exists p (p \in ℤ_{\geq 3} \land \neg (2^{p} \mod p = 2 \mod p \to p \in ℙ))$
67		df-rex	$⊢ \exists p \in ℤ_{\geq 3} \neg (2^{p} \mod p = 2 \mod p \to p \in ℙ) \leftrightarrow \exists p (p \in ℤ_{\geq 3} \land \neg (2^{p} \mod p = 2 \mod p \to p \in ℙ))$
68	66 67	mpbir	$⊢ \exists p \in ℤ_{\geq 3} \neg (2^{p} \mod p = 2 \mod p \to p \in ℙ)$

Metamath Proof Explorer

Theorem nfermltl2rev

Proof