Proof of Theorem 2mulprm
Step | Hyp | Ref
| Expression |
1 | | zre 12614 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
2 | | 0red 11261 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 0 ∈
ℝ) |
3 | 1, 2 | leloed 11401 |
. . . . 5
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 ↔ (𝐴 < 0 ∨ 𝐴 = 0))) |
4 | | prmnn 16707 |
. . . . . . . . . 10
⊢ ((2
· 𝐴) ∈ ℙ
→ (2 · 𝐴)
∈ ℕ) |
5 | | nnnn0 12530 |
. . . . . . . . . 10
⊢ ((2
· 𝐴) ∈ ℕ
→ (2 · 𝐴)
∈ ℕ0) |
6 | | nn0ge0 12548 |
. . . . . . . . . 10
⊢ ((2
· 𝐴) ∈
ℕ0 → 0 ≤ (2 · 𝐴)) |
7 | | 2pos 12366 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
2 |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℤ → 0 <
2) |
9 | 8 | anim1i 615 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (0 < 2 ∧
𝐴 < 0)) |
10 | 9 | olcd 874 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ((2 < 0 ∧
0 < 𝐴) ∨ (0 < 2
∧ 𝐴 <
0))) |
11 | | 2re 12337 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 2 ∈
ℝ) |
13 | 1 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 𝐴 ∈
ℝ) |
14 | 12, 13 | mul2lt0bi 13138 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ((2 ·
𝐴) < 0 ↔ ((2 < 0
∧ 0 < 𝐴) ∨ (0
< 2 ∧ 𝐴 <
0)))) |
15 | 10, 14 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (2 ·
𝐴) < 0) |
16 | 12, 13 | remulcld 11288 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (2 ·
𝐴) ∈
ℝ) |
17 | | 0red 11261 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 0 ∈
ℝ) |
18 | 16, 17 | ltnled 11405 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ((2 ·
𝐴) < 0 ↔ ¬ 0
≤ (2 · 𝐴))) |
19 | 15, 18 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ¬ 0 ≤ (2
· 𝐴)) |
20 | 19 | ex 412 |
. . . . . . . . . . . 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 7438 |
. . . . . . . . 9
⊢ (𝐴 = 0 → (2 · 𝐴) = (2 ·
0)) |
28 | | 2t0e0 12432 |
. . . . . . . . 9
⊢ (2
· 0) = 0 |
29 | 27, 28 | eqtrdi 2790 |
. . . . . . . 8
⊢ (𝐴 = 0 → (2 · 𝐴) = 0) |
30 | | 0nprm 16711 |
. . . . . . . . 9
⊢ ¬ 0
∈ ℙ |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 = 0 → ¬ 0 ∈
ℙ) |
32 | 29, 31 | eqneltrd 2858 |
. . . . . . 7
⊢ (𝐴 = 0 → ¬ (2 ·
𝐴) ∈
ℙ) |
33 | 32 | a1i13 27 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 = 0 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
34 | 26, 33 | jaod 859 |
. . . . 5
⊢ (𝐴 ∈ ℤ → ((𝐴 < 0 ∨ 𝐴 = 0) → (¬ 𝐴 = 1 → ¬ (2 · 𝐴) ∈
ℙ))) |
35 | 3, 34 | sylbid 240 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
36 | | 2z 12646 |
. . . . . . 7
⊢ 2 ∈
ℤ |
37 | | uzid 12890 |
. . . . . . 7
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
38 | 36, 37 | ax-mp 5 |
. . . . . 6
⊢ 2 ∈
(ℤ≥‘2) |
39 | 36 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 2 ∈
ℤ) |
40 | | simp1 1135 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 𝐴 ∈ ℤ) |
41 | | df-ne 2938 |
. . . . . . . . 9
⊢ (𝐴 ≠ 1 ↔ ¬ 𝐴 = 1) |
42 | | 1red 11259 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → 1 ∈
ℝ) |
43 | 42, 1 | ltlend 11403 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 ↔ (1 ≤ 𝐴 ∧ 𝐴 ≠ 1))) |
44 | | 1zzd 12645 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℤ → 1 ∈
ℤ) |
45 | | zltp1le 12664 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ 𝐴
∈ ℤ) → (1 < 𝐴 ↔ (1 + 1) ≤ 𝐴)) |
46 | 44, 45 | mpancom 688 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 ↔ (1 + 1) ≤ 𝐴)) |
47 | 46 | biimpd 229 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 → (1 + 1) ≤ 𝐴)) |
48 | | df-2 12326 |
. . . . . . . . . . . . 13
⊢ 2 = (1 +
1) |
49 | 48 | breq1i 5154 |
. . . . . . . . . . . 12
⊢ (2 ≤
𝐴 ↔ (1 + 1) ≤ 𝐴) |
50 | 47, 49 | imbitrrdi 252 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 → 2 ≤ 𝐴)) |
51 | 43, 50 | sylbird 260 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → ((1 ≤
𝐴 ∧ 𝐴 ≠ 1) → 2 ≤ 𝐴)) |
52 | 51 | expdimp 452 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴) → (𝐴 ≠ 1 → 2 ≤ 𝐴)) |
53 | 41, 52 | biimtrrid 243 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴) → (¬ 𝐴 = 1 → 2 ≤ 𝐴)) |
54 | 53 | 3impia 1116 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 2 ≤ 𝐴) |
55 | | eluz2 12881 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤
𝐴)) |
56 | 39, 40, 54, 55 | syl3anbrc 1342 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 𝐴 ∈
(ℤ≥‘2)) |
57 | | nprm 16721 |
. . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝐴 ∈ (ℤ≥‘2))
→ ¬ (2 · 𝐴)
∈ ℙ) |
58 | 38, 56, 57 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → ¬ (2 ·
𝐴) ∈
ℙ) |
59 | 58 | 3exp 1118 |
. . . 4
⊢ (𝐴 ∈ ℤ → (1 ≤
𝐴 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
60 | | zle0orge1 12627 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 ∨ 1 ≤ 𝐴)) |
61 | 35, 59, 60 | mpjaod 860 |
. . 3
⊢ (𝐴 ∈ ℤ → (¬
𝐴 = 1 → ¬ (2
· 𝐴) ∈
ℙ)) |
62 | 61 | con4d 115 |
. 2
⊢ (𝐴 ∈ ℤ → ((2
· 𝐴) ∈ ℙ
→ 𝐴 =
1)) |
63 | | oveq2 7438 |
. . . 4
⊢ (𝐴 = 1 → (2 · 𝐴) = (2 ·
1)) |
64 | | 2t1e2 12426 |
. . . 4
⊢ (2
· 1) = 2 |
65 | 63, 64 | eqtrdi 2790 |
. . 3
⊢ (𝐴 = 1 → (2 · 𝐴) = 2) |
66 | | 2prm 16725 |
. . 3
⊢ 2 ∈
ℙ |
67 | 65, 66 | eqeltrdi 2846 |
. 2
⊢ (𝐴 = 1 → (2 · 𝐴) ∈
ℙ) |
68 | 62, 67 | impbid1 225 |
1
⊢ (𝐴 ∈ ℤ → ((2
· 𝐴) ∈ ℙ
↔ 𝐴 =
1)) |