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 4 5 6 22 4syl ( ( 2 · 𝐴 ) ∈ ℙ → ( 𝐴 ∈ ℤ → ¬ 𝐴 < 0 ) )
24 23 com12 ( 𝐴 ∈ ℤ → ( ( 2 · 𝐴 ) ∈ ℙ → ¬ 𝐴 < 0 ) )
25 24 con2d ( 𝐴 ∈ ℤ → ( 𝐴 < 0 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) )
26 25 a1dd ( 𝐴 ∈ ℤ → ( 𝐴 < 0 → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) )
27 oveq2 ( 𝐴 = 0 → ( 2 · 𝐴 ) = ( 2 · 0 ) )
28 2t0e0 ( 2 · 0 ) = 0
29 27 28 eqtrdi ( 𝐴 = 0 → ( 2 · 𝐴 ) = 0 )
30 0nprm ¬ 0 ∈ ℙ
31 30 a1i ( 𝐴 = 0 → ¬ 0 ∈ ℙ )
32 29 31 eqneltrd ( 𝐴 = 0 → ¬ ( 2 · 𝐴 ) ∈ ℙ )
33 32 a1i13 ( 𝐴 ∈ ℤ → ( 𝐴 = 0 → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) )
34 26 33 jaod ( 𝐴 ∈ ℤ → ( ( 𝐴 < 0 ∨ 𝐴 = 0 ) → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) )
35 3 34 sylbid ( 𝐴 ∈ ℤ → ( 𝐴 ≤ 0 → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) )
36 2z 2 ∈ ℤ
37 uzid ( 2 ∈ ℤ → 2 ∈ ( ℤ ‘ 2 ) )
38 36 37 ax-mp 2 ∈ ( ℤ ‘ 2 )
39 36 a1i ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ ¬ 𝐴 = 1 ) → 2 ∈ ℤ )
40 simp1 ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ ¬ 𝐴 = 1 ) → 𝐴 ∈ ℤ )
41 df-ne ( 𝐴 ≠ 1 ↔ ¬ 𝐴 = 1 )
42 1red ( 𝐴 ∈ ℤ → 1 ∈ ℝ )
43 42 1 ltlend ( 𝐴 ∈ ℤ → ( 1 < 𝐴 ↔ ( 1 ≤ 𝐴𝐴 ≠ 1 ) ) )
44 1zzd ( 𝐴 ∈ ℤ → 1 ∈ ℤ )
45 zltp1le ( ( 1 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 1 < 𝐴 ↔ ( 1 + 1 ) ≤ 𝐴 ) )
46 44 45 mpancom ( 𝐴 ∈ ℤ → ( 1 < 𝐴 ↔ ( 1 + 1 ) ≤ 𝐴 ) )
47 46 biimpd ( 𝐴 ∈ ℤ → ( 1 < 𝐴 → ( 1 + 1 ) ≤ 𝐴 ) )
48 df-2 2 = ( 1 + 1 )
49 48 breq1i ( 2 ≤ 𝐴 ↔ ( 1 + 1 ) ≤ 𝐴 )
50 47 49 imbitrrdi ( 𝐴 ∈ ℤ → ( 1 < 𝐴 → 2 ≤ 𝐴 ) )
51 43 50 sylbird ( 𝐴 ∈ ℤ → ( ( 1 ≤ 𝐴𝐴 ≠ 1 ) → 2 ≤ 𝐴 ) )
52 51 expdimp ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ) → ( 𝐴 ≠ 1 → 2 ≤ 𝐴 ) )
53 41 52 biimtrrid ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ) → ( ¬ 𝐴 = 1 → 2 ≤ 𝐴 ) )
54 53 3impia ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ ¬ 𝐴 = 1 ) → 2 ≤ 𝐴 )
55 eluz2 ( 𝐴 ∈ ( ℤ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) )
56 39 40 54 55 syl3anbrc ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ ¬ 𝐴 = 1 ) → 𝐴 ∈ ( ℤ ‘ 2 ) )
57 nprm ( ( 2 ∈ ( ℤ ‘ 2 ) ∧ 𝐴 ∈ ( ℤ ‘ 2 ) ) → ¬ ( 2 · 𝐴 ) ∈ ℙ )
58 38 56 57 sylancr ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ ¬ 𝐴 = 1 ) → ¬ ( 2 · 𝐴 ) ∈ ℙ )
59 58 3exp ( 𝐴 ∈ ℤ → ( 1 ≤ 𝐴 → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) )
60 zle0orge1 ( 𝐴 ∈ ℤ → ( 𝐴 ≤ 0 ∨ 1 ≤ 𝐴 ) )
61 35 59 60 mpjaod ( 𝐴 ∈ ℤ → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) )
62 61 con4d ( 𝐴 ∈ ℤ → ( ( 2 · 𝐴 ) ∈ ℙ → 𝐴 = 1 ) )
63 oveq2 ( 𝐴 = 1 → ( 2 · 𝐴 ) = ( 2 · 1 ) )
64 2t1e2 ( 2 · 1 ) = 2
65 63 64 eqtrdi ( 𝐴 = 1 → ( 2 · 𝐴 ) = 2 )
66 2prm 2 ∈ ℙ
67 65 66 eqeltrdi ( 𝐴 = 1 → ( 2 · 𝐴 ) ∈ ℙ )
68 62 67 impbid1 ( 𝐴 ∈ ℤ → ( ( 2 · 𝐴 ) ∈ ℙ ↔ 𝐴 = 1 ) )