Metamath Proof Explorer

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 ) ) )