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 
|- ( ph -> X e. ( -u 1 [,) +oo ) )
Assertion 2xp3dxp2ge1d 
|- ( ph -> 1 <_ ( ( ( 2 x. X ) + 3 ) / ( X + 2 ) ) )

Proof

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