Theorem chto1ub

Description: The theta function is upper bounded by a linear term. Corollary of chtub . (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	chto1ub	$$⊢\left(x\in {ℝ}^{+}⟼\frac{\theta \left(x\right)}{x}\right)\in 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
2	1	a1i	$$⊢\top \to {ℝ}^{+}\subseteq ℝ$$
3		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
4		chtcl	$$⊢x\in ℝ\to \theta \left(x\right)\in ℝ$$
5	3 4	syl	$$⊢x\in {ℝ}^{+}\to \theta \left(x\right)\in ℝ$$
6		rerpdivcl	$$⊢\left(\theta \left(x\right)\in ℝ\wedge x\in {ℝ}^{+}\right)\to \frac{\theta \left(x\right)}{x}\in ℝ$$
7	5 6	mpancom	$$⊢x\in {ℝ}^{+}\to \frac{\theta \left(x\right)}{x}\in ℝ$$
8	7	recnd	$$⊢x\in {ℝ}^{+}\to \frac{\theta \left(x\right)}{x}\in ℂ$$
9	8	adantl	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \frac{\theta \left(x\right)}{x}\in ℂ$$
10		3re	$$⊢3\in ℝ$$
11	10	a1i	$$⊢\top \to 3\in ℝ$$
12		2rp	$$⊢2\in {ℝ}^{+}$$
13		relogcl	$$⊢2\in {ℝ}^{+}\to \log 2\in ℝ$$
14	12 13	ax-mp	$$⊢\log 2\in ℝ$$
15		2re	$$⊢2\in ℝ$$
16	14 15	remulcli	$$⊢\log 2\cdot 2\in ℝ$$
17	16	a1i	$$⊢\top \to \log 2\cdot 2\in ℝ$$
18		chtge0	$$⊢x\in ℝ\to 0\le \theta \left(x\right)$$
19	3 18	syl	$$⊢x\in {ℝ}^{+}\to 0\le \theta \left(x\right)$$
20		rpregt0	$$⊢x\in {ℝ}^{+}\to \left(x\in ℝ\wedge 0<x\right)$$
21		divge0	$$⊢\left(\left(\theta \left(x\right)\in ℝ\wedge 0\le \theta \left(x\right)\right)\wedge \left(x\in ℝ\wedge 0<x\right)\right)\to 0\le \frac{\theta \left(x\right)}{x}$$
22	5 19 20 21	syl21anc	$$⊢x\in {ℝ}^{+}\to 0\le \frac{\theta \left(x\right)}{x}$$
23	7 22	absidd	$$⊢x\in {ℝ}^{+}\to \left|\frac{\theta \left(x\right)}{x}\right|=\frac{\theta \left(x\right)}{x}$$
24	23	adantr	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \left|\frac{\theta \left(x\right)}{x}\right|=\frac{\theta \left(x\right)}{x}$$
25	7	adantr	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \frac{\theta \left(x\right)}{x}\in ℝ$$
26	16	a1i	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \log 2\cdot 2\in ℝ$$
27	5	adantr	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \theta \left(x\right)\in ℝ$$
28	3	adantr	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to x\in ℝ$$
29		remulcl	$$⊢\left(2\in ℝ\wedge x\in ℝ\right)\to 2x\in ℝ$$
30	15 28 29	sylancr	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to 2x\in ℝ$$
31		resubcl	$$⊢\left(2x\in ℝ\wedge 3\in ℝ\right)\to 2x-3\in ℝ$$
32	30 10 31	sylancl	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to 2x-3\in ℝ$$
33		remulcl	$$⊢\left(\log 2\in ℝ\wedge 2x-3\in ℝ\right)\to \log 2\left(2x-3\right)\in ℝ$$
34	14 32 33	sylancr	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \log 2\left(2x-3\right)\in ℝ$$
35		remulcl	$$⊢\left(\log 2\in ℝ\wedge 2x\in ℝ\right)\to \log 22x\in ℝ$$
36	14 30 35	sylancr	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \log 22x\in ℝ$$
37	15	a1i	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to 2\in ℝ$$
38	10	a1i	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to 3\in ℝ$$
39		2lt3	$$⊢2<3$$
40	39	a1i	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to 2<3$$
41		simpr	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to 3\le x$$
42	37 38 28 40 41	ltletrd	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to 2<x$$
43		chtub	$$⊢\left(x\in ℝ\wedge 2<x\right)\to \theta \left(x\right)<\log 2\left(2x-3\right)$$
44	28 42 43	syl2anc	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \theta \left(x\right)<\log 2\left(2x-3\right)$$
45		3rp	$$⊢3\in {ℝ}^{+}$$
46		ltsubrp	$$⊢\left(2x\in ℝ\wedge 3\in {ℝ}^{+}\right)\to 2x-3<2x$$
47	30 45 46	sylancl	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to 2x-3<2x$$
48		1lt2	$$⊢1<2$$
49		rplogcl	$$⊢\left(2\in ℝ\wedge 1<2\right)\to \log 2\in {ℝ}^{+}$$
50	15 48 49	mp2an	$$⊢\log 2\in {ℝ}^{+}$$
51		elrp	$$⊢\log 2\in {ℝ}^{+}\leftrightarrow \left(\log 2\in ℝ\wedge 0<\log 2\right)$$
52	50 51	mpbi	$$⊢\left(\log 2\in ℝ\wedge 0<\log 2\right)$$
53	52	a1i	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \left(\log 2\in ℝ\wedge 0<\log 2\right)$$
54		ltmul2	$$⊢\left(2x-3\in ℝ\wedge 2x\in ℝ\wedge \left(\log 2\in ℝ\wedge 0<\log 2\right)\right)\to \left(2x-3<2x\leftrightarrow \log 2\left(2x-3\right)<\log 22x\right)$$
55	32 30 53 54	syl3anc	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \left(2x-3<2x\leftrightarrow \log 2\left(2x-3\right)<\log 22x\right)$$
56	47 55	mpbid	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \log 2\left(2x-3\right)<\log 22x$$
57	27 34 36 44 56	lttrd	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \theta \left(x\right)<\log 22x$$
58	14	recni	$$⊢\log 2\in ℂ$$
59	58	a1i	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \log 2\in ℂ$$
60		2cnd	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to 2\in ℂ$$
61	3	recnd	$$⊢x\in {ℝ}^{+}\to x\in ℂ$$
62	61	adantr	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to x\in ℂ$$
63	59 60 62	mulassd	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \log 2\cdot 2x=\log 22x$$
64	57 63	breqtrrd	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \theta \left(x\right)<\log 2\cdot 2x$$
65	20	adantr	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \left(x\in ℝ\wedge 0<x\right)$$
66		ltdivmul2	$$⊢\left(\theta \left(x\right)\in ℝ\wedge \log 2\cdot 2\in ℝ\wedge \left(x\in ℝ\wedge 0<x\right)\right)\to \left(\frac{\theta \left(x\right)}{x}<\log 2\cdot 2\leftrightarrow \theta \left(x\right)<\log 2\cdot 2x\right)$$
67	27 26 65 66	syl3anc	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \left(\frac{\theta \left(x\right)}{x}<\log 2\cdot 2\leftrightarrow \theta \left(x\right)<\log 2\cdot 2x\right)$$
68	64 67	mpbird	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \frac{\theta \left(x\right)}{x}<\log 2\cdot 2$$
69	25 26 68	ltled	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \frac{\theta \left(x\right)}{x}\le \log 2\cdot 2$$
70	24 69	eqbrtrd	$$⊢\left(x\in {ℝ}^{+}\wedge 3\le x\right)\to \left|\frac{\theta \left(x\right)}{x}\right|\le \log 2\cdot 2$$
71	70	adantl	$$⊢\left(\top \wedge \left(x\in {ℝ}^{+}\wedge 3\le x\right)\right)\to \left|\frac{\theta \left(x\right)}{x}\right|\le \log 2\cdot 2$$
72	2 9 11 17 71	elo1d	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\frac{\theta \left(x\right)}{x}\right)\in 𝑂\left(1\right)$$
73	72	mptru	$$⊢\left(x\in {ℝ}^{+}⟼\frac{\theta \left(x\right)}{x}\right)\in 𝑂\left(1\right)$$