Metamath Proof Explorer

Theorem pntrlog2bndlem6a

Description: Lemma for pntrlog2bndlem6 . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses pntsval.1 ⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
pntrlog2bnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
pntrlog2bnd.t ⊢ 𝑇 = ( 𝑎 ∈ ℝ ↦ if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) )
pntrlog2bndlem5.1 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
pntrlog2bndlem5.2 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐵 )
pntrlog2bndlem6.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
pntrlog2bndlem6.2 ⊢ ( 𝜑 → 1 ≤ 𝐴 )
Assertion pntrlog2bndlem6a ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 pntsval.1 ⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
2 pntrlog2bnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
3 pntrlog2bnd.t ⊢ 𝑇 = ( 𝑎 ∈ ℝ ↦ if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) )
4 pntrlog2bndlem5.1 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
5 pntrlog2bndlem5.2 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐵 )
6 pntrlog2bndlem6.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
7 pntrlog2bndlem6.2 ⊢ ( 𝜑 → 1 ≤ 𝐴 )
8 elioore ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
10 1rp ⊢ 1 ∈ ℝ+
11 10 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
12 11 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
13 eliooord ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
15 14 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
16 12 9 15 ltled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 )
17 9 11 16 rpgecld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
18 10 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
19 6 18 7 rpgecld ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℝ+ )
21 17 20 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / 𝐴 ) ∈ ℝ+ )
22 21 rprege0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑥 / 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 / 𝐴 ) ) )
23 flge0nn0 ⊢ ( ( ( 𝑥 / 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 / 𝐴 ) ) → ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ∈ ℕ0 )
24 nn0p1nn ⊢ ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ∈ ℕ )
25 22 23 24 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ∈ ℕ )
26 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
27 25 26 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
28 21 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / 𝐴 ) ∈ ℝ )
29 17 rpge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 𝑥 )
30 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝐴 )
31 11 20 9 29 30 lediv2ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / 𝐴 ) ≤ ( 𝑥 / 1 ) )
32 9 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ )
33 32 div1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / 1 ) = 𝑥 )
34 31 33 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / 𝐴 ) ≤ 𝑥 )
35 flword2 ⊢ ( ( ( 𝑥 / 𝐴 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝑥 / 𝐴 ) ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) )
36 28 9 34 35 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) )
37 fzsplit2 ⊢ ( ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) )
38 27 36 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) )