This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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