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 
|- ( A e. ZZ -> ( ( 2 x. A ) e. Prime <-> A = 1 ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( A e. ZZ -> A e. RR )
2 0red 
 |-  ( A e. ZZ -> 0 e. RR )
3 1 2 leloed 
 |-  ( A e. ZZ -> ( A <_ 0 <-> ( A < 0 \/ A = 0 ) ) )
4 prmnn 
 |-  ( ( 2 x. A ) e. Prime -> ( 2 x. A ) e. NN )
5 nnnn0 
 |-  ( ( 2 x. A ) e. NN -> ( 2 x. A ) e. NN0 )
6 nn0ge0 
 |-  ( ( 2 x. A ) e. NN0 -> 0 <_ ( 2 x. A ) )
7 2pos 
 |-  0 < 2
8 7 a1i 
 |-  ( A e. ZZ -> 0 < 2 )
9 8 anim1i 
 |-  ( ( A e. ZZ /\ A < 0 ) -> ( 0 < 2 /\ A < 0 ) )
10 9 olcd 
 |-  ( ( A e. ZZ /\ A < 0 ) -> ( ( 2 < 0 /\ 0 < A ) \/ ( 0 < 2 /\ A < 0 ) ) )
11 2re 
 |-  2 e. RR
12 11 a1i 
 |-  ( ( A e. ZZ /\ A < 0 ) -> 2 e. RR )
13 1 adantr 
 |-  ( ( A e. ZZ /\ A < 0 ) -> A e. RR )
14 12 13 mul2lt0bi 
 |-  ( ( A e. ZZ /\ A < 0 ) -> ( ( 2 x. A ) < 0 <-> ( ( 2 < 0 /\ 0 < A ) \/ ( 0 < 2 /\ A < 0 ) ) ) )
15 10 14 mpbird 
 |-  ( ( A e. ZZ /\ A < 0 ) -> ( 2 x. A ) < 0 )
16 12 13 remulcld 
 |-  ( ( A e. ZZ /\ A < 0 ) -> ( 2 x. A ) e. RR )
17 0red 
 |-  ( ( A e. ZZ /\ A < 0 ) -> 0 e. RR )
18 16 17 ltnled 
 |-  ( ( A e. ZZ /\ A < 0 ) -> ( ( 2 x. A ) < 0 <-> -. 0 <_ ( 2 x. A ) ) )
19 15 18 mpbid 
 |-  ( ( A e. ZZ /\ A < 0 ) -> -. 0 <_ ( 2 x. A ) )
20 19 ex 
 |-  ( A e. ZZ -> ( A < 0 -> -. 0 <_ ( 2 x. A ) ) )
21 20 con2d 
 |-  ( A e. ZZ -> ( 0 <_ ( 2 x. A ) -> -. A < 0 ) )
22 21 com12 
 |-  ( 0 <_ ( 2 x. A ) -> ( A e. ZZ -> -. A < 0 ) )
23 6 22 syl 
 |-  ( ( 2 x. A ) e. NN0 -> ( A e. ZZ -> -. A < 0 ) )
24 4 5 23 3syl 
 |-  ( ( 2 x. A ) e. Prime -> ( A e. ZZ -> -. A < 0 ) )
25 24 com12 
 |-  ( A e. ZZ -> ( ( 2 x. A ) e. Prime -> -. A < 0 ) )
26 25 con2d 
 |-  ( A e. ZZ -> ( A < 0 -> -. ( 2 x. A ) e. Prime ) )
27 26 a1dd 
 |-  ( A e. ZZ -> ( A < 0 -> ( -. A = 1 -> -. ( 2 x. A ) e. Prime ) ) )
28 oveq2 
 |-  ( A = 0 -> ( 2 x. A ) = ( 2 x. 0 ) )
29 2t0e0 
 |-  ( 2 x. 0 ) = 0
30 28 29 eqtrdi 
 |-  ( A = 0 -> ( 2 x. A ) = 0 )
31 0nprm 
 |-  -. 0 e. Prime
32 31 a1i 
 |-  ( A = 0 -> -. 0 e. Prime )
33 30 32 eqneltrd 
 |-  ( A = 0 -> -. ( 2 x. A ) e. Prime )
34 33 a1i13 
 |-  ( A e. ZZ -> ( A = 0 -> ( -. A = 1 -> -. ( 2 x. A ) e. Prime ) ) )
35 27 34 jaod 
 |-  ( A e. ZZ -> ( ( A < 0 \/ A = 0 ) -> ( -. A = 1 -> -. ( 2 x. A ) e. Prime ) ) )
36 3 35 sylbid 
 |-  ( A e. ZZ -> ( A <_ 0 -> ( -. A = 1 -> -. ( 2 x. A ) e. Prime ) ) )
37 2z 
 |-  2 e. ZZ
38 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
39 37 38 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
40 37 a1i 
 |-  ( ( A e. ZZ /\ 1 <_ A /\ -. A = 1 ) -> 2 e. ZZ )
41 simp1 
 |-  ( ( A e. ZZ /\ 1 <_ A /\ -. A = 1 ) -> A e. ZZ )
42 df-ne 
 |-  ( A =/= 1 <-> -. A = 1 )
43 1red 
 |-  ( A e. ZZ -> 1 e. RR )
44 43 1 ltlend 
 |-  ( A e. ZZ -> ( 1 < A <-> ( 1 <_ A /\ A =/= 1 ) ) )
45 1zzd 
 |-  ( A e. ZZ -> 1 e. ZZ )
46 zltp1le 
 |-  ( ( 1 e. ZZ /\ A e. ZZ ) -> ( 1 < A <-> ( 1 + 1 ) <_ A ) )
47 45 46 mpancom 
 |-  ( A e. ZZ -> ( 1 < A <-> ( 1 + 1 ) <_ A ) )
48 47 biimpd 
 |-  ( A e. ZZ -> ( 1 < A -> ( 1 + 1 ) <_ A ) )
49 df-2 
 |-  2 = ( 1 + 1 )
50 49 breq1i 
 |-  ( 2 <_ A <-> ( 1 + 1 ) <_ A )
51 48 50 syl6ibr 
 |-  ( A e. ZZ -> ( 1 < A -> 2 <_ A ) )
52 44 51 sylbird 
 |-  ( A e. ZZ -> ( ( 1 <_ A /\ A =/= 1 ) -> 2 <_ A ) )
53 52 expdimp 
 |-  ( ( A e. ZZ /\ 1 <_ A ) -> ( A =/= 1 -> 2 <_ A ) )
54 42 53 syl5bir 
 |-  ( ( A e. ZZ /\ 1 <_ A ) -> ( -. A = 1 -> 2 <_ A ) )
55 54 3impia 
 |-  ( ( A e. ZZ /\ 1 <_ A /\ -. A = 1 ) -> 2 <_ A )
56 eluz2 
 |-  ( A e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ A e. ZZ /\ 2 <_ A ) )
57 40 41 55 56 syl3anbrc 
 |-  ( ( A e. ZZ /\ 1 <_ A /\ -. A = 1 ) -> A e. ( ZZ>= ` 2 ) )
58 nprm 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ A e. ( ZZ>= ` 2 ) ) -> -. ( 2 x. A ) e. Prime )
59 39 57 58 sylancr 
 |-  ( ( A e. ZZ /\ 1 <_ A /\ -. A = 1 ) -> -. ( 2 x. A ) e. Prime )
60 59 3exp 
 |-  ( A e. ZZ -> ( 1 <_ A -> ( -. A = 1 -> -. ( 2 x. A ) e. Prime ) ) )
61 zle0orge1 
 |-  ( A e. ZZ -> ( A <_ 0 \/ 1 <_ A ) )
62 36 60 61 mpjaod 
 |-  ( A e. ZZ -> ( -. A = 1 -> -. ( 2 x. A ) e. Prime ) )
63 62 con4d 
 |-  ( A e. ZZ -> ( ( 2 x. A ) e. Prime -> A = 1 ) )
64 oveq2 
 |-  ( A = 1 -> ( 2 x. A ) = ( 2 x. 1 ) )
65 2t1e2 
 |-  ( 2 x. 1 ) = 2
66 64 65 eqtrdi 
 |-  ( A = 1 -> ( 2 x. A ) = 2 )
67 2prm 
 |-  2 e. Prime
68 66 67 eqeltrdi 
 |-  ( A = 1 -> ( 2 x. A ) e. Prime )
69 63 68 impbid1 
 |-  ( A e. ZZ -> ( ( 2 x. A ) e. Prime <-> A = 1 ) )