Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Basic algebraic structures (extension)
Auxiliary theorems
ztprmneprm
Next ⟩
2t6m3t4e0
Metamath Proof Explorer
Ascii
Unicode
Theorem
ztprmneprm
Description:
A prime is not an integer multiple of another prime.
(Contributed by
AV
, 23-May-2019)
Ref
Expression
Assertion
ztprmneprm
⊢
Z
∈
ℤ
∧
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
Proof
Step
Hyp
Ref
Expression
1
elznn0nn
⊢
Z
∈
ℤ
↔
Z
∈
ℕ
0
∨
Z
∈
ℝ
∧
−
Z
∈
ℕ
2
elnn0
⊢
Z
∈
ℕ
0
↔
Z
∈
ℕ
∨
Z
=
0
3
elnn1uz2
⊢
Z
∈
ℕ
↔
Z
=
1
∨
Z
∈
ℤ
≥
2
4
oveq1
⊢
Z
=
1
→
Z
A
=
1
A
5
4
adantr
⊢
Z
=
1
∧
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
1
A
6
5
eqeq1d
⊢
Z
=
1
∧
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
↔
1
A
=
B
7
prmz
⊢
A
∈
ℙ
→
A
∈
ℤ
8
7
zcnd
⊢
A
∈
ℙ
→
A
∈
ℂ
9
8
mulid2d
⊢
A
∈
ℙ
→
1
A
=
A
10
9
adantr
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
1
A
=
A
11
10
eqeq1d
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
1
A
=
B
↔
A
=
B
12
11
biimpd
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
1
A
=
B
→
A
=
B
13
12
adantl
⊢
Z
=
1
∧
A
∈
ℙ
∧
B
∈
ℙ
→
1
A
=
B
→
A
=
B
14
6
13
sylbid
⊢
Z
=
1
∧
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
15
14
ex
⊢
Z
=
1
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
16
prmuz2
⊢
A
∈
ℙ
→
A
∈
ℤ
≥
2
17
16
adantr
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
A
∈
ℤ
≥
2
18
nprm
⊢
Z
∈
ℤ
≥
2
∧
A
∈
ℤ
≥
2
→
¬
Z
A
∈
ℙ
19
17
18
sylan2
⊢
Z
∈
ℤ
≥
2
∧
A
∈
ℙ
∧
B
∈
ℙ
→
¬
Z
A
∈
ℙ
20
eleq1
⊢
Z
A
=
B
→
Z
A
∈
ℙ
↔
B
∈
ℙ
21
20
notbid
⊢
Z
A
=
B
→
¬
Z
A
∈
ℙ
↔
¬
B
∈
ℙ
22
pm2.24
⊢
B
∈
ℙ
→
¬
B
∈
ℙ
→
A
=
B
23
22
adantl
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
¬
B
∈
ℙ
→
A
=
B
24
23
adantl
⊢
Z
∈
ℤ
≥
2
∧
A
∈
ℙ
∧
B
∈
ℙ
→
¬
B
∈
ℙ
→
A
=
B
25
24
com12
⊢
¬
B
∈
ℙ
→
Z
∈
ℤ
≥
2
∧
A
∈
ℙ
∧
B
∈
ℙ
→
A
=
B
26
21
25
syl6bi
⊢
Z
A
=
B
→
¬
Z
A
∈
ℙ
→
Z
∈
ℤ
≥
2
∧
A
∈
ℙ
∧
B
∈
ℙ
→
A
=
B
27
26
com3l
⊢
¬
Z
A
∈
ℙ
→
Z
∈
ℤ
≥
2
∧
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
28
19
27
mpcom
⊢
Z
∈
ℤ
≥
2
∧
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
29
28
ex
⊢
Z
∈
ℤ
≥
2
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
30
15
29
jaoi
⊢
Z
=
1
∨
Z
∈
ℤ
≥
2
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
31
3
30
sylbi
⊢
Z
∈
ℕ
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
32
oveq1
⊢
Z
=
0
→
Z
A
=
0
⋅
A
33
32
eqeq1d
⊢
Z
=
0
→
Z
A
=
B
↔
0
⋅
A
=
B
34
prmnn
⊢
A
∈
ℙ
→
A
∈
ℕ
35
34
nnred
⊢
A
∈
ℙ
→
A
∈
ℝ
36
mul02lem2
⊢
A
∈
ℝ
→
0
⋅
A
=
0
37
35
36
syl
⊢
A
∈
ℙ
→
0
⋅
A
=
0
38
37
adantr
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
0
⋅
A
=
0
39
38
eqeq1d
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
0
⋅
A
=
B
↔
0
=
B
40
prmnn
⊢
B
∈
ℙ
→
B
∈
ℕ
41
elnnne0
⊢
B
∈
ℕ
↔
B
∈
ℕ
0
∧
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
∈
ℕ
0
∧
B
≠
0
→
0
=
B
→
A
=
B
46
41
45
sylbi
⊢
B
∈
ℕ
→
0
=
B
→
A
=
B
47
40
46
syl
⊢
B
∈
ℙ
→
0
=
B
→
A
=
B
48
47
adantl
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
0
=
B
→
A
=
B
49
39
48
sylbid
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
0
⋅
A
=
B
→
A
=
B
50
49
com12
⊢
0
⋅
A
=
B
→
A
∈
ℙ
∧
B
∈
ℙ
→
A
=
B
51
33
50
syl6bi
⊢
Z
=
0
→
Z
A
=
B
→
A
∈
ℙ
∧
B
∈
ℙ
→
A
=
B
52
51
com23
⊢
Z
=
0
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
53
31
52
jaoi
⊢
Z
∈
ℕ
∨
Z
=
0
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
54
2
53
sylbi
⊢
Z
∈
ℕ
0
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
55
elnnz
⊢
−
Z
∈
ℕ
↔
−
Z
∈
ℤ
∧
0
<
−
Z
56
lt0neg1
⊢
Z
∈
ℝ
→
Z
<
0
↔
0
<
−
Z
57
34
nngt0d
⊢
A
∈
ℙ
→
0
<
A
58
57
adantr
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
0
<
A
59
simpr
⊢
Z
∈
ℝ
∧
Z
<
0
→
Z
<
0
60
58
59
anim12ci
⊢
A
∈
ℙ
∧
B
∈
ℙ
∧
Z
∈
ℝ
∧
Z
<
0
→
Z
<
0
∧
0
<
A
61
60
orcd
⊢
A
∈
ℙ
∧
B
∈
ℙ
∧
Z
∈
ℝ
∧
Z
<
0
→
Z
<
0
∧
0
<
A
∨
0
<
Z
∧
A
<
0
62
simprl
⊢
A
∈
ℙ
∧
B
∈
ℙ
∧
Z
∈
ℝ
∧
Z
<
0
→
Z
∈
ℝ
63
35
adantr
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
A
∈
ℝ
64
63
adantr
⊢
A
∈
ℙ
∧
B
∈
ℙ
∧
Z
∈
ℝ
∧
Z
<
0
→
A
∈
ℝ
65
62
64
mul2lt0bi
⊢
A
∈
ℙ
∧
B
∈
ℙ
∧
Z
∈
ℝ
∧
Z
<
0
→
Z
A
<
0
↔
Z
<
0
∧
0
<
A
∨
0
<
Z
∧
A
<
0
66
61
65
mpbird
⊢
A
∈
ℙ
∧
B
∈
ℙ
∧
Z
∈
ℝ
∧
Z
<
0
→
Z
A
<
0
67
66
ex
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
Z
∈
ℝ
∧
Z
<
0
→
Z
A
<
0
68
breq1
⊢
Z
A
=
B
→
Z
A
<
0
↔
B
<
0
69
68
adantl
⊢
A
∈
ℙ
∧
B
∈
ℙ
∧
Z
A
=
B
→
Z
A
<
0
↔
B
<
0
70
nnnn0
⊢
B
∈
ℕ
→
B
∈
ℕ
0
71
nn0nlt0
⊢
B
∈
ℕ
0
→
¬
B
<
0
72
71
pm2.21d
⊢
B
∈
ℕ
0
→
B
<
0
→
A
=
B
73
70
72
syl
⊢
B
∈
ℕ
→
B
<
0
→
A
=
B
74
40
73
syl
⊢
B
∈
ℙ
→
B
<
0
→
A
=
B
75
74
adantl
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
B
<
0
→
A
=
B
76
75
adantr
⊢
A
∈
ℙ
∧
B
∈
ℙ
∧
Z
A
=
B
→
B
<
0
→
A
=
B
77
69
76
sylbid
⊢
A
∈
ℙ
∧
B
∈
ℙ
∧
Z
A
=
B
→
Z
A
<
0
→
A
=
B
78
77
ex
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
Z
A
<
0
→
A
=
B
79
78
com23
⊢
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
<
0
→
Z
A
=
B
→
A
=
B
80
67
79
syldc
⊢
Z
∈
ℝ
∧
Z
<
0
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
81
80
ex
⊢
Z
∈
ℝ
→
Z
<
0
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
82
56
81
sylbird
⊢
Z
∈
ℝ
→
0
<
−
Z
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
83
82
adantld
⊢
Z
∈
ℝ
→
−
Z
∈
ℤ
∧
0
<
−
Z
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
84
55
83
syl5bi
⊢
Z
∈
ℝ
→
−
Z
∈
ℕ
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
85
84
imp
⊢
Z
∈
ℝ
∧
−
Z
∈
ℕ
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
86
54
85
jaoi
⊢
Z
∈
ℕ
0
∨
Z
∈
ℝ
∧
−
Z
∈
ℕ
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
87
1
86
sylbi
⊢
Z
∈
ℤ
→
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B
88
87
3impib
⊢
Z
∈
ℤ
∧
A
∈
ℙ
∧
B
∈
ℙ
→
Z
A
=
B
→
A
=
B