Metamath Proof Explorer

Theorem iooelexlt

Description: An element of an open interval is not its smallest element. (Contributed by ML, 2-Aug-2020)

Ref Expression
Assertion iooelexlt 
|- ( X e. ( A (,) B ) -> E. y e. ( A (,) B ) y < X )

Proof

Step Hyp Ref Expression
1 eliooxr 
 |-  ( X e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* ) )
2 1 simpld 
 |-  ( X e. ( A (,) B ) -> A e. RR* )
3 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
4 19.3v 
 |-  ( A. y ( X e. ( A (,) B ) /\ A e. RR ) <-> ( X e. ( A (,) B ) /\ A e. RR ) )
5 ovex 
 |-  ( ( A + X ) / 2 ) e. _V
6 nfcv 
 |-  F/_ y ( ( A + X ) / 2 )
7 nfre1 
 |-  F/ y E. y e. ( A (,) B ) y < X
8 elioore 
 |-  ( X e. ( A (,) B ) -> X e. RR )
9 readdcl 
 |-  ( ( A e. RR /\ X e. RR ) -> ( A + X ) e. RR )
10 9 rehalfcld 
 |-  ( ( A e. RR /\ X e. RR ) -> ( ( A + X ) / 2 ) e. RR )
11 8 10 sylan2 
 |-  ( ( A e. RR /\ X e. ( A (,) B ) ) -> ( ( A + X ) / 2 ) e. RR )
12 11 ancoms 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> ( ( A + X ) / 2 ) e. RR )
13 12 rexrd 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> ( ( A + X ) / 2 ) e. RR* )
14 eliooord 
 |-  ( X e. ( A (,) B ) -> ( A < X /\ X < B ) )
15 14 simpld 
 |-  ( X e. ( A (,) B ) -> A < X )
16 15 adantr 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> A < X )
17 avglt1 
 |-  ( ( A e. RR /\ X e. RR ) -> ( A < X <-> A < ( ( A + X ) / 2 ) ) )
18 8 17 sylan2 
 |-  ( ( A e. RR /\ X e. ( A (,) B ) ) -> ( A < X <-> A < ( ( A + X ) / 2 ) ) )
19 18 ancoms 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> ( A < X <-> A < ( ( A + X ) / 2 ) ) )
20 16 19 mpbid 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> A < ( ( A + X ) / 2 ) )
21 8 rexrd 
 |-  ( X e. ( A (,) B ) -> X e. RR* )
22 21 adantr 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> X e. RR* )
23 1 simprd 
 |-  ( X e. ( A (,) B ) -> B e. RR* )
24 23 adantr 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> B e. RR* )
25 avglt2 
 |-  ( ( A e. RR /\ X e. RR ) -> ( A < X <-> ( ( A + X ) / 2 ) < X ) )
26 8 25 sylan2 
 |-  ( ( A e. RR /\ X e. ( A (,) B ) ) -> ( A < X <-> ( ( A + X ) / 2 ) < X ) )
27 26 ancoms 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> ( A < X <-> ( ( A + X ) / 2 ) < X ) )
28 16 27 mpbid 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> ( ( A + X ) / 2 ) < X )
29 14 simprd 
 |-  ( X e. ( A (,) B ) -> X < B )
30 29 adantr 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> X < B )
31 13 22 24 28 30 xrlttrd 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> ( ( A + X ) / 2 ) < B )
32 elioo1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( A + X ) / 2 ) e. ( A (,) B ) <-> ( ( ( A + X ) / 2 ) e. RR* /\ A < ( ( A + X ) / 2 ) /\ ( ( A + X ) / 2 ) < B ) ) )
33 1 32 syl 
 |-  ( X e. ( A (,) B ) -> ( ( ( A + X ) / 2 ) e. ( A (,) B ) <-> ( ( ( A + X ) / 2 ) e. RR* /\ A < ( ( A + X ) / 2 ) /\ ( ( A + X ) / 2 ) < B ) ) )
34 33 adantr 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> ( ( ( A + X ) / 2 ) e. ( A (,) B ) <-> ( ( ( A + X ) / 2 ) e. RR* /\ A < ( ( A + X ) / 2 ) /\ ( ( A + X ) / 2 ) < B ) ) )
35 13 20 31 34 mpbir3and 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> ( ( A + X ) / 2 ) e. ( A (,) B ) )
36 35 28 jca 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> ( ( ( A + X ) / 2 ) e. ( A (,) B ) /\ ( ( A + X ) / 2 ) < X ) )
37 eleq1 
 |-  ( y = ( ( A + X ) / 2 ) -> ( y e. ( A (,) B ) <-> ( ( A + X ) / 2 ) e. ( A (,) B ) ) )
38 breq1 
 |-  ( y = ( ( A + X ) / 2 ) -> ( y < X <-> ( ( A + X ) / 2 ) < X ) )
39 37 38 anbi12d 
 |-  ( y = ( ( A + X ) / 2 ) -> ( ( y e. ( A (,) B ) /\ y < X ) <-> ( ( ( A + X ) / 2 ) e. ( A (,) B ) /\ ( ( A + X ) / 2 ) < X ) ) )
40 36 39 imbitrrid 
 |-  ( y = ( ( A + X ) / 2 ) -> ( ( X e. ( A (,) B ) /\ A e. RR ) -> ( y e. ( A (,) B ) /\ y < X ) ) )
41 rspe 
 |-  ( ( y e. ( A (,) B ) /\ y < X ) -> E. y e. ( A (,) B ) y < X )
42 40 41 syl6 
 |-  ( y = ( ( A + X ) / 2 ) -> ( ( X e. ( A (,) B ) /\ A e. RR ) -> E. y e. ( A (,) B ) y < X ) )
43 6 7 42 spcimgf 
 |-  ( ( ( A + X ) / 2 ) e. _V -> ( A. y ( X e. ( A (,) B ) /\ A e. RR ) -> E. y e. ( A (,) B ) y < X ) )
44 5 43 ax-mp 
 |-  ( A. y ( X e. ( A (,) B ) /\ A e. RR ) -> E. y e. ( A (,) B ) y < X )
45 4 44 sylbir 
 |-  ( ( X e. ( A (,) B ) /\ A e. RR ) -> E. y e. ( A (,) B ) y < X )
46 45 expcom 
 |-  ( A e. RR -> ( X e. ( A (,) B ) -> E. y e. ( A (,) B ) y < X ) )
47 simpl 
 |-  ( ( X e. ( A (,) B ) /\ A = +oo ) -> X e. ( A (,) B ) )
48 oveq1 
 |-  ( A = +oo -> ( A (,) B ) = ( +oo (,) B ) )
49 48 eleq2d 
 |-  ( A = +oo -> ( X e. ( A (,) B ) <-> X e. ( +oo (,) B ) ) )
50 49 adantl 
 |-  ( ( X e. ( A (,) B ) /\ A = +oo ) -> ( X e. ( A (,) B ) <-> X e. ( +oo (,) B ) ) )
51 pnfxr 
 |-  +oo e. RR*
52 elioo2 
 |-  ( ( +oo e. RR* /\ B e. RR* ) -> ( X e. ( +oo (,) B ) <-> ( X e. RR /\ +oo < X /\ X < B ) ) )
53 51 52 mpan 
 |-  ( B e. RR* -> ( X e. ( +oo (,) B ) <-> ( X e. RR /\ +oo < X /\ X < B ) ) )
54 53 biimpd 
 |-  ( B e. RR* -> ( X e. ( +oo (,) B ) -> ( X e. RR /\ +oo < X /\ X < B ) ) )
55 elioore 
 |-  ( X e. ( +oo (,) B ) -> X e. RR )
56 rexr 
 |-  ( X e. RR -> X e. RR* )
57 pnfnlt 
 |-  ( X e. RR* -> -. +oo < X )
58 56 57 syl 
 |-  ( X e. RR -> -. +oo < X )
59 58 intn3an2d 
 |-  ( X e. RR -> -. ( X e. RR /\ +oo < X /\ X < B ) )
60 55 59 syl 
 |-  ( X e. ( +oo (,) B ) -> -. ( X e. RR /\ +oo < X /\ X < B ) )
61 60 a1i 
 |-  ( B e. RR* -> ( X e. ( +oo (,) B ) -> -. ( X e. RR /\ +oo < X /\ X < B ) ) )
62 54 61 pm2.65d 
 |-  ( B e. RR* -> -. X e. ( +oo (,) B ) )
63 23 62 syl 
 |-  ( X e. ( A (,) B ) -> -. X e. ( +oo (,) B ) )
64 63 pm2.21d 
 |-  ( X e. ( A (,) B ) -> ( X e. ( +oo (,) B ) -> E. y e. ( A (,) B ) y < X ) )
65 64 adantr 
 |-  ( ( X e. ( A (,) B ) /\ A = +oo ) -> ( X e. ( +oo (,) B ) -> E. y e. ( A (,) B ) y < X ) )
66 50 65 sylbid 
 |-  ( ( X e. ( A (,) B ) /\ A = +oo ) -> ( X e. ( A (,) B ) -> E. y e. ( A (,) B ) y < X ) )
67 47 66 mpd 
 |-  ( ( X e. ( A (,) B ) /\ A = +oo ) -> E. y e. ( A (,) B ) y < X )
68 67 expcom 
 |-  ( A = +oo -> ( X e. ( A (,) B ) -> E. y e. ( A (,) B ) y < X ) )
69 19.3v 
 |-  ( A. y ( X e. ( A (,) B ) /\ A = -oo ) <-> ( X e. ( A (,) B ) /\ A = -oo ) )
70 ovex 
 |-  ( X - 1 ) e. _V
71 nfcv 
 |-  F/_ y ( X - 1 )
72 peano2rem 
 |-  ( X e. RR -> ( X - 1 ) e. RR )
73 8 72 syl 
 |-  ( X e. ( A (,) B ) -> ( X - 1 ) e. RR )
74 mnflt 
 |-  ( ( X - 1 ) e. RR -> -oo < ( X - 1 ) )
75 73 74 syl 
 |-  ( X e. ( A (,) B ) -> -oo < ( X - 1 ) )
76 73 rexrd 
 |-  ( X e. ( A (,) B ) -> ( X - 1 ) e. RR* )
77 8 ltm1d 
 |-  ( X e. ( A (,) B ) -> ( X - 1 ) < X )
78 76 21 23 77 29 xrlttrd 
 |-  ( X e. ( A (,) B ) -> ( X - 1 ) < B )
79 mnfxr 
 |-  -oo e. RR*
80 elioo2 
 |-  ( ( -oo e. RR* /\ B e. RR* ) -> ( ( X - 1 ) e. ( -oo (,) B ) <-> ( ( X - 1 ) e. RR /\ -oo < ( X - 1 ) /\ ( X - 1 ) < B ) ) )
81 79 80 mpan 
 |-  ( B e. RR* -> ( ( X - 1 ) e. ( -oo (,) B ) <-> ( ( X - 1 ) e. RR /\ -oo < ( X - 1 ) /\ ( X - 1 ) < B ) ) )
82 23 81 syl 
 |-  ( X e. ( A (,) B ) -> ( ( X - 1 ) e. ( -oo (,) B ) <-> ( ( X - 1 ) e. RR /\ -oo < ( X - 1 ) /\ ( X - 1 ) < B ) ) )
83 73 75 78 82 mpbir3and 
 |-  ( X e. ( A (,) B ) -> ( X - 1 ) e. ( -oo (,) B ) )
84 83 adantr 
 |-  ( ( X e. ( A (,) B ) /\ A = -oo ) -> ( X - 1 ) e. ( -oo (,) B ) )
85 oveq1 
 |-  ( A = -oo -> ( A (,) B ) = ( -oo (,) B ) )
86 85 eleq2d 
 |-  ( A = -oo -> ( ( X - 1 ) e. ( A (,) B ) <-> ( X - 1 ) e. ( -oo (,) B ) ) )
87 86 adantl 
 |-  ( ( X e. ( A (,) B ) /\ A = -oo ) -> ( ( X - 1 ) e. ( A (,) B ) <-> ( X - 1 ) e. ( -oo (,) B ) ) )
88 84 87 mpbird 
 |-  ( ( X e. ( A (,) B ) /\ A = -oo ) -> ( X - 1 ) e. ( A (,) B ) )
89 77 adantr 
 |-  ( ( X e. ( A (,) B ) /\ A = -oo ) -> ( X - 1 ) < X )
90 88 89 jca 
 |-  ( ( X e. ( A (,) B ) /\ A = -oo ) -> ( ( X - 1 ) e. ( A (,) B ) /\ ( X - 1 ) < X ) )
91 90 adantr 
 |-  ( ( ( X e. ( A (,) B ) /\ A = -oo ) /\ y = ( X - 1 ) ) -> ( ( X - 1 ) e. ( A (,) B ) /\ ( X - 1 ) < X ) )
92 eleq1 
 |-  ( y = ( X - 1 ) -> ( y e. ( A (,) B ) <-> ( X - 1 ) e. ( A (,) B ) ) )
93 breq1 
 |-  ( y = ( X - 1 ) -> ( y < X <-> ( X - 1 ) < X ) )
94 92 93 anbi12d 
 |-  ( y = ( X - 1 ) -> ( ( y e. ( A (,) B ) /\ y < X ) <-> ( ( X - 1 ) e. ( A (,) B ) /\ ( X - 1 ) < X ) ) )
95 94 adantl 
 |-  ( ( ( X e. ( A (,) B ) /\ A = -oo ) /\ y = ( X - 1 ) ) -> ( ( y e. ( A (,) B ) /\ y < X ) <-> ( ( X - 1 ) e. ( A (,) B ) /\ ( X - 1 ) < X ) ) )
96 91 95 mpbird 
 |-  ( ( ( X e. ( A (,) B ) /\ A = -oo ) /\ y = ( X - 1 ) ) -> ( y e. ( A (,) B ) /\ y < X ) )
97 96 41 syl 
 |-  ( ( ( X e. ( A (,) B ) /\ A = -oo ) /\ y = ( X - 1 ) ) -> E. y e. ( A (,) B ) y < X )
98 97 expcom 
 |-  ( y = ( X - 1 ) -> ( ( X e. ( A (,) B ) /\ A = -oo ) -> E. y e. ( A (,) B ) y < X ) )
99 71 7 98 spcimgf 
 |-  ( ( X - 1 ) e. _V -> ( A. y ( X e. ( A (,) B ) /\ A = -oo ) -> E. y e. ( A (,) B ) y < X ) )
100 70 99 ax-mp 
 |-  ( A. y ( X e. ( A (,) B ) /\ A = -oo ) -> E. y e. ( A (,) B ) y < X )
101 69 100 sylbir 
 |-  ( ( X e. ( A (,) B ) /\ A = -oo ) -> E. y e. ( A (,) B ) y < X )
102 101 expcom 
 |-  ( A = -oo -> ( X e. ( A (,) B ) -> E. y e. ( A (,) B ) y < X ) )
103 46 68 102 3jaoi 
 |-  ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( X e. ( A (,) B ) -> E. y e. ( A (,) B ) y < X ) )
104 3 103 sylbi 
 |-  ( A e. RR* -> ( X e. ( A (,) B ) -> E. y e. ( A (,) B ) y < X ) )
105 2 104 mpcom 
 |-  ( X e. ( A (,) B ) -> E. y e. ( A (,) B ) y < X )