Metamath Proof Explorer

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 ) )