Step | Hyp | Ref
| Expression |
1 | | dvdsnprmd.d |
. 2
⊢ (𝜑 → 𝐴 ∥ 𝑁) |
2 | | dvdszrcl 15968 |
. . . 4
⊢ (𝐴 ∥ 𝑁 → (𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
3 | | divides 15965 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝐴) = 𝑁)) |
4 | 1, 2, 3 | 3syl 18 |
. . 3
⊢ (𝜑 → (𝐴 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝐴) = 𝑁)) |
5 | | 2z 12352 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → 2 ∈ ℤ) |
7 | | simplr 766 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → 𝑘 ∈ ℤ) |
8 | | dvdsnprmd.l |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝑁) |
9 | 8 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝐴 < 𝑁) |
10 | 9 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → 𝐴 < 𝑁) |
11 | | breq2 5078 |
. . . . . . . . . . 11
⊢ ((𝑘 · 𝐴) = 𝑁 → (𝐴 < (𝑘 · 𝐴) ↔ 𝐴 < 𝑁)) |
12 | 11 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → (𝐴 < (𝑘 · 𝐴) ↔ 𝐴 < 𝑁)) |
13 | 10, 12 | mpbird 256 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → 𝐴 < (𝑘 · 𝐴)) |
14 | | dvdsnprmd.g |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 < 𝐴) |
15 | | zre 12323 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
16 | 15 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ 1 <
𝐴 ∧ 𝑘 ∈ ℤ) → 𝐴 ∈ ℝ) |
17 | | zre 12323 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℝ) |
18 | 17 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ 1 <
𝐴 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ) |
19 | | 0lt1 11497 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
1 |
20 | | 0red 10978 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ ℤ → 0 ∈
ℝ) |
21 | | 1red 10976 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ ℤ → 1 ∈
ℝ) |
22 | | lttr 11051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < 1 ∧ 1
< 𝐴) → 0 < 𝐴)) |
23 | 20, 21, 15, 22 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ ℤ → ((0 <
1 ∧ 1 < 𝐴) → 0
< 𝐴)) |
24 | 19, 23 | mpani 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 → 0 < 𝐴)) |
25 | 24 | imp 407 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℤ ∧ 1 <
𝐴) → 0 < 𝐴) |
26 | 25 | 3adant3 1131 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ 1 <
𝐴 ∧ 𝑘 ∈ ℤ) → 0 < 𝐴) |
27 | 16, 18, 26 | 3jca 1127 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 1 <
𝐴 ∧ 𝑘 ∈ ℤ) → (𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴)) |
28 | 27 | 3exp 1118 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 → (𝑘 ∈ ℤ → (𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 <
𝐴)))) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 <
𝐴 → (𝑘 ∈ ℤ → (𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 <
𝐴)))) |
30 | 1, 2, 29 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 < 𝐴 → (𝑘 ∈ ℤ → (𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴)))) |
31 | 14, 30 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ ℤ → (𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴))) |
32 | 31 | imp 407 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴)) |
33 | 32 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → (𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴)) |
34 | | ltmulgt12 11836 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 <
𝐴) → (1 < 𝑘 ↔ 𝐴 < (𝑘 · 𝐴))) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → (1 < 𝑘 ↔ 𝐴 < (𝑘 · 𝐴))) |
36 | 13, 35 | mpbird 256 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → 1 < 𝑘) |
37 | | df-2 12036 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
38 | 37 | breq1i 5081 |
. . . . . . . . 9
⊢ (2 ≤
𝑘 ↔ (1 + 1) ≤ 𝑘) |
39 | | 1zzd 12351 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → 1 ∈
ℤ) |
40 | | zltp1le 12370 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℤ ∧ 𝑘
∈ ℤ) → (1 < 𝑘 ↔ (1 + 1) ≤ 𝑘)) |
41 | 39, 40 | mpancom 685 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℤ → (1 <
𝑘 ↔ (1 + 1) ≤ 𝑘)) |
42 | 41 | bicomd 222 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℤ → ((1 + 1)
≤ 𝑘 ↔ 1 < 𝑘)) |
43 | 42 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → ((1 + 1) ≤ 𝑘 ↔ 1 < 𝑘)) |
44 | 43 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → ((1 + 1) ≤ 𝑘 ↔ 1 < 𝑘)) |
45 | 38, 44 | bitrid 282 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → (2 ≤ 𝑘 ↔ 1 < 𝑘)) |
46 | 36, 45 | mpbird 256 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → 2 ≤ 𝑘) |
47 | | eluz2 12588 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 2 ≤
𝑘)) |
48 | 6, 7, 46, 47 | syl3anbrc 1342 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → 𝑘 ∈
(ℤ≥‘2)) |
49 | 5 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 1 <
𝐴) → 2 ∈
ℤ) |
50 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 1 <
𝐴) → 𝐴 ∈ ℤ) |
51 | | 1zzd 12351 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℤ → 1 ∈
ℤ) |
52 | | zltp1le 12370 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℤ ∧ 𝐴
∈ ℤ) → (1 < 𝐴 ↔ (1 + 1) ≤ 𝐴)) |
53 | 51, 52 | mpancom 685 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 ↔ (1 + 1) ≤ 𝐴)) |
54 | 53 | biimpa 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 1 <
𝐴) → (1 + 1) ≤
𝐴) |
55 | 37 | breq1i 5081 |
. . . . . . . . . . . . . . 15
⊢ (2 ≤
𝐴 ↔ (1 + 1) ≤ 𝐴) |
56 | 54, 55 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 1 <
𝐴) → 2 ≤ 𝐴) |
57 | 49, 50, 56 | 3jca 1127 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 1 <
𝐴) → (2 ∈ ℤ
∧ 𝐴 ∈ ℤ
∧ 2 ≤ 𝐴)) |
58 | 57 | ex 413 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 → (2 ∈ ℤ
∧ 𝐴 ∈ ℤ
∧ 2 ≤ 𝐴))) |
59 | 58 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 <
𝐴 → (2 ∈ ℤ
∧ 𝐴 ∈ ℤ
∧ 2 ≤ 𝐴))) |
60 | 1, 2, 59 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (1 < 𝐴 → (2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤
𝐴))) |
61 | 14, 60 | mpd 15 |
. . . . . . . . 9
⊢ (𝜑 → (2 ∈ ℤ ∧
𝐴 ∈ ℤ ∧ 2
≤ 𝐴)) |
62 | | eluz2 12588 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤
𝐴)) |
63 | 61, 62 | sylibr 233 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘2)) |
64 | 63 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝐴 ∈
(ℤ≥‘2)) |
65 | 64 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → 𝐴 ∈
(ℤ≥‘2)) |
66 | | nprm 16393 |
. . . . . 6
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ 𝐴 ∈ (ℤ≥‘2))
→ ¬ (𝑘 ·
𝐴) ∈
ℙ) |
67 | 48, 65, 66 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → ¬ (𝑘 · 𝐴) ∈ ℙ) |
68 | | eleq1 2826 |
. . . . . . 7
⊢ ((𝑘 · 𝐴) = 𝑁 → ((𝑘 · 𝐴) ∈ ℙ ↔ 𝑁 ∈ ℙ)) |
69 | 68 | notbid 318 |
. . . . . 6
⊢ ((𝑘 · 𝐴) = 𝑁 → (¬ (𝑘 · 𝐴) ∈ ℙ ↔ ¬ 𝑁 ∈
ℙ)) |
70 | 69 | adantl 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → (¬ (𝑘 · 𝐴) ∈ ℙ ↔ ¬ 𝑁 ∈
ℙ)) |
71 | 67, 70 | mpbid 231 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ (𝑘 · 𝐴) = 𝑁) → ¬ 𝑁 ∈ ℙ) |
72 | 71 | rexlimdva2 3216 |
. . 3
⊢ (𝜑 → (∃𝑘 ∈ ℤ (𝑘 · 𝐴) = 𝑁 → ¬ 𝑁 ∈ ℙ)) |
73 | 4, 72 | sylbid 239 |
. 2
⊢ (𝜑 → (𝐴 ∥ 𝑁 → ¬ 𝑁 ∈ ℙ)) |
74 | 1, 73 | mpd 15 |
1
⊢ (𝜑 → ¬ 𝑁 ∈ ℙ) |