This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bpos1lem

Description: Lemma for bpos1 . (Contributed by Mario Carneiro, 12-Mar-2014)

Ref Expression
Hypotheses bpos1.1 ⊢ ( ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) → 𝜑 )
bpos1.2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑃 ) → 𝜑 )
bpos1.3 ⊢ 𝑃 ∈ ℙ
bpos1.4 ⊢ 𝐴 ∈ ℕ0
bpos1.5 ⊢ ( 𝐴 · 2 ) = 𝐵
bpos1.6 ⊢ 𝐴 < 𝑃
bpos1.7 ⊢ ( 𝑃 < 𝐵 ∨ 𝑃 = 𝐵 )
Assertion bpos1lem ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝜑 )

Proof

Step Hyp Ref Expression
1 bpos1.1 ⊢ ( ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) → 𝜑 )
2 bpos1.2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑃 ) → 𝜑 )
3 bpos1.3 ⊢ 𝑃 ∈ ℙ
4 bpos1.4 ⊢ 𝐴 ∈ ℕ0
5 bpos1.5 ⊢ ( 𝐴 · 2 ) = 𝐵
6 bpos1.6 ⊢ 𝐴 < 𝑃
7 bpos1.7 ⊢ ( 𝑃 < 𝐵 ∨ 𝑃 = 𝐵 )
8 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
9 3 8 ax-mp ⊢ 𝑃 ∈ ℕ
10 9 nnzi ⊢ 𝑃 ∈ ℤ
11 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑁 ∈ ℤ )
12 eluz ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑃 ) ↔ 𝑃 ≤ 𝑁 ) )
13 10 11 12 sylancr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑃 ) ↔ 𝑃 ≤ 𝑁 ) )
14 13 2 biimtrrdi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝑃 ≤ 𝑁 → 𝜑 ) )
15 9 nnrei ⊢ 𝑃 ∈ ℝ
16 15 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑃 ∈ ℝ )
17 4 nn0rei ⊢ 𝐴 ∈ ℝ
18 2re ⊢ 2 ∈ ℝ
19 17 18 remulcli ⊢ ( 𝐴 · 2 ) ∈ ℝ
20 5 19 eqeltrri ⊢ 𝐵 ∈ ℝ
21 20 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℝ )
22 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑁 ∈ ℝ )
23 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 2 · 𝑁 ) ∈ ℝ )
24 18 22 23 sylancr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 2 · 𝑁 ) ∈ ℝ )
25 15 20 leloei ⊢ ( 𝑃 ≤ 𝐵 ↔ ( 𝑃 < 𝐵 ∨ 𝑃 = 𝐵 ) )
26 7 25 mpbir ⊢ 𝑃 ≤ 𝐵
27 26 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑃 ≤ 𝐵 )
28 4 nn0cni ⊢ 𝐴 ∈ ℂ
29 2cn ⊢ 2 ∈ ℂ
30 28 29 5 mulcomli ⊢ ( 2 · 𝐴 ) = 𝐵
31 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐴 ≤ 𝑁 )
32 2pos ⊢ 0 < 2
33 18 32 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
34 lemul2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝐴 ≤ 𝑁 ↔ ( 2 · 𝐴 ) ≤ ( 2 · 𝑁 ) ) )
35 17 33 34 mp3an13 ⊢ ( 𝑁 ∈ ℝ → ( 𝐴 ≤ 𝑁 ↔ ( 2 · 𝐴 ) ≤ ( 2 · 𝑁 ) ) )
36 22 35 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ≤ 𝑁 ↔ ( 2 · 𝐴 ) ≤ ( 2 · 𝑁 ) ) )
37 31 36 mpbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 2 · 𝐴 ) ≤ ( 2 · 𝑁 ) )
38 30 37 eqbrtrrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ≤ ( 2 · 𝑁 ) )
39 16 21 24 27 38 letrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑃 ≤ ( 2 · 𝑁 ) )
40 39 anim2i ⊢ ( ( 𝑁 < 𝑃 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑁 < 𝑃 ∧ 𝑃 ≤ ( 2 · 𝑁 ) ) )
41 breq2 ⊢ ( 𝑝 = 𝑃 → ( 𝑁 < 𝑝 ↔ 𝑁 < 𝑃 ) )
42 breq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ≤ ( 2 · 𝑁 ) ↔ 𝑃 ≤ ( 2 · 𝑁 ) ) )
43 41 42 anbi12d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ↔ ( 𝑁 < 𝑃 ∧ 𝑃 ≤ ( 2 · 𝑁 ) ) ) )
44 43 rspcev ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 < 𝑃 ∧ 𝑃 ≤ ( 2 · 𝑁 ) ) ) → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
45 3 40 44 sylancr ⊢ ( ( 𝑁 < 𝑃 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
46 45 1 syl ⊢ ( ( 𝑁 < 𝑃 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝜑 )
47 46 expcom ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝑁 < 𝑃 → 𝜑 ) )
48 lelttric ⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑃 ≤ 𝑁 ∨ 𝑁 < 𝑃 ) )
49 15 22 48 sylancr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝑃 ≤ 𝑁 ∨ 𝑁 < 𝑃 ) )
50 14 47 49 mpjaod ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝜑 )