Theorem 2mulprm

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

	Ref	Expression
Assertion	2mulprm	⊢ ( 𝐴 ∈ ℤ → ( ( 2 · 𝐴 ) ∈ ℙ ↔ 𝐴 = 1 ) )

Proof

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