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	⊢ ( 𝜑 → 𝑋 ∈ ( - 1 [,) +∞ ) )
Assertion	2xp3dxp2ge1d	⊢ ( 𝜑 → 1 ≤ ( ( ( 2 · 𝑋 ) + 3 ) / ( 𝑋 + 2 ) ) )

Proof

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