Theorem chpo1ubb 26712

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

Assertion

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

Distinct variable group:   𝑥,𝑐

Proof of Theorem chpo1ubb

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rpssre 12817	. . . . 5 ⊢ ℝ+ ⊆ ℝ
2	1	a1i 11	. . . 4 ⊢ (⊤ → ℝ+ ⊆ ℝ)
3		1red 11056	. . . 4 ⊢ (⊤ → 1 ∈ ℝ)
4		simpr 485	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
5	4	rpred 12852	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
6		chpcl 26356	. . . . . 6 ⊢ (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
7	5, 6	syl 17	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℝ)
8	7, 4	rerpdivcld 12883	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
9		chpo1ub 26711	. . . . . 6 ⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)
10	9	a1i 11	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1))
11	8, 10	o1lo1d 15327	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ ≤𝑂(1))
12		chpcl 26356	. . . . . 6 ⊢ (𝑦 ∈ ℝ → (ψ‘𝑦) ∈ ℝ)
13	12	ad2antrl 725	. . . . 5 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → (ψ‘𝑦) ∈ ℝ)
14	13	rehalfcld 12300	. . . 4 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → ((ψ‘𝑦) / 2) ∈ ℝ)
15	5	adantr 481	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ)
16		chpeq0 26439	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → ((ψ‘𝑥) = 0 ↔ 𝑥 < 2))
17	15, 16	syl 17	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((ψ‘𝑥) = 0 ↔ 𝑥 < 2))
18	17	biimpar 478	. . . . . . 7 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → (ψ‘𝑥) = 0)
19	18	oveq1d 7332	. . . . . 6 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → ((ψ‘𝑥) / 𝑥) = (0 / 𝑥))
20	4	adantr 481	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ+)
21	20	rpcnd 12854	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℂ)
22	20	rpne0d 12857	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ≠ 0)
23	21, 22	div0d 11830	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (0 / 𝑥) = 0)
24	13	ad2ant2r 744	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (ψ‘𝑦) ∈ ℝ)
25		2rp 12815	. . . . . . . . . 10 ⊢ 2 ∈ ℝ+
26	25	a1i 11	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈ ℝ+)
27		simprll 776	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ)
28		chpge0 26358	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ → 0 ≤ (ψ‘𝑦))
29	27, 28	syl 17	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (ψ‘𝑦))
30	24, 26, 29	divge0d 12892	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ ((ψ‘𝑦) / 2))
31	23, 30	eqbrtrd 5109	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (0 / 𝑥) ≤ ((ψ‘𝑦) / 2))
32	31	adantr 481	. . . . . 6 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → (0 / 𝑥) ≤ ((ψ‘𝑦) / 2))
33	19, 32	eqbrtrd 5109	. . . . 5 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑥 < 2) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑦) / 2))
34	7	ad2antrr 723	. . . . . 6 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → (ψ‘𝑥) ∈ ℝ)
35	24	adantr 481	. . . . . 6 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → (ψ‘𝑦) ∈ ℝ)
36	25	a1i 11	. . . . . 6 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 2 ∈ ℝ+)
37	15	adantr 481	. . . . . 6 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 𝑥 ∈ ℝ)
38		chpge0 26358	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → 0 ≤ (ψ‘𝑥))
39	37, 38	syl 17	. . . . . 6 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 0 ≤ (ψ‘𝑥))
40	27	adantr 481	. . . . . . 7 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 𝑦 ∈ ℝ)
41		simprr 770	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 < 𝑦)
42	15, 27, 41	ltled 11203	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ≤ 𝑦)
43	42	adantr 481	. . . . . . 7 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 𝑥 ≤ 𝑦)
44		chpwordi 26389	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (ψ‘𝑥) ≤ (ψ‘𝑦))
45	37, 40, 43, 44	syl3anc 1370	. . . . . 6 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → (ψ‘𝑥) ≤ (ψ‘𝑦))
46		simpr 485	. . . . . 6 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → 2 ≤ 𝑥)
47	34, 35, 36, 37, 39, 45, 46	lediv12ad 12911	. . . . 5 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 2 ≤ 𝑥) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑦) / 2))
48		2re 12127	. . . . . 6 ⊢ 2 ∈ ℝ
49	48	a1i 11	. . . . 5 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈ ℝ)
50	33, 47, 15, 49	ltlecasei 11163	. . . 4 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((ψ‘𝑥) / 𝑥) ≤ ((ψ‘𝑦) / 2))
51	2, 3, 8, 11, 14, 50	lo1bddrp 15313	. . 3 ⊢ (⊤ → ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) / 𝑥) ≤ 𝑐)
52	51	mptru 1547	. 2 ⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) / 𝑥) ≤ 𝑐
53		simpr 485	. . . . . . 7 ⊢ ((𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
54	53	rpred 12852	. . . . . 6 ⊢ ((𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
55	54, 6	syl 17	. . . . 5 ⊢ ((𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℝ)
56		simpl 483	. . . . . 6 ⊢ ((𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → 𝑐 ∈ ℝ+)
57	56	rpred 12852	. . . . 5 ⊢ ((𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → 𝑐 ∈ ℝ)
58	55, 57, 53	ledivmul2d 12906	. . . 4 ⊢ ((𝑐 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) / 𝑥) ≤ 𝑐 ↔ (ψ‘𝑥) ≤ (𝑐 · 𝑥)))
59	58	ralbidva 3169	. . 3 ⊢ (𝑐 ∈ ℝ+ → (∀𝑥 ∈ ℝ+ ((ψ‘𝑥) / 𝑥) ≤ 𝑐 ↔ ∀𝑥 ∈ ℝ+ (ψ‘𝑥) ≤ (𝑐 · 𝑥)))
60	59	rexbiia 3092	. 2 ⊢ (∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) / 𝑥) ≤ 𝑐 ↔ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ (ψ‘𝑥) ≤ (𝑐 · 𝑥))
61	52, 60	mpbi 229	1 ⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ (ψ‘𝑥) ≤ (𝑐 · 𝑥)

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1540  ⊤wtru 1541   ∈ wcel 2105  ∀wral 3062  ∃wrex 3071   ⊆ wss 3897   class class class wbr 5087   ↦ cmpt 5170  ‘cfv 6466  (class class class)co 7317  ℝcr 10950  0cc0 10951  1c1 10952   · cmul 10956   < clt 11089   ≤ cle 11090   / cdiv 11712  2c2 12108  ℝ⁺crp 12810  𝑂(1)co1 15274  ψcchp 26325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-inf2 9477  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028  ax-pre-sup 11029  ax-addf 11030  ax-mulf 11031

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-se 5564  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-isom 6475  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-of 7575  df-om 7760  df-1st 7878  df-2nd 7879  df-supp 8027  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-2o 8347  df-oadd 8350  df-er 8548  df-map 8667  df-pm 8668  df-ixp 8736  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-fsupp 9206  df-fi 9247  df-sup 9278  df-inf 9279  df-oi 9346  df-dju 9737  df-card 9775  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-div 11713  df-nn 12054  df-2 12116  df-3 12117  df-4 12118  df-5 12119  df-6 12120  df-7 12121  df-8 12122  df-9 12123  df-n0 12314  df-xnn0 12386  df-z 12400  df-dec 12518  df-uz 12663  df-q 12769  df-rp 12811  df-xneg 12928  df-xadd 12929  df-xmul 12930  df-ioo 13163  df-ioc 13164  df-ico 13165  df-icc 13166  df-fz 13320  df-fzo 13463  df-fl 13592  df-mod 13670  df-seq 13802  df-exp 13863  df-fac 14068  df-bc 14097  df-hash 14125  df-shft 14857  df-cj 14889  df-re 14890  df-im 14891  df-sqrt 15025  df-abs 15026  df-limsup 15259  df-clim 15276  df-rlim 15277  df-o1 15278  df-lo1 15279  df-sum 15477  df-ef 15856  df-e 15857  df-sin 15858  df-cos 15859  df-pi 15861  df-dvds 16043  df-gcd 16281  df-prm 16454  df-pc 16615  df-struct 16925  df-sets 16942  df-slot 16960  df-ndx 16972  df-base 16990  df-ress 17019  df-plusg 17052  df-mulr 17053  df-starv 17054  df-sca 17055  df-vsca 17056  df-ip 17057  df-tset 17058  df-ple 17059  df-ds 17061  df-unif 17062  df-hom 17063  df-cco 17064  df-rest 17210  df-topn 17211  df-0g 17229  df-gsum 17230  df-topgen 17231  df-pt 17232  df-prds 17235  df-xrs 17290  df-qtop 17295  df-imas 17296  df-xps 17298  df-mre 17372  df-mrc 17373  df-acs 17375  df-mgm 18403  df-sgrp 18452  df-mnd 18463  df-submnd 18508  df-mulg 18777  df-cntz 18999  df-cmn 19463  df-psmet 20672  df-xmet 20673  df-met 20674  df-bl 20675  df-mopn 20676  df-fbas 20677  df-fg 20678  df-cnfld 20681  df-top 22126  df-topon 22143  df-topsp 22165  df-bases 22179  df-cld 22253  df-ntr 22254  df-cls 22255  df-nei 22332  df-lp 22370  df-perf 22371  df-cn 22461  df-cnp 22462  df-haus 22549  df-tx 22796  df-hmeo 22989  df-fil 23080  df-fm 23172  df-flim 23173  df-flf 23174  df-xms 23556  df-ms 23557  df-tms 23558  df-cncf 24124  df-limc 25113  df-dv 25114  df-log 25795  df-cxp 25796  df-cht 26329  df-vma 26330  df-chp 26331  df-ppi 26332

This theorem is referenced by:  pntrlog2bndlem3  26810