chpo1ubb

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

		Ref	Expression
	Assertion	chpo1ubb	$⊢ \exists c \in ℝ^{+} \forall x \in ℝ^{+} ψ (x) \leq c x$

Proof

Step	Hyp	Ref	Expression
1		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
2	1	a1i	$⊢ ⊤ \to ℝ^{+} \subseteq ℝ$
3		1red	$⊢ ⊤ \to 1 \in ℝ$
4		simpr	$⊢ (⊤ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
5	4	rpred	$⊢ (⊤ \land x \in ℝ^{+}) \to x \in ℝ$
6		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
7	5 6	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to ψ (x) \in ℝ$
8	7 4	rerpdivcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x)}{x} \in ℝ$
9		chpo1ub	$⊢ (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$
10	9	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$
11	8 10	o1lo1d	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in \leq 𝑂 (1)$
12		chpcl	$⊢ y \in ℝ \to ψ (y) \in ℝ$
13	12	ad2antrl	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to ψ (y) \in ℝ$
14	13	rehalfcld	$⊢ (⊤ \land (y \in ℝ \land 1 \leq y)) \to \frac{ψ (y)}{2} \in ℝ$
15	5	adantr	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \in ℝ$
16		chpeq0	$⊢ x \in ℝ \to (ψ (x) = 0 \leftrightarrow x < 2)$
17	15 16	syl	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (ψ (x) = 0 \leftrightarrow x < 2)$
18	17	biimpar	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land x < 2) \to ψ (x) = 0$
19	18	oveq1d	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land x < 2) \to \frac{ψ (x)}{x} = \frac{0}{x}$
20	4	adantr	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \in ℝ^{+}$
21	20	rpcnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \in ℂ$
22	20	rpne0d	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \neq 0$
23	21 22	div0d	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{0}{x} = 0$
24	13	ad2ant2r	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ψ (y) \in ℝ$
25		2rp	$⊢ 2 \in ℝ^{+}$
26	25	a1i	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 2 \in ℝ^{+}$
27		simprll	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to y \in ℝ$
28		chpge0	$⊢ y \in ℝ \to 0 \leq ψ (y)$
29	27 28	syl	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq ψ (y)$
30	24 26 29	divge0d	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq \frac{ψ (y)}{2}$
31	23 30	eqbrtrd	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{0}{x} \leq \frac{ψ (y)}{2}$
32	31	adantr	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land x < 2) \to \frac{0}{x} \leq \frac{ψ (y)}{2}$
33	19 32	eqbrtrd	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land x < 2) \to \frac{ψ (x)}{x} \leq \frac{ψ (y)}{2}$
34	7	ad2antrr	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land 2 \leq x) \to ψ (x) \in ℝ$
35	24	adantr	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land 2 \leq x) \to ψ (y) \in ℝ$
36	25	a1i	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land 2 \leq x) \to 2 \in ℝ^{+}$
37	15	adantr	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land 2 \leq x) \to x \in ℝ$
38		chpge0	$⊢ x \in ℝ \to 0 \leq ψ (x)$
39	37 38	syl	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land 2 \leq x) \to 0 \leq ψ (x)$
40	27	adantr	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land 2 \leq x) \to y \in ℝ$
41		simprr	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x < y$
42	15 27 41	ltled	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \leq y$
43	42	adantr	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land 2 \leq x) \to x \leq y$
44		chpwordi	$⊢ (x \in ℝ \land y \in ℝ \land x \leq y) \to ψ (x) \leq ψ (y)$
45	37 40 43 44	syl3anc	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land 2 \leq x) \to ψ (x) \leq ψ (y)$
46		simpr	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land 2 \leq x) \to 2 \leq x$
47	34 35 36 37 39 45 46	lediv12ad	$⊢ (((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land 2 \leq x) \to \frac{ψ (x)}{x} \leq \frac{ψ (y)}{2}$
48		2re	$⊢ 2 \in ℝ$
49	48	a1i	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 2 \in ℝ$
50	33 47 15 49	ltlecasei	$⊢ ((⊤ \land x \in ℝ^{+}) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{ψ (x)}{x} \leq \frac{ψ (y)}{2}$
51	2 3 8 11 14 50	lo1bddrp	$⊢ ⊤ \to \exists c \in ℝ^{+} \forall x \in ℝ^{+} \frac{ψ (x)}{x} \leq c$
52	51	mptru	$⊢ \exists c \in ℝ^{+} \forall x \in ℝ^{+} \frac{ψ (x)}{x} \leq c$
53		simpr	$⊢ (c \in ℝ^{+} \land x \in ℝ^{+}) \to x \in ℝ^{+}$
54	53	rpred	$⊢ (c \in ℝ^{+} \land x \in ℝ^{+}) \to x \in ℝ$
55	54 6	syl	$⊢ (c \in ℝ^{+} \land x \in ℝ^{+}) \to ψ (x) \in ℝ$
56		simpl	$⊢ (c \in ℝ^{+} \land x \in ℝ^{+}) \to c \in ℝ^{+}$
57	56	rpred	$⊢ (c \in ℝ^{+} \land x \in ℝ^{+}) \to c \in ℝ$
58	55 57 53	ledivmul2d	$⊢ (c \in ℝ^{+} \land x \in ℝ^{+}) \to (\frac{ψ (x)}{x} \leq c \leftrightarrow ψ (x) \leq c x)$
59	58	ralbidva	$⊢ c \in ℝ^{+} \to (\forall x \in ℝ^{+} \frac{ψ (x)}{x} \leq c \leftrightarrow \forall x \in ℝ^{+} ψ (x) \leq c x)$
60	59	rexbiia	$⊢ \exists c \in ℝ^{+} \forall x \in ℝ^{+} \frac{ψ (x)}{x} \leq c \leftrightarrow \exists c \in ℝ^{+} \forall x \in ℝ^{+} ψ (x) \leq c x$
61	52 60	mpbi	$⊢ \exists c \in ℝ^{+} \forall x \in ℝ^{+} ψ (x) \leq c x$

Metamath Proof Explorer

Theorem chpo1ubb

Proof