Metamath Proof Explorer

Theorem bposlem4

Description: Lemma for bpos . (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Hypotheses bpos.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 5 ) )
bpos.2 ⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
bpos.3 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
bpos.4 ⊢ 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
bpos.5 ⊢ 𝑀 = ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) )
Assertion bposlem4 ( 𝜑 → 𝑀 ∈ ( 3 ... 𝐾 ) )

Proof

Step Hyp Ref Expression
1 bpos.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 5 ) )
2 bpos.2 ⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
3 bpos.3 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
4 bpos.4 ⊢ 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
5 bpos.5 ⊢ 𝑀 = ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) )
6 2nn ⊢ 2 ∈ ℕ
7 5nn ⊢ 5 ∈ ℕ
8 eluznn ⊢ ( ( 5 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 5 ) ) → 𝑁 ∈ ℕ )
9 7 1 8 sylancr ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
10 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
11 6 9 10 sylancr ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ )
12 11 nnred ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
13 11 nnrpd ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ+ )
14 13 rpge0d ⊢ ( 𝜑 → 0 ≤ ( 2 · 𝑁 ) )
15 12 14 resqrtcld ⊢ ( 𝜑 → ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ )
16 15 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ℤ )
17 sqrt9 ⊢ ( √ ‘ 9 ) = 3
18 9re ⊢ 9 ∈ ℝ
19 18 a1i ⊢ ( 𝜑 → 9 ∈ ℝ )
20 10re ⊢ 1 0 ∈ ℝ
21 20 a1i ⊢ ( 𝜑 → 1 0 ∈ ℝ )
22 lep1 ⊢ ( 9 ∈ ℝ → 9 ≤ ( 9 + 1 ) )
23 18 22 ax-mp ⊢ 9 ≤ ( 9 + 1 )
24 9p1e10 ⊢ ( 9 + 1 ) = 1 0
25 23 24 breqtri ⊢ 9 ≤ 1 0
26 25 a1i ⊢ ( 𝜑 → 9 ≤ 1 0 )
27 5cn ⊢ 5 ∈ ℂ
28 2cn ⊢ 2 ∈ ℂ
29 5t2e10 ⊢ ( 5 · 2 ) = 1 0
30 27 28 29 mulcomli ⊢ ( 2 · 5 ) = 1 0
31 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 5 ≤ 𝑁 )
32 1 31 syl ⊢ ( 𝜑 → 5 ≤ 𝑁 )
33 9 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
34 5re ⊢ 5 ∈ ℝ
35 2re ⊢ 2 ∈ ℝ
36 2pos ⊢ 0 < 2
37 35 36 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
38 lemul2 ⊢ ( ( 5 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) )
39 34 37 38 mp3an13 ⊢ ( 𝑁 ∈ ℝ → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) )
40 33 39 syl ⊢ ( 𝜑 → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) )
41 32 40 mpbid ⊢ ( 𝜑 → ( 2 · 5 ) ≤ ( 2 · 𝑁 ) )
42 30 41 eqbrtrrid ⊢ ( 𝜑 → 1 0 ≤ ( 2 · 𝑁 ) )
43 19 21 12 26 42 letrd ⊢ ( 𝜑 → 9 ≤ ( 2 · 𝑁 ) )
44 0re ⊢ 0 ∈ ℝ
45 9pos ⊢ 0 < 9
46 44 18 45 ltleii ⊢ 0 ≤ 9
47 18 46 pm3.2i ⊢ ( 9 ∈ ℝ ∧ 0 ≤ 9 )
48 13 rprege0d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑁 ) ) )
49 sqrtle ⊢ ( ( ( 9 ∈ ℝ ∧ 0 ≤ 9 ) ∧ ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑁 ) ) ) → ( 9 ≤ ( 2 · 𝑁 ) ↔ ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) )
50 47 48 49 sylancr ⊢ ( 𝜑 → ( 9 ≤ ( 2 · 𝑁 ) ↔ ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) )
51 43 50 mpbid ⊢ ( 𝜑 → ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
52 17 51 eqbrtrrid ⊢ ( 𝜑 → 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
53 3z ⊢ 3 ∈ ℤ
54 flge ⊢ ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ 3 ∈ ℤ ) → ( 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
55 15 53 54 sylancl ⊢ ( 𝜑 → ( 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
56 52 55 mpbid ⊢ ( 𝜑 → 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) )
57 53 eluz1i ⊢ ( ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ( ℤ≥ ‘ 3 ) ↔ ( ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ℤ ∧ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
58 16 56 57 sylanbrc ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ( ℤ≥ ‘ 3 ) )
59 3nn ⊢ 3 ∈ ℕ
60 nndivre ⊢ ( ( ( 2 · 𝑁 ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ )
61 12 59 60 sylancl ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ )
62 3re ⊢ 3 ∈ ℝ
63 62 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
64 13 sqrtgt0d ⊢ ( 𝜑 → 0 < ( √ ‘ ( 2 · 𝑁 ) ) )
65 lemul2 ⊢ ( ( 3 ∈ ℝ ∧ ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ 0 < ( √ ‘ ( 2 · 𝑁 ) ) ) ) → ( 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ ( ( √ ‘ ( 2 · 𝑁 ) ) · 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) · ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
66 63 15 15 64 65 syl112anc ⊢ ( 𝜑 → ( 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ ( ( √ ‘ ( 2 · 𝑁 ) ) · 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) · ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
67 52 66 mpbid ⊢ ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) · 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) · ( √ ‘ ( 2 · 𝑁 ) ) ) )
68 remsqsqrt ⊢ ( ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑁 ) ) → ( ( √ ‘ ( 2 · 𝑁 ) ) · ( √ ‘ ( 2 · 𝑁 ) ) ) = ( 2 · 𝑁 ) )
69 12 14 68 syl2anc ⊢ ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) · ( √ ‘ ( 2 · 𝑁 ) ) ) = ( 2 · 𝑁 ) )
70 67 69 breqtrd ⊢ ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) · 3 ) ≤ ( 2 · 𝑁 ) )
71 3pos ⊢ 0 < 3
72 62 71 pm3.2i ⊢ ( 3 ∈ ℝ ∧ 0 < 3 )
73 72 a1i ⊢ ( 𝜑 → ( 3 ∈ ℝ ∧ 0 < 3 ) )
74 lemuldiv ⊢ ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( ( ( √ ‘ ( 2 · 𝑁 ) ) · 3 ) ≤ ( 2 · 𝑁 ) ↔ ( √ ‘ ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) / 3 ) ) )
75 15 12 73 74 syl3anc ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) · 3 ) ≤ ( 2 · 𝑁 ) ↔ ( √ ‘ ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) / 3 ) ) )
76 70 75 mpbid ⊢ ( 𝜑 → ( √ ‘ ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) / 3 ) )
77 flword2 ⊢ ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ ∧ ( √ ‘ ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) / 3 ) ) → ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
78 15 61 76 77 syl3anc ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
79 elfzuzb ⊢ ( ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ( 3 ... ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) ) ↔ ( ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ( ℤ≥ ‘ 3 ) ∧ ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) ) )
80 58 78 79 sylanbrc ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ( 3 ... ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) ) )
81 4 oveq2i ⊢ ( 3 ... 𝐾 ) = ( 3 ... ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) )
82 80 5 81 3eltr4g ⊢ ( 𝜑 → 𝑀 ∈ ( 3 ... 𝐾 ) )