Proof of Theorem 2mulprm
Step | Hyp | Ref
| Expression |
1 | | zre 12616 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
2 | | 0red 11269 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 0 ∈
ℝ) |
3 | 1, 2 | leloed 11409 |
. . . . 5
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 ↔ (𝐴 < 0 ∨ 𝐴 = 0))) |
4 | | prmnn 16677 |
. . . . . . . . . 10
⊢ ((2
· 𝐴) ∈ ℙ
→ (2 · 𝐴)
∈ ℕ) |
5 | | nnnn0 12533 |
. . . . . . . . . 10
⊢ ((2
· 𝐴) ∈ ℕ
→ (2 · 𝐴)
∈ ℕ0) |
6 | | nn0ge0 12551 |
. . . . . . . . . 10
⊢ ((2
· 𝐴) ∈
ℕ0 → 0 ≤ (2 · 𝐴)) |
7 | | 2pos 12369 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
2 |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℤ → 0 <
2) |
9 | 8 | anim1i 613 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (0 < 2 ∧
𝐴 < 0)) |
10 | 9 | olcd 872 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ((2 < 0 ∧
0 < 𝐴) ∨ (0 < 2
∧ 𝐴 <
0))) |
11 | | 2re 12340 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 2 ∈
ℝ) |
13 | 1 | adantr 479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 𝐴 ∈
ℝ) |
14 | 12, 13 | mul2lt0bi 13136 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ((2 ·
𝐴) < 0 ↔ ((2 < 0
∧ 0 < 𝐴) ∨ (0
< 2 ∧ 𝐴 <
0)))) |
15 | 10, 14 | mpbird 256 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (2 ·
𝐴) < 0) |
16 | 12, 13 | remulcld 11296 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (2 ·
𝐴) ∈
ℝ) |
17 | | 0red 11269 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 0 ∈
ℝ) |
18 | 16, 17 | ltnled 11413 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ((2 ·
𝐴) < 0 ↔ ¬ 0
≤ (2 · 𝐴))) |
19 | 15, 18 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ¬ 0 ≤ (2
· 𝐴)) |
20 | 19 | ex 411 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (𝐴 < 0 → ¬ 0 ≤ (2
· 𝐴))) |
21 | 20 | con2d 134 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (0 ≤
(2 · 𝐴) → ¬
𝐴 < 0)) |
22 | 21 | com12 32 |
. . . . . . . . . 10
⊢ (0 ≤
(2 · 𝐴) →
(𝐴 ∈ ℤ →
¬ 𝐴 <
0)) |
23 | 4, 5, 6, 22 | 4syl 19 |
. . . . . . . . 9
⊢ ((2
· 𝐴) ∈ ℙ
→ (𝐴 ∈ ℤ
→ ¬ 𝐴 <
0)) |
24 | 23 | com12 32 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → ((2
· 𝐴) ∈ ℙ
→ ¬ 𝐴 <
0)) |
25 | 24 | con2d 134 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ → (𝐴 < 0 → ¬ (2 ·
𝐴) ∈
ℙ)) |
26 | 25 | a1dd 50 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 < 0 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
27 | | oveq2 7434 |
. . . . . . . . 9
⊢ (𝐴 = 0 → (2 · 𝐴) = (2 ·
0)) |
28 | | 2t0e0 12435 |
. . . . . . . . 9
⊢ (2
· 0) = 0 |
29 | 27, 28 | eqtrdi 2782 |
. . . . . . . 8
⊢ (𝐴 = 0 → (2 · 𝐴) = 0) |
30 | | 0nprm 16681 |
. . . . . . . . 9
⊢ ¬ 0
∈ ℙ |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 = 0 → ¬ 0 ∈
ℙ) |
32 | 29, 31 | eqneltrd 2846 |
. . . . . . 7
⊢ (𝐴 = 0 → ¬ (2 ·
𝐴) ∈
ℙ) |
33 | 32 | a1i13 27 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 = 0 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
34 | 26, 33 | jaod 857 |
. . . . 5
⊢ (𝐴 ∈ ℤ → ((𝐴 < 0 ∨ 𝐴 = 0) → (¬ 𝐴 = 1 → ¬ (2 · 𝐴) ∈
ℙ))) |
35 | 3, 34 | sylbid 239 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
36 | | 2z 12648 |
. . . . . . 7
⊢ 2 ∈
ℤ |
37 | | uzid 12891 |
. . . . . . 7
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
38 | 36, 37 | ax-mp 5 |
. . . . . 6
⊢ 2 ∈
(ℤ≥‘2) |
39 | 36 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 2 ∈
ℤ) |
40 | | simp1 1133 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 𝐴 ∈ ℤ) |
41 | | df-ne 2931 |
. . . . . . . . 9
⊢ (𝐴 ≠ 1 ↔ ¬ 𝐴 = 1) |
42 | | 1red 11267 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → 1 ∈
ℝ) |
43 | 42, 1 | ltlend 11411 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 ↔ (1 ≤ 𝐴 ∧ 𝐴 ≠ 1))) |
44 | | 1zzd 12647 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℤ → 1 ∈
ℤ) |
45 | | zltp1le 12666 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ 𝐴
∈ ℤ) → (1 < 𝐴 ↔ (1 + 1) ≤ 𝐴)) |
46 | 44, 45 | mpancom 686 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 ↔ (1 + 1) ≤ 𝐴)) |
47 | 46 | biimpd 228 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 → (1 + 1) ≤ 𝐴)) |
48 | | df-2 12329 |
. . . . . . . . . . . . 13
⊢ 2 = (1 +
1) |
49 | 48 | breq1i 5162 |
. . . . . . . . . . . 12
⊢ (2 ≤
𝐴 ↔ (1 + 1) ≤ 𝐴) |
50 | 47, 49 | imbitrrdi 251 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 → 2 ≤ 𝐴)) |
51 | 43, 50 | sylbird 259 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → ((1 ≤
𝐴 ∧ 𝐴 ≠ 1) → 2 ≤ 𝐴)) |
52 | 51 | expdimp 451 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴) → (𝐴 ≠ 1 → 2 ≤ 𝐴)) |
53 | 41, 52 | biimtrrid 242 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴) → (¬ 𝐴 = 1 → 2 ≤ 𝐴)) |
54 | 53 | 3impia 1114 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 2 ≤ 𝐴) |
55 | | eluz2 12882 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤
𝐴)) |
56 | 39, 40, 54, 55 | syl3anbrc 1340 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 𝐴 ∈
(ℤ≥‘2)) |
57 | | nprm 16691 |
. . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝐴 ∈ (ℤ≥‘2))
→ ¬ (2 · 𝐴)
∈ ℙ) |
58 | 38, 56, 57 | sylancr 585 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → ¬ (2 ·
𝐴) ∈
ℙ) |
59 | 58 | 3exp 1116 |
. . . 4
⊢ (𝐴 ∈ ℤ → (1 ≤
𝐴 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
60 | | zle0orge1 12629 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 ∨ 1 ≤ 𝐴)) |
61 | 35, 59, 60 | mpjaod 858 |
. . 3
⊢ (𝐴 ∈ ℤ → (¬
𝐴 = 1 → ¬ (2
· 𝐴) ∈
ℙ)) |
62 | 61 | con4d 115 |
. 2
⊢ (𝐴 ∈ ℤ → ((2
· 𝐴) ∈ ℙ
→ 𝐴 =
1)) |
63 | | oveq2 7434 |
. . . 4
⊢ (𝐴 = 1 → (2 · 𝐴) = (2 ·
1)) |
64 | | 2t1e2 12429 |
. . . 4
⊢ (2
· 1) = 2 |
65 | 63, 64 | eqtrdi 2782 |
. . 3
⊢ (𝐴 = 1 → (2 · 𝐴) = 2) |
66 | | 2prm 16695 |
. . 3
⊢ 2 ∈
ℙ |
67 | 65, 66 | eqeltrdi 2834 |
. 2
⊢ (𝐴 = 1 → (2 · 𝐴) ∈
ℙ) |
68 | 62, 67 | impbid1 224 |
1
⊢ (𝐴 ∈ ℤ → ((2
· 𝐴) ∈ ℙ
↔ 𝐴 =
1)) |