Theorem 2xp3dxp2ge1d

Description: 2x+3 is greater than or equal to x+2 for x >= -1, a deduction version (Contributed by metakunt, 21-Apr-2024)

	Ref	Expression
Hypothesis	2xp3dxp2ge1d.1	$$⊢\phi \to X\in \left[-1,\mathrm{+\infty }\right)$$
Assertion	2xp3dxp2ge1d	$$⊢\phi \to 1\le \frac{2X+3}{X+2}$$

Proof

Step	Hyp	Ref	Expression
1		2xp3dxp2ge1d.1	$$⊢\phi \to X\in \left[-1,\mathrm{+\infty }\right)$$
2		neg1rr	$$⊢-1\in ℝ$$
3		elicopnf	$$⊢-1\in ℝ\to \left(X\in \left[-1,\mathrm{+\infty }\right)\leftrightarrow \left(X\in ℝ\wedge -1\le X\right)\right)$$
4	2 3	ax-mp	$$⊢X\in \left[-1,\mathrm{+\infty }\right)\leftrightarrow \left(X\in ℝ\wedge -1\le X\right)$$
5	1 4	sylib	$$⊢\phi \to \left(X\in ℝ\wedge -1\le X\right)$$
6	5	simpld	$$⊢\phi \to X\in ℝ$$
7		2re	$$⊢2\in ℝ$$
8		readdcl	$$⊢\left(X\in ℝ\wedge 2\in ℝ\right)\to X+2\in ℝ$$
9	7 8	mpan2	$$⊢X\in ℝ\to X+2\in ℝ$$
10	6 9	syl	$$⊢\phi \to X+2\in ℝ$$
11		neg1cn	$$⊢-1\in ℂ$$
12		2cn	$$⊢2\in ℂ$$
13		addcom	$$⊢\left(-1\in ℂ\wedge 2\in ℂ\right)\to -1+2=2+-1$$
14	11 12 13	mp2an	$$⊢-1+2=2+-1$$
15		ax-1cn	$$⊢1\in ℂ$$
16		negsub	$$⊢\left(2\in ℂ\wedge 1\in ℂ\right)\to 2+-1=2-1$$
17	12 15 16	mp2an	$$⊢2+-1=2-1$$
18		2m1e1	$$⊢2-1=1$$
19	14 17 18	3eqtri	$$⊢-1+2=1$$
20	5	simprd	$$⊢\phi \to -1\le X$$
21		leadd1	$$⊢\left(-1\in ℝ\wedge X\in ℝ\wedge 2\in ℝ\right)\to \left(-1\le X\leftrightarrow -1+2\le X+2\right)$$
22	2 7 21	mp3an13	$$⊢X\in ℝ\to \left(-1\le X\leftrightarrow -1+2\le X+2\right)$$
23	6 22	syl	$$⊢\phi \to \left(-1\le X\leftrightarrow -1+2\le X+2\right)$$
24	20 23	mpbid	$$⊢\phi \to -1+2\le X+2$$
25	19 24	eqbrtrrid	$$⊢\phi \to 1\le X+2$$
26		0lt1	$$⊢0<1$$
27	25 26	jctil	$$⊢\phi \to \left(0<1\wedge 1\le X+2\right)$$
28		0re	$$⊢0\in ℝ$$
29		1re	$$⊢1\in ℝ$$
30		ltletr	$$⊢\left(0\in ℝ\wedge 1\in ℝ\wedge X+2\in ℝ\right)\to \left(\left(0<1\wedge 1\le X+2\right)\to 0<X+2\right)$$
31	28 29 30	mp3an12	$$⊢X+2\in ℝ\to \left(\left(0<1\wedge 1\le X+2\right)\to 0<X+2\right)$$
32	10 31	syl	$$⊢\phi \to \left(\left(0<1\wedge 1\le X+2\right)\to 0<X+2\right)$$
33	27 32	mpd	$$⊢\phi \to 0<X+2$$
34	10 33	jca	$$⊢\phi \to \left(X+2\in ℝ\wedge 0<X+2\right)$$
35		elrp	$$⊢X+2\in {ℝ}^{+}\leftrightarrow \left(X+2\in ℝ\wedge 0<X+2\right)$$
36	35	imbi2i	$$⊢\left(\phi \to X+2\in {ℝ}^{+}\right)\leftrightarrow \left(\phi \to \left(X+2\in ℝ\wedge 0<X+2\right)\right)$$
37	34 36	mpbir	$$⊢\phi \to X+2\in {ℝ}^{+}$$
38		remulcl	$$⊢\left(2\in ℝ\wedge X\in ℝ\right)\to 2X\in ℝ$$
39	7 38	mpan	$$⊢X\in ℝ\to 2X\in ℝ$$
40	6 39	syl	$$⊢\phi \to 2X\in ℝ$$
41		3re	$$⊢3\in ℝ$$
42		readdcl	$$⊢\left(2X\in ℝ\wedge 3\in ℝ\right)\to 2X+3\in ℝ$$
43	41 42	mpan2	$$⊢2X\in ℝ\to 2X+3\in ℝ$$
44	40 43	syl	$$⊢\phi \to 2X+3\in ℝ$$
45	7	a1i	$$⊢\phi \to 2\in ℝ$$
46		1red	$$⊢\phi \to 1\in ℝ$$
47	40 46	readdcld	$$⊢\phi \to 2X+1\in ℝ$$
48		recn	$$⊢X\in ℝ\to X\in ℂ$$
49		addrid	$$⊢X\in ℂ\to X+0=X$$
50	48 49	syl	$$⊢X\in ℝ\to X+0=X$$
51	6 50	syl	$$⊢\phi \to X+0=X$$
52	11 15	addcomi	$$⊢-1+1=1+-1$$
53	15	negidi	$$⊢1+-1=0$$
54	52 53	eqtri	$$⊢-1+1=0$$
55		leadd1	$$⊢\left(-1\in ℝ\wedge X\in ℝ\wedge 1\in ℝ\right)\to \left(-1\le X\leftrightarrow -1+1\le X+1\right)$$
56	2 29 55	mp3an13	$$⊢X\in ℝ\to \left(-1\le X\leftrightarrow -1+1\le X+1\right)$$
57	6 56	syl	$$⊢\phi \to \left(-1\le X\leftrightarrow -1+1\le X+1\right)$$
58	20 57	mpbid	$$⊢\phi \to -1+1\le X+1$$
59	54 58	eqbrtrrid	$$⊢\phi \to 0\le X+1$$
60		readdcl	$$⊢\left(X\in ℝ\wedge 1\in ℝ\right)\to X+1\in ℝ$$
61	29 60	mpan2	$$⊢X\in ℝ\to X+1\in ℝ$$
62	6 61	syl	$$⊢\phi \to X+1\in ℝ$$
63	62 6	jca	$$⊢\phi \to \left(X+1\in ℝ\wedge X\in ℝ\right)$$
64		leadd2	$$⊢\left(0\in ℝ\wedge X+1\in ℝ\wedge X\in ℝ\right)\to \left(0\le X+1\leftrightarrow X+0\le X+X+1\right)$$
65	28 64	mp3an1	$$⊢\left(X+1\in ℝ\wedge X\in ℝ\right)\to \left(0\le X+1\leftrightarrow X+0\le X+X+1\right)$$
66	63 65	syl	$$⊢\phi \to \left(0\le X+1\leftrightarrow X+0\le X+X+1\right)$$
67	59 66	mpbid	$$⊢\phi \to X+0\le X+X+1$$
68	6 48	syl	$$⊢\phi \to X\in ℂ$$
69	68	2timesd	$$⊢\phi \to 2X=X+X$$
70	69	oveq1d	$$⊢\phi \to 2X+1=X+X+1$$
71		addass	$$⊢\left(X\in ℂ\wedge X\in ℂ\wedge 1\in ℂ\right)\to X+X+1=X+X+1$$
72	15 71	mp3an3	$$⊢\left(X\in ℂ\wedge X\in ℂ\right)\to X+X+1=X+X+1$$
73	72	anidms	$$⊢X\in ℂ\to X+X+1=X+X+1$$
74	68 73	syl	$$⊢\phi \to X+X+1=X+X+1$$
75	70 74	eqtrd	$$⊢\phi \to 2X+1=X+X+1$$
76	67 75	breqtrrd	$$⊢\phi \to X+0\le 2X+1$$
77	51 76	eqbrtrrd	$$⊢\phi \to X\le 2X+1$$
78	45	leidd	$$⊢\phi \to 2\le 2$$
79	6 45 47 45 77 78	le2addd	$$⊢\phi \to X+2\le 2X+1+2$$
80	40	recnd	$$⊢\phi \to 2X\in ℂ$$
81	15	a1i	$$⊢\phi \to 1\in ℂ$$
82	12	a1i	$$⊢\phi \to 2\in ℂ$$
83	80 81 82	addassd	$$⊢\phi \to 2X+1+2=2X+1+2$$
84		1p2e3	$$⊢1+2=3$$
85		oveq2	$$⊢1+2=3\to 2X+1+2=2X+3$$
86	84 85	ax-mp	$$⊢2X+1+2=2X+3$$
87	83 86	eqtrdi	$$⊢\phi \to 2X+1+2=2X+3$$
88	79 87	breqtrd	$$⊢\phi \to X+2\le 2X+3$$
89	37 44 88	3jca	$$⊢\phi \to \left(X+2\in {ℝ}^{+}\wedge 2X+3\in ℝ\wedge X+2\le 2X+3\right)$$
90		divge1	$$⊢\left(X+2\in {ℝ}^{+}\wedge 2X+3\in ℝ\wedge X+2\le 2X+3\right)\to 1\le \frac{2X+3}{X+2}$$
91	89 90	syl	$$⊢\phi \to 1\le \frac{2X+3}{X+2}$$