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 ⊢ φ → X ∈ − 1 +∞
Assertion 2xp3dxp2ge1d ⊢ φ → 1 ≤ 2 ⁢ X + 3 X + 2

Proof

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