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