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 ⊢ ( ( 𝑍 ∈ ℤ ∧ 𝐴 ∈ ℙ ∧ 𝐵 ∈ ℙ ) → ( ( 𝑍 · 𝐴 ) = 𝐵 → 𝐴 = 𝐵 ) )