Proof of Theorem bpos1lem
Step | Hyp | Ref
| Expression |
1 | | bpos1.3 |
. . . . . 6
⊢ 𝑃 ∈ ℙ |
2 | | prmnn 16231 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ 𝑃 ∈ ℕ |
4 | 3 | nnzi 12201 |
. . . 4
⊢ 𝑃 ∈ ℤ |
5 | | eluzelz 12448 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝑁 ∈ ℤ) |
6 | | eluz 12452 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝑃) ↔ 𝑃 ≤ 𝑁)) |
7 | 4, 5, 6 | sylancr 590 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (𝑁 ∈ (ℤ≥‘𝑃) ↔ 𝑃 ≤ 𝑁)) |
8 | | bpos1.2 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑃) → 𝜑) |
9 | 7, 8 | syl6bir 257 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (𝑃 ≤ 𝑁 → 𝜑)) |
10 | 3 | nnrei 11839 |
. . . . . . . 8
⊢ 𝑃 ∈ ℝ |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝑃 ∈ ℝ) |
12 | | bpos1.5 |
. . . . . . . . 9
⊢ (𝐴 · 2) = 𝐵 |
13 | | bpos1.4 |
. . . . . . . . . . 11
⊢ 𝐴 ∈
ℕ0 |
14 | 13 | nn0rei 12101 |
. . . . . . . . . 10
⊢ 𝐴 ∈ ℝ |
15 | | 2re 11904 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
16 | 14, 15 | remulcli 10849 |
. . . . . . . . 9
⊢ (𝐴 · 2) ∈
ℝ |
17 | 12, 16 | eqeltrri 2835 |
. . . . . . . 8
⊢ 𝐵 ∈ ℝ |
18 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝐵 ∈ ℝ) |
19 | | eluzelre 12449 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝑁 ∈ ℝ) |
20 | | remulcl 10814 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 · 𝑁) ∈ ℝ) |
21 | 15, 19, 20 | sylancr 590 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (2 · 𝑁) ∈ ℝ) |
22 | | bpos1.7 |
. . . . . . . . 9
⊢ (𝑃 < 𝐵 ∨ 𝑃 = 𝐵) |
23 | 10, 17 | leloei 10949 |
. . . . . . . . 9
⊢ (𝑃 ≤ 𝐵 ↔ (𝑃 < 𝐵 ∨ 𝑃 = 𝐵)) |
24 | 22, 23 | mpbir 234 |
. . . . . . . 8
⊢ 𝑃 ≤ 𝐵 |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝑃 ≤ 𝐵) |
26 | 13 | nn0cni 12102 |
. . . . . . . . 9
⊢ 𝐴 ∈ ℂ |
27 | | 2cn 11905 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
28 | 26, 27, 12 | mulcomli 10842 |
. . . . . . . 8
⊢ (2
· 𝐴) = 𝐵 |
29 | | eluzle 12451 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝐴 ≤ 𝑁) |
30 | | 2pos 11933 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
31 | 15, 30 | pm3.2i 474 |
. . . . . . . . . . 11
⊢ (2 ∈
ℝ ∧ 0 < 2) |
32 | | lemul2 11685 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → (𝐴 ≤ 𝑁 ↔ (2 · 𝐴) ≤ (2 · 𝑁))) |
33 | 14, 31, 32 | mp3an13 1454 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℝ → (𝐴 ≤ 𝑁 ↔ (2 · 𝐴) ≤ (2 · 𝑁))) |
34 | 19, 33 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (𝐴 ≤ 𝑁 ↔ (2 · 𝐴) ≤ (2 · 𝑁))) |
35 | 29, 34 | mpbid 235 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (2 · 𝐴) ≤ (2 · 𝑁)) |
36 | 28, 35 | eqbrtrrid 5089 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝐵 ≤ (2 · 𝑁)) |
37 | 11, 18, 21, 25, 36 | letrd 10989 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝑃 ≤ (2 · 𝑁)) |
38 | 37 | anim2i 620 |
. . . . 5
⊢ ((𝑁 < 𝑃 ∧ 𝑁 ∈ (ℤ≥‘𝐴)) → (𝑁 < 𝑃 ∧ 𝑃 ≤ (2 · 𝑁))) |
39 | | breq2 5057 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → (𝑁 < 𝑝 ↔ 𝑁 < 𝑃)) |
40 | | breq1 5056 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑃 ≤ (2 · 𝑁))) |
41 | 39, 40 | anbi12d 634 |
. . . . . 6
⊢ (𝑝 = 𝑃 → ((𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑃 ∧ 𝑃 ≤ (2 · 𝑁)))) |
42 | 41 | rspcev 3537 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 < 𝑃 ∧ 𝑃 ≤ (2 · 𝑁))) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) |
43 | 1, 38, 42 | sylancr 590 |
. . . 4
⊢ ((𝑁 < 𝑃 ∧ 𝑁 ∈ (ℤ≥‘𝐴)) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) |
44 | | bpos1.1 |
. . . 4
⊢
(∃𝑝 ∈
ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) → 𝜑) |
45 | 43, 44 | syl 17 |
. . 3
⊢ ((𝑁 < 𝑃 ∧ 𝑁 ∈ (ℤ≥‘𝐴)) → 𝜑) |
46 | 45 | expcom 417 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (𝑁 < 𝑃 → 𝜑)) |
47 | | lelttric 10939 |
. . 3
⊢ ((𝑃 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑃 ≤ 𝑁 ∨ 𝑁 < 𝑃)) |
48 | 10, 19, 47 | sylancr 590 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (𝑃 ≤ 𝑁 ∨ 𝑁 < 𝑃)) |
49 | 9, 46, 48 | mpjaod 860 |
1
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝜑) |