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 ZABZA=BA=B

Proof

Step Hyp Ref Expression
1 elznn0nn ZZ0ZZ
2 elnn0 Z0ZZ=0
3 elnn1uz2 ZZ=1Z2
4 oveq1 Z=1ZA=1A
5 4 adantr Z=1ABZA=1A
6 5 eqeq1d Z=1ABZA=B1A=B
7 prmz AA
8 7 zcnd AA
9 8 mulid2d A1A=A
10 9 adantr AB1A=A
11 10 eqeq1d AB1A=BA=B
12 11 biimpd AB1A=BA=B
13 12 adantl Z=1AB1A=BA=B
14 6 13 sylbid Z=1ABZA=BA=B
15 14 ex Z=1ABZA=BA=B
16 prmuz2 AA2
17 16 adantr ABA2
18 nprm Z2A2¬ZA
19 17 18 sylan2 Z2AB¬ZA
20 eleq1 ZA=BZAB
21 20 notbid ZA=B¬ZA¬B
22 pm2.24 B¬BA=B
23 22 adantl AB¬BA=B
24 23 adantl Z2AB¬BA=B
25 24 com12 ¬BZ2ABA=B
26 21 25 syl6bi ZA=B¬ZAZ2ABA=B
27 26 com3l ¬ZAZ2ABZA=BA=B
28 19 27 mpcom Z2ABZA=BA=B
29 28 ex Z2ABZA=BA=B
30 15 29 jaoi Z=1Z2ABZA=BA=B
31 3 30 sylbi ZABZA=BA=B
32 oveq1 Z=0ZA=0A
33 32 eqeq1d Z=0ZA=B0A=B
34 prmnn AA
35 34 nnred AA
36 mul02lem2 A0A=0
37 35 36 syl A0A=0
38 37 adantr AB0A=0
39 38 eqeq1d AB0A=B0=B
40 prmnn BB
41 elnnne0 BB0B0
42 eqneqall B=0B0A=B
43 42 eqcoms 0=BB0A=B
44 43 com12 B00=BA=B
45 44 adantl B0B00=BA=B
46 41 45 sylbi B0=BA=B
47 40 46 syl B0=BA=B
48 47 adantl AB0=BA=B
49 39 48 sylbid AB0A=BA=B
50 49 com12 0A=BABA=B
51 33 50 syl6bi Z=0ZA=BABA=B
52 51 com23 Z=0ABZA=BA=B
53 31 52 jaoi ZZ=0ABZA=BA=B
54 2 53 sylbi Z0ABZA=BA=B
55 elnnz ZZ0<Z
56 lt0neg1 ZZ<00<Z
57 34 nngt0d A0<A
58 57 adantr AB0<A
59 simpr ZZ<0Z<0
60 58 59 anim12ci ABZZ<0Z<00<A
61 60 orcd ABZZ<0Z<00<A0<ZA<0
62 simprl ABZZ<0Z
63 35 adantr ABA
64 63 adantr ABZZ<0A
65 62 64 mul2lt0bi ABZZ<0ZA<0Z<00<A0<ZA<0
66 61 65 mpbird ABZZ<0ZA<0
67 66 ex ABZZ<0ZA<0
68 breq1 ZA=BZA<0B<0
69 68 adantl ABZA=BZA<0B<0
70 nnnn0 BB0
71 nn0nlt0 B0¬B<0
72 71 pm2.21d B0B<0A=B
73 70 72 syl BB<0A=B
74 40 73 syl BB<0A=B
75 74 adantl ABB<0A=B
76 75 adantr ABZA=BB<0A=B
77 69 76 sylbid ABZA=BZA<0A=B
78 77 ex ABZA=BZA<0A=B
79 78 com23 ABZA<0ZA=BA=B
80 67 79 syldc ZZ<0ABZA=BA=B
81 80 ex ZZ<0ABZA=BA=B
82 56 81 sylbird Z0<ZABZA=BA=B
83 82 adantld ZZ0<ZABZA=BA=B
84 55 83 syl5bi ZZABZA=BA=B
85 84 imp ZZABZA=BA=B
86 54 85 jaoi Z0ZZABZA=BA=B
87 1 86 sylbi ZABZA=BA=B
88 87 3impib ZABZA=BA=B