Proof of Theorem bpos1lem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | bpos1.3 | . . . . . 6
⊢ 𝑃 ∈ ℙ | 
| 2 |  | prmnn 16712 | . . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 3 | 1, 2 | ax-mp 5 | . . . . 5
⊢ 𝑃 ∈ ℕ | 
| 4 | 3 | nnzi 12643 | . . . 4
⊢ 𝑃 ∈ ℤ | 
| 5 |  | eluzelz 12889 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝑁 ∈ ℤ) | 
| 6 |  | eluz 12893 | . . . 4
⊢ ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝑃) ↔ 𝑃 ≤ 𝑁)) | 
| 7 | 4, 5, 6 | sylancr 587 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (𝑁 ∈ (ℤ≥‘𝑃) ↔ 𝑃 ≤ 𝑁)) | 
| 8 |  | bpos1.2 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑃) → 𝜑) | 
| 9 | 7, 8 | biimtrrdi 254 | . 2
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (𝑃 ≤ 𝑁 → 𝜑)) | 
| 10 | 3 | nnrei 12276 | . . . . . . . 8
⊢ 𝑃 ∈ ℝ | 
| 11 | 10 | a1i 11 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝑃 ∈ ℝ) | 
| 12 |  | bpos1.5 | . . . . . . . . 9
⊢ (𝐴 · 2) = 𝐵 | 
| 13 |  | bpos1.4 | . . . . . . . . . . 11
⊢ 𝐴 ∈
ℕ0 | 
| 14 | 13 | nn0rei 12539 | . . . . . . . . . 10
⊢ 𝐴 ∈ ℝ | 
| 15 |  | 2re 12341 | . . . . . . . . . 10
⊢ 2 ∈
ℝ | 
| 16 | 14, 15 | remulcli 11278 | . . . . . . . . 9
⊢ (𝐴 · 2) ∈
ℝ | 
| 17 | 12, 16 | eqeltrri 2837 | . . . . . . . 8
⊢ 𝐵 ∈ ℝ | 
| 18 | 17 | a1i 11 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝐵 ∈ ℝ) | 
| 19 |  | eluzelre 12890 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝑁 ∈ ℝ) | 
| 20 |  | remulcl 11241 | . . . . . . . 8
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 · 𝑁) ∈ ℝ) | 
| 21 | 15, 19, 20 | sylancr 587 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (2 · 𝑁) ∈ ℝ) | 
| 22 |  | bpos1.7 | . . . . . . . . 9
⊢ (𝑃 < 𝐵 ∨ 𝑃 = 𝐵) | 
| 23 | 10, 17 | leloei 11379 | . . . . . . . . 9
⊢ (𝑃 ≤ 𝐵 ↔ (𝑃 < 𝐵 ∨ 𝑃 = 𝐵)) | 
| 24 | 22, 23 | mpbir 231 | . . . . . . . 8
⊢ 𝑃 ≤ 𝐵 | 
| 25 | 24 | a1i 11 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝑃 ≤ 𝐵) | 
| 26 | 13 | nn0cni 12540 | . . . . . . . . 9
⊢ 𝐴 ∈ ℂ | 
| 27 |  | 2cn 12342 | . . . . . . . . 9
⊢ 2 ∈
ℂ | 
| 28 | 26, 27, 12 | mulcomli 11271 | . . . . . . . 8
⊢ (2
· 𝐴) = 𝐵 | 
| 29 |  | eluzle 12892 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝐴 ≤ 𝑁) | 
| 30 |  | 2pos 12370 | . . . . . . . . . . . 12
⊢ 0 <
2 | 
| 31 | 15, 30 | pm3.2i 470 | . . . . . . . . . . 11
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 32 |  | lemul2 12121 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → (𝐴 ≤ 𝑁 ↔ (2 · 𝐴) ≤ (2 · 𝑁))) | 
| 33 | 14, 31, 32 | mp3an13 1453 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℝ → (𝐴 ≤ 𝑁 ↔ (2 · 𝐴) ≤ (2 · 𝑁))) | 
| 34 | 19, 33 | syl 17 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (𝐴 ≤ 𝑁 ↔ (2 · 𝐴) ≤ (2 · 𝑁))) | 
| 35 | 29, 34 | mpbid 232 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (2 · 𝐴) ≤ (2 · 𝑁)) | 
| 36 | 28, 35 | eqbrtrrid 5178 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝐵 ≤ (2 · 𝑁)) | 
| 37 | 11, 18, 21, 25, 36 | letrd 11419 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝑃 ≤ (2 · 𝑁)) | 
| 38 | 37 | anim2i 617 | . . . . 5
⊢ ((𝑁 < 𝑃 ∧ 𝑁 ∈ (ℤ≥‘𝐴)) → (𝑁 < 𝑃 ∧ 𝑃 ≤ (2 · 𝑁))) | 
| 39 |  | breq2 5146 | . . . . . . 7
⊢ (𝑝 = 𝑃 → (𝑁 < 𝑝 ↔ 𝑁 < 𝑃)) | 
| 40 |  | breq1 5145 | . . . . . . 7
⊢ (𝑝 = 𝑃 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑃 ≤ (2 · 𝑁))) | 
| 41 | 39, 40 | anbi12d 632 | . . . . . 6
⊢ (𝑝 = 𝑃 → ((𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑃 ∧ 𝑃 ≤ (2 · 𝑁)))) | 
| 42 | 41 | rspcev 3621 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 < 𝑃 ∧ 𝑃 ≤ (2 · 𝑁))) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) | 
| 43 | 1, 38, 42 | sylancr 587 | . . . 4
⊢ ((𝑁 < 𝑃 ∧ 𝑁 ∈ (ℤ≥‘𝐴)) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) | 
| 44 |  | bpos1.1 | . . . 4
⊢
(∃𝑝 ∈
ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) → 𝜑) | 
| 45 | 43, 44 | syl 17 | . . 3
⊢ ((𝑁 < 𝑃 ∧ 𝑁 ∈ (ℤ≥‘𝐴)) → 𝜑) | 
| 46 | 45 | expcom 413 | . 2
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (𝑁 < 𝑃 → 𝜑)) | 
| 47 |  | lelttric 11369 | . . 3
⊢ ((𝑃 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑃 ≤ 𝑁 ∨ 𝑁 < 𝑃)) | 
| 48 | 10, 19, 47 | sylancr 587 | . 2
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → (𝑃 ≤ 𝑁 ∨ 𝑁 < 𝑃)) | 
| 49 | 9, 46, 48 | mpjaod 860 | 1
⊢ (𝑁 ∈
(ℤ≥‘𝐴) → 𝜑) |