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	6 22	syl	$⊢ 2 A \in ℕ_{0} \to (A \in ℤ \to \neg A < 0)$
24	4 5 23	3syl	$⊢ 2 A \in ℙ \to (A \in ℤ \to \neg A < 0)$
25	24	com12	$⊢ A \in ℤ \to (2 A \in ℙ \to \neg A < 0)$
26	25	con2d	$⊢ A \in ℤ \to (A < 0 \to \neg 2 A \in ℙ)$
27	26	a1dd	$⊢ A \in ℤ \to (A < 0 \to (\neg A = 1 \to \neg 2 A \in ℙ))$
28		oveq2	$⊢ A = 0 \to 2 A = 2 \cdot 0$
29		2t0e0	$⊢ 2 \cdot 0 = 0$
30	28 29	eqtrdi	$⊢ A = 0 \to 2 A = 0$
31		0nprm	$⊢ \neg 0 \in ℙ$
32	31	a1i	$⊢ A = 0 \to \neg 0 \in ℙ$
33	30 32	eqneltrd	$⊢ A = 0 \to \neg 2 A \in ℙ$
34	33	a1i13	$⊢ A \in ℤ \to (A = 0 \to (\neg A = 1 \to \neg 2 A \in ℙ))$
35	27 34	jaod	$⊢ A \in ℤ \to ((A < 0 \lor A = 0) \to (\neg A = 1 \to \neg 2 A \in ℙ))$
36	3 35	sylbid	$⊢ A \in ℤ \to (A \leq 0 \to (\neg A = 1 \to \neg 2 A \in ℙ))$
37		2z	$⊢ 2 \in ℤ$
38		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
39	37 38	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
40	37	a1i	$⊢ (A \in ℤ \land 1 \leq A \land \neg A = 1) \to 2 \in ℤ$
41		simp1	$⊢ (A \in ℤ \land 1 \leq A \land \neg A = 1) \to A \in ℤ$
42		df-ne	$⊢ A \neq 1 \leftrightarrow \neg A = 1$
43		1red	$⊢ A \in ℤ \to 1 \in ℝ$
44	43 1	ltlend	$⊢ A \in ℤ \to (1 < A \leftrightarrow (1 \leq A \land A \neq 1))$
45		1zzd	$⊢ A \in ℤ \to 1 \in ℤ$
46		zltp1le	$⊢ (1 \in ℤ \land A \in ℤ) \to (1 < A \leftrightarrow 1 + 1 \leq A)$
47	45 46	mpancom	$⊢ A \in ℤ \to (1 < A \leftrightarrow 1 + 1 \leq A)$
48	47	biimpd	$⊢ A \in ℤ \to (1 < A \to 1 + 1 \leq A)$
49		df-2	$⊢ 2 = 1 + 1$
50	49	breq1i	$⊢ 2 \leq A \leftrightarrow 1 + 1 \leq A$
51	48 50	syl6ibr	$⊢ A \in ℤ \to (1 < A \to 2 \leq A)$
52	44 51	sylbird	$⊢ A \in ℤ \to ((1 \leq A \land A \neq 1) \to 2 \leq A)$
53	52	expdimp	$⊢ (A \in ℤ \land 1 \leq A) \to (A \neq 1 \to 2 \leq A)$
54	42 53	syl5bir	$⊢ (A \in ℤ \land 1 \leq A) \to (\neg A = 1 \to 2 \leq A)$
55	54	3impia	$⊢ (A \in ℤ \land 1 \leq A \land \neg A = 1) \to 2 \leq A$
56		eluz2	$⊢ A \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land A \in ℤ \land 2 \leq A)$
57	40 41 55 56	syl3anbrc	$⊢ (A \in ℤ \land 1 \leq A \land \neg A = 1) \to A \in ℤ_{\geq 2}$
58		nprm	$⊢ (2 \in ℤ_{\geq 2} \land A \in ℤ_{\geq 2}) \to \neg 2 A \in ℙ$
59	39 57 58	sylancr	$⊢ (A \in ℤ \land 1 \leq A \land \neg A = 1) \to \neg 2 A \in ℙ$
60	59	3exp	$⊢ A \in ℤ \to (1 \leq A \to (\neg A = 1 \to \neg 2 A \in ℙ))$
61		zle0orge1	$⊢ A \in ℤ \to (A \leq 0 \lor 1 \leq A)$
62	36 60 61	mpjaod	$⊢ A \in ℤ \to (\neg A = 1 \to \neg 2 A \in ℙ)$
63	62	con4d	$⊢ A \in ℤ \to (2 A \in ℙ \to A = 1)$
64		oveq2	$⊢ A = 1 \to 2 A = 2 \cdot 1$
65		2t1e2	$⊢ 2 \cdot 1 = 2$
66	64 65	eqtrdi	$⊢ A = 1 \to 2 A = 2$
67		2prm	$⊢ 2 \in ℙ$
68	66 67	eqeltrdi	$⊢ A = 1 \to 2 A \in ℙ$
69	63 68	impbid1	$⊢ A \in ℤ \to (2 A \in ℙ \leftrightarrow A = 1)$

Metamath Proof Explorer

Theorem 2mulprm

Proof