2mulprm

Description: A multiple of two is prime iff the multiplier is one. (Contributed by AV, 8-Jun-2023)

		Ref	Expression
	Assertion	2mulprm	$⊢ A \in ℤ \to (2 A \in ℙ \leftrightarrow A = 1)$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ A \in ℤ \to A \in ℝ$
2		0red	$⊢ A \in ℤ \to 0 \in ℝ$
3	1 2	leloed	$⊢ A \in ℤ \to (A \leq 0 \leftrightarrow (A < 0 \lor A = 0))$
4		prmnn	$⊢ 2 A \in ℙ \to 2 A \in ℕ$
5		nnnn0	$⊢ 2 A \in ℕ \to 2 A \in ℕ_{0}$
6		nn0ge0	$⊢ 2 A \in ℕ_{0} \to 0 \leq 2 A$
7		2pos	$⊢ 0 < 2$
8	7	a1i	$⊢ A \in ℤ \to 0 < 2$
9	8	anim1i	$⊢ (A \in ℤ \land A < 0) \to (0 < 2 \land A < 0)$
10	9	olcd	$⊢ (A \in ℤ \land A < 0) \to ((2 < 0 \land 0 < A) \lor (0 < 2 \land A < 0))$
11		2re	$⊢ 2 \in ℝ$
12	11	a1i	$⊢ (A \in ℤ \land A < 0) \to 2 \in ℝ$
13	1	adantr	$⊢ (A \in ℤ \land A < 0) \to A \in ℝ$
14	12 13	mul2lt0bi	$⊢ (A \in ℤ \land A < 0) \to (2 A < 0 \leftrightarrow ((2 < 0 \land 0 < A) \lor (0 < 2 \land A < 0)))$
15	10 14	mpbird	$⊢ (A \in ℤ \land A < 0) \to 2 A < 0$
16	12 13	remulcld	$⊢ (A \in ℤ \land A < 0) \to 2 A \in ℝ$
17		0red	$⊢ (A \in ℤ \land A < 0) \to 0 \in ℝ$
18	16 17	ltnled	$⊢ (A \in ℤ \land A < 0) \to (2 A < 0 \leftrightarrow \neg 0 \leq 2 A)$
19	15 18	mpbid	$⊢ (A \in ℤ \land A < 0) \to \neg 0 \leq 2 A$
20	19	ex	$⊢ A \in ℤ \to (A < 0 \to \neg 0 \leq 2 A)$
21	20	con2d	$⊢ A \in ℤ \to (0 \leq 2 A \to \neg A < 0)$
22	21	com12	$⊢ 0 \leq 2 A \to (A \in ℤ \to \neg A < 0)$
23	4 5 6 22	4syl	$⊢ 2 A \in ℙ \to (A \in ℤ \to \neg A < 0)$
24	23	com12	$⊢ A \in ℤ \to (2 A \in ℙ \to \neg A < 0)$
25	24	con2d	$⊢ A \in ℤ \to (A < 0 \to \neg 2 A \in ℙ)$
26	25	a1dd	$⊢ A \in ℤ \to (A < 0 \to (\neg A = 1 \to \neg 2 A \in ℙ))$
27		oveq2	$⊢ A = 0 \to 2 A = 2 \cdot 0$
28		2t0e0	$⊢ 2 \cdot 0 = 0$
29	27 28	eqtrdi	$⊢ A = 0 \to 2 A = 0$
30		0nprm	$⊢ \neg 0 \in ℙ$
31	30	a1i	$⊢ A = 0 \to \neg 0 \in ℙ$
32	29 31	eqneltrd	$⊢ A = 0 \to \neg 2 A \in ℙ$
33	32	a1i13	$⊢ A \in ℤ \to (A = 0 \to (\neg A = 1 \to \neg 2 A \in ℙ))$
34	26 33	jaod	$⊢ A \in ℤ \to ((A < 0 \lor A = 0) \to (\neg A = 1 \to \neg 2 A \in ℙ))$
35	3 34	sylbid	$⊢ A \in ℤ \to (A \leq 0 \to (\neg A = 1 \to \neg 2 A \in ℙ))$
36		2z	$⊢ 2 \in ℤ$
37		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
38	36 37	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
39	36	a1i	$⊢ (A \in ℤ \land 1 \leq A \land \neg A = 1) \to 2 \in ℤ$
40		simp1	$⊢ (A \in ℤ \land 1 \leq A \land \neg A = 1) \to A \in ℤ$
41		df-ne	$⊢ A \neq 1 \leftrightarrow \neg A = 1$
42		1red	$⊢ A \in ℤ \to 1 \in ℝ$
43	42 1	ltlend	$⊢ A \in ℤ \to (1 < A \leftrightarrow (1 \leq A \land A \neq 1))$
44		1zzd	$⊢ A \in ℤ \to 1 \in ℤ$
45		zltp1le	$⊢ (1 \in ℤ \land A \in ℤ) \to (1 < A \leftrightarrow 1 + 1 \leq A)$
46	44 45	mpancom	$⊢ A \in ℤ \to (1 < A \leftrightarrow 1 + 1 \leq A)$
47	46	biimpd	$⊢ A \in ℤ \to (1 < A \to 1 + 1 \leq A)$
48		df-2	$⊢ 2 = 1 + 1$
49	48	breq1i	$⊢ 2 \leq A \leftrightarrow 1 + 1 \leq A$
50	47 49	imbitrrdi	$⊢ A \in ℤ \to (1 < A \to 2 \leq A)$
51	43 50	sylbird	$⊢ A \in ℤ \to ((1 \leq A \land A \neq 1) \to 2 \leq A)$
52	51	expdimp	$⊢ (A \in ℤ \land 1 \leq A) \to (A \neq 1 \to 2 \leq A)$
53	41 52	biimtrrid	$⊢ (A \in ℤ \land 1 \leq A) \to (\neg A = 1 \to 2 \leq A)$
54	53	3impia	$⊢ (A \in ℤ \land 1 \leq A \land \neg A = 1) \to 2 \leq A$
55		eluz2	$⊢ A \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land A \in ℤ \land 2 \leq A)$
56	39 40 54 55	syl3anbrc	$⊢ (A \in ℤ \land 1 \leq A \land \neg A = 1) \to A \in ℤ_{\geq 2}$
57		nprm	$⊢ (2 \in ℤ_{\geq 2} \land A \in ℤ_{\geq 2}) \to \neg 2 A \in ℙ$
58	38 56 57	sylancr	$⊢ (A \in ℤ \land 1 \leq A \land \neg A = 1) \to \neg 2 A \in ℙ$
59	58	3exp	$⊢ A \in ℤ \to (1 \leq A \to (\neg A = 1 \to \neg 2 A \in ℙ))$
60		zle0orge1	$⊢ A \in ℤ \to (A \leq 0 \lor 1 \leq A)$
61	35 59 60	mpjaod	$⊢ A \in ℤ \to (\neg A = 1 \to \neg 2 A \in ℙ)$
62	61	con4d	$⊢ A \in ℤ \to (2 A \in ℙ \to A = 1)$
63		oveq2	$⊢ A = 1 \to 2 A = 2 \cdot 1$
64		2t1e2	$⊢ 2 \cdot 1 = 2$
65	63 64	eqtrdi	$⊢ A = 1 \to 2 A = 2$
66		2prm	$⊢ 2 \in ℙ$
67	65 66	eqeltrdi	$⊢ A = 1 \to 2 A \in ℙ$
68	62 67	impbid1	$⊢ A \in ℤ \to (2 A \in ℙ \leftrightarrow A = 1)$

Metamath Proof Explorer

Theorem 2mulprm

Proof