Proof of Theorem 2mulprm
Step | Hyp | Ref
| Expression |
1 | | zre 12333 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
2 | | 0red 10988 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 0 ∈
ℝ) |
3 | 1, 2 | leloed 11128 |
. . . . 5
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 ↔ (𝐴 < 0 ∨ 𝐴 = 0))) |
4 | | prmnn 16389 |
. . . . . . . . . 10
⊢ ((2
· 𝐴) ∈ ℙ
→ (2 · 𝐴)
∈ ℕ) |
5 | | nnnn0 12250 |
. . . . . . . . . 10
⊢ ((2
· 𝐴) ∈ ℕ
→ (2 · 𝐴)
∈ ℕ0) |
6 | | nn0ge0 12268 |
. . . . . . . . . . 11
⊢ ((2
· 𝐴) ∈
ℕ0 → 0 ≤ (2 · 𝐴)) |
7 | | 2pos 12086 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 <
2 |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℤ → 0 <
2) |
9 | 8 | anim1i 615 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (0 < 2 ∧
𝐴 < 0)) |
10 | 9 | olcd 871 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ((2 < 0 ∧
0 < 𝐴) ∨ (0 < 2
∧ 𝐴 <
0))) |
11 | | 2re 12057 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 2 ∈
ℝ) |
13 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 𝐴 ∈
ℝ) |
14 | 12, 13 | mul2lt0bi 12846 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ((2 ·
𝐴) < 0 ↔ ((2 < 0
∧ 0 < 𝐴) ∨ (0
< 2 ∧ 𝐴 <
0)))) |
15 | 10, 14 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (2 ·
𝐴) < 0) |
16 | 12, 13 | remulcld 11015 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (2 ·
𝐴) ∈
ℝ) |
17 | | 0red 10988 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 0 ∈
ℝ) |
18 | 16, 17 | ltnled 11132 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ((2 ·
𝐴) < 0 ↔ ¬ 0
≤ (2 · 𝐴))) |
19 | 15, 18 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ¬ 0 ≤ (2
· 𝐴)) |
20 | 19 | ex 413 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℤ → (𝐴 < 0 → ¬ 0 ≤ (2
· 𝐴))) |
21 | 20 | con2d 134 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (0 ≤
(2 · 𝐴) → ¬
𝐴 < 0)) |
22 | 21 | com12 32 |
. . . . . . . . . . 11
⊢ (0 ≤
(2 · 𝐴) →
(𝐴 ∈ ℤ →
¬ 𝐴 <
0)) |
23 | 6, 22 | syl 17 |
. . . . . . . . . 10
⊢ ((2
· 𝐴) ∈
ℕ0 → (𝐴 ∈ ℤ → ¬ 𝐴 < 0)) |
24 | 4, 5, 23 | 3syl 18 |
. . . . . . . . 9
⊢ ((2
· 𝐴) ∈ ℙ
→ (𝐴 ∈ ℤ
→ ¬ 𝐴 <
0)) |
25 | 24 | com12 32 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → ((2
· 𝐴) ∈ ℙ
→ ¬ 𝐴 <
0)) |
26 | 25 | con2d 134 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ → (𝐴 < 0 → ¬ (2 ·
𝐴) ∈
ℙ)) |
27 | 26 | a1dd 50 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 < 0 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
28 | | oveq2 7275 |
. . . . . . . . 9
⊢ (𝐴 = 0 → (2 · 𝐴) = (2 ·
0)) |
29 | | 2t0e0 12152 |
. . . . . . . . 9
⊢ (2
· 0) = 0 |
30 | 28, 29 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝐴 = 0 → (2 · 𝐴) = 0) |
31 | | 0nprm 16393 |
. . . . . . . . 9
⊢ ¬ 0
∈ ℙ |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 = 0 → ¬ 0 ∈
ℙ) |
33 | 30, 32 | eqneltrd 2858 |
. . . . . . 7
⊢ (𝐴 = 0 → ¬ (2 ·
𝐴) ∈
ℙ) |
34 | 33 | a1i13 27 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 = 0 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
35 | 27, 34 | jaod 856 |
. . . . 5
⊢ (𝐴 ∈ ℤ → ((𝐴 < 0 ∨ 𝐴 = 0) → (¬ 𝐴 = 1 → ¬ (2 · 𝐴) ∈
ℙ))) |
36 | 3, 35 | sylbid 239 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
37 | | 2z 12362 |
. . . . . . 7
⊢ 2 ∈
ℤ |
38 | | uzid 12607 |
. . . . . . 7
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
39 | 37, 38 | ax-mp 5 |
. . . . . 6
⊢ 2 ∈
(ℤ≥‘2) |
40 | 37 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 2 ∈
ℤ) |
41 | | simp1 1135 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 𝐴 ∈ ℤ) |
42 | | df-ne 2944 |
. . . . . . . . 9
⊢ (𝐴 ≠ 1 ↔ ¬ 𝐴 = 1) |
43 | | 1red 10986 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → 1 ∈
ℝ) |
44 | 43, 1 | ltlend 11130 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 ↔ (1 ≤ 𝐴 ∧ 𝐴 ≠ 1))) |
45 | | 1zzd 12361 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℤ → 1 ∈
ℤ) |
46 | | zltp1le 12380 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ 𝐴
∈ ℤ) → (1 < 𝐴 ↔ (1 + 1) ≤ 𝐴)) |
47 | 45, 46 | mpancom 685 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 ↔ (1 + 1) ≤ 𝐴)) |
48 | 47 | biimpd 228 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 → (1 + 1) ≤ 𝐴)) |
49 | | df-2 12046 |
. . . . . . . . . . . . 13
⊢ 2 = (1 +
1) |
50 | 49 | breq1i 5080 |
. . . . . . . . . . . 12
⊢ (2 ≤
𝐴 ↔ (1 + 1) ≤ 𝐴) |
51 | 48, 50 | syl6ibr 251 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 → 2 ≤ 𝐴)) |
52 | 44, 51 | sylbird 259 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → ((1 ≤
𝐴 ∧ 𝐴 ≠ 1) → 2 ≤ 𝐴)) |
53 | 52 | expdimp 453 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴) → (𝐴 ≠ 1 → 2 ≤ 𝐴)) |
54 | 42, 53 | syl5bir 242 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴) → (¬ 𝐴 = 1 → 2 ≤ 𝐴)) |
55 | 54 | 3impia 1116 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 2 ≤ 𝐴) |
56 | | eluz2 12598 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤
𝐴)) |
57 | 40, 41, 55, 56 | syl3anbrc 1342 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 𝐴 ∈
(ℤ≥‘2)) |
58 | | nprm 16403 |
. . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝐴 ∈ (ℤ≥‘2))
→ ¬ (2 · 𝐴)
∈ ℙ) |
59 | 39, 57, 58 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → ¬ (2 ·
𝐴) ∈
ℙ) |
60 | 59 | 3exp 1118 |
. . . 4
⊢ (𝐴 ∈ ℤ → (1 ≤
𝐴 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
61 | | zle0orge1 12346 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 ∨ 1 ≤ 𝐴)) |
62 | 36, 60, 61 | mpjaod 857 |
. . 3
⊢ (𝐴 ∈ ℤ → (¬
𝐴 = 1 → ¬ (2
· 𝐴) ∈
ℙ)) |
63 | 62 | con4d 115 |
. 2
⊢ (𝐴 ∈ ℤ → ((2
· 𝐴) ∈ ℙ
→ 𝐴 =
1)) |
64 | | oveq2 7275 |
. . . 4
⊢ (𝐴 = 1 → (2 · 𝐴) = (2 ·
1)) |
65 | | 2t1e2 12146 |
. . . 4
⊢ (2
· 1) = 2 |
66 | 64, 65 | eqtrdi 2794 |
. . 3
⊢ (𝐴 = 1 → (2 · 𝐴) = 2) |
67 | | 2prm 16407 |
. . 3
⊢ 2 ∈
ℙ |
68 | 66, 67 | eqeltrdi 2847 |
. 2
⊢ (𝐴 = 1 → (2 · 𝐴) ∈
ℙ) |
69 | 63, 68 | impbid1 224 |
1
⊢ (𝐴 ∈ ℤ → ((2
· 𝐴) ∈ ℙ
↔ 𝐴 =
1)) |