Metamath Proof Explorer

Theorem chpdifbndlem1

Description: Lemma for chpdifbnd . (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypotheses chpdifbnd.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
chpdifbnd.1 ⊢ ( 𝜑 → 1 ≤ 𝐴 )
chpdifbnd.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
chpdifbnd.2 ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝐵 )
chpdifbnd.c ⊢ 𝐶 = ( ( 𝐵 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) )
chpdifbnd.x ⊢ ( 𝜑 → 𝑋 ∈ ( 1 (,) +∞ ) )
chpdifbnd.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 [,] ( 𝐴 · 𝑋 ) ) )
Assertion chpdifbndlem1 ( 𝜑 → ( ( ψ ‘ 𝑌 ) − ( ψ ‘ 𝑋 ) ) ≤ ( ( 2 · ( 𝑌 − 𝑋 ) ) + ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chpdifbnd.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 chpdifbnd.1 ⊢ ( 𝜑 → 1 ≤ 𝐴 )
3 chpdifbnd.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4 chpdifbnd.2 ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝐵 )
5 chpdifbnd.c ⊢ 𝐶 = ( ( 𝐵 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) )
6 chpdifbnd.x ⊢ ( 𝜑 → 𝑋 ∈ ( 1 (,) +∞ ) )
7 chpdifbnd.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 [,] ( 𝐴 · 𝑋 ) ) )
8 ioossre ⊢ ( 1 (,) +∞ ) ⊆ ℝ
9 8 6 sselid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
10 1 rpred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
11 10 9 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ℝ )
12 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ ( 𝐴 · 𝑋 ) ∈ ℝ ) → ( 𝑌 ∈ ( 𝑋 [,] ( 𝐴 · 𝑋 ) ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ ( 𝐴 · 𝑋 ) ) ) )
13 9 11 12 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 [,] ( 𝐴 · 𝑋 ) ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ ( 𝐴 · 𝑋 ) ) ) )
14 7 13 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ ( 𝐴 · 𝑋 ) ) )
15 14 simp1d ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
16 chpcl ⊢ ( 𝑌 ∈ ℝ → ( ψ ‘ 𝑌 ) ∈ ℝ )
17 15 16 syl ⊢ ( 𝜑 → ( ψ ‘ 𝑌 ) ∈ ℝ )
18 chpcl ⊢ ( 𝑋 ∈ ℝ → ( ψ ‘ 𝑋 ) ∈ ℝ )
19 9 18 syl ⊢ ( 𝜑 → ( ψ ‘ 𝑋 ) ∈ ℝ )
20 17 19 resubcld ⊢ ( 𝜑 → ( ( ψ ‘ 𝑌 ) − ( ψ ‘ 𝑋 ) ) ∈ ℝ )
21 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
22 1re ⊢ 1 ∈ ℝ
23 22 a1i ⊢ ( 𝜑 → 1 ∈ ℝ )
24 0lt1 ⊢ 0 < 1
25 24 a1i ⊢ ( 𝜑 → 0 < 1 )
26 eliooord ⊢ ( 𝑋 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑋 ∧ 𝑋 < +∞ ) )
27 6 26 syl ⊢ ( 𝜑 → ( 1 < 𝑋 ∧ 𝑋 < +∞ ) )
28 27 simpld ⊢ ( 𝜑 → 1 < 𝑋 )
29 21 23 9 25 28 lttrd ⊢ ( 𝜑 → 0 < 𝑋 )
30 9 29 elrpd ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
31 30 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℝ )
32 20 31 remulcld ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑌 ) − ( ψ ‘ 𝑋 ) ) · ( log ‘ 𝑋 ) ) ∈ ℝ )
33 2re ⊢ 2 ∈ ℝ
34 15 9 resubcld ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℝ )
35 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( 𝑌 − 𝑋 ) ∈ ℝ ) → ( 2 · ( 𝑌 − 𝑋 ) ) ∈ ℝ )
36 33 34 35 sylancr ⊢ ( 𝜑 → ( 2 · ( 𝑌 − 𝑋 ) ) ∈ ℝ )
37 36 31 remulcld ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) ∈ ℝ )
38 3 rpred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
39 15 9 readdcld ⊢ ( 𝜑 → ( 𝑌 + 𝑋 ) ∈ ℝ )
40 38 39 remulcld ⊢ ( 𝜑 → ( 𝐵 · ( 𝑌 + 𝑋 ) ) ∈ ℝ )
41 1 relogcld ⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℝ )
42 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( log ‘ 𝐴 ) ∈ ℝ ) → ( 2 · ( log ‘ 𝐴 ) ) ∈ ℝ )
43 33 41 42 sylancr ⊢ ( 𝜑 → ( 2 · ( log ‘ 𝐴 ) ) ∈ ℝ )
44 43 15 remulcld ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ∈ ℝ )
45 40 44 readdcld ⊢ ( 𝜑 → ( ( 𝐵 · ( 𝑌 + 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) ∈ ℝ )
46 37 45 readdcld ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( ( 𝐵 · ( 𝑌 + 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) ) ∈ ℝ )
47 peano2re ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
48 10 47 syl ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℝ )
49 38 48 remulcld ⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 + 1 ) ) ∈ ℝ )
50 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 2 · 𝐴 ) ∈ ℝ )
51 33 10 50 sylancr ⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℝ )
52 51 41 remulcld ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) ∈ ℝ )
53 49 52 readdcld ⊢ ( 𝜑 → ( ( 𝐵 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) ) ∈ ℝ )
54 5 53 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
55 54 9 remulcld ⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∈ ℝ )
56 37 55 readdcld ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( 𝐶 · 𝑋 ) ) ∈ ℝ )
57 17 31 remulcld ⊢ ( 𝜑 → ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑋 ) ) ∈ ℝ )
58 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝑋 ) ) ∈ Fin )
59 14 simp2d ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
60 flword2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌 ) → ( ⌊ ‘ 𝑌 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑋 ) ) )
61 9 15 59 60 syl3anc ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑋 ) ) )
62 fzss2 ⊢ ( ( ⌊ ‘ 𝑌 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑋 ) ) → ( 1 ... ( ⌊ ‘ 𝑋 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑌 ) ) )
63 61 62 syl ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝑋 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑌 ) ) )
64 63 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) )
65 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) → 𝑛 ∈ ℕ )
66 65 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑛 ∈ ℕ )
67 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
68 66 67 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
69 nndivre ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑋 / 𝑛 ) ∈ ℝ )
70 9 65 69 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( 𝑋 / 𝑛 ) ∈ ℝ )
71 chpcl ⊢ ( ( 𝑋 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝑋 / 𝑛 ) ) ∈ ℝ )
72 70 71 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( ψ ‘ ( 𝑋 / 𝑛 ) ) ∈ ℝ )
73 68 72 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ∈ ℝ )
74 64 73 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ∈ ℝ )
75 58 74 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ∈ ℝ )
76 57 75 readdcld ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) ∈ ℝ )
77 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( log ‘ 𝑋 ) ∈ ℝ ) → ( 2 · ( log ‘ 𝑋 ) ) ∈ ℝ )
78 33 31 77 sylancr ⊢ ( 𝜑 → ( 2 · ( log ‘ 𝑋 ) ) ∈ ℝ )
79 78 38 resubcld ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) ∈ ℝ )
80 79 9 remulcld ⊢ ( 𝜑 → ( ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) · 𝑋 ) ∈ ℝ )
81 1 30 rpmulcld ⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ℝ+ )
82 81 relogcld ⊢ ( 𝜑 → ( log ‘ ( 𝐴 · 𝑋 ) ) ∈ ℝ )
83 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( log ‘ ( 𝐴 · 𝑋 ) ) ∈ ℝ ) → ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ∈ ℝ )
84 33 82 83 sylancr ⊢ ( 𝜑 → ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ∈ ℝ )
85 38 84 readdcld ⊢ ( 𝜑 → ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) ∈ ℝ )
86 85 15 remulcld ⊢ ( 𝜑 → ( ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) · 𝑌 ) ∈ ℝ )
87 19 31 remulcld ⊢ ( 𝜑 → ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) ∈ ℝ )
88 87 75 readdcld ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) ∈ ℝ )
89 21 9 15 29 59 ltletrd ⊢ ( 𝜑 → 0 < 𝑌 )
90 15 89 elrpd ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
91 90 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑌 ) ∈ ℝ )
92 17 91 remulcld ⊢ ( 𝜑 → ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) ∈ ℝ )
93 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝑌 ) ) ∈ Fin )
94 nndivre ⊢ ( ( 𝑌 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑌 / 𝑛 ) ∈ ℝ )
95 15 65 94 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( 𝑌 / 𝑛 ) ∈ ℝ )
96 chpcl ⊢ ( ( 𝑌 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝑌 / 𝑛 ) ) ∈ ℝ )
97 95 96 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( ψ ‘ ( 𝑌 / 𝑛 ) ) ∈ ℝ )
98 68 97 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ∈ ℝ )
99 93 98 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ∈ ℝ )
100 92 99 readdcld ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) ∈ ℝ )
101 chpge0 ⊢ ( 𝑌 ∈ ℝ → 0 ≤ ( ψ ‘ 𝑌 ) )
102 15 101 syl ⊢ ( 𝜑 → 0 ≤ ( ψ ‘ 𝑌 ) )
103 30 90 logled ⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ( log ‘ 𝑋 ) ≤ ( log ‘ 𝑌 ) ) )
104 59 103 mpbid ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ≤ ( log ‘ 𝑌 ) )
105 31 91 17 102 104 lemul2ad ⊢ ( 𝜑 → ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑋 ) ) ≤ ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) )
106 93 73 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ∈ ℝ )
107 vmage0 ⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) )
108 66 107 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
109 chpge0 ⊢ ( ( 𝑋 / 𝑛 ) ∈ ℝ → 0 ≤ ( ψ ‘ ( 𝑋 / 𝑛 ) ) )
110 70 109 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → 0 ≤ ( ψ ‘ ( 𝑋 / 𝑛 ) ) )
111 68 72 108 110 mulge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) )
112 93 73 111 63 fsumless ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) )
113 9 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑋 ∈ ℝ )
114 15 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑌 ∈ ℝ )
115 66 nnrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑛 ∈ ℝ+ )
116 59 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑋 ≤ 𝑌 )
117 113 114 115 116 lediv1dd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( 𝑋 / 𝑛 ) ≤ ( 𝑌 / 𝑛 ) )
118 chpwordi ⊢ ( ( ( 𝑋 / 𝑛 ) ∈ ℝ ∧ ( 𝑌 / 𝑛 ) ∈ ℝ ∧ ( 𝑋 / 𝑛 ) ≤ ( 𝑌 / 𝑛 ) ) → ( ψ ‘ ( 𝑋 / 𝑛 ) ) ≤ ( ψ ‘ ( 𝑌 / 𝑛 ) ) )
119 70 95 117 118 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( ψ ‘ ( 𝑋 / 𝑛 ) ) ≤ ( ψ ‘ ( 𝑌 / 𝑛 ) ) )
120 72 97 68 108 119 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ≤ ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) )
121 93 73 98 120 fsumle ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) )
122 75 106 99 112 121 letrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) )
123 57 75 92 99 105 122 le2addd ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) ≤ ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) )
124 100 90 rerpdivcld ⊢ ( 𝜑 → ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) ∈ ℝ )
125 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( log ‘ 𝑌 ) ∈ ℝ ) → ( 2 · ( log ‘ 𝑌 ) ) ∈ ℝ )
126 33 91 125 sylancr ⊢ ( 𝜑 → ( 2 · ( log ‘ 𝑌 ) ) ∈ ℝ )
127 38 126 readdcld ⊢ ( 𝜑 → ( 𝐵 + ( 2 · ( log ‘ 𝑌 ) ) ) ∈ ℝ )
128 124 126 resubcld ⊢ ( 𝜑 → ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) − ( 2 · ( log ‘ 𝑌 ) ) ) ∈ ℝ )
129 128 recnd ⊢ ( 𝜑 → ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) − ( 2 · ( log ‘ 𝑌 ) ) ) ∈ ℂ )
130 129 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) − ( 2 · ( log ‘ 𝑌 ) ) ) ) ∈ ℝ )
131 128 leabsd ⊢ ( 𝜑 → ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) − ( 2 · ( log ‘ 𝑌 ) ) ) ≤ ( abs ‘ ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) − ( 2 · ( log ‘ 𝑌 ) ) ) ) )
132 fveq2 ⊢ ( 𝑧 = 𝑌 → ( ψ ‘ 𝑧 ) = ( ψ ‘ 𝑌 ) )
133 fveq2 ⊢ ( 𝑧 = 𝑌 → ( log ‘ 𝑧 ) = ( log ‘ 𝑌 ) )
134 132 133 oveq12d ⊢ ( 𝑧 = 𝑌 → ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) = ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) )
135 fveq2 ⊢ ( 𝑚 = 𝑛 → ( Λ ‘ 𝑚 ) = ( Λ ‘ 𝑛 ) )
136 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑧 / 𝑚 ) = ( 𝑧 / 𝑛 ) )
137 136 fveq2d ⊢ ( 𝑚 = 𝑛 → ( ψ ‘ ( 𝑧 / 𝑚 ) ) = ( ψ ‘ ( 𝑧 / 𝑛 ) ) )
138 135 137 oveq12d ⊢ ( 𝑚 = 𝑛 → ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) = ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) )
139 138 cbvsumv ⊢ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) )
140 fveq2 ⊢ ( 𝑧 = 𝑌 → ( ⌊ ‘ 𝑧 ) = ( ⌊ ‘ 𝑌 ) )
141 140 oveq2d ⊢ ( 𝑧 = 𝑌 → ( 1 ... ( ⌊ ‘ 𝑧 ) ) = ( 1 ... ( ⌊ ‘ 𝑌 ) ) )
142 simpl ⊢ ( ( 𝑧 = 𝑌 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑧 = 𝑌 )
143 142 fvoveq1d ⊢ ( ( 𝑧 = 𝑌 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( ψ ‘ ( 𝑧 / 𝑛 ) ) = ( ψ ‘ ( 𝑌 / 𝑛 ) ) )
144 143 oveq2d ⊢ ( ( 𝑧 = 𝑌 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) = ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) )
145 141 144 sumeq12rdv ⊢ ( 𝑧 = 𝑌 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) )
146 139 145 syl5eq ⊢ ( 𝑧 = 𝑌 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) )
147 134 146 oveq12d ⊢ ( 𝑧 = 𝑌 → ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) = ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) )
148 id ⊢ ( 𝑧 = 𝑌 → 𝑧 = 𝑌 )
149 147 148 oveq12d ⊢ ( 𝑧 = 𝑌 → ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) = ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) )
150 133 oveq2d ⊢ ( 𝑧 = 𝑌 → ( 2 · ( log ‘ 𝑧 ) ) = ( 2 · ( log ‘ 𝑌 ) ) )
151 149 150 oveq12d ⊢ ( 𝑧 = 𝑌 → ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) = ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) − ( 2 · ( log ‘ 𝑌 ) ) ) )
152 151 fveq2d ⊢ ( 𝑧 = 𝑌 → ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) = ( abs ‘ ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) − ( 2 · ( log ‘ 𝑌 ) ) ) ) )
153 152 breq1d ⊢ ( 𝑧 = 𝑌 → ( ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝐵 ↔ ( abs ‘ ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) − ( 2 · ( log ‘ 𝑌 ) ) ) ) ≤ 𝐵 ) )
154 23 9 28 ltled ⊢ ( 𝜑 → 1 ≤ 𝑋 )
155 23 9 15 154 59 letrd ⊢ ( 𝜑 → 1 ≤ 𝑌 )
156 elicopnf ⊢ ( 1 ∈ ℝ → ( 𝑌 ∈ ( 1 [,) +∞ ) ↔ ( 𝑌 ∈ ℝ ∧ 1 ≤ 𝑌 ) ) )
157 22 156 ax-mp ⊢ ( 𝑌 ∈ ( 1 [,) +∞ ) ↔ ( 𝑌 ∈ ℝ ∧ 1 ≤ 𝑌 ) )
158 15 155 157 sylanbrc ⊢ ( 𝜑 → 𝑌 ∈ ( 1 [,) +∞ ) )
159 153 4 158 rspcdva ⊢ ( 𝜑 → ( abs ‘ ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) − ( 2 · ( log ‘ 𝑌 ) ) ) ) ≤ 𝐵 )
160 128 130 38 131 159 letrd ⊢ ( 𝜑 → ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) − ( 2 · ( log ‘ 𝑌 ) ) ) ≤ 𝐵 )
161 124 126 38 lesubaddd ⊢ ( 𝜑 → ( ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) − ( 2 · ( log ‘ 𝑌 ) ) ) ≤ 𝐵 ↔ ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) ≤ ( 𝐵 + ( 2 · ( log ‘ 𝑌 ) ) ) ) )
162 160 161 mpbid ⊢ ( 𝜑 → ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) ≤ ( 𝐵 + ( 2 · ( log ‘ 𝑌 ) ) ) )
163 14 simp3d ⊢ ( 𝜑 → 𝑌 ≤ ( 𝐴 · 𝑋 ) )
164 90 81 logled ⊢ ( 𝜑 → ( 𝑌 ≤ ( 𝐴 · 𝑋 ) ↔ ( log ‘ 𝑌 ) ≤ ( log ‘ ( 𝐴 · 𝑋 ) ) ) )
165 163 164 mpbid ⊢ ( 𝜑 → ( log ‘ 𝑌 ) ≤ ( log ‘ ( 𝐴 · 𝑋 ) ) )
166 2pos ⊢ 0 < 2
167 33 166 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
168 167 a1i ⊢ ( 𝜑 → ( 2 ∈ ℝ ∧ 0 < 2 ) )
169 lemul2 ⊢ ( ( ( log ‘ 𝑌 ) ∈ ℝ ∧ ( log ‘ ( 𝐴 · 𝑋 ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( log ‘ 𝑌 ) ≤ ( log ‘ ( 𝐴 · 𝑋 ) ) ↔ ( 2 · ( log ‘ 𝑌 ) ) ≤ ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) )
170 91 82 168 169 syl3anc ⊢ ( 𝜑 → ( ( log ‘ 𝑌 ) ≤ ( log ‘ ( 𝐴 · 𝑋 ) ) ↔ ( 2 · ( log ‘ 𝑌 ) ) ≤ ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) )
171 165 170 mpbid ⊢ ( 𝜑 → ( 2 · ( log ‘ 𝑌 ) ) ≤ ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) )
172 126 84 38 171 leadd2dd ⊢ ( 𝜑 → ( 𝐵 + ( 2 · ( log ‘ 𝑌 ) ) ) ≤ ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) )
173 124 127 85 162 172 letrd ⊢ ( 𝜑 → ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) ≤ ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) )
174 100 85 90 ledivmul2d ⊢ ( 𝜑 → ( ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) / 𝑌 ) ≤ ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) ↔ ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) ≤ ( ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) · 𝑌 ) ) )
175 173 174 mpbid ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑌 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑌 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑌 / 𝑛 ) ) ) ) ≤ ( ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) · 𝑌 ) )
176 76 100 86 123 175 letrd ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) ≤ ( ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) · 𝑌 ) )
177 fveq2 ⊢ ( 𝑧 = 𝑋 → ( ψ ‘ 𝑧 ) = ( ψ ‘ 𝑋 ) )
178 fveq2 ⊢ ( 𝑧 = 𝑋 → ( log ‘ 𝑧 ) = ( log ‘ 𝑋 ) )
179 177 178 oveq12d ⊢ ( 𝑧 = 𝑋 → ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) = ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) )
180 fveq2 ⊢ ( 𝑧 = 𝑋 → ( ⌊ ‘ 𝑧 ) = ( ⌊ ‘ 𝑋 ) )
181 180 oveq2d ⊢ ( 𝑧 = 𝑋 → ( 1 ... ( ⌊ ‘ 𝑧 ) ) = ( 1 ... ( ⌊ ‘ 𝑋 ) ) )
182 simpl ⊢ ( ( 𝑧 = 𝑋 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝑧 = 𝑋 )
183 182 fvoveq1d ⊢ ( ( 𝑧 = 𝑋 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( ψ ‘ ( 𝑧 / 𝑛 ) ) = ( ψ ‘ ( 𝑋 / 𝑛 ) ) )
184 183 oveq2d ⊢ ( ( 𝑧 = 𝑋 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) = ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) )
185 181 184 sumeq12rdv ⊢ ( 𝑧 = 𝑋 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑧 / 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) )
186 139 185 syl5eq ⊢ ( 𝑧 = 𝑋 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) )
187 179 186 oveq12d ⊢ ( 𝑧 = 𝑋 → ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) = ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) )
188 id ⊢ ( 𝑧 = 𝑋 → 𝑧 = 𝑋 )
189 187 188 oveq12d ⊢ ( 𝑧 = 𝑋 → ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) = ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) )
190 178 oveq2d ⊢ ( 𝑧 = 𝑋 → ( 2 · ( log ‘ 𝑧 ) ) = ( 2 · ( log ‘ 𝑋 ) ) )
191 189 190 oveq12d ⊢ ( 𝑧 = 𝑋 → ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) = ( ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) − ( 2 · ( log ‘ 𝑋 ) ) ) )
192 191 fveq2d ⊢ ( 𝑧 = 𝑋 → ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) = ( abs ‘ ( ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) − ( 2 · ( log ‘ 𝑋 ) ) ) ) )
193 192 breq1d ⊢ ( 𝑧 = 𝑋 → ( ( abs ‘ ( ( ( ( ( ψ ‘ 𝑧 ) · ( log ‘ 𝑧 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑧 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑧 / 𝑚 ) ) ) ) / 𝑧 ) − ( 2 · ( log ‘ 𝑧 ) ) ) ) ≤ 𝐵 ↔ ( abs ‘ ( ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) − ( 2 · ( log ‘ 𝑋 ) ) ) ) ≤ 𝐵 ) )
194 elicopnf ⊢ ( 1 ∈ ℝ → ( 𝑋 ∈ ( 1 [,) +∞ ) ↔ ( 𝑋 ∈ ℝ ∧ 1 ≤ 𝑋 ) ) )
195 22 194 ax-mp ⊢ ( 𝑋 ∈ ( 1 [,) +∞ ) ↔ ( 𝑋 ∈ ℝ ∧ 1 ≤ 𝑋 ) )
196 9 154 195 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ ( 1 [,) +∞ ) )
197 193 4 196 rspcdva ⊢ ( 𝜑 → ( abs ‘ ( ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) − ( 2 · ( log ‘ 𝑋 ) ) ) ) ≤ 𝐵 )
198 88 30 rerpdivcld ⊢ ( 𝜑 → ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) ∈ ℝ )
199 198 78 38 absdifled ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) − ( 2 · ( log ‘ 𝑋 ) ) ) ) ≤ 𝐵 ↔ ( ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) ≤ ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) ∧ ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) ≤ ( ( 2 · ( log ‘ 𝑋 ) ) + 𝐵 ) ) ) )
200 197 199 mpbid ⊢ ( 𝜑 → ( ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) ≤ ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) ∧ ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) ≤ ( ( 2 · ( log ‘ 𝑋 ) ) + 𝐵 ) ) )
201 200 simpld ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) ≤ ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) )
202 79 88 30 lemuldivd ⊢ ( 𝜑 → ( ( ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) · 𝑋 ) ≤ ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) ↔ ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) ≤ ( ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) / 𝑋 ) ) )
203 201 202 mpbird ⊢ ( 𝜑 → ( ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) · 𝑋 ) ≤ ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) )
204 76 80 86 88 176 203 le2subd ⊢ ( 𝜑 → ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) − ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) ) ≤ ( ( ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) · 𝑌 ) − ( ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) · 𝑋 ) ) )
205 57 recnd ⊢ ( 𝜑 → ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑋 ) ) ∈ ℂ )
206 87 recnd ⊢ ( 𝜑 → ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) ∈ ℂ )
207 75 recnd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ∈ ℂ )
208 205 206 207 pnpcan2d ⊢ ( 𝜑 → ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) − ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) ) = ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑋 ) ) − ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) ) )
209 17 recnd ⊢ ( 𝜑 → ( ψ ‘ 𝑌 ) ∈ ℂ )
210 19 recnd ⊢ ( 𝜑 → ( ψ ‘ 𝑋 ) ∈ ℂ )
211 31 recnd ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℂ )
212 209 210 211 subdird ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑌 ) − ( ψ ‘ 𝑋 ) ) · ( log ‘ 𝑋 ) ) = ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑋 ) ) − ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) ) )
213 208 212 eqtr4d ⊢ ( 𝜑 → ( ( ( ( ψ ‘ 𝑌 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) − ( ( ( ψ ‘ 𝑋 ) · ( log ‘ 𝑋 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑋 / 𝑛 ) ) ) ) ) = ( ( ( ψ ‘ 𝑌 ) − ( ψ ‘ 𝑋 ) ) · ( log ‘ 𝑋 ) ) )
214 78 15 remulcld ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑌 ) ∈ ℝ )
215 214 recnd ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑌 ) ∈ ℂ )
216 38 43 readdcld ⊢ ( 𝜑 → ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) ∈ ℝ )
217 216 15 remulcld ⊢ ( 𝜑 → ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) ∈ ℝ )
218 217 recnd ⊢ ( 𝜑 → ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) ∈ ℂ )
219 78 9 remulcld ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) ∈ ℝ )
220 219 recnd ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) ∈ ℂ )
221 38 9 remulcld ⊢ ( 𝜑 → ( 𝐵 · 𝑋 ) ∈ ℝ )
222 221 recnd ⊢ ( 𝜑 → ( 𝐵 · 𝑋 ) ∈ ℂ )
223 222 negcld ⊢ ( 𝜑 → - ( 𝐵 · 𝑋 ) ∈ ℂ )
224 215 218 220 223 addsub4d ⊢ ( 𝜑 → ( ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑌 ) + ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) ) − ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) + - ( 𝐵 · 𝑋 ) ) ) = ( ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑌 ) − ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) ) + ( ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) − - ( 𝐵 · 𝑋 ) ) ) )
225 41 recnd ⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℂ )
226 1 30 relogmuld ⊢ ( 𝜑 → ( log ‘ ( 𝐴 · 𝑋 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝑋 ) ) )
227 225 211 226 comraddd ⊢ ( 𝜑 → ( log ‘ ( 𝐴 · 𝑋 ) ) = ( ( log ‘ 𝑋 ) + ( log ‘ 𝐴 ) ) )
228 227 oveq2d ⊢ ( 𝜑 → ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) = ( 2 · ( ( log ‘ 𝑋 ) + ( log ‘ 𝐴 ) ) ) )
229 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
230 229 211 225 adddid ⊢ ( 𝜑 → ( 2 · ( ( log ‘ 𝑋 ) + ( log ‘ 𝐴 ) ) ) = ( ( 2 · ( log ‘ 𝑋 ) ) + ( 2 · ( log ‘ 𝐴 ) ) ) )
231 228 230 eqtrd ⊢ ( 𝜑 → ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) = ( ( 2 · ( log ‘ 𝑋 ) ) + ( 2 · ( log ‘ 𝐴 ) ) ) )
232 231 oveq2d ⊢ ( 𝜑 → ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) = ( 𝐵 + ( ( 2 · ( log ‘ 𝑋 ) ) + ( 2 · ( log ‘ 𝐴 ) ) ) ) )
233 38 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
234 78 recnd ⊢ ( 𝜑 → ( 2 · ( log ‘ 𝑋 ) ) ∈ ℂ )
235 43 recnd ⊢ ( 𝜑 → ( 2 · ( log ‘ 𝐴 ) ) ∈ ℂ )
236 233 234 235 add12d ⊢ ( 𝜑 → ( 𝐵 + ( ( 2 · ( log ‘ 𝑋 ) ) + ( 2 · ( log ‘ 𝐴 ) ) ) ) = ( ( 2 · ( log ‘ 𝑋 ) ) + ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) ) )
237 232 236 eqtrd ⊢ ( 𝜑 → ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) = ( ( 2 · ( log ‘ 𝑋 ) ) + ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) ) )
238 237 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) · 𝑌 ) = ( ( ( 2 · ( log ‘ 𝑋 ) ) + ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) ) · 𝑌 ) )
239 216 recnd ⊢ ( 𝜑 → ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) ∈ ℂ )
240 15 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
241 234 239 240 adddird ⊢ ( 𝜑 → ( ( ( 2 · ( log ‘ 𝑋 ) ) + ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) ) · 𝑌 ) = ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑌 ) + ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) ) )
242 238 241 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) · 𝑌 ) = ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑌 ) + ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) ) )
243 9 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
244 234 233 243 subdird ⊢ ( 𝜑 → ( ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) · 𝑋 ) = ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) − ( 𝐵 · 𝑋 ) ) )
245 220 222 negsubd ⊢ ( 𝜑 → ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) + - ( 𝐵 · 𝑋 ) ) = ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) − ( 𝐵 · 𝑋 ) ) )
246 244 245 eqtr4d ⊢ ( 𝜑 → ( ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) · 𝑋 ) = ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) + - ( 𝐵 · 𝑋 ) ) )
247 242 246 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) · 𝑌 ) − ( ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) · 𝑋 ) ) = ( ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑌 ) + ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) ) − ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) + - ( 𝐵 · 𝑋 ) ) ) )
248 34 recnd ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℂ )
249 229 248 211 mul32d ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) = ( ( 2 · ( log ‘ 𝑋 ) ) · ( 𝑌 − 𝑋 ) ) )
250 234 240 243 subdid ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝑋 ) ) · ( 𝑌 − 𝑋 ) ) = ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑌 ) − ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) ) )
251 249 250 eqtrd ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) = ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑌 ) − ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) ) )
252 38 15 remulcld ⊢ ( 𝜑 → ( 𝐵 · 𝑌 ) ∈ ℝ )
253 252 recnd ⊢ ( 𝜑 → ( 𝐵 · 𝑌 ) ∈ ℂ )
254 44 recnd ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ∈ ℂ )
255 253 222 254 add32d ⊢ ( 𝜑 → ( ( ( 𝐵 · 𝑌 ) + ( 𝐵 · 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) = ( ( ( 𝐵 · 𝑌 ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) + ( 𝐵 · 𝑋 ) ) )
256 233 240 243 adddid ⊢ ( 𝜑 → ( 𝐵 · ( 𝑌 + 𝑋 ) ) = ( ( 𝐵 · 𝑌 ) + ( 𝐵 · 𝑋 ) ) )
257 256 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 · ( 𝑌 + 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) = ( ( ( 𝐵 · 𝑌 ) + ( 𝐵 · 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) )
258 233 235 240 adddird ⊢ ( 𝜑 → ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) = ( ( 𝐵 · 𝑌 ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) )
259 258 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) + ( 𝐵 · 𝑋 ) ) = ( ( ( 𝐵 · 𝑌 ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) + ( 𝐵 · 𝑋 ) ) )
260 255 257 259 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐵 · ( 𝑌 + 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) = ( ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) + ( 𝐵 · 𝑋 ) ) )
261 218 222 subnegd ⊢ ( 𝜑 → ( ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) − - ( 𝐵 · 𝑋 ) ) = ( ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) + ( 𝐵 · 𝑋 ) ) )
262 260 261 eqtr4d ⊢ ( 𝜑 → ( ( 𝐵 · ( 𝑌 + 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) = ( ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) − - ( 𝐵 · 𝑋 ) ) )
263 251 262 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( ( 𝐵 · ( 𝑌 + 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) ) = ( ( ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑌 ) − ( ( 2 · ( log ‘ 𝑋 ) ) · 𝑋 ) ) + ( ( ( 𝐵 + ( 2 · ( log ‘ 𝐴 ) ) ) · 𝑌 ) − - ( 𝐵 · 𝑋 ) ) ) )
264 224 247 263 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐵 + ( 2 · ( log ‘ ( 𝐴 · 𝑋 ) ) ) ) · 𝑌 ) − ( ( ( 2 · ( log ‘ 𝑋 ) ) − 𝐵 ) · 𝑋 ) ) = ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( ( 𝐵 · ( 𝑌 + 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) ) )
265 204 213 264 3brtr3d ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑌 ) − ( ψ ‘ 𝑋 ) ) · ( log ‘ 𝑋 ) ) ≤ ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( ( 𝐵 · ( 𝑌 + 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) ) )
266 49 9 remulcld ⊢ ( 𝜑 → ( ( 𝐵 · ( 𝐴 + 1 ) ) · 𝑋 ) ∈ ℝ )
267 52 9 remulcld ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) · 𝑋 ) ∈ ℝ )
268 15 11 9 163 leadd1dd ⊢ ( 𝜑 → ( 𝑌 + 𝑋 ) ≤ ( ( 𝐴 · 𝑋 ) + 𝑋 ) )
269 10 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
270 269 243 adddirp1d ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝑋 ) )
271 268 270 breqtrrd ⊢ ( 𝜑 → ( 𝑌 + 𝑋 ) ≤ ( ( 𝐴 + 1 ) · 𝑋 ) )
272 48 9 remulcld ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) · 𝑋 ) ∈ ℝ )
273 39 272 3 lemul2d ⊢ ( 𝜑 → ( ( 𝑌 + 𝑋 ) ≤ ( ( 𝐴 + 1 ) · 𝑋 ) ↔ ( 𝐵 · ( 𝑌 + 𝑋 ) ) ≤ ( 𝐵 · ( ( 𝐴 + 1 ) · 𝑋 ) ) ) )
274 271 273 mpbid ⊢ ( 𝜑 → ( 𝐵 · ( 𝑌 + 𝑋 ) ) ≤ ( 𝐵 · ( ( 𝐴 + 1 ) · 𝑋 ) ) )
275 48 recnd ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℂ )
276 233 275 243 mulassd ⊢ ( 𝜑 → ( ( 𝐵 · ( 𝐴 + 1 ) ) · 𝑋 ) = ( 𝐵 · ( ( 𝐴 + 1 ) · 𝑋 ) ) )
277 274 276 breqtrrd ⊢ ( 𝜑 → ( 𝐵 · ( 𝑌 + 𝑋 ) ) ≤ ( ( 𝐵 · ( 𝐴 + 1 ) ) · 𝑋 ) )
278 33 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
279 0le2 ⊢ 0 ≤ 2
280 279 a1i ⊢ ( 𝜑 → 0 ≤ 2 )
281 log1 ⊢ ( log ‘ 1 ) = 0
282 1rp ⊢ 1 ∈ ℝ+
283 logleb ⊢ ( ( 1 ∈ ℝ+ ∧ 𝐴 ∈ ℝ+ ) → ( 1 ≤ 𝐴 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ) )
284 282 1 283 sylancr ⊢ ( 𝜑 → ( 1 ≤ 𝐴 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ) )
285 2 284 mpbid ⊢ ( 𝜑 → ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) )
286 281 285 eqbrtrrid ⊢ ( 𝜑 → 0 ≤ ( log ‘ 𝐴 ) )
287 278 41 280 286 mulge0d ⊢ ( 𝜑 → 0 ≤ ( 2 · ( log ‘ 𝐴 ) ) )
288 15 11 43 287 163 lemul2ad ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ≤ ( ( 2 · ( log ‘ 𝐴 ) ) · ( 𝐴 · 𝑋 ) ) )
289 51 recnd ⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℂ )
290 289 225 243 mulassd ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) · 𝑋 ) = ( ( 2 · 𝐴 ) · ( ( log ‘ 𝐴 ) · 𝑋 ) ) )
291 229 269 225 243 mul4d ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · ( ( log ‘ 𝐴 ) · 𝑋 ) ) = ( ( 2 · ( log ‘ 𝐴 ) ) · ( 𝐴 · 𝑋 ) ) )
292 290 291 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) · 𝑋 ) = ( ( 2 · ( log ‘ 𝐴 ) ) · ( 𝐴 · 𝑋 ) ) )
293 288 292 breqtrrd ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ≤ ( ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) · 𝑋 ) )
294 40 44 266 267 277 293 le2addd ⊢ ( 𝜑 → ( ( 𝐵 · ( 𝑌 + 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) ≤ ( ( ( 𝐵 · ( 𝐴 + 1 ) ) · 𝑋 ) + ( ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) · 𝑋 ) ) )
295 5 oveq1i ⊢ ( 𝐶 · 𝑋 ) = ( ( ( 𝐵 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) ) · 𝑋 )
296 49 recnd ⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 + 1 ) ) ∈ ℂ )
297 52 recnd ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) ∈ ℂ )
298 296 297 243 adddird ⊢ ( 𝜑 → ( ( ( 𝐵 · ( 𝐴 + 1 ) ) + ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) ) · 𝑋 ) = ( ( ( 𝐵 · ( 𝐴 + 1 ) ) · 𝑋 ) + ( ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) · 𝑋 ) ) )
299 295 298 syl5eq ⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) = ( ( ( 𝐵 · ( 𝐴 + 1 ) ) · 𝑋 ) + ( ( ( 2 · 𝐴 ) · ( log ‘ 𝐴 ) ) · 𝑋 ) ) )
300 294 299 breqtrrd ⊢ ( 𝜑 → ( ( 𝐵 · ( 𝑌 + 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) ≤ ( 𝐶 · 𝑋 ) )
301 45 55 37 300 leadd2dd ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( ( 𝐵 · ( 𝑌 + 𝑋 ) ) + ( ( 2 · ( log ‘ 𝐴 ) ) · 𝑌 ) ) ) ≤ ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( 𝐶 · 𝑋 ) ) )
302 32 46 56 265 301 letrd ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑌 ) − ( ψ ‘ 𝑋 ) ) · ( log ‘ 𝑋 ) ) ≤ ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( 𝐶 · 𝑋 ) ) )
303 36 recnd ⊢ ( 𝜑 → ( 2 · ( 𝑌 − 𝑋 ) ) ∈ ℂ )
304 9 28 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℝ+ )
305 9 304 rerpdivcld ⊢ ( 𝜑 → ( 𝑋 / ( log ‘ 𝑋 ) ) ∈ ℝ )
306 54 305 remulcld ⊢ ( 𝜑 → ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) ∈ ℝ )
307 306 recnd ⊢ ( 𝜑 → ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) ∈ ℂ )
308 303 307 211 adddird ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 − 𝑋 ) ) + ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) ) · ( log ‘ 𝑋 ) ) = ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) · ( log ‘ 𝑋 ) ) ) )
309 54 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
310 305 recnd ⊢ ( 𝜑 → ( 𝑋 / ( log ‘ 𝑋 ) ) ∈ ℂ )
311 309 310 211 mulassd ⊢ ( 𝜑 → ( ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) · ( log ‘ 𝑋 ) ) = ( 𝐶 · ( ( 𝑋 / ( log ‘ 𝑋 ) ) · ( log ‘ 𝑋 ) ) ) )
312 304 rpne0d ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ≠ 0 )
313 243 211 312 divcan1d ⊢ ( 𝜑 → ( ( 𝑋 / ( log ‘ 𝑋 ) ) · ( log ‘ 𝑋 ) ) = 𝑋 )
314 313 oveq2d ⊢ ( 𝜑 → ( 𝐶 · ( ( 𝑋 / ( log ‘ 𝑋 ) ) · ( log ‘ 𝑋 ) ) ) = ( 𝐶 · 𝑋 ) )
315 311 314 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) · ( log ‘ 𝑋 ) ) = ( 𝐶 · 𝑋 ) )
316 315 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) · ( log ‘ 𝑋 ) ) ) = ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( 𝐶 · 𝑋 ) ) )
317 308 316 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 − 𝑋 ) ) + ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) ) · ( log ‘ 𝑋 ) ) = ( ( ( 2 · ( 𝑌 − 𝑋 ) ) · ( log ‘ 𝑋 ) ) + ( 𝐶 · 𝑋 ) ) )
318 302 317 breqtrrd ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑌 ) − ( ψ ‘ 𝑋 ) ) · ( log ‘ 𝑋 ) ) ≤ ( ( ( 2 · ( 𝑌 − 𝑋 ) ) + ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) ) · ( log ‘ 𝑋 ) ) )
319 36 306 readdcld ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 − 𝑋 ) ) + ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) ) ∈ ℝ )
320 20 319 304 lemul1d ⊢ ( 𝜑 → ( ( ( ψ ‘ 𝑌 ) − ( ψ ‘ 𝑋 ) ) ≤ ( ( 2 · ( 𝑌 − 𝑋 ) ) + ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) ) ↔ ( ( ( ψ ‘ 𝑌 ) − ( ψ ‘ 𝑋 ) ) · ( log ‘ 𝑋 ) ) ≤ ( ( ( 2 · ( 𝑌 − 𝑋 ) ) + ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) ) · ( log ‘ 𝑋 ) ) ) )
321 318 320 mpbird ⊢ ( 𝜑 → ( ( ψ ‘ 𝑌 ) − ( ψ ‘ 𝑋 ) ) ≤ ( ( 2 · ( 𝑌 − 𝑋 ) ) + ( 𝐶 · ( 𝑋 / ( log ‘ 𝑋 ) ) ) ) )