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 ( ( ๐‘ โˆˆ โ„ค โˆง ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) )

Proof

Step Hyp Ref Expression
1 elznn0nn โŠข ( ๐‘ โˆˆ โ„ค โ†” ( ๐‘ โˆˆ โ„•0 โˆจ ( ๐‘ โˆˆ โ„ โˆง - ๐‘ โˆˆ โ„• ) ) )
2 elnn0 โŠข ( ๐‘ โˆˆ โ„•0 โ†” ( ๐‘ โˆˆ โ„• โˆจ ๐‘ = 0 ) )
3 elnn1uz2 โŠข ( ๐‘ โˆˆ โ„• โ†” ( ๐‘ = 1 โˆจ ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
4 oveq1 โŠข ( ๐‘ = 1 โ†’ ( ๐‘ ยท ๐ด ) = ( 1 ยท ๐ด ) )
5 4 adantr โŠข ( ( ๐‘ = 1 โˆง ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) ) โ†’ ( ๐‘ ยท ๐ด ) = ( 1 ยท ๐ด ) )
6 5 eqeq1d โŠข ( ( ๐‘ = 1 โˆง ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†” ( 1 ยท ๐ด ) = ๐ต ) )
7 prmz โŠข ( ๐ด โˆˆ โ„™ โ†’ ๐ด โˆˆ โ„ค )
8 7 zcnd โŠข ( ๐ด โˆˆ โ„™ โ†’ ๐ด โˆˆ โ„‚ )
9 8 mulid2d โŠข ( ๐ด โˆˆ โ„™ โ†’ ( 1 ยท ๐ด ) = ๐ด )
10 9 adantr โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( 1 ยท ๐ด ) = ๐ด )
11 10 eqeq1d โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( 1 ยท ๐ด ) = ๐ต โ†” ๐ด = ๐ต ) )
12 11 biimpd โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( 1 ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) )
13 12 adantl โŠข ( ( ๐‘ = 1 โˆง ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) ) โ†’ ( ( 1 ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) )
14 6 13 sylbid โŠข ( ( ๐‘ = 1 โˆง ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) )
15 14 ex โŠข ( ๐‘ = 1 โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
16 prmuz2 โŠข ( ๐ด โˆˆ โ„™ โ†’ ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
17 16 adantr โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
18 nprm โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ยฌ ( ๐‘ ยท ๐ด ) โˆˆ โ„™ )
19 17 18 sylan2 โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) ) โ†’ ยฌ ( ๐‘ ยท ๐ด ) โˆˆ โ„™ )
20 eleq1 โŠข ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ( ( ๐‘ ยท ๐ด ) โˆˆ โ„™ โ†” ๐ต โˆˆ โ„™ ) )
21 20 notbid โŠข ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ( ยฌ ( ๐‘ ยท ๐ด ) โˆˆ โ„™ โ†” ยฌ ๐ต โˆˆ โ„™ ) )
22 pm2.24 โŠข ( ๐ต โˆˆ โ„™ โ†’ ( ยฌ ๐ต โˆˆ โ„™ โ†’ ๐ด = ๐ต ) )
23 22 adantl โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ยฌ ๐ต โˆˆ โ„™ โ†’ ๐ด = ๐ต ) )
24 23 adantl โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) ) โ†’ ( ยฌ ๐ต โˆˆ โ„™ โ†’ ๐ด = ๐ต ) )
25 24 com12 โŠข ( ยฌ ๐ต โˆˆ โ„™ โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) ) โ†’ ๐ด = ๐ต ) )
26 21 25 syl6bi โŠข ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ( ยฌ ( ๐‘ ยท ๐ด ) โˆˆ โ„™ โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) ) โ†’ ๐ด = ๐ต ) ) )
27 26 com3l โŠข ( ยฌ ( ๐‘ ยท ๐ด ) โˆˆ โ„™ โ†’ ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
28 19 27 mpcom โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) )
29 28 ex โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
30 15 29 jaoi โŠข ( ( ๐‘ = 1 โˆจ ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
31 3 30 sylbi โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
32 oveq1 โŠข ( ๐‘ = 0 โ†’ ( ๐‘ ยท ๐ด ) = ( 0 ยท ๐ด ) )
33 32 eqeq1d โŠข ( ๐‘ = 0 โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†” ( 0 ยท ๐ด ) = ๐ต ) )
34 prmnn โŠข ( ๐ด โˆˆ โ„™ โ†’ ๐ด โˆˆ โ„• )
35 34 nnred โŠข ( ๐ด โˆˆ โ„™ โ†’ ๐ด โˆˆ โ„ )
36 mul02lem2 โŠข ( ๐ด โˆˆ โ„ โ†’ ( 0 ยท ๐ด ) = 0 )
37 35 36 syl โŠข ( ๐ด โˆˆ โ„™ โ†’ ( 0 ยท ๐ด ) = 0 )
38 37 adantr โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( 0 ยท ๐ด ) = 0 )
39 38 eqeq1d โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( 0 ยท ๐ด ) = ๐ต โ†” 0 = ๐ต ) )
40 prmnn โŠข ( ๐ต โˆˆ โ„™ โ†’ ๐ต โˆˆ โ„• )
41 elnnne0 โŠข ( ๐ต โˆˆ โ„• โ†” ( ๐ต โˆˆ โ„•0 โˆง ๐ต โ‰  0 ) )
42 eqneqall โŠข ( ๐ต = 0 โ†’ ( ๐ต โ‰  0 โ†’ ๐ด = ๐ต ) )
43 42 eqcoms โŠข ( 0 = ๐ต โ†’ ( ๐ต โ‰  0 โ†’ ๐ด = ๐ต ) )
44 43 com12 โŠข ( ๐ต โ‰  0 โ†’ ( 0 = ๐ต โ†’ ๐ด = ๐ต ) )
45 44 adantl โŠข ( ( ๐ต โˆˆ โ„•0 โˆง ๐ต โ‰  0 ) โ†’ ( 0 = ๐ต โ†’ ๐ด = ๐ต ) )
46 41 45 sylbi โŠข ( ๐ต โˆˆ โ„• โ†’ ( 0 = ๐ต โ†’ ๐ด = ๐ต ) )
47 40 46 syl โŠข ( ๐ต โˆˆ โ„™ โ†’ ( 0 = ๐ต โ†’ ๐ด = ๐ต ) )
48 47 adantl โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( 0 = ๐ต โ†’ ๐ด = ๐ต ) )
49 39 48 sylbid โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( 0 ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) )
50 49 com12 โŠข ( ( 0 ยท ๐ด ) = ๐ต โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ๐ด = ๐ต ) )
51 33 50 syl6bi โŠข ( ๐‘ = 0 โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ๐ด = ๐ต ) ) )
52 51 com23 โŠข ( ๐‘ = 0 โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
53 31 52 jaoi โŠข ( ( ๐‘ โˆˆ โ„• โˆจ ๐‘ = 0 ) โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
54 2 53 sylbi โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
55 elnnz โŠข ( - ๐‘ โˆˆ โ„• โ†” ( - ๐‘ โˆˆ โ„ค โˆง 0 < - ๐‘ ) )
56 lt0neg1 โŠข ( ๐‘ โˆˆ โ„ โ†’ ( ๐‘ < 0 โ†” 0 < - ๐‘ ) )
57 34 nngt0d โŠข ( ๐ด โˆˆ โ„™ โ†’ 0 < ๐ด )
58 57 adantr โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ 0 < ๐ด )
59 simpr โŠข ( ( ๐‘ โˆˆ โ„ โˆง ๐‘ < 0 ) โ†’ ๐‘ < 0 )
60 58 59 anim12ci โŠข ( ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โˆง ( ๐‘ โˆˆ โ„ โˆง ๐‘ < 0 ) ) โ†’ ( ๐‘ < 0 โˆง 0 < ๐ด ) )
61 60 orcd โŠข ( ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โˆง ( ๐‘ โˆˆ โ„ โˆง ๐‘ < 0 ) ) โ†’ ( ( ๐‘ < 0 โˆง 0 < ๐ด ) โˆจ ( 0 < ๐‘ โˆง ๐ด < 0 ) ) )
62 simprl โŠข ( ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โˆง ( ๐‘ โˆˆ โ„ โˆง ๐‘ < 0 ) ) โ†’ ๐‘ โˆˆ โ„ )
63 35 adantr โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ๐ด โˆˆ โ„ )
64 63 adantr โŠข ( ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โˆง ( ๐‘ โˆˆ โ„ โˆง ๐‘ < 0 ) ) โ†’ ๐ด โˆˆ โ„ )
65 62 64 mul2lt0bi โŠข ( ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โˆง ( ๐‘ โˆˆ โ„ โˆง ๐‘ < 0 ) ) โ†’ ( ( ๐‘ ยท ๐ด ) < 0 โ†” ( ( ๐‘ < 0 โˆง 0 < ๐ด ) โˆจ ( 0 < ๐‘ โˆง ๐ด < 0 ) ) ) )
66 61 65 mpbird โŠข ( ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โˆง ( ๐‘ โˆˆ โ„ โˆง ๐‘ < 0 ) ) โ†’ ( ๐‘ ยท ๐ด ) < 0 )
67 66 ex โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ โˆˆ โ„ โˆง ๐‘ < 0 ) โ†’ ( ๐‘ ยท ๐ด ) < 0 ) )
68 breq1 โŠข ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ( ( ๐‘ ยท ๐ด ) < 0 โ†” ๐ต < 0 ) )
69 68 adantl โŠข ( ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โˆง ( ๐‘ ยท ๐ด ) = ๐ต ) โ†’ ( ( ๐‘ ยท ๐ด ) < 0 โ†” ๐ต < 0 ) )
70 nnnn0 โŠข ( ๐ต โˆˆ โ„• โ†’ ๐ต โˆˆ โ„•0 )
71 nn0nlt0 โŠข ( ๐ต โˆˆ โ„•0 โ†’ ยฌ ๐ต < 0 )
72 71 pm2.21d โŠข ( ๐ต โˆˆ โ„•0 โ†’ ( ๐ต < 0 โ†’ ๐ด = ๐ต ) )
73 70 72 syl โŠข ( ๐ต โˆˆ โ„• โ†’ ( ๐ต < 0 โ†’ ๐ด = ๐ต ) )
74 40 73 syl โŠข ( ๐ต โˆˆ โ„™ โ†’ ( ๐ต < 0 โ†’ ๐ด = ๐ต ) )
75 74 adantl โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ๐ต < 0 โ†’ ๐ด = ๐ต ) )
76 75 adantr โŠข ( ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โˆง ( ๐‘ ยท ๐ด ) = ๐ต ) โ†’ ( ๐ต < 0 โ†’ ๐ด = ๐ต ) )
77 69 76 sylbid โŠข ( ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โˆง ( ๐‘ ยท ๐ด ) = ๐ต ) โ†’ ( ( ๐‘ ยท ๐ด ) < 0 โ†’ ๐ด = ๐ต ) )
78 77 ex โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ( ( ๐‘ ยท ๐ด ) < 0 โ†’ ๐ด = ๐ต ) ) )
79 78 com23 โŠข ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) < 0 โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
80 67 79 syldc โŠข ( ( ๐‘ โˆˆ โ„ โˆง ๐‘ < 0 ) โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
81 80 ex โŠข ( ๐‘ โˆˆ โ„ โ†’ ( ๐‘ < 0 โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) ) )
82 56 81 sylbird โŠข ( ๐‘ โˆˆ โ„ โ†’ ( 0 < - ๐‘ โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) ) )
83 82 adantld โŠข ( ๐‘ โˆˆ โ„ โ†’ ( ( - ๐‘ โˆˆ โ„ค โˆง 0 < - ๐‘ ) โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) ) )
84 55 83 syl5bi โŠข ( ๐‘ โˆˆ โ„ โ†’ ( - ๐‘ โˆˆ โ„• โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) ) )
85 84 imp โŠข ( ( ๐‘ โˆˆ โ„ โˆง - ๐‘ โˆˆ โ„• ) โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
86 54 85 jaoi โŠข ( ( ๐‘ โˆˆ โ„•0 โˆจ ( ๐‘ โˆˆ โ„ โˆง - ๐‘ โˆˆ โ„• ) ) โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
87 1 86 sylbi โŠข ( ๐‘ โˆˆ โ„ค โ†’ ( ( ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) ) )
88 87 3impib โŠข ( ( ๐‘ โˆˆ โ„ค โˆง ๐ด โˆˆ โ„™ โˆง ๐ต โˆˆ โ„™ ) โ†’ ( ( ๐‘ ยท ๐ด ) = ๐ต โ†’ ๐ด = ๐ต ) )