This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infleinflem2

Description: Lemma for infleinf , when inf ( B , RR* , < ) = -oo . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses infleinflem2.a 
|- ( ph -> A C_ RR* )
infleinflem2.b 
|- ( ph -> B C_ RR* )
infleinflem2.r 
|- ( ph -> R e. RR )
infleinflem2.x 
|- ( ph -> X e. B )
infleinflem2.t 
|- ( ph -> X < ( R - 2 ) )
infleinflem2.z 
|- ( ph -> Z e. A )
infleinflem2.l 
|- ( ph -> Z <_ ( X +e 1 ) )
Assertion infleinflem2 
|- ( ph -> Z < R )

Proof

Step Hyp Ref Expression
1 infleinflem2.a 
 |-  ( ph -> A C_ RR* )
2 infleinflem2.b 
 |-  ( ph -> B C_ RR* )
3 infleinflem2.r 
 |-  ( ph -> R e. RR )
4 infleinflem2.x 
 |-  ( ph -> X e. B )
5 infleinflem2.t 
 |-  ( ph -> X < ( R - 2 ) )
6 infleinflem2.z 
 |-  ( ph -> Z e. A )
7 infleinflem2.l 
 |-  ( ph -> Z <_ ( X +e 1 ) )
8 3 adantr 
 |-  ( ( ph /\ Z = -oo ) -> R e. RR )
9 simpr 
 |-  ( ( ph /\ Z = -oo ) -> Z = -oo )
10 simpr 
 |-  ( ( R e. RR /\ Z = -oo ) -> Z = -oo )
11 mnflt 
 |-  ( R e. RR -> -oo < R )
12 11 adantr 
 |-  ( ( R e. RR /\ Z = -oo ) -> -oo < R )
13 10 12 eqbrtrd 
 |-  ( ( R e. RR /\ Z = -oo ) -> Z < R )
14 8 9 13 syl2anc 
 |-  ( ( ph /\ Z = -oo ) -> Z < R )
15 simpl 
 |-  ( ( ph /\ -. Z = -oo ) -> ph )
16 neqne 
 |-  ( -. Z = -oo -> Z =/= -oo )
17 16 adantl 
 |-  ( ( ph /\ -. Z = -oo ) -> Z =/= -oo )
18 3 adantr 
 |-  ( ( ph /\ Z =/= -oo ) -> R e. RR )
19 id 
 |-  ( ph -> ph )
20 2 sselda 
 |-  ( ( ph /\ X e. B ) -> X e. RR* )
21 19 4 20 syl2anc 
 |-  ( ph -> X e. RR* )
22 21 adantr 
 |-  ( ( ph /\ Z =/= -oo ) -> X e. RR* )
23 1 sselda 
 |-  ( ( ph /\ Z e. A ) -> Z e. RR* )
24 19 6 23 syl2anc 
 |-  ( ph -> Z e. RR* )
25 24 adantr 
 |-  ( ( ph /\ Z =/= -oo ) -> Z e. RR* )
26 simpr 
 |-  ( ( ph /\ Z =/= -oo ) -> Z =/= -oo )
27 pnfxr 
 |-  +oo e. RR*
28 27 a1i 
 |-  ( ph -> +oo e. RR* )
29 peano2rem 
 |-  ( R e. RR -> ( R - 1 ) e. RR )
30 29 rexrd 
 |-  ( R e. RR -> ( R - 1 ) e. RR* )
31 3 30 syl 
 |-  ( ph -> ( R - 1 ) e. RR* )
32 2 4 sseldd 
 |-  ( ph -> X e. RR* )
33 id 
 |-  ( X e. RR* -> X e. RR* )
34 1xr 
 |-  1 e. RR*
35 34 a1i 
 |-  ( X e. RR* -> 1 e. RR* )
36 33 35 xaddcld 
 |-  ( X e. RR* -> ( X +e 1 ) e. RR* )
37 32 36 syl 
 |-  ( ph -> ( X +e 1 ) e. RR* )
38 oveq1 
 |-  ( X = -oo -> ( X +e 1 ) = ( -oo +e 1 ) )
39 1re 
 |-  1 e. RR
40 renepnf 
 |-  ( 1 e. RR -> 1 =/= +oo )
41 39 40 ax-mp 
 |-  1 =/= +oo
42 xaddmnf2 
 |-  ( ( 1 e. RR* /\ 1 =/= +oo ) -> ( -oo +e 1 ) = -oo )
43 34 41 42 mp2an 
 |-  ( -oo +e 1 ) = -oo
44 43 a1i 
 |-  ( X = -oo -> ( -oo +e 1 ) = -oo )
45 38 44 eqtrd 
 |-  ( X = -oo -> ( X +e 1 ) = -oo )
46 45 adantl 
 |-  ( ( R e. RR /\ X = -oo ) -> ( X +e 1 ) = -oo )
47 29 mnfltd 
 |-  ( R e. RR -> -oo < ( R - 1 ) )
48 47 adantr 
 |-  ( ( R e. RR /\ X = -oo ) -> -oo < ( R - 1 ) )
49 46 48 eqbrtrd 
 |-  ( ( R e. RR /\ X = -oo ) -> ( X +e 1 ) < ( R - 1 ) )
50 49 adantlr 
 |-  ( ( ( R e. RR /\ X e. RR* ) /\ X = -oo ) -> ( X +e 1 ) < ( R - 1 ) )
51 50 3adantl3 
 |-  ( ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) /\ X = -oo ) -> ( X +e 1 ) < ( R - 1 ) )
52 simpl 
 |-  ( ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) /\ -. X = -oo ) -> ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) )
53 simpl2 
 |-  ( ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) /\ -. X = -oo ) -> X e. RR* )
54 neqne 
 |-  ( -. X = -oo -> X =/= -oo )
55 54 adantl 
 |-  ( ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) /\ -. X = -oo ) -> X =/= -oo )
56 simp2 
 |-  ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) -> X e. RR* )
57 27 a1i 
 |-  ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) -> +oo e. RR* )
58 id 
 |-  ( R e. RR -> R e. RR )
59 2re 
 |-  2 e. RR
60 59 a1i 
 |-  ( R e. RR -> 2 e. RR )
61 58 60 resubcld 
 |-  ( R e. RR -> ( R - 2 ) e. RR )
62 61 rexrd 
 |-  ( R e. RR -> ( R - 2 ) e. RR* )
63 62 3ad2ant1 
 |-  ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) -> ( R - 2 ) e. RR* )
64 simp3 
 |-  ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) -> X < ( R - 2 ) )
65 61 ltpnfd 
 |-  ( R e. RR -> ( R - 2 ) < +oo )
66 65 3ad2ant1 
 |-  ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) -> ( R - 2 ) < +oo )
67 56 63 57 64 66 xrlttrd 
 |-  ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) -> X < +oo )
68 56 57 67 xrltned 
 |-  ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) -> X =/= +oo )
69 68 adantr 
 |-  ( ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) /\ -. X = -oo ) -> X =/= +oo )
70 53 55 69 xrred 
 |-  ( ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) /\ -. X = -oo ) -> X e. RR )
71 id 
 |-  ( X e. RR -> X e. RR )
72 71 ad2antlr 
 |-  ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) -> X e. RR )
73 61 ad2antrr 
 |-  ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) -> ( R - 2 ) e. RR )
74 1red 
 |-  ( X e. RR -> 1 e. RR )
75 72 74 syl 
 |-  ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) -> 1 e. RR )
76 simpr 
 |-  ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) -> X < ( R - 2 ) )
77 72 73 75 76 ltadd1dd 
 |-  ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) -> ( X + 1 ) < ( ( R - 2 ) + 1 ) )
78 recn 
 |-  ( R e. RR -> R e. CC )
79 id 
 |-  ( R e. CC -> R e. CC )
80 2cnd 
 |-  ( R e. CC -> 2 e. CC )
81 1cnd 
 |-  ( R e. CC -> 1 e. CC )
82 79 80 81 subsubd 
 |-  ( R e. CC -> ( R - ( 2 - 1 ) ) = ( ( R - 2 ) + 1 ) )
83 2m1e1 
 |-  ( 2 - 1 ) = 1
84 83 oveq2i 
 |-  ( R - ( 2 - 1 ) ) = ( R - 1 )
85 84 a1i 
 |-  ( R e. CC -> ( R - ( 2 - 1 ) ) = ( R - 1 ) )
86 82 85 eqtr3d 
 |-  ( R e. CC -> ( ( R - 2 ) + 1 ) = ( R - 1 ) )
87 78 86 syl 
 |-  ( R e. RR -> ( ( R - 2 ) + 1 ) = ( R - 1 ) )
88 87 ad2antrr 
 |-  ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) -> ( ( R - 2 ) + 1 ) = ( R - 1 ) )
89 77 88 breqtrd 
 |-  ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) -> ( X + 1 ) < ( R - 1 ) )
90 71 74 rexaddd 
 |-  ( X e. RR -> ( X +e 1 ) = ( X + 1 ) )
91 90 breq1d 
 |-  ( X e. RR -> ( ( X +e 1 ) < ( R - 1 ) <-> ( X + 1 ) < ( R - 1 ) ) )
92 91 ad2antlr 
 |-  ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) -> ( ( X +e 1 ) < ( R - 1 ) <-> ( X + 1 ) < ( R - 1 ) ) )
93 89 92 mpbird 
 |-  ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) -> ( X +e 1 ) < ( R - 1 ) )
94 93 an32s 
 |-  ( ( ( R e. RR /\ X < ( R - 2 ) ) /\ X e. RR ) -> ( X +e 1 ) < ( R - 1 ) )
95 94 3adantl2 
 |-  ( ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) /\ X e. RR ) -> ( X +e 1 ) < ( R - 1 ) )
96 52 70 95 syl2anc 
 |-  ( ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) /\ -. X = -oo ) -> ( X +e 1 ) < ( R - 1 ) )
97 51 96 pm2.61dan 
 |-  ( ( R e. RR /\ X e. RR* /\ X < ( R - 2 ) ) -> ( X +e 1 ) < ( R - 1 ) )
98 3 32 5 97 syl3anc 
 |-  ( ph -> ( X +e 1 ) < ( R - 1 ) )
99 24 37 31 7 98 xrlelttrd 
 |-  ( ph -> Z < ( R - 1 ) )
100 29 ltpnfd 
 |-  ( R e. RR -> ( R - 1 ) < +oo )
101 3 100 syl 
 |-  ( ph -> ( R - 1 ) < +oo )
102 24 31 28 99 101 xrlttrd 
 |-  ( ph -> Z < +oo )
103 24 28 102 xrltned 
 |-  ( ph -> Z =/= +oo )
104 103 adantr 
 |-  ( ( ph /\ Z =/= -oo ) -> Z =/= +oo )
105 25 26 104 xrred 
 |-  ( ( ph /\ Z =/= -oo ) -> Z e. RR )
106 7 adantr 
 |-  ( ( ph /\ Z =/= -oo ) -> Z <_ ( X +e 1 ) )
107 simpl3 
 |-  ( ( ( Z e. RR /\ X e. RR* /\ Z <_ ( X +e 1 ) ) /\ X = -oo ) -> Z <_ ( X +e 1 ) )
108 45 adantl 
 |-  ( ( Z e. RR /\ X = -oo ) -> ( X +e 1 ) = -oo )
109 mnflt 
 |-  ( Z e. RR -> -oo < Z )
110 109 adantr 
 |-  ( ( Z e. RR /\ X = -oo ) -> -oo < Z )
111 108 110 eqbrtrd 
 |-  ( ( Z e. RR /\ X = -oo ) -> ( X +e 1 ) < Z )
112 mnfxr 
 |-  -oo e. RR*
113 108 112 eqeltrdi 
 |-  ( ( Z e. RR /\ X = -oo ) -> ( X +e 1 ) e. RR* )
114 rexr 
 |-  ( Z e. RR -> Z e. RR* )
115 114 adantr 
 |-  ( ( Z e. RR /\ X = -oo ) -> Z e. RR* )
116 113 115 xrltnled 
 |-  ( ( Z e. RR /\ X = -oo ) -> ( ( X +e 1 ) < Z <-> -. Z <_ ( X +e 1 ) ) )
117 111 116 mpbid 
 |-  ( ( Z e. RR /\ X = -oo ) -> -. Z <_ ( X +e 1 ) )
118 117 3ad2antl1 
 |-  ( ( ( Z e. RR /\ X e. RR* /\ Z <_ ( X +e 1 ) ) /\ X = -oo ) -> -. Z <_ ( X +e 1 ) )
119 107 118 pm2.65da 
 |-  ( ( Z e. RR /\ X e. RR* /\ Z <_ ( X +e 1 ) ) -> -. X = -oo )
120 119 neqned 
 |-  ( ( Z e. RR /\ X e. RR* /\ Z <_ ( X +e 1 ) ) -> X =/= -oo )
121 105 22 106 120 syl3anc 
 |-  ( ( ph /\ Z =/= -oo ) -> X =/= -oo )
122 3 21 5 68 syl3anc 
 |-  ( ph -> X =/= +oo )
123 122 adantr 
 |-  ( ( ph /\ Z =/= -oo ) -> X =/= +oo )
124 22 121 123 xrred 
 |-  ( ( ph /\ Z =/= -oo ) -> X e. RR )
125 5 adantr 
 |-  ( ( ph /\ Z =/= -oo ) -> X < ( R - 2 ) )
126 18 124 125 jca31 
 |-  ( ( ph /\ Z =/= -oo ) -> ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) )
127 simplr 
 |-  ( ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) /\ Z <_ ( X +e 1 ) ) -> Z e. RR )
128 simp-4r 
 |-  ( ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) /\ Z <_ ( X +e 1 ) ) -> X e. RR )
129 71 74 readdcld 
 |-  ( X e. RR -> ( X + 1 ) e. RR )
130 90 129 eqeltrd 
 |-  ( X e. RR -> ( X +e 1 ) e. RR )
131 128 130 syl 
 |-  ( ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) /\ Z <_ ( X +e 1 ) ) -> ( X +e 1 ) e. RR )
132 58 ad4antr 
 |-  ( ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) /\ Z <_ ( X +e 1 ) ) -> R e. RR )
133 simpr 
 |-  ( ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) /\ Z <_ ( X +e 1 ) ) -> Z <_ ( X +e 1 ) )
134 130 ad3antlr 
 |-  ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) -> ( X +e 1 ) e. RR )
135 29 ad3antrrr 
 |-  ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) -> ( R - 1 ) e. RR )
136 58 ad3antrrr 
 |-  ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) -> R e. RR )
137 93 adantr 
 |-  ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) -> ( X +e 1 ) < ( R - 1 ) )
138 136 ltm1d 
 |-  ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) -> ( R - 1 ) < R )
139 134 135 136 137 138 lttrd 
 |-  ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) -> ( X +e 1 ) < R )
140 139 adantr 
 |-  ( ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) /\ Z <_ ( X +e 1 ) ) -> ( X +e 1 ) < R )
141 127 131 132 133 140 lelttrd 
 |-  ( ( ( ( ( R e. RR /\ X e. RR ) /\ X < ( R - 2 ) ) /\ Z e. RR ) /\ Z <_ ( X +e 1 ) ) -> Z < R )
142 126 105 106 141 syl21anc 
 |-  ( ( ph /\ Z =/= -oo ) -> Z < R )
143 15 17 142 syl2anc 
 |-  ( ( ph /\ -. Z = -oo ) -> Z < R )
144 14 143 pm2.61dan 
 |-  ( ph -> Z < R )