Metamath Proof Explorer

Theorem ztprmneprm

Description: A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019)

Ref Expression
Assertion ztprmneprm 
|- ( ( Z e. ZZ /\ A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) )

Proof

Step Hyp Ref Expression
1 elznn0nn 
 |-  ( Z e. ZZ <-> ( Z e. NN0 \/ ( Z e. RR /\ -u Z e. NN ) ) )
2 elnn0 
 |-  ( Z e. NN0 <-> ( Z e. NN \/ Z = 0 ) )
3 elnn1uz2 
 |-  ( Z e. NN <-> ( Z = 1 \/ Z e. ( ZZ>= ` 2 ) ) )
4 oveq1 
 |-  ( Z = 1 -> ( Z x. A ) = ( 1 x. A ) )
5 4 adantr 
 |-  ( ( Z = 1 /\ ( A e. Prime /\ B e. Prime ) ) -> ( Z x. A ) = ( 1 x. A ) )
6 5 eqeq1d 
 |-  ( ( Z = 1 /\ ( A e. Prime /\ B e. Prime ) ) -> ( ( Z x. A ) = B <-> ( 1 x. A ) = B ) )
7 prmz 
 |-  ( A e. Prime -> A e. ZZ )
8 7 zcnd 
 |-  ( A e. Prime -> A e. CC )
9 8 mulid2d 
 |-  ( A e. Prime -> ( 1 x. A ) = A )
10 9 adantr 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( 1 x. A ) = A )
11 10 eqeq1d 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( ( 1 x. A ) = B <-> A = B ) )
12 11 biimpd 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( ( 1 x. A ) = B -> A = B ) )
13 12 adantl 
 |-  ( ( Z = 1 /\ ( A e. Prime /\ B e. Prime ) ) -> ( ( 1 x. A ) = B -> A = B ) )
14 6 13 sylbid 
 |-  ( ( Z = 1 /\ ( A e. Prime /\ B e. Prime ) ) -> ( ( Z x. A ) = B -> A = B ) )
15 14 ex 
 |-  ( Z = 1 -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) )
16 prmuz2 
 |-  ( A e. Prime -> A e. ( ZZ>= ` 2 ) )
17 16 adantr 
 |-  ( ( A e. Prime /\ B e. Prime ) -> A e. ( ZZ>= ` 2 ) )
18 nprm 
 |-  ( ( Z e. ( ZZ>= ` 2 ) /\ A e. ( ZZ>= ` 2 ) ) -> -. ( Z x. A ) e. Prime )
19 17 18 sylan2 
 |-  ( ( Z e. ( ZZ>= ` 2 ) /\ ( A e. Prime /\ B e. Prime ) ) -> -. ( Z x. A ) e. Prime )
20 eleq1 
 |-  ( ( Z x. A ) = B -> ( ( Z x. A ) e. Prime <-> B e. Prime ) )
21 20 notbid 
 |-  ( ( Z x. A ) = B -> ( -. ( Z x. A ) e. Prime <-> -. B e. Prime ) )
22 pm2.24 
 |-  ( B e. Prime -> ( -. B e. Prime -> A = B ) )
23 22 adantl 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( -. B e. Prime -> A = B ) )
24 23 adantl 
 |-  ( ( Z e. ( ZZ>= ` 2 ) /\ ( A e. Prime /\ B e. Prime ) ) -> ( -. B e. Prime -> A = B ) )
25 24 com12 
 |-  ( -. B e. Prime -> ( ( Z e. ( ZZ>= ` 2 ) /\ ( A e. Prime /\ B e. Prime ) ) -> A = B ) )
26 21 25 syl6bi 
 |-  ( ( Z x. A ) = B -> ( -. ( Z x. A ) e. Prime -> ( ( Z e. ( ZZ>= ` 2 ) /\ ( A e. Prime /\ B e. Prime ) ) -> A = B ) ) )
27 26 com3l 
 |-  ( -. ( Z x. A ) e. Prime -> ( ( Z e. ( ZZ>= ` 2 ) /\ ( A e. Prime /\ B e. Prime ) ) -> ( ( Z x. A ) = B -> A = B ) ) )
28 19 27 mpcom 
 |-  ( ( Z e. ( ZZ>= ` 2 ) /\ ( A e. Prime /\ B e. Prime ) ) -> ( ( Z x. A ) = B -> A = B ) )
29 28 ex 
 |-  ( Z e. ( ZZ>= ` 2 ) -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) )
30 15 29 jaoi 
 |-  ( ( Z = 1 \/ Z e. ( ZZ>= ` 2 ) ) -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) )
31 3 30 sylbi 
 |-  ( Z e. NN -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) )
32 oveq1 
 |-  ( Z = 0 -> ( Z x. A ) = ( 0 x. A ) )
33 32 eqeq1d 
 |-  ( Z = 0 -> ( ( Z x. A ) = B <-> ( 0 x. A ) = B ) )
34 prmnn 
 |-  ( A e. Prime -> A e. NN )
35 34 nnred 
 |-  ( A e. Prime -> A e. RR )
36 mul02lem2 
 |-  ( A e. RR -> ( 0 x. A ) = 0 )
37 35 36 syl 
 |-  ( A e. Prime -> ( 0 x. A ) = 0 )
38 37 adantr 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( 0 x. A ) = 0 )
39 38 eqeq1d 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( ( 0 x. A ) = B <-> 0 = B ) )
40 prmnn 
 |-  ( B e. Prime -> B e. NN )
41 elnnne0 
 |-  ( B e. NN <-> ( B e. NN0 /\ B =/= 0 ) )
42 eqneqall 
 |-  ( B = 0 -> ( B =/= 0 -> A = B ) )
43 42 eqcoms 
 |-  ( 0 = B -> ( B =/= 0 -> A = B ) )
44 43 com12 
 |-  ( B =/= 0 -> ( 0 = B -> A = B ) )
45 44 adantl 
 |-  ( ( B e. NN0 /\ B =/= 0 ) -> ( 0 = B -> A = B ) )
46 41 45 sylbi 
 |-  ( B e. NN -> ( 0 = B -> A = B ) )
47 40 46 syl 
 |-  ( B e. Prime -> ( 0 = B -> A = B ) )
48 47 adantl 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( 0 = B -> A = B ) )
49 39 48 sylbid 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( ( 0 x. A ) = B -> A = B ) )
50 49 com12 
 |-  ( ( 0 x. A ) = B -> ( ( A e. Prime /\ B e. Prime ) -> A = B ) )
51 33 50 syl6bi 
 |-  ( Z = 0 -> ( ( Z x. A ) = B -> ( ( A e. Prime /\ B e. Prime ) -> A = B ) ) )
52 51 com23 
 |-  ( Z = 0 -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) )
53 31 52 jaoi 
 |-  ( ( Z e. NN \/ Z = 0 ) -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) )
54 2 53 sylbi 
 |-  ( Z e. NN0 -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) )
55 elnnz 
 |-  ( -u Z e. NN <-> ( -u Z e. ZZ /\ 0 < -u Z ) )
56 lt0neg1 
 |-  ( Z e. RR -> ( Z < 0 <-> 0 < -u Z ) )
57 34 nngt0d 
 |-  ( A e. Prime -> 0 < A )
58 57 adantr 
 |-  ( ( A e. Prime /\ B e. Prime ) -> 0 < A )
59 simpr 
 |-  ( ( Z e. RR /\ Z < 0 ) -> Z < 0 )
60 58 59 anim12ci 
 |-  ( ( ( A e. Prime /\ B e. Prime ) /\ ( Z e. RR /\ Z < 0 ) ) -> ( Z < 0 /\ 0 < A ) )
61 60 orcd 
 |-  ( ( ( A e. Prime /\ B e. Prime ) /\ ( Z e. RR /\ Z < 0 ) ) -> ( ( Z < 0 /\ 0 < A ) \/ ( 0 < Z /\ A < 0 ) ) )
62 simprl 
 |-  ( ( ( A e. Prime /\ B e. Prime ) /\ ( Z e. RR /\ Z < 0 ) ) -> Z e. RR )
63 35 adantr 
 |-  ( ( A e. Prime /\ B e. Prime ) -> A e. RR )
64 63 adantr 
 |-  ( ( ( A e. Prime /\ B e. Prime ) /\ ( Z e. RR /\ Z < 0 ) ) -> A e. RR )
65 62 64 mul2lt0bi 
 |-  ( ( ( A e. Prime /\ B e. Prime ) /\ ( Z e. RR /\ Z < 0 ) ) -> ( ( Z x. A ) < 0 <-> ( ( Z < 0 /\ 0 < A ) \/ ( 0 < Z /\ A < 0 ) ) ) )
66 61 65 mpbird 
 |-  ( ( ( A e. Prime /\ B e. Prime ) /\ ( Z e. RR /\ Z < 0 ) ) -> ( Z x. A ) < 0 )
67 66 ex 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( ( Z e. RR /\ Z < 0 ) -> ( Z x. A ) < 0 ) )
68 breq1 
 |-  ( ( Z x. A ) = B -> ( ( Z x. A ) < 0 <-> B < 0 ) )
69 68 adantl 
 |-  ( ( ( A e. Prime /\ B e. Prime ) /\ ( Z x. A ) = B ) -> ( ( Z x. A ) < 0 <-> B < 0 ) )
70 nnnn0 
 |-  ( B e. NN -> B e. NN0 )
71 nn0nlt0 
 |-  ( B e. NN0 -> -. B < 0 )
72 71 pm2.21d 
 |-  ( B e. NN0 -> ( B < 0 -> A = B ) )
73 70 72 syl 
 |-  ( B e. NN -> ( B < 0 -> A = B ) )
74 40 73 syl 
 |-  ( B e. Prime -> ( B < 0 -> A = B ) )
75 74 adantl 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( B < 0 -> A = B ) )
76 75 adantr 
 |-  ( ( ( A e. Prime /\ B e. Prime ) /\ ( Z x. A ) = B ) -> ( B < 0 -> A = B ) )
77 69 76 sylbid 
 |-  ( ( ( A e. Prime /\ B e. Prime ) /\ ( Z x. A ) = B ) -> ( ( Z x. A ) < 0 -> A = B ) )
78 77 ex 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> ( ( Z x. A ) < 0 -> A = B ) ) )
79 78 com23 
 |-  ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) < 0 -> ( ( Z x. A ) = B -> A = B ) ) )
80 67 79 syldc 
 |-  ( ( Z e. RR /\ Z < 0 ) -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) )
81 80 ex 
 |-  ( Z e. RR -> ( Z < 0 -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) ) )
82 56 81 sylbird 
 |-  ( Z e. RR -> ( 0 < -u Z -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) ) )
83 82 adantld 
 |-  ( Z e. RR -> ( ( -u Z e. ZZ /\ 0 < -u Z ) -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) ) )
84 55 83 syl5bi 
 |-  ( Z e. RR -> ( -u Z e. NN -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) ) )
85 84 imp 
 |-  ( ( Z e. RR /\ -u Z e. NN ) -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) )
86 54 85 jaoi 
 |-  ( ( Z e. NN0 \/ ( Z e. RR /\ -u Z e. NN ) ) -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) )
87 1 86 sylbi 
 |-  ( Z e. ZZ -> ( ( A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) ) )
88 87 3impib 
 |-  ( ( Z e. ZZ /\ A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) )