Metamath Proof Explorer

Theorem chpo1ubb

Description: The psi function is upper bounded by a linear term. (Contributed by Mario Carneiro, 31-May-2016)

Ref Expression
Assertion chpo1ubb ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ψ ‘ 𝑥 ) ≤ ( 𝑐 · 𝑥 )

Proof

Step Hyp Ref Expression
1 rpssre ⊢ ℝ+ ⊆ ℝ
2 1 a1i ⊢ ( ⊤ → ℝ+ ⊆ ℝ )
3 1red ⊢ ( ⊤ → 1 ∈ ℝ )
4 simpr ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
5 4 rpred ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
6 chpcl ⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
7 5 6 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
8 7 4 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
9 chpo1ub ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1)
10 9 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) )
11 8 10 o1lo1d ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ ≤𝑂(1) )
12 chpcl ⊢ ( 𝑦 ∈ ℝ → ( ψ ‘ 𝑦 ) ∈ ℝ )
13 12 ad2antrl ⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( ψ ‘ 𝑦 ) ∈ ℝ )
14 13 rehalfcld ⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( ( ψ ‘ 𝑦 ) / 2 ) ∈ ℝ )
15 5 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ℝ )
16 chpeq0 ⊢ ( 𝑥 ∈ ℝ → ( ( ψ ‘ 𝑥 ) = 0 ↔ 𝑥 < 2 ) )
17 15 16 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ψ ‘ 𝑥 ) = 0 ↔ 𝑥 < 2 ) )
18 17 biimpar ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑥 < 2 ) → ( ψ ‘ 𝑥 ) = 0 )
19 18 oveq1d ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑥 < 2 ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) = ( 0 / 𝑥 ) )
20 4 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ℝ+ )
21 20 rpcnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ℂ )
22 20 rpne0d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ≠ 0 )
23 21 22 div0d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 0 / 𝑥 ) = 0 )
24 13 ad2ant2r ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ψ ‘ 𝑦 ) ∈ ℝ )
25 2rp ⊢ 2 ∈ ℝ+
26 25 a1i ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 2 ∈ ℝ+ )
27 simprll ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ℝ )
28 chpge0 ⊢ ( 𝑦 ∈ ℝ → 0 ≤ ( ψ ‘ 𝑦 ) )
29 27 28 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( ψ ‘ 𝑦 ) )
30 24 26 29 divge0d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( ( ψ ‘ 𝑦 ) / 2 ) )
31 23 30 eqbrtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 0 / 𝑥 ) ≤ ( ( ψ ‘ 𝑦 ) / 2 ) )
32 31 adantr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑥 < 2 ) → ( 0 / 𝑥 ) ≤ ( ( ψ ‘ 𝑦 ) / 2 ) )
33 19 32 eqbrtrd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑥 < 2 ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ≤ ( ( ψ ‘ 𝑦 ) / 2 ) )
34 7 ad2antrr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 2 ≤ 𝑥 ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
35 24 adantr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 2 ≤ 𝑥 ) → ( ψ ‘ 𝑦 ) ∈ ℝ )
36 25 a1i ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 2 ≤ 𝑥 ) → 2 ∈ ℝ+ )
37 15 adantr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 2 ≤ 𝑥 ) → 𝑥 ∈ ℝ )
38 chpge0 ⊢ ( 𝑥 ∈ ℝ → 0 ≤ ( ψ ‘ 𝑥 ) )
39 37 38 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 2 ≤ 𝑥 ) → 0 ≤ ( ψ ‘ 𝑥 ) )
40 27 adantr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 2 ≤ 𝑥 ) → 𝑦 ∈ ℝ )
41 simprr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 < 𝑦 )
42 15 27 41 ltled ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ≤ 𝑦 )
43 42 adantr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 2 ≤ 𝑥 ) → 𝑥 ≤ 𝑦 )
44 chpwordi ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ) → ( ψ ‘ 𝑥 ) ≤ ( ψ ‘ 𝑦 ) )
45 37 40 43 44 syl3anc ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 2 ≤ 𝑥 ) → ( ψ ‘ 𝑥 ) ≤ ( ψ ‘ 𝑦 ) )
46 simpr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 2 ≤ 𝑥 ) → 2 ≤ 𝑥 )
47 34 35 36 37 39 45 46 lediv12ad ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 2 ≤ 𝑥 ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ≤ ( ( ψ ‘ 𝑦 ) / 2 ) )
48 2re ⊢ 2 ∈ ℝ
49 48 a1i ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 2 ∈ ℝ )
50 33 47 15 49 ltlecasei ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ≤ ( ( ψ ‘ 𝑦 ) / 2 ) )
51 2 3 8 11 14 50 lo1bddrp ⊢ ( ⊤ → ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ≤ 𝑐 )
52 51 mptru ⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ≤ 𝑐
53 simpr ⊢ ( ( 𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
54 53 rpred ⊢ ( ( 𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
55 54 6 syl ⊢ ( ( 𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
56 simpl ⊢ ( ( 𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → 𝑐 ∈ ℝ+ )
57 56 rpred ⊢ ( ( 𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → 𝑐 ∈ ℝ )
58 55 57 53 ledivmul2d ⊢ ( ( 𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) ≤ 𝑐 ↔ ( ψ ‘ 𝑥 ) ≤ ( 𝑐 · 𝑥 ) ) )
59 58 ralbidva ⊢ ( 𝑐 ∈ ℝ+ → ( ∀ 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ≤ 𝑐 ↔ ∀ 𝑥 ∈ ℝ+ ( ψ ‘ 𝑥 ) ≤ ( 𝑐 · 𝑥 ) ) )
60 59 rexbiia ⊢ ( ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ≤ 𝑐 ↔ ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ψ ‘ 𝑥 ) ≤ ( 𝑐 · 𝑥 ) )
61 52 60 mpbi ⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( ψ ‘ 𝑥 ) ≤ ( 𝑐 · 𝑥 )