Proof of Theorem 2mulprm
| Step | Hyp | Ref
| Expression |
| 1 | | zre 12617 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
| 2 | | 0red 11264 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 0 ∈
ℝ) |
| 3 | 1, 2 | leloed 11404 |
. . . . 5
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 ↔ (𝐴 < 0 ∨ 𝐴 = 0))) |
| 4 | | prmnn 16711 |
. . . . . . . . . 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 615 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (0 < 2 ∧
𝐴 < 0)) |
| 10 | 9 | olcd 875 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ((2 < 0 ∧
0 < 𝐴) ∨ (0 < 2
∧ 𝐴 <
0))) |
| 11 | | 2re 12340 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
| 12 | 11 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 2 ∈
ℝ) |
| 13 | 1 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 𝐴 ∈
ℝ) |
| 14 | 12, 13 | mul2lt0bi 13141 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → ((2 ·
𝐴) < 0 ↔ ((2 < 0
∧ 0 < 𝐴) ∨ (0
< 2 ∧ 𝐴 <
0)))) |
| 15 | 10, 14 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (2 ·
𝐴) < 0) |
| 16 | 12, 13 | remulcld 11291 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → (2 ·
𝐴) ∈
ℝ) |
| 17 | | 0red 11264 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 0) → 0 ∈
ℝ) |
| 18 | 16, 17 | ltnled 11408 |
. . . . . . . . . . . . . 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 7439 |
. . . . . . . . 9
⊢ (𝐴 = 0 → (2 · 𝐴) = (2 ·
0)) |
| 28 | | 2t0e0 12435 |
. . . . . . . . 9
⊢ (2
· 0) = 0 |
| 29 | 27, 28 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝐴 = 0 → (2 · 𝐴) = 0) |
| 30 | | 0nprm 16715 |
. . . . . . . . 9
⊢ ¬ 0
∈ ℙ |
| 31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 = 0 → ¬ 0 ∈
ℙ) |
| 32 | 29, 31 | eqneltrd 2861 |
. . . . . . 7
⊢ (𝐴 = 0 → ¬ (2 ·
𝐴) ∈
ℙ) |
| 33 | 32 | a1i13 27 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝐴 = 0 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
| 34 | 26, 33 | jaod 860 |
. . . . 5
⊢ (𝐴 ∈ ℤ → ((𝐴 < 0 ∨ 𝐴 = 0) → (¬ 𝐴 = 1 → ¬ (2 · 𝐴) ∈
ℙ))) |
| 35 | 3, 34 | sylbid 240 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
| 36 | | 2z 12649 |
. . . . . . 7
⊢ 2 ∈
ℤ |
| 37 | | uzid 12893 |
. . . . . . 7
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
| 38 | 36, 37 | ax-mp 5 |
. . . . . 6
⊢ 2 ∈
(ℤ≥‘2) |
| 39 | 36 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 2 ∈
ℤ) |
| 40 | | simp1 1137 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 𝐴 ∈ ℤ) |
| 41 | | df-ne 2941 |
. . . . . . . . 9
⊢ (𝐴 ≠ 1 ↔ ¬ 𝐴 = 1) |
| 42 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → 1 ∈
ℝ) |
| 43 | 42, 1 | ltlend 11406 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (1 <
𝐴 ↔ (1 ≤ 𝐴 ∧ 𝐴 ≠ 1))) |
| 44 | | 1zzd 12648 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℤ → 1 ∈
ℤ) |
| 45 | | zltp1le 12667 |
. . . . . . . . . . . . . 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 12329 |
. . . . . . . . . . . . 13
⊢ 2 = (1 +
1) |
| 49 | 48 | breq1i 5150 |
. . . . . . . . . . . 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 1118 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 2 ≤ 𝐴) |
| 55 | | eluz2 12884 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤
𝐴)) |
| 56 | 39, 40, 54, 55 | syl3anbrc 1344 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → 𝐴 ∈
(ℤ≥‘2)) |
| 57 | | nprm 16725 |
. . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝐴 ∈ (ℤ≥‘2))
→ ¬ (2 · 𝐴)
∈ ℙ) |
| 58 | 38, 56, 57 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 1 ≤
𝐴 ∧ ¬ 𝐴 = 1) → ¬ (2 ·
𝐴) ∈
ℙ) |
| 59 | 58 | 3exp 1120 |
. . . 4
⊢ (𝐴 ∈ ℤ → (1 ≤
𝐴 → (¬ 𝐴 = 1 → ¬ (2 ·
𝐴) ∈
ℙ))) |
| 60 | | zle0orge1 12630 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐴 ≤ 0 ∨ 1 ≤ 𝐴)) |
| 61 | 35, 59, 60 | mpjaod 861 |
. . 3
⊢ (𝐴 ∈ ℤ → (¬
𝐴 = 1 → ¬ (2
· 𝐴) ∈
ℙ)) |
| 62 | 61 | con4d 115 |
. 2
⊢ (𝐴 ∈ ℤ → ((2
· 𝐴) ∈ ℙ
→ 𝐴 =
1)) |
| 63 | | oveq2 7439 |
. . . 4
⊢ (𝐴 = 1 → (2 · 𝐴) = (2 ·
1)) |
| 64 | | 2t1e2 12429 |
. . . 4
⊢ (2
· 1) = 2 |
| 65 | 63, 64 | eqtrdi 2793 |
. . 3
⊢ (𝐴 = 1 → (2 · 𝐴) = 2) |
| 66 | | 2prm 16729 |
. . 3
⊢ 2 ∈
ℙ |
| 67 | 65, 66 | eqeltrdi 2849 |
. 2
⊢ (𝐴 = 1 → (2 · 𝐴) ∈
ℙ) |
| 68 | 62, 67 | impbid1 225 |
1
⊢ (𝐴 ∈ ℤ → ((2
· 𝐴) ∈ ℙ
↔ 𝐴 =
1)) |