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